安全协议形式化分析方法  

On Methods and Techniques for Formal Analysis of Security Protocols

作　　者：韩继红[1] 郭渊博[1] 王亚弟[1] 

机构地区：[1]信息工程大学电子技术学院,河南郑州450004

出　　处：《信息工程大学学报》2008年第3期272-276,共5页Journal of Information Engineering University

基　　金：国家自然科学基金资助项目(60503012)

摘　　要：安全协议的形式化分析是检验协议安全性的必要手段。为了实现协议的规范描述和合理完备的安全性验证,各种数学理论和人工智能方法被引进安全协议形式化分析与自动化验证领域。主要从逻辑方法、模型检测方法和证明方法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.

关 键 词：安全协议 形式化方法 逻辑 模型检测 证明 

分 类 号：TN918[电子电信—通信与信息系统]