安全协议的形式化分析是检验协议安全性的必要手段。为了实现协议的规范描述和合理完备的安全性验证，各种数学理论和人工智能方法被引进安全协议形式化分析与自动化验证领域。主要从逻辑方法、模型检测方法和证明方法3个方面对符号化的安全协议形式化分析方法进行了综述，并指出了今后该领域的研究方向。