论文部分内容阅读
在众多的安全协议分析方法中,基于串空间的形式化分析方法是当前的研究热点之一。串空间理论发展过程中有两个重要事件:其一是Guttman提出的串空间模型认证测试方法;其二是Song在串空间模型上提出的Athena方法。本文对Athena方法进行了深入分析,针对目前安全协议分析领域中公开的“开端”问题以及Athena方法自身的局限性,对该方法进行了扩展。取得的主要成果如下:(1)对Athena方法进行了系统的分析,介绍了Athena的假设条件,给出了Athena的语法和语义,分析了该逻辑的优点和局限性。在此基础上,分析了Athena的核心算法,讨论了Athena算法自动高效的原因,以及该算法如何避免状态空间爆炸的技术,指出了该算法的缺陷,形成原因以及解决的一般方法。最后,以Andrew协议为例,使用Athena方法,对其进行了分析和改进,消除其所存在的漏洞;以NS协议为例,分别使用Athena方法与模型检验工具SMV进行了分析,并对分析结果进行了比较。(2)Athena分析方法由于没有抽象更多的密码学原语,因此不能分析较复杂的安全协议。本文针对互联网密钥交换协议(IKEv2),对Athena方法进行了扩展。修改消息项结构,扩展密码学原语,使其能分析DH(Diffie-Hellman)密钥协商问题;修改内在项关系,使其能应对更复杂的消息构造情况;给出并证明了一个新的消减规则,并对相关命题和定理进行了扩展。(3)开端协议(Open-Ended Protocol)的分析是安全协议领域中一个待解决的重要问题。本文针对“开端”结构,引入集合的数学概念,建立新的消息类型,重新定义了串空间中的消息项、替换、入侵者模型,以及Athena相应的内在项、目标和目标绑定,给出了一个新的替代关系。应用扩展后的方法,对IKEv2协议进行了进一步的研究,发现一个新的认证性缺陷,给出了解决该缺陷的方法。