密码协议是在不可靠或者有敌意的通信环境下，保障一定安全属性的网络协议，敌手在此环境中可以具备多样的攻击手段，包括窃听、篡改、重放、中间人攻击、反射攻击、类型攻击、代数攻击等，因此密码协议分析就是要在多样的敌手模型下验证协议是否满足所需的安全属性。密码协议分析主要有两类方法：一类基于计算方法；一类基于形式化方法。计算方法是将消息当作位串，加密运算当作一种具体的算法，通过高效敌手只能以可以忽略概率成功实施攻击来定义安全性，最后用归约的形式进行安全分析。形式化方法将消息当作形式化表达式，将加密运算抽象为一种函数，用形式化公式对安全性进行建模，最后用形式化推理的方式对协议进行安全分析。

计算方法又称密码学方法，是以计算复杂性为基础提出的，起源于20世纪80年代，通过严格定义协议的安全性，并采用尽可能弱的明确假设，最后采用归约的方法将对协议的成功攻击转化为对密码元件的成功攻击，即由密码协议的不安全性推导出密码元件的不安全性，同时明确了密码协议的安全属性和对元件的安全假设。此方法需要建立适当的模型对协议及其安全性进行建模。1993年Bellare和Rogaway提出了BR93模型，首次将密码学方法用于对认证协议安全证明中，随后人们不断完善对敌手能力以及安全属性的描述，提出了BCK模型、模拟模型，以及CK和eCK等强安全模型。

在形式化方法出现前，安全协议分析几乎没有可以遵循的过程。即使在形式化方法出现之后，也是通过观察的方式，对协议直观地说明它们的安全性。形式化分析方法起源于20世纪80年代，1981年Dolev和Yao首次明确提出一种协议形式化分析模型，即Dolev-Yao模型（简称DY模型）。随后，针对密码协议分析，人们提出了许多形式化分析方法，包括形式逻辑分析、模型检测分析和定理证明分析。基于形式化方法易于自动化的特点，在形式化方法原理的基础上，人们提出多种形式化分析工具，将协议流程、敌手能力以及安全属性通过形式化语言进行描述并输入，工具自动分析出密码协议安全性分析结果。当前主流的工具包括FDR、AVISPA、ProVerif、Scyther、Tamarin和CryptoVerif等。

上述两种方法各有利弊：计算方法可以保证计算可靠性，安全性结论更为量化和具体，可行度更强，但较为复杂，不易理解，扩展性差，难以自动化；形式化方法简洁、直观，避免了显示涉及概率的论证，易于自动化，但是采用了完善假设，降低了分析结果的可信度，不能保证计算可靠性。2002年Abadi和Rogaway首次试图将计算方法和形式化方法关联起来，即证明一个协议在形式化模型下具有某种安全属性，则其在计算模型下也保持相应的安全属性，随着基于映射方法、基于模拟方法、计算方法直接形式化等方法的提出，计算安全的密码协议形式化分析成为又一重要的研究方向。计算方法发展至CK和eCK等强安全模型时便进入发展瓶颈，随后没有突破性进展。随之迎来形式化方法的发展热潮，各类形式化方法和工具纷纷提出，其较低的使用操作门槛和更加准确的分析结果吸引了更多协议分析者的研究和关注。