协议安全分析的方法有攻击检测方法和形式化分析方法。
攻击检测也称为渗透检测，是一种非正式的分析方法。它根据几种已知的攻击方法攻击协议，以验证攻击是否有效验证协议是否安全。这种方法的缺点是只能发现已知的安全漏洞和缺陷，并且无法发现未知的安全漏洞和缺陷。
早期协议安全性分析主要采用攻击检测方法，但仍具有重要价值。
协议的形式化分析使协议的描述形式化，并使用手动和计算机分析来推断确定协议是否安全。与非正式分析方法相比，形式分析方法可以全面深入地检测协议的微妙安全漏洞和缺陷。它不仅可以发现已知的安全漏洞和缺陷，还可以发现对未知安全漏洞和缺陷协议的正式分析，这些漏洞极大地促进了加密协议设计：
1）在协议设计阶段启用分析以避免可能发生的设计错误。
2）已经为协议的设计提出了许多新的设计原则。
协议的正式分析方法一般有以下三类：
(1)形式逻辑方法
这种分析方法定义了协议的目标，并在协议的最初时刻确定了参与者的知识和信念,通过协议中的发送和接收步骤生成新知识，并使用推理规则来推导最终的知识和信念。如果最终的一组知识和信念不包含要获得的目标知识和信念的陈述,则表明该协议存在安全缺陷。
(2)模型检测方法
模型检测方法的基本思想是将加密协议视为分布式系统。执行协议的每个主体的过程构成本地状态，并且所有本地状态构成系统的全局状态。每个主体的收发行为将导致本地状态的变化，这将导致全球状态的变化。在系统可到达的每个全局状态中是否满足协议的安全属性，如果不满足，则检测协议的安全缺陷。
模型检测方法已被证明是一种非常有效的方法,它具有高度自动化,检测过程不需要用户参与,如果协议存在安全漏洞，它可以自动生成反例。然而，因为该方法通过耗尽对所有可能的执行路径的搜索来发现协议的所有可能的执行缺陷,所以它具有易于发生状态空间爆炸并且不适合于检测复杂协议的缺点。
（3）定理证明方法
定理证明方法试图证明协议满足安全属性,而不是寻找对协议的攻击。因此，定理证明方法是一种正证明方法。
定理证明方法是一种相对较新的协议分析方法，仍有很大的发展空间。它的缺点是难以完全自动化。
