一类具有“开端”结构的安全协议分析方法研究

Formal Analysis Approach for a Kind of Open-ended Protocols

开端协议(Open-ended Protocol)的分析是安全协议领域中一个待解决的重要问题,而IKE则是一个有代表性的具有"开端"结构的安全协议。本文基于串空间的Athena方法,针对IKEv2协议中的"开端"结构涉及的DH(Dif-fie-Hellman)问题,增加了群、散列函数等原语,给出并证明了一个新的消减规则;针对"开端"结构,引入了集合的数学概念,建立了新的消息类型,重新定义了串空间中的消息项、替换、入侵者模型,以及Athena相应的内在项、目标和目标绑定,给出了一个新的替代关系。应用扩展后的方法,分析了协议,发现一个新的认证性缺陷,给出了解决该缺陷的方法。

The formal analysis of Open-ended Protocols is one of emerging areas of research. The IKEv2 protocol offers a complex example. Our work is based on Athena which is an efficient automatic checking approach. We introduce set theory to deal with Open-ended structure. The new notion of message terms, substitution and the penetrator model are given and the relevant propositions or theorem such as interm relation, goal and goal-binding are therefore modified and proved. A new relation is proposed which is used in order to keep the character of Athena approach. We also introduce the ability on modeling the DH problem to Athena according to IKEv2 protocol, a new pruning theorem is given and proved. Based on the research, we analyze IKEv2 protocol, and find a new weakness of authentication. An amendment is given.