協議安全分析的方法有攻擊檢測方法和形式化分析方法。

攻擊檢測也稱為滲透檢測，是一種非正式的分析方法。它根據幾種已知的攻擊方法攻擊協議，以驗證攻擊是否有效驗證協議是否安全。這種方法的缺點是只能發現已知的安全漏洞和缺陷，並且無法發現未知的安全漏洞和缺陷。

早期協議安全性分析主要採用攻擊檢測方法，但仍具有重要價值。

協議的形式化分析使協議的描述形式化，並使用手動和計算機分析來推斷確定協議是否安全。與非正式分析方法相比，形式分析方法可以全面深入地檢測協議的微妙安全漏洞和缺陷。它不僅可以發現已知的安全漏洞和缺陷，還可以發現對未知安全漏洞和缺陷協議的正式分析，這些漏洞極大地促進了加密協議設計：

1）在協議設計階段啟用分析以避免可能發生的設計錯誤。

2）已經為協議的設計提出了許多新的設計原則。

協議的正式分析方法一般有以下三類：

(1)形式邏輯方法

這種分析方法定義了協議的目標，並在協議的最初時刻確定了參與者的知識和信念,顺利获得協議中的發送和接收步驟生成新知識，並使用推理規則來推導最終的知識和信念。如果最終的一組知識和信念不包含要取得的目標知識和信念的陳述,則表明該協議存在安全缺陷。

(2)模型檢測方法

模型檢測方法的基本思想是將加密協議視為分佈式系統。執行協議的每個主體的過程構成本地狀態，並且所有本地狀態構成系統的全局狀態。每個主體的收發行為將導致本地狀態的變化，這將導致全球狀態的變化。在系統可到達的每個全局狀態中是否滿足協議的安全屬性，如果不滿足，則檢測協議的安全缺陷。

模型檢測方法已被證明是一種非常有效的方法,它具有高度自動化,檢測過程不需要用戶參與,如果協議存在安全漏洞，它可以自動生成反例。然而，因為該方法顺利获得耗盡對所有可能的執行路徑的搜索來發現協議的所有可能的執行缺陷,所以它具有易於發生狀態空間爆炸並且不適合於檢測複雜協議的缺點。

（3）定理證明方法

定理證明方法試圖證明協議滿足安全屬性,而不是尋找對協議的攻擊。因此，定理證明方法是一種正證明方法。

定理證明方法是一種相對較新的協議分析方法，仍有很大的开展空間。它的缺點是難以完全自動化。