安全协议形式化分析方法研究综述  

A Review of Formal Analysis Methods for Security Protocols

作　　者：缪祥华[1,2] 黄明巍 张世奇 张世杰 王欣源 MIAO Xiang-hua;HUANG Ming-wei;ZHANG Shi-qi;ZHANG Shi-jie;WANG Xin-yuan(Faculty of Information Engineering and Automation,Kunming University of Science and Technology;Yunnan Key Laboratory of Computer Technology Applications)

机构地区：[1]昆明理工大学信息工程与自动化学院 [2]云南省计算机技术应用重点实验室

出　　处：《化工自动化及仪表》2024年第3期367-378,共12页Control and Instruments in Chemical Industry

摘　　要：介绍了安全协议的基本概念和分类,然后对安全协议形式化分析方法进行了详细介绍,包括基于模态逻辑的方法、基于模型检测的方法、基于定理证明的方法和基于可证明安全性理论的方法。其中,基于模型检测的方法是目前应用最广泛的一种方法,因此详细介绍了一些常用的基于模型检测方法的工具。最后,总结了当前安全协议形式化分析方法的研究热点和未来的发展方向。The basic concepts and classifications of security protocols were introduced and then,the formal analysis methods for security protocols were described,including methods based on modal logic and those based on model detection,theorem proving and provable security theory,of them,that based on model detec-tion is the most widely used method.In addition,some commonly-used tools based on model detection methods were introduced in detail and both research hotspots and future development directions of formal analysis methods for security protocols were summarized.

关 键 词：安全协议 形式化分析 模态逻辑 模型检测 定理证明 可证明安全性 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]