随着网络技术的迅速普及与发展,网络中敏感信息的保护已变得越来越重要。密码协议正是为通信的双方或多方提供这样的安全保证。然而,由于网络本身的开放性,其中存在着严重的安全威胁,攻击者可以通过各种方式对密码协议进行攻击,破坏其安全特性。因此,对密码协议进行安全性分析至关重要。本文按照密码协议不同的应用环境将其分为两种,一种是应用于传统计算机网络的密码协议,这种协议在设计时不必考虑密码原语的复杂度,仅以保证协议的安全性为目标,称为传统密码协议;另外一种是应用于RFID系统的密码协议,这种密码协议由于受到标签成本限制,在设计时必须采用结构简单、计算复杂度低的密码原语,并利用他们的代数性质进行代数运算和等式推导来实现协议的安全目标,称为轻量级协议。当前,对这两种协议的分析方法也有所不同:针对传统的密码协议,一般采用形式化方法。形式化方法具有严格、明确、清晰和反直觉等特点,因此是分析密码协议的有效工具,但由于其抽象化程度太高,不能分析带有代数运算和等式推导的协议,因此对于应用于RFID系统的轻量级协议,只能采用手工验证方法。本文对这两种方法都进行了研究,对于传统的密码协议,研究了基于SAT模型检测的方法,并对该方法进行了功能扩展;对于轻量级协议,采用手工验证方法,分析了两个优秀的轻量级协议的安全性,找到了两个独特的攻击。本文的主要研究成果如下:(1)提出了一个新的可以检测类型缺陷攻击的模型SAT-1。该模型通过在匹配模式中引入无类型变量,并通过无类型消息的概念,解除了原SAT模型检测器对未知消息的类型限制。同时,通过增加消息匹配算法,使诚实主体能够接受带有类型缺陷的消息,从而实现了类型缺陷攻击的检测。在对Otway-Rees协议的检测中,不仅发现了已有的针对发起者A的类型缺陷攻击,而且发现了新的针对响应者B的类型缺陷攻击,证明了SAT-1模型的可靠性。(2)针对当前模型检测工具普遍不能检测带有异或运算密码协议的问题,提出了一个新的模型SAT-2。该模型通过引入抽象异或项的概念及其运算规则,大大降低了攻击者生成的异或消息数量,解决了由于引入异或运算所导致的状态空间爆炸问题。在此基础上,通过在SAT模型中增加基于抽象异或项的重写规则,扩展了攻击者的异或运算能力,实现了对带有异或运算密码协议的自动化检测。最后通过对BULL协议的检测,证明了抽象异或项的实用性,同时也证明了SAT-2模型检测器的可靠性。(3)设计了一个多协议攻击自动化检测系统ADMA。该系统由协议搜索子系统和攻击确认子系统两部分组成。协议搜索子系统根据多协议攻击中目标协议与辅助协议加密消息类型一致性的条件,自动化搜索可能对目标协议构成威胁的候选辅助协议。攻击确认子系统通过改进的SAT模型检测方法,自动化确认目标协议与候选辅助协议是否存在多协议攻击。试验结果表明,ADMA系统能够实现多协议攻击的自动化检测,并且检测中发现了新的多协议攻击。(4)提出了一个可变攻击者模型构造方案CIM。该方案利用异或运算,阿贝尔加法群运算以及阿贝尔乘法群运算的代数性质,定义了抽象项的概念及其运算规则,大大降低了攻击者进行代数运算的复杂度。在此基础上,将攻击者所有的攻击行为转化为重写规则,并定义了攻击者行为库和攻击规则选择算法,使检测者能够根据不同的协议选择并组合不同的攻击行为,构造可变的攻击者模型。与传统固定的攻击者模型方案相比,该方案能够根据不同的协议动态调整攻击者模型,并且能够降低攻击者执行代数运算的复杂度,因此保证了协议分析的效率和准确性。(5)针对Lee等人提出的应用于RFID系统的身份传输协议,提出了一个独特的三会话攻击。在该三会话攻击中,攻击者利用第一个会话监听目标标签和阅读器之间传递的消息,然后利用第二个会话收集目标标签的响应信息,最后通过第三个会话发动中间人攻击并对目标标签进行追踪,破坏了协议的不可追踪性。与传统的两会话攻击相比,三会话攻击更难于发现并且对攻击者要求更高,因此对三会话攻击进行了可行性分析,指出了其攻击成功的条件。(6)发现了三个针对Kulseng等人提出的应用于RFID系统的互认证协议的攻击。在这三个攻击中,第一个攻击通过修改两个会话中标签发送给阅读器的消息,成功的对标签进行了追踪,实现了追踪攻击。利用这个攻击,攻击者可以判断出了两条消息是否为同一个标签发送,然后利用线型移位寄存器的弱点,计算出标签和阅读器之间共享的秘密,从而成功的破坏了协议的机密性。在获得了标签和阅读器共享的秘密之后,攻击者能够在后续的会话中,模仿阅读器或标签与真正的标签或阅读器进行通信,最终破坏协议的互认证性。