安全协议的形式化研究始于20世纪70年代末，安全协议的形式化分析就是采用形式化的语言或模型，为安全协议建立模型，使用规定的假设和验证方法作用于协议模型，从而证明协议的安全性。

安全协议形式化分析的思想由Needham和Schroeder两人在1978年最先提出。1981年，Denning和Sacco指出NS私钥协议的一个错误，人们开始关注安全协议的形式化分析。在这一领域具有里程碑意义的事情发生于20世纪80年代，Danny Dolev和Andrew C.Yao发表了文章On the Security of Public Key Protocols，真正开始了使用形式化方法分析安全协议的历史，自此之后使用形式化方法研究安全协议逐渐兴起。Dolev和Yao在他们的文章中开创性地给出了安全协议可以多步并发执行的形式化系统模型，在这个系统模型中，包含那些可以对信息流进行恶意窃取、修改和删除的入侵者和不诚实的参与者，同时密码算法被认为是完备的，在分析时仅仅把它看作是一个满足一些代数性质的黑盒子，即使是主动攻击者也无法通过密码学算法对安全协议进行攻击。紧接着，Dolev、Even和Karp开发研究出了一系列的多项式时间算法，使用这些算法来分析一个限制严格的安全协议簇。但遗憾的是，在随后的研究中发现它们可以分析的协议太有限，一旦稍许放宽对这个协议簇的限定都将使得协议的安全性变成不确定的问题，因此这方面的工作并未得到进一步的展开。随后，在Dolev-Yao模型及其变形的基础上发展了很多形式化分析安全协议的工具。它们大部分采用状态搜索的技术，即首先定义一个状态空间和安全协议的系统模型，然后在此模型内进行搜索检测以确定是否存在一条路径对应于攻击者的一次成功的攻击。还有一些研究者采用归纳定理推证技术（简称定理证明）开发了安全协议分析的通用工具，并取得了一定的成果。(www.daowen.com)

1989年，Burrows、Abadi和Needham引入了逻辑的方法，提出了BAN逻辑的概念，并逐渐引起了人们的广泛关注。BAN逻辑采用了与状态搜索技术完全不同的方法，它是关于主体拥有的知识与信仰，以及用于从已有信仰推知新的信仰的推理规则的逻辑。这种逻辑通过对认证协议的运行进行形式化分析，来研究认证双方如何通过相互发送和接收消息的方式，从最初的信仰逐渐发展到协议运行最终要达到的目的——认证双方的最终信仰。BAN逻辑的规则十分简洁和直观，因此易于使用。BAN逻辑成功地对NS协议、Kerberos协议等几个著名的协议进行了分析，找到了其中若干已知和未知的漏洞。BAN逻辑的成功极大地激发了密码学家对安全协议形式化分析的兴趣，并导致许多安全协议形式化分析方法的产生。但是，由于逻辑的方法是对安全协议分析问题的一种更高层次上的抽象，所以在一般情况下它的能力要弱于状态搜索和定理证明技术。1996年，Gavin Lowe使用通用的模型检测工具FDR发现了NS公钥密码协议中存在着中间人攻击。在这之后，在Dolev-Yao模型及其变形的基础上结合使用状态搜索技术和定理证明方法的分析研究工作又取得了很大的进展，并不断涌现出一些新的形式化方法和工具，比如，1997年Paulson提出的基于协议消息和事件的攻击结构方法注记的证明方法（也被称为Paulson归纳法），1999年由Fabrega、Herzog和Guttman提出的基于协议消息节点间一种偏序关系的可证安全的串空间（Strand Space）模型。利用串空间原理，Song发展了一种自动检测工具Athena。