安全協議的形式化分析是檢驗協議安全性的必要手段。為了實現協議的規范描述和合理完備的安全性驗證，各種數學理論和人工智能方法被引進安全協議形式化分析與自動化驗證領域。主要從邏輯方法、模型檢測方法和證明方法3個方面對符號化的安全協議形式化分析方法進行了綜述，并指出了今后該領域的研究方向。