安全协议形式化分析方法

On Methods and Techniques for Formal Analysis of Security Protocols

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

Formal analysis of security protocols is the necessary measure for proof-testing of protocol security properties. In order to implement the specification of protocols and verification of security properties soundly and completely, many mathematical theories and artificial intelligence approaches are brought into the security protocols＇ formal analysis and automatic verification fields. In this pa- per, a survey in formal analysis methods for security protocols is presented, including logic-based, model checking based and proof-based, several research directions are pointed out in the end.