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

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