密码协议的安全性是网络安全的关键,协议分析是揭示密码协议是否存在安全漏洞的重要途径。与非形式化方法相比,密码协议的形式化分析与验证能全面地检测密码协议存在的安全漏洞。在对现有密码协议形式化分析方法和计算方法深入系统分析的基础上,本论文主要对以下几个方面的密码协议形式化分析理论进行了深入的分析和研究:第一,本文对形式化模型中的完美加密假设进行弱化,即允许攻击者通过一些特殊的操作来破解加密,这只能在一些适合的假设下才会出现,因此攻击者不能中断协议的运行。为此由计算模型利用概率和计算复杂性限制攻击者能力的思想,本文给出Dolev-Yao攻击者的概率定义,随后利用消息保密性和认证性这两个性质,对本文的概率Dolev-Yao攻击者和标准的Dolev-Yao攻击者进行比较。第二,本文分析另一个形式化模型中经常用到的自由代数假设,实际上仅使用下面的密码学概念就可以给出一个非常广泛的协议类型:(对称或非对称)加密、数字签名、杂凑和配对,这些概念可以直接用项来建模:enc(m,k)或者enc(m,pub(k)),sig(m,pri(k)),hash(m),cons(m1,m2),其中m为消息,k为密钥,pub(k)和pri(k)分别为公开和秘密密钥。在形式化模型中,由这些概念给定的算法通常被假定为自由的,即如果只考虑对称加密,有enc(m1,k1)=enc(m2,k2),当且仅当m1=m2,k1=k2,这个自由性质确保值与项之间是一一对应的。本文研究对符合等价关系的项集合进行过逼近的问题,这个等价性不是固定的,但是可以由任一项重写系统来解释。通过重写规则,本文可以解释很多密码学概念的规则,而不需要选择一个特殊的固定的密码学概念集合。所以利用这种方法,我们既可以弱化自由代数假设,也可以降低对操作限定集合的依赖性。为此,本文利用非确定性的有限树自动机来逼近符合重写规则的项,我们给出一系列的算法来计算合理的逼近。第三,本文对密码协议进行分析和验证,其中对协议的描述,我们定义一个进程演算,还定义与所使用密码学概念无关的语义,这些密码学概念仍然可以通过重写系统进行定义,随后研究协议的静态分析。本文参考的是控制流分析方法,这种方法静态地计算协议运行时所交换消息的一个超集的有限表示,所以不在超集内的项是不能进行通信的,这可以用于证明数据的保密性。对控制流分析方法进行改进,使之适合我们的进程演算,由第三章的逼近算法,这种改进能够处理符合重写的项,这使得我们可以静态地推理密码协议的安全性质。第四,在深入分析Spi演算语法结构和基于测试等价方法的基础上,对Spi演算进行改进,形成了扩展Spi演算描述语言,使之成为自动验证系统输入协议的描述语言,对自动化验证中密码协议安全特性的形式化描述和验证方法进行研究,利用扩展Spi演算对加密密钥交换(Encrypted-Key-Exchange,EKE)协议进行分析。通过对上述内容的分析和研究,本论文的贡献及其意义主要体现在以下几点:第一,对于密码协议使用的密码学概念,本文提出一个进程演算,定义其语法和语义。第二,基于本文的进程演算,给出Dolev-Yao模型的概率定义,对标准Dolev-Yao模型的改进是为了使攻击者能够猜测解密截取消息的密钥。第三,在本文的演算中,给出保密性和认证的概率定义,并在攻击者以一个可忽略概率的猜测成功的假设以及攻击者可以利用的资源是多项式限定的假设下,证明改进的攻击者模型与标准的Dolev-Yao模型具有相同的能力。第四,本文提出一个计算符合重写规则的项语言的有限逼近方法,我们用树自动机来表示这个项语言,同样逼近也是一个项自动机,而且它具体化了重写,即项语言包含了所有初始的项以及项所有可能的重写,并给出其语义。最后给出实现逼近的算法,并对逼近的准确性进行了改进。第五,对于密码协议的描述,本文给出一个进程演算,随后定义该演算的静态语义和动态语义。第六,通过对控制流分析方法进行改进,本文提出一个适合于我们演算的控制流分析方法,对密码协议进行静态地分析。第七,对Spi演算进行改进,形成了扩展Spi演算描述语言,使之成为自动验证系统输入协议的描述语言,并对自动化验证中密码协议安全特性的形式化描述和验证方法进行了研究,利用该系统对现有的许多密码协议进行分析,结果表明该系统是可靠的和可行的,对EKE协议进行分析,发现了该协议在并行会话攻击下是不安全的。