论文部分内容阅读
随着网络技术的发展,网络应用己经日益渗透到我们生活的方方面面,但网络给人们带来巨大便利的同时也带来了一些潜伏的不安全因素。作为通信基础的协议,承载着网络中通信的所有数据和信息,担当着通信方之间的通信桥梁,如何从协议的角度实现安全是一个重要而基本的研究课题。使用密码算法的安全协议为开放网络中的安全通信提供了基本保证,但实践证明,即便是一个简单的协议,其分析也是不容易的。协议的分析需要一套严格的形式化方法。形式化的分析方法是采用各种形式化的语言或者模型,为安全协议建立模型,并按照规定的假设和分析、验证方法证明协议的安全性。形式化的分析方法是当前分析安全协议领域研究的热点。近几年来,密码学家提出了许多关于安全协议的形式化分析方法,以检验协议中是否存在安全缺陷。串空间模型是一种著名的安全协议形式化模型,它的提出本身体现了协议形式化分析领域的发展方向,它结合了多种形式化方法的思想和技术,而且串空间理论是定理证明方法,可以手动的完成证明,得到可信的结果。该理论简洁易用,而且基于图论对协议进行描述,可以使用图形表示在协议证明中提供辅助说明。从串空间模型提出到现在,已经有研究者利用它发现了一些协议的漏洞,也有不少研究者利用它设计出了新型的安全协议自动分析工具。可见,这是一种很有研究前景的形式化模型。但是基本的串空间理论只能分析简单的使用连接、加密操作的安全协议,且对攻击者的能力描述有限,大大限制了其可分析的协议的范围。随着二十世纪七十年代以来,各种密码算法已经大量应用于安全协议中,如签名、散列函数等。为了能够分析更多类型的数据类型和操作,我们对串空间理论进行了扩展和完善。本文的主要工作有以下几个方面:●原理性阐述了几个具有代表性的安全协议形式化分析技术,其中详细阐述了串空间理论的定义、分析协议的方法和原理。●从语义上研究串空间模型,针对BAN逻辑语义不明确的问题,给出了基于串空间模型的逻辑的语义表示,并对BAN逻辑进行扩展,重新定义了BAN逻辑的协议分析过程。●介绍了串空间理论两个重要的发展:理想和认证测试。●对基本串空间理论和认证测试进行了扩展,包括项代数的扩展和攻击者模型的扩展,加入了对散列操作、签名操作的描述和分析能力。本文的主要创新之处为:●给出了基于串空间模型的BAN逻辑的语义表示,并对BAN逻辑进行扩展。●扩展串空间模型,使其能够分析含有签名、散列函数的协议。