基于观察等价性的协议猜测攻击形式化检测方法_苗旭阳.pdf

密码学报ISSN 2095-7025 CN 10-1195/TNJournal of Cryptologic Research,2023,10(2):306319密码学报编辑部版权所有.E-mail:http:/Tel/Fax:+86-10-82789618基于观察等价性的协议猜测攻击形式化检测方法苗旭阳1,2,顾纯祥1,2,陆思奇1,21.数学工程与先进计算国家重点实验室,郑州 4500012.网络密码技术河南省重点实验室,郑州 450001通信作者:顾纯祥,E-mail:摘要:由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用 Tamarin 形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对 EKE、SPAKE 等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性.关键词:形式化分析;观察等价性;口令猜测攻击;Tamarin-Prover中图分类号:TP309.7文献标识码:ADOI:10.13868/ki.jcr.000596中文引用格式:苗旭阳,顾纯祥,陆思奇.基于观察等价性的协议猜测攻击形式化检测方法J.密码学报,2023,10(2):306319.DOI:10.13868/ki.jcr.000596英文引用格式:MIAO X Y,GU C X,LU S Q.Formal analysis method of protocol guessing attackbased on observation equivalenceJ.Journal of Cryptologic Research,2023,10(2):306319.DOI:10.13868/ki.jcr.000596Formal Analysis Method of Protocol Guessing Attack Based onObservation EquivalenceMIAO Xu-Yang1,2,GU Chun-Xiang1,2,LU Si-Qi1,21.State Key Laboratory of Mathematical Engineering and Advanced Computing,Zhengzhou 450001,China2.Henan Key Laboratory of Network Cryptography Technology,Zhengzhou 450001,ChinaCorresponding author:GU Chun-Xiang,E-mail:Abstract:Password-based security protocols are widely used.Due to the low entropy of passwords,such protocols are vulnerable to password guessing attacks.However,the current formal semanticsdo not have a proper description about the conditions for attackers to perform password guessing at-tacks.There is no uniform formal security attribute definition about the resistance against the protocolguessing attacks.For this reason,this paper proposes a formal detection method for protocol guessingattacks based on observation equivalence,uses multi-sets of rewriting rules to formally model the pro-tocol interaction process,gives standardized rules for password initialization and password guessing收稿日期:2021-12-26定稿日期:2022-03-01苗旭阳 等:基于观察等价性的协议猜测攻击形式化检测方法307behavior,and modifies the password-based symmetric encryption primitives to support password-basedsymmetric encryption protocol verification,theoretically transforms the formal analysis and detectionof the protocol password guessing attack into the judgment problem of whether the observation equiv-alence of the multi-set rewriting rule bi-system is established based the correctness of the guess.In theimplementation,this paper uses the analysis tool,Tamarin,to achieve automatic analysis on whetherthe password guessing attack is effective on the protocol.The proposed method is used to formallymodel and analyze traditional password authentication protocols such as EKE,SPAKE,and multi-factor authentication protocols,and automatically generates feasible password guessing attack pathsfor protocols in which password guessing attacks exist,hence the correctness and effectiveness of themethod are verified.Key words:formal analysis;observational equivalence;password guessing attack;Tamarin-Prover1引言基于口令的认证协议1能够有效保证用户信息的安全性,这种方式由于简便、易部署等特点在网络中得到广泛应用25.但由于用户选择的口令具有低熵性6,安全协议可能会存在在线或离线口令猜测攻击.执行在线猜测攻击的攻击者不断向服务器发送猜测的口令验证数据,根据服务器的回复信息来判断猜测数据的正确性.这种方法需要在网络中向服务器发送大量相同格式的数据包,攻击行为易于被服务器发现并自动识别,服务器可以通过设置访问策略等方法来防止这种攻击.而离线口令猜测攻击者通过窃听、阻截、重放信道上的消息等方式获取与口令相关的验证元,在本地对口令使用字典遍历、暴力破解等方式来获得口令.相比于在线猜测攻击,离线口令攻击行为更隐蔽,只需要对信道进行被动窃听和少量的主动请求消息发送,攻击行为难以被发现.并且,对于现实破解而言,离线口令破解可以借助并行加速等技术极大地提高破解效率,Hashcat、John the Ripper 等工具提供了开源平台.幸运的是,并不是所有口令协议都存在离线口令猜测攻击.Lowe7指出,攻击者必须能够使用验证元来测试它的猜测是否正确,一般情况下验证元来源于协议消息的冗余.验证元的存在是实施离线口令猜测攻击的必要条件,因此检测口令猜测攻击的本质归结到验证元的构造或检测过程.需要注意的是,在形式化分析过程中,我们不考虑实际情况中,攻击者对于口令的猜测使用字典遍历或者暴力穷举等方式的效率和实际有效性,例如口令分布8,9对于猜测攻击的影响或是口令库的生成10,11,仅考虑协议是否存在口令猜测攻击的理论可能.安全协议的符号模型形式化分析大多基于Dolev-Yao 敌手模型12,并假设理想的密码学原语模型.在 Dolev-Yao 模型中,敌手可以窃听、截获、篡改、重放公共信道上的任何消息.在理想模型中,对于加解密原语,敌手只有知道对应密钥才能解密消息;对于哈希函数模型,敌手不能从哈希值中获取到任何原始信息.Gong 等人13的早期工作开始尝试定义或检测离线口令猜测攻击.Lowe7对安全协议的离线口令猜测攻击进行了形式化定义,在进程代数 CSP 中对这种攻击进行了形式化建模,并使用模型检测器 FDR来对攻击进行检测,开启了对猜测攻击进行形式化分析的先河,但 Lowe 的定义依赖于验证元的人工选择,同时只支持被动攻击者的行为描述,自动化寻找依赖于人工经验.后续出现了多种验证猜测攻击的方法与工具1416,但验证规则缺乏一般性,不能描述猜测攻击的所有情况.Corin 等人17首先使用应用 演算的静态等价来表示猜测攻击,使用静态等价来导出检测猜测攻击的过程,但只考虑了基础项作为猜测值,不具有通用性.Blanchet 等人18在此基础上通过加强观察等价的条件来完善对于猜测攻击的定义,但只停留在理论层面.在安全协议的形式化分析中,大多数理论方法研究和工具开发都集中在跟踪属性(traceproperty)上,包括可达性、保密性和认证性等.但目前观察等价性19受到越来越多的关注,并且已经用来表示密码协议中的安全属性,例如投票协议20中的隐私性、匿名性,密文的不可区分性21等.根据文献综述研究22,23,部分密码协议形式化分析工具支持密码协议对于观察等价性的验证.Tamarin24使用双系统约束求解25基于多集重写技术添加观察等价性,支持用户可添加的等式理论和环境描述,可对不同能力的攻击者进行建模.ProVerif26使用应用 演算支持无限数量会话的观察等价性自动证明,但在工具中协议执行环境被隐式定义,不支持可变状态27和等式理论扩展.APTE28和308Journal of Cryptologic Research 密码学报 Vol.10,No.2,Apr.2023AKISS29支持验证观察等价性,但仅限于有限数量的会话,且不支持分支流程和自定义信道.SPEC30使用 spi 演算验证双系统的观察等价性,但只支持固定数量的加密原语,仅支持有限数量会话.Maude-NPA31基于多集重写技术支持观察等价性,类似于 Tamarin,但对于观察等价性满足的情况存在无法终止的问题,因此只提供观察等价性不成立的证明.本文的主要贡献如下:(1)提出了一种基于观察等价性的对口令认证协议中离线口令猜测攻击的形式化分析方法,对于基于口令的认证协议给出了通用性的口令初始化规则、协议流程建模方法、猜测攻击检验规则和对于口令加密原语的修改,将口令猜测攻击的形式化检验转化为由正确和错误猜测导出的双系统的观察等价性是否成立的判断,并给出了合理性证明.