被动攻击主要是收集信息而不是进行访问，数据的合法用户对这种活动一点也不会觉察到。被动攻击包括嗅探、信息收集等攻击方法。对被动攻击的检测十分困难，因为攻击并不涉及数据的任何改变。然而阻止这些攻击的成功是可行的，因此，对被动攻击强调的是阻止而不是检测。

在实际应用中，对协议的攻击方法是多种多样的。这里简单介绍几个常用的攻击方法[4]：

（1）重放攻击

重放攻击是指协议之前运行记录的消息，被攻击者在协议现在运行的过程中作为消息重放。根据Dolev-Yao[5]模型，攻击者完全能够控制整个通信信道。攻击者知道会话秘钥和协议之前运行生成的短期私密信息。在协议顺序执行的体系中，假设攻击者有重放之前会话消息的能力，而这些会话中可能包含已经被泄露的会话秘钥。

（2）类型缺陷攻击

类型缺陷攻击是指攻击者向接收者将消息解释成不同的类型（如：将随机数作为秘钥接收），使得接收者认为该消息是有效的。为了能够实现对协议的类型缺陷攻击，须假设数据是字节流的形式。不同的数据类型是以不同的字节流数据类型表现的。论文网

（3）并行会话攻击

并行会话攻击是指此攻击者利用从协议运行过程中收集到的知识，发起一个新的运行过程。并行会话攻击有几种不同的形式，例如oracle攻击、多重攻击、中间人攻击。

1.1.3 安全协议的设计规范

对安全协议进行设计时，将常见的设计规范总结如下[6]：

（1）采用一次随机数代替时间戳

（2）能抵御常见攻击

（3）适用于任何网络结构的任何协议层

（4）能对任何类型的数据进行处理

（5）可采用任何密码算法

（6）不受出口的限制

（7）便于进行功能扩充

（8）尽可能少的安全假设

1.2 安全协议模型检测概述

图1.1 模型检测方法的发展

安全协议的验证方法有很多种，如：定理证明、演绎法、程序设计逻辑、模型检测等。每种方法都有自己的优势和劣势。基于逻辑的方法和演绎法可验证安全协议是否满足其以形式化描述定义的目标，但不能产生对那个协议的攻击。而模型检测可以发现协议的攻击，通过搜索系统中的某些状态的性能是否被违背，模型检测工具也被成功地用来检测安全协议。图1.1描述了模型检测的发展过程[7]，可以看出如今模型检是将高级语言描述的模型抽象化，再用模型检测工具对其进行检测。

1.2.1 模型检测的原理

模型检测的原理[4]是构建一个系统状态图，然后从初始状态查找到状态中协议的不变量（例如“攻击者不知道私密消息X”或“如果Alice在状态1则Bob在状态2”）被违背，如图1.2所示，黑色的圈表示不变量被违背的状态。这些不变量的违背是单调的，也就是一旦不变量无效，就不会再变成有效。

图1.2 一个系统的状态和一个状态中的不变量被违背

图1.3 从初始状态到不满足条件的状态的轨迹

图1.3表示从初始状态到不满足条件的轨迹（虚线所示），可以用来产生被检测到攻击的详细信息。

1.2.2 模型检测器的工作原理文献综述

图1.4表示模型检测器的工作原理，从输出可以看出模型检测器检测协议状态是否满足条件，有着自动化和提供反例等诸多优点。

图1.4 模型检测器的工作原理