信息安全研究2025，Vol.11Issue(8)：727-735,9.DOI:10.12379/j.issn.2096-1057.2025.08.06
基于先验路径选择的安全协议形式化分析优化方法
Optimization Method for Formal Analysis of Security Protocols Based on Prior Path Selection
摘要
Abstract
Formal analysis techniques can detect security vulnerabilities in security protocols,but when analyzing complex security protocols,the state space explosion problem often prevents the analysis from terminating.The fundamental cause of this issue is the exponential increase in the number of protocol states due to an excessive number of redundant nodes.To address this,the prior path selection method was proposed,which used the nodes of already searched paths to guide the selection of subsequent nodes,reducing the number of protocol states and effectively circumventing the state space ex-plosion,thus improving efficiency.Further,by utilizing the Oracle interface of the Tamarin model checking tool,this method was applied to the analysis of security protocols,and comparative experiments were conducted on 5 protocols with 8 lemmas.The experimental results show that the Prior Path Selection method successfully provides analysis results for protocols where conventional path search is ineffective,mitigating the state space explosion problem.关键词
先验路径选择法/状态空间爆炸/形式化分析/模型检测/TamarinKey words
prior path selection method/state space explosion/formal analysis/model checking/Tamarin分类
信息技术与安全科学引用本文复制引用
蔡光英,蔡柳佳,陆思奇,王永娟,王向宇..基于先验路径选择的安全协议形式化分析优化方法[J].信息安全研究,2025,11(8):727-735,9.基金项目
国家重点研发计划项目(2023YFB2705000) （2023YFB2705000）
河南省重大公益项目(201300210200) （201300210200）
