该文采用形式化逻辑模型,对安全协议的形式化分析和验证技术进行研究.根据采用的技术和方法的不同,形式化逻辑模型又分为逻辑推导方法、攻击检测方法和定理证明方法.逻辑推导方法简单、易用,但是如何给出一个令人信服的、功能强大且简洁的逻辑系统,不是一件容易的事情.攻击检测方法大多对某个限定的协议空间进行检测,以验证协议的正确性,这样得到的安全性证明是有条件的.定理证明则是从证明的角度给出协议的安全性分析,无需对验证的空间进行特别的约束.这三种方法从不同的角度实现对协议的分析,各有利弊.逻辑方法简洁易用,如果协议存在漏洞,可以有效的分析攻击产生的原因,并给出修改意见,但是其对协议的安全分析结果并不能令人非常信服;攻击检测方法对协议可能的攻击进行检测,如果协议存在漏洞,则可以给出攻击路径,但无法有效描述攻击产生的原因,且需要对搜索空间进行限定.定理证明方法无需对分析的协议进行空间上的限定,其对协议的证明是可信服的,但是如果无法给出协议安全性证明,也无法有效的给出可能的攻击,但是可以描述攻击存在的原因.目前将多种方法进行融合互补,从而得到更优的方法是形式化方法分析协议的一个发展方向,该文中讨论的研究思路和技术也体现了这样的思想.该文从理论到实践两个层面上研究了安全协议的形式化分析的相关技术,其工作主要有以下几个方面:■对基本串空间理论进行了扩展和完善,加入了对散列操作、签名操作、DH操作以及非原子密钥、口令的描述和分析能力,同时增加了对攻击者的动态知识扩展能力的描述和分析,从而可以对更多类型的协议进行描述和安全性分析.■使用扩展串空间理论实现对群组协议的描述及其静态和动态安全性的分析.设计一个完整的群组密钥协商协议(包括初始协议和动态协议),使用我们的方法对其安全性进行了分析.指出针对一类群组密钥协商协议——广播者群组协商协议的两个新的攻击,并给出了避免攻击的协议设计原则.■提出项结点图模型,用以更有效的描述和分析构成协议消息的项及项之间的关系,借鉴计算模型的部分分析思想实现对安全协议的分析.■使用项结点图模型分析了一类协议——基于口令的密钥交换协议的安全性,并得出基于口令的三方密钥交换协议的安全性的一个必要条件.■结合串空间理论和项结点图模型,实现并优化了对一些认证协议和密钥交换协议的自动分析.提出全信息项和冗余协议的概念,基于协议自动分析器,提出一个自动设计认证协议的框架模型.