密码学报ISSN2095-7025CN10-1195/TNJournalofCryptologicResearch,2023,10(2):306–319©《密码学报》编辑部版权所有.E-mail:jcr@cacrnet.org.cnhttp://www.jcr.cacrnet.org.cnTel/Fax:+86-10-82789618基于观察等价性的协议猜测攻击形式化检测方法苗旭阳1,2,顾纯祥1,2,陆思奇1,21.数学工程与先进计算国家重点实验室,郑州4500012.网络密码技术河南省重点实验室,郑州450001通信作者:顾纯祥,E-mail:gcxiang5209@163.com摘要:由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用Tamarin形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对EKE、SPAKE等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性.关键词:形式化分析;观察等价性;口令猜测攻击;Tamarin-Prover中图分类号:TP309.7文献标识码:ADOI:10.13868/j.cnki.jcr.000596中文引用格式:苗旭阳,顾纯祥,陆思奇.基于观察等价性的协议猜测攻击形式化检测方法[J].密码学报,2023,10(2):306–319.[DOI:10.13868/j.cnki.jcr.000596]英文引用格式:MIAOXY,GUCX,LUSQ.Formalanalysismethodofprotocolguessingattackbasedonobservationequivalence[J].JournalofCryptologicResearch,2023,10(2):306–319.[DOI:10.13868/j.cnki.jcr.000596]FormalAnalysisMethodofProtocolGuessingAttackBasedonObservationEquivalenceMIAOXu-Yang1,2,GUChun-Xiang1,2,LUSi-Qi1,21.StateKeyLaboratoryofMathematicalEngineeringandAdvancedComputing,Zhengzhou450001,China2.HenanKeyLaboratoryofNetworkCryptographyTechnology,Zhengzhou450001,ChinaCorrespondingauthor:GUChun-Xiang,E-mail:gcxiang5209@163.comAbstract:Password-basedsecurityprotoco...
