Model Checking Turotial Overview
reactive system：反应性系统 in 第一章
模型检查。一个总览教程。
摘要
我们调查了反应系统自动分析的模型检验技术原理。通过对Needham-Schroeder公钥协议的分析来举例说明模型检查的使用。 然后，我们正式定义过渡系统，时间逻辑，ω-自动机及其关系。 定义了线性和分支时间时序逻辑的基本模型检查算法，然后介绍了符号模型检查和偏序约简技术。 本文以一些更高级主题的参考列表结尾。
【1】介绍
计算系统遍及我们的日常生活。我们依靠数字控制器来监督汽车，飞机和工业厂房的关键功能。数字交换技术已取代电信行业中的模拟组件，并且安全协议使电子贸易应用程序成为可能并且保护它的隐私。
在重要的投资甚至人类的生命受到威胁的情况下，底层硬件和软件组件的质量保证变成了最重要的东西，这需要正式的模型在一个适当的抽象层次来描述系统的相关部分。
我们关注的系统呈现出持续地与环境进行交互（例如，受控系统或通信网络的其他组件），因此该系统被称为反应性系统[60，94]。将计算机程序描述为根据给定输入值计算某些结果的传统模型不足以描述反应性系统。
相反，反应性系统的行为通常由过渡系统建模。
术语——模型检查指明了用于自动分析反应性系统的技术的集合。
可以（已经发现）以这种方式发现安全关键系统设计中的细微错误，而这些错误通常是传统的仿真和测试技术所无法企及的。
由于它已被证明具有成本效益，并且可以与传统设计方法很好地集成在一起，因此模型检查已被用作反应性系统质量保证的标准程序。
模型检查器的输入是被分析系统的一个描述，也是大量的属性，通常被表达为时序逻辑的公式，这些公式有望被保留在系统中。
模型检查器也可以确认某些属性是否保留，或者举报那些违法的属性。
在后一种情况下，它提供了一个反例：违反该属性的运行。这样的运行可以提供有价值的反馈并指出设计错误。实际上，这种观点似乎有些理想化：经常，可用资源仅允许分析系统的较粗略模型。这样，来自模型检查器的肯定判断就没有什么价值了，因为错误很可能会被必须应用于模型的简化所隐藏。
像代码审查之类的标准流程是十分重要的，它可以确保抽象模型充分地反映出实际系统的行为，为了确保利益的属性被建立或篡改。
模型检查器在此验证任务中可能会有所帮助，因为可以执行“健全性检查”，例如，确保一定可以进行某些运行或确保模型没有死锁。
本文旨在基于对大量模型检查文献的主观选择，对模型检查的一些基本原理进行教程概述。
我们从第2节中的案例研究开始，其中从用户的角度考虑模型检查的应用。
第三部分回顾了过渡系统，时间逻辑和自动机理论技术，这些技术是模型检查的基础。 第4节介绍了线性时间和分支时间逻辑的基本模型检查算法。 最后，第5节收集了一些对更高级主题的粗略参考。 有关该卷的其他文章以及有关该主题的教科书和调查报告[27，28，69，97，124]中可以找到更多的材料。
本文包含对相关文献的许多参考，希望该调查也可以用作带注释的书目。
【2】密码协议分析
【2.1】协议描述
让我们首先以示例方式考虑使用模型检查器SPIN对Needham和Schroeder建议的公钥身份验证协议进行分析。
两个代理A（lice）和B（ob）试图通过不安全的通道建立一个共同秘钥，以使双方都确信彼此的存在，并且没有入侵者可以在不破坏底层加密算法的情况下掌握该秘钥。
这是密码学中的基本问题之一：例如，共享秘钥可用于生成会话**，以进行代理之间的频繁通信。
在整个过程中，我们假设底层加密算法是安全的，那个诚实的代理的私钥是不受影响的。
因此，只有代理C可以解密<M>c来获得M。
- 爱丽丝通过生成一个随机数NA并将消息<A，NA> B发送给Bob来启动协议（在密码术语中，诸如NA之类的数字称为现时数，表示任何诚实代理仅应使用它们一次）。消息的第一部分通知Bob发起者的身份。第二部分代表秘密的“一半”。
- 鲍勃类似地生成一个随机数NB并以消息<NA, NB>A响应。
第一步中生成的随机数NA的存在（只有Bob可以解密）使Alice确信消息的真实性。
因此，她接受<NA，NB>对作为共同的秘钥。 - 最后，爱丽丝以消息<NB>B响应。
通过与上述相同的论点，Bob得出结论，此消息必须起源于Alice，因此也接受<NA，NB>作为公共秘密。
我们假设所有消息都是通过不安全的媒体发送的。 攻击者可能会截获消息，进行存储，甚至可能稍后再播。他们还可以参与协议的常规运行，启动运行或响应由诚实的代理发起的运行，这些代理不需要知道其伙伴的真实身份。 但是，即使是攻击者也只能解密使用自己的公共**加密的消息。
该协议包含一个严重的缺陷，请读者在继续之前先找到它。 在协议首次发布后约17年，使用模型检查技术发现了该错误[91]。