形式化方法在计算机科学中的应用由来已久。形式化方法以其技术特点来分有两大类：一类是定理证明，另一类是模型检测。这两类方法都被应用到密码协议的分析之中了。原有的模型也就通过改造，形成了相应的密码协议分析方法。不仅如此，人们认识到密码协议的特点，设计了一些新的方法专门用于分析密码协议，还延伸出一类混合技术，即定理证明与模型检测相结合的方法。

根据攻击者的模型类型，将分析密码协议的形式化方法分为两类。

1.Dolev-Yao模型下的形式化方法

形式化方法中最流行的攻击者模型是Dolev-Yao模型。在协议运行的开始或者运行过程中，攻击者可以窃听、消去以及任意安排公开通道上的消息。他也可以从观察到的消息产生新的消息，并将它们加入信道中。攻击者可以将非加密消息分成若干个新的消息或者将若干个已知的消息合并成一个新的消息，攻击者可以用自己已知的密钥对任意的消息加密，攻击者还可以解密一个收到的密文，前提是攻击者知道正确的密钥。攻击者可以根据需要，截断信道上传输的任何消息，注入自己产生的新的消息，发送该消息至依赖的目标主体或者任何其他主体。

形式化分析的通常做法是：把协议视为状态迁移系统，分析所有可能的轨迹，判定安全性性质是否在所有的轨迹上都被保持。

在Dolev-Yao方法下，我们又根据不同方法的技术特点，把它们划分为定理证明方法、模型检测方法以及混合方法。概率模型下又有概率互模拟方法与黑盒子互模拟方法。

2.互模拟等价模型

（1）完善保密下的互模拟等价

Spi演算系统将协议的诚实主体描述为一个进程，这个进程可以重复执行任意多个，也就意味着可以有任意多个会话并发运行，攻击者可以观察和参加任意的通信。这个模型也依赖于完善密码系统假设，协议的安全属性被描述为两个系统的观察等价。一个系统是任意一个进程A与实际协议的交互，另一个是A与理想进程的交互。如果两个进程在进程演算的意义下是观察等价的，则这个协议就是安全的。相比Dolev-Yao模型，互模拟等价模型可以分析更多的安全性质。(www.daowen.com)

（2）概率意义下的互模拟等价

概率意义下的互模拟等价就是用概率模型替代对称密码学的“黑盒子”式的抽象。这类模型的代表有：概率多项式时间的进程演算以及基于密码学传统的模拟模型。

为了理解每一类型的技术特点，我们在每个类型之中选择一种影响较大的方法进行分析。这里我们给出它们的典型代表（包括计算意义下的分析方法）。

（1）Dolev-Yao模型：定理证明法，包括逻辑系统（BAN逻辑等）以及Paulson、串空间等；模型检测（CSP方法）；混合系统（NRL分析器）。

（2）互模拟等价模型：黑盒子互模拟等价模型（Spi演算）。

（3）计算（密码学）方法：概率互模拟模型（BPW方法）、LMMS概率进程演算方法、随机问答方法、复合性可证明安全的方法等。

我们将对前两项中的典型模型进行技术特点的分析，在进行具体分析之前，首先对定理证明、模型检测以及互模拟的基本特征加以介绍。