安全协议是网络通信和安全应用的基础，是安全基础设施的重要组成部分。安全协议的设计和分析是协议工程领域主要的研究内容，在设计、建模、验证、性能分析、实现、测试和维护等协议工程的各个环节中，协议验证是最为关键的一个环节。自20世纪70年代以来，人们提出多种协议分析、验证的形式化方法，它们可以大致划分为四种：基于BAN类逻辑的模态逻辑方法，基于有限状态机理论的模型检验方法，基于安全代数模型的定理证明方法和程序分析技术。在这些方法中，定理证明方法能够给出协议的安全性证明，因此也是密码协议分析的主要研究内容。由于密码协议本身安全目标定义的微妙性，运行环境的复杂性，攻击者能力的不确定性和协议执行的高并发性，使得安全协议的验证存在一系列困难，因此协议分析也采用了一些特殊的技术，如：状态检测、不变集技术、等价验证技术等。本文对基于定理证明的安全协议形式化验证方法进行了详细的分析，其中主要研究了基于~π演算密码协议分析方法，包括spi演算，应用pi演算和协议验证的框架互模拟方法，其中主要的工作和贡献如下：(1)对spi演算进行详细的分析，包括其协议验证思想，系统框架、操作语意以及进程等价证明方法，并使用spi演算对Otway—Rees变体协议的安全性进行分析，证明其不能满足安全性。(2)spi演算通过对π演算中的项和进程进行扩展，使其能够表示基本的密码操作进而对协议建模，但是spi忽略了密码操作的安全意义，限制了它在协议分析中的应用。本文通过引入消息起源的标准测试证明了ZG非可否认协议的非可否认性和公平性，扩展了spi演算在协议分析中的应用范围。(3)框架互模拟是证明协议满足观察等价的有效手段，其中用框架、理论偶表示协议运行环境的信息，通过证明规范进程与协议进程的框架互模拟关系验证协议的安全性。本文对其语法，操作语意，验证方法以及主要结论进行了简要的总结。(4)应用pi演算是Abadi等将π演算对协议进行特化而建立的协议验证方法：其中使用函数应用建模密码操作，大大增强了对攻击者能力的描述；使用等式理论表示函数应用上的约简规则，并提出评价上下文表示进程执行环境，最后，使用标记互模拟证明协议的安全性。本文在应用pi演算和框架互模拟的基础上对复合协议中协议、子协议的相关性进行分析，提出了协议验证不相关定理，并说明了其在协议分析，协议综合上的应用。