安全协议的形式化分析技术可使协议设计者通过系统分析将注意力集中于接口、系统环境的假设、系统在不同条件下的状态、条件不满足时系统出现的情况以及系统不变的属性，并通过系统验证，提供协议必要的安全保证。通俗地讲，安全协议的形式化分析是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标。因此，安全协议的形式化分析有助于：

（1）界定安全协议的边界，即协议系统与其运行环境的界面；

（2）更准确地描述安全协议的行为；

（3）更准确地定义安全协议的特性；

（4）证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说明。

安全协议形式化分析理论与方法的研究过程可归纳为以下四个阶段。

1.早期阶段

这一阶段的研究主要集中于对具体协议的检测、分析。最早提出对安全协议进行形式化分析思想的是Needham和Schroeder，他们为进行共享和公钥认证服务器系统的实现建立了安全协议。1981年Denning和Sacco指出了NS共享密钥协议的一个错误，使得人们开始关注安全协议分析。(www.daowen.com)

2.初期阶段

这一阶段以Dolev-Yao的工作为标志。BAN类逻辑及CKT5等基于知识逻辑的有效应用标志着研究进入了以信念逻辑为主体的时期。

3.转折阶段

以G.Lowe发表著名的论文《关于Needham-Schroeder公钥协议的一个攻击》为标志，各种一般用途的模型检测方法被用于协议分析的研究。

4.理论证明阶段

以1999年Fabrega、Herzog和Guttman的串空间（Strand Space）理论及Paulson的归纳方法为代表，开始了协议分析理论的发展时期。