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.

Key words: prior path selection method, state space explosion, formal analysis, model checking, Tamarin

摘要： 形式化分析技术能够检测出安全协议存在的安全漏洞，但是对一些复杂的安全协议进行分析时，往往会出现状态空间爆炸问题导致分析无法终止.无用节点过多使得协议状态数量剧增是导致状态空间爆炸的根本，针对这一问题提出了先验路径选择法，利用已搜索的路径节点指导后续节点的选择，减少协议状态数量，有效规避了状态空间爆炸并提高了效率.进一步通过Tamarin模型检测工具的Oracle接口，将这种方法应用于安全协议的分析，并针对5个协议8个引理开展了对比实验.实验结果表明，先验路径选择法对于常规路径搜索无效的协议，成功给出了分析结果，缓解了状态空间爆炸问题.

关键词: 先验路径选择法, 状态空间爆炸, 形式化分析, 模型检测, Tamarin