基于串空间模型的安全协议验证及算法研究

郑州大学硕士学位论文基于串空间模型的安全协议验证及算法研究姓名：马中良申请学位级别：硕士专业：计算机软件与理论指导教师：周清雷20070501基于串空间模型的安全协议验证及算法研究作者：马中良学位授予单位：郑州大学相似文献(10条)1.会议论文解云峰.李之棠.石曙东基于串空间模型的安全协议形式化分析方法研究2004用于安全协议形式化分析的串空间(strandspace)模型,是一种结合定理证明和协议迹的混合方法,可以有效地描述和证明安全协议的正确性.本文对串空间模型近年来在扩展性、与其它形式化方法的关系、安全协议自动检验技术以及串空间模型的应用等几个研究层面作了全面介绍.2.学位论文刘冰基于串空间模型的安全协议形式化分析技术研究2007随着网络技术的发展，网络应用己经日益渗透到我们生活的方方面面，但网络给人们带来巨大便利的同时也带来了一些潜伏的不安全因素。作为通信基础的协议，承载着网络中通信的所有数据和信息，担当着通信方之间的通信桥梁，如何从协议的角度实现安全是一个重要而基本的研究课题。使用密码算法的安全协议为开放网络中的安全通信提供了基本保证，但实践证明，即便是一个简单的协议，其分析也是不容易的。协议的分析需要一套严格的形式化方法。形式化的分析方法是采用各种形式化的语言或者模型，为安全协议建立模型，并按照规定的假设和分析、验证方法证明协议的安全性。形式化的分析方法是当前分析安全协议领域研究的热点。近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是否存在安全缺陷。串空间模型是一种著名的安全协议形式化模型，它的提出本身体现了协议形式化分析领域的发展方向，它结合了多种形式化方法的思想和技术，而且串空间理论是定理证明方法，可以手动的完成证明，得到可信的结果。该理论简洁易用，而且基于图论对协议进行描述，可以使用图形表示在协议证明中提供辅助说明。从串空间模型提出到现在，已经有研究者利用它发现了一些协议的漏洞，也有不少研究者利用它设计出了新型的安全协议自动分析工具。可见，这是一种很有研究前景的形式化模型。但是基本的串空间理论只能分析简单的使用连接、加密操作的安全协议，且对攻击者的能力描述有限，大大限制了其可分析的协议的范围。随着二十世纪七十年代以来，各种密码算法已经大量应用于安全协议中，如签名、散列函数等。为了能够分析更多类型的数据类型和操作，我们对串空间理论进行了扩展和完善。本文的主要工作有以下几个方面：·原理性阐述了几个具有代表性的安全协议形式化分析技术，其中详细阐述了串空间理论的定义、分析协议的方法和原理。·从语义上研究串空间模型，针对BAN逻辑语义不明确的问题，给出了基于串空间模型的逻辑的语义表示，并对BAN逻辑进行扩展，重新定义了BAN逻辑的协议分析过程。·介绍了串空间理论两个重要的发展：理想和认证测试。·对基本串空间理论和认证测试进行了扩展，包括项代数的扩展和攻击者模型的扩展，加入了对散列操作、签名操作的描述和分析能力。本文的主要创新之处为：·给出了基于串空间模型的BAN逻辑的语义表示，并对BAN逻辑进行扩展。·扩展串空间模型，使其能够分析含有签名、散列函数的协议。3.期刊论文慕建君.MUJian-jun一种形式化分析安全协议的新模型-西安电子科技大学学报（自然科学版）2006,33(3)串空间是安全协议形式化分析的一种新模型.利用次序关系的理论证明了借助串空间模型进行安全协议形式化分析的一个重要结论.通过构造入侵者串的方法,针对Woo-Lam协议提出了一个入侵者串空间模型,同时利用此入侵者串空间模型分析了该协议存在的缺陷,说明了改进后的Woo-Lam协议可克服此缺陷.与现有安全协议形式化分析方法相比较,串空间模型不仅具有简洁直观的优点,而且还可避免状态空间爆炸的问题.4.会议论文黄寄洪.胡振宇.吕双双网络安全协议的形式化分析与应用2002串空间模型(strandspace)是一种有效的安全协议形式化分析工具.利用串空间模型,我们设计了一个安全电子商务协议SSECT.从中展示了串空间模型怎样利用加密和随机数来实现协议成员的认证.所设计的SSECT协议在功能和安全保证上实现了电子商务交易标准(SET)所要求的购买申请,支付认证,付款等功能.5.学位论文李谢华基于串空间模型的安全协议形式化验证方法的研究2007安全协议是构建网络安全环境的基石,是网络安全通信系统的核心技术,它正确性对整个网络环境的安全起着至关重要的作用.然而如何保证安全协议的全性,如何使协议的设计能够满足安全性的要求,如何提高安全协议自动化验的效率等,都是安全协议研究领域不断探索的问题.为了保证安全协议的安全研究人员提出了形式化的方法.虽然形式化方法已经成功地发现了许多安全协议的漏洞和攻击,但是这些方法仍然存在很多问题.一些形式化的方法本身并完善,因此无法适用于某些安全协议的验证；一些理论完善的形式化方法由于杂而缺乏自动化工具的支持；现有的自动化协议验证工具资源占用量大,要求高.鉴于此,本文以串空间模型理论和认证测试方法为基础,针对上上方面的问题进行了深入的研究,并且提出了有效的解决方案,取得了一定的科研成果.论文的研究内容主要包括以下三个方面:首先,对于串空间模型和认证测试方法理论在典型安全协议验证中的应用进行了深入的研究,通过形式化的验证指出协议中存在的安全漏洞,构造可能的攻击方式,并以理论分析结果为指导提出对这些协议的改进方案,最后使用理论方法验证改进协议的安全性.本文还以认证测试方法为理论基础,对通用安全协议的设计方法进行了研究.以Needham-Schroeder协议为例,使用基于认证测试的通用安全协议设计方法指导该协议的重新设计,并对重新设计后的协议应用形式化的理论方法证明其安全性.其次,在对认证测试方法深入研究的基础上,指出该方法在对称密钥协议验证中存在无法确定消息项初始产生主体的问题,以及由此可能引起的消息重放攻击和类型攻击.通过引入消息类型对认证测试方法进行了改进,提出了基于消息类型检测的改进认证测试方法,并通过对认证协议的验证表明了改进的认证测试方法能够有效地发现原有认证测试方法没有发现的类型攻击.与此同时,还将改进的认证测试方法应用于无线认证协议的验证,证明了改进的认证测试方法对无线认证协议安全性验证的有效性.然后,以改进的认证测试方法为基础,提出了安全协议的认证属性中不仅要满足一致性属性,还要满足测试分量的唯一性属性.通过定义测试分量唯一性,排除由于消息重放而引起攻击的可能性.并提出了安全协议自动化验证算法--AAAP(AutomaticAnalyzerofAuthenticationProtocols),AAAP算法在多种认证协议证明中的应用说明了该算法能够有效发现协议中存在的漏洞并及时终止算法的运行；而与类似算法相比,AAAP算法在协议验证中具有遍历状态空间少、运行效率高的优点.最后,基于AAAP算法开发了安全协议自动化验证原型系统,并通过对多个经典认证协议的实验验证说明该原型系统的有效性.本文创新性的工作主要有:1.改进了认证测试方法,使之能够为对称密钥协议提供更为完善的验证.通过引入消息类型的概念,提出了基于消息类型检测的改进认证测试方法,用于检测协议中是否存在由消息重放而引起的攻击,解决了原有认证测试方法无法发现重放攻击的问题,在理论上具有创新性.2.提出了测试分量唯一性属性,完善了协议认证属性的描述.通过对测试分量唯一性的证明,验证协议抵抗重放攻击和类型攻击的能力,在理论上具有创新性.3.提出了基于改进认证测试方法的AAAP算法.通过对协议一致性属性和唯一性属性的自动化证明,验证协议能够达到的安全目标.AAAP算法对多种认证协议的验证说明该算法能够及时发现协议中存在的漏洞并终止协议运行,与同类型算法相比资源耗费小,在理论的应用上具有创新的特点.4.开发了基于AAAP算法的安全协议自动化验证原型系统,将理论模型应用于实际的安全协议验证.应用该原型系统验证了Needham-Schroeder公钥协议、NSL协议、Neuman-Stubblebine认证协议、Woo-Lam单向认证协议的安全性,验证的结果与使用理论模型的验证结果具有较好的一致性,在理论的应用上具有创新的特点.6.期刊论文皮建勇.杨雷.刘心松.李泽平.PIJian-yong.YANGLe.LIUXin-song.LIZe-ping一种新的安全协议及其串空间模型分析-计算机科学2010,37(1)针对有限域上计算离散对数的困难,提出了一种新的身份认证与密钥协商安全协议--PJY.PJY安全协议通过两次握手就可以验证通信双方的身份,同时产生对等的会话密钥.采用串空间模型分析该安全协议的正确性,通过构造渗透串空间模型,采用认证测试证明了PJY安全协议在任意一种攻击串模式下都具有单射一致性和机密性,从而证明了PJY安全协议的正确性.7.学位论文方燕萍串空间模型及其认证测试方法的扩展与应用2009安全协议提供安全服务，是构建网络安全的基石。随着网络的迅速发展，越来越多的密码技术被应用到安全协议中，保证了网络不同程度的安全性。然而各种针对协议的攻击技术也不断出现，这对安全协议的分析提出了更高的要求。形式化方法是一种非常有效的安全协议分析的方法。串空间模型及相关理论的出现推动了安全协议的形式化分析研究。然而原始的串空间模型及其认证方法在分析一些安全协议时还存在一些不足，因此本文针对基于丰富密码学的安全协议和基于猜测攻击的安全协议，扩展了串空间模型和认证测试方法。由于原始的串空间模型仅考虑了一些简单操作，无法描述和分析在安全协议中使用越来越广泛的其他一些操作，如散列函数、签名运算和DH计算等，因此需要扩展串空间模型。由于认证测试方法以串空间模型为基础，因此串空间模型中存在的一些不足在认证测试方法中同样存在，因此本文还提出了一种基于丰富密码学的扩展认证测试方法。扩展后的模型和方法能够更精确地描述和分析安全协议的安全性，并能够应用于更广泛的领域。由于分析安全协议猜测攻击时需要考虑密码系统不完善所产生的问题，而原始的认证测试方法对密码系统做了完善的假设，需要三个基本前提假设，难以发现安全协议中存在的猜测攻击。本文提出了一种基于猜测攻击的扩展认证测试方法。首先定义了猜测数据和验证项，并将其引入到串空间模型中；然后定义了验证项判断规则和验证项判断算法，并将其引入到认证测试方法中。扩展后的模型和方法能够发现安全协议中存在的猜测攻击。为验证扩展串空间模型和认证测试方法的有效性，本文首先分析了SSL3.0和TLS1.0握手协议，验证了协议的认证性；然后分析了Yahalom-BAN和EXE协议，发现了协议中存在的猜测攻击。实例分析结果说明了扩展说明了扩展串空间模型和认证测试方法的正确性和有效性。8.期刊论文董军.杨秀娟.赵艳芹.DONGJun.YANGXiu-juan.ZHAOYan-qin基于串空间模型安全协议形式化分析方法的研究-计算机技术与发展2008,18(4)从串空间模型理论人手,提出了三种典型的串空间形式化方法(基于极小元理论的串空间方法、基于理想与诚实理论的串空间方法、基于认证测试理论的串空间方法),并对每一种方法的证明步骤及优缺点进行了分析.在此基础上,应用提出的串空间方法对Yahalom协议的秘密性和认证性进行了分析.分析结果表明利用不同方法的优点,能更好地保证安全协议形式化分析的准确性.9.期刊论文周清雷.王峰.赵东明.ZHOUQing-Lei.WANGFeng.ZHAODong-Ming基于认证测试的一种安全协议一致性分析方法-计算机科学2007,34(10)认证测试[1]技术是串空间(strandspace)理论的进一步发展,不仅用于认证协议的安全性分析而且还用于指导认证协议的设计[2].但在分析安全协议为何不正确以及如何改进方面,与其他的形式化验证方法一样,也不能提供更深入有效的分析.本文提出了参数一致性矩阵的概念并运用参数一致性矩阵对协议的一致性进行分析,说明了协议失败的原因并给出改进的方向.分析过程的形式化有利于协议分析自动化工具的实