针对猜测攻击的Athena方法的扩展

Extensions to Athena for Analyzing Guessing Attack

猜测攻击是安全协议中一类特殊问题,对其进行研究具有现实意义。本文针对猜测攻击,引入了基于串空间模型的Athena分析方法,并考虑了攻击者对弱口令的猜测能力。为此,在串空间模型的消息项中引入了可验证项的概念,以描述猜测攻击条件中的验证项,同时扩展了串空间中攻击者的能力,赋予了攻击者对弱口令的猜测能力;为在Athena后继函数搜索算法中实现对验证项的关联,以判断猜测攻击,在Athena方法的状态表示法中引入猜测验证目标及猜测验证目标绑定的概念,对状态、推理规则进行相应的修改,同时扩展后继状态函数,使扩展后的函数具备分析猜测攻击的能力;最后运用扩展后的Athena方法对会话密钥建立协议(key-establishment protocol)进行分析。分析发现,当pk为对称密钥时,协议存在猜测攻击,并给出了攻击路径。

In this paper we extend Athena approach based on strand space, considering the intruder＇s guessing poorlychosen password ability for analyzing guessing attack automatically and efficiently. Firstly, we present a new notion and its expression of verifiable term to describe the conditions of guess attacks and enhance the intruder＇s ability in strand space to endue the intruder＇s guessing poorly-chosen password talent. Then, in order to relate verifiers in the search process of the next-state function of Athena, two new notions of guessing verifier goal and guessing verifier goal binding are presented. Accordingly, the state expressive way and inference rules are adapted. In addition, next-state functions is extended, so that it is able to analyse guessing attacks. Finally, we analyze the key-establishment protocol using the extended Athena approach, and find a guessing attack when pk is a symmetric key.