基于先验路径选择的安全协议形式化分析优化方法.pdfVIP

DOl:10.12379/j.issn.2096-1057.2025.08.06学术论文

ResearchPapers

基于先验路径选择的安全协议形式化分析优化方法

蔡光英蔡柳佳陆思奇王永娟王向宇

450001)

（河南省网络密码技术重点实验室郑州

(cguangying163@163.com)

OptimizationMethodforFormalAnalysisofSecurityProtocols

BasedonPriorPathSelection

CaiGuangying,CaiLiujia,LuSiqi,WangYongjuan,andWangXiangyu

(HenanKeyLaboratoryofNetworkCryptographyTechnology,Zhengzhou450001)

AbstractFormalanalysistechniquescandetectsecurityvulnerabilitiesinsecurityprotocols,but

whenanalyzingcomplexsecurityprotocols,thestatespaceexplosionproblemoftenpreventsthe

analysisfromterminating.Thefundamentalcauseofthisissueistheexponentialincreaseinthe

numberofprotocolstatesduetoanexcessivenumberofredundantnodes.Toaddressthis,the

priorpathselectionmethodwasproposed,whichusedthenodesofalreadysearchedpathstoguide

theselectionofsubsequentnodes,reducingthenumberofprotocolstatesandeffectively

circumventingthestatespaceex-plosion,thusimprovingefficiency.Further,byutilizingthe

OracleinterfaceoftheTamarinmodelcheckingtool,thismethodwasappliedtotheanalysisof

securityprotocols,andcomparativeexperimentswereconductedon5protocolswith8lemmas.

TheexperimentalresultsshowthatthePriorPathSelectionmethodsuccessfullyprovidesanalysis

resultsforprotocolswhereconventionalpathsearchisineffective,mitigatingthestatespace

explosionproblem.

Keywordspriorpathselectionmethod;statespaceexplosion;formalanalysis;modelchecking;

Tamarin

摘要形式化分析技术能够检测出安全协议存在的安全漏洞，但是对一些复杂的安全协议进行分

析时，往往会出现状态空间爆炸问题导致分析无法终止.无用节点过多使得协议状态数量剧增是导

致状态空间爆炸的根本，针对这一问题提出了先验路径选择法，利用已有哪些信誉好的足球投注网站的路径节点指导后续节

点的选择，减少协议状态数量，有效规避了状态空间爆炸并提高了效率.进一步通过Tamarin模型检

测工具的Oracle接口，将这种方法应用于安