基于petri网的安全协议分析与检测方法的研究

贵州大学硕士学位论文基于Petri网的安全协议分析与检测方法的研究姓名：梅翀申请学位级别：硕士专业：计算机应用技术指导教师：孟传良20080501基于Petri网的安全协议分析与检测方法的研究作者：梅翀学位授予单位：贵州大学相似文献(10条)1.期刊论文刘进.陈丹.肖德宝.LIUJin.CHENDan.XIAODebao基于着色petri网的安全协议验证方法-华中师范大学学报（自然科学版）2006,40(3)设计安全协议时,协议的安全性验证是消除安全协议脆弱性和不精确性的关键步骤,验证安全协议的模型和工具有很多.提出了一种基于着色petri网的安全协议验证方法.通过采用该方法对一个STS协议进行了分析,证明了这种方法的有效性,并根据分析结果给出了改进后的STS协议.2.学位论文顾明甲基于网络协议的Petri网研究——利用着色Petri网分析验证安全协议2009在因特网技术飞速发展的今天，信息安全问题已经成为日益突出的问题。安全协议的出现虽然在很大程度上提高了网络信息传输的安全性，但同时因为设计上的缺陷性，安全协议也存在着很多漏洞。在当前，安全协议的形式化分析已经成了一个热点研究问题。目前安全协议的形式化分析方法主要包括：形式逻辑方法[1]、模型检测方法[2]、定理证明方法和Petri网方法[3-4]，这些方法各有自己的优点和缺点。本文采用的研究方法是基于着色Petri网的安全协议形式化分析，开展了以下主要工作：1.介绍了安全协议的基础知识和常见的安全协议形式化分析方法；阐述了Petri网的定义和Petri网的动态特性，并介绍了着色Petri网的相关知识。2.采用一种基于着色Petri网的安全协议验证方法，该方法采用逆向状态分析方法以及Petri网的可达性分析思想。而后，用两个安全协议实例来验证这种方法的有效性，同时，发现随着安全协议复杂性的增加，Petri网模型的状态空间爆炸问题也随之发生，并且此模型只能验证已知的安全协议漏洞，无法检测未知的安全攻击。3.尝试采用一种基于CPNTools的安全协议分析与验证方法来改进状态空间爆炸问题，文中以TMN协议为例，验证了该方法的有效性。方法中提出了DB-place概念，使入侵模型变得简单明了，并且制定令牌传递机制来改善状态空间爆炸问题。关键字：安全协议；协议漏洞；形式化分析；着色Petri网；可达性；状态空间爆炸；重放攻击；CPNTools3.期刊论文郑君杰.肖军模.杨明.刘志华.叶松.周延年.ZHENGJun-Jie.XIAOJun-Mo.YANGMing.LIUZhi-Hua.YESong.ZHOUYan-Nian基于有色Petri网的安全协议安全性仿真-系统仿真学报2006,18(11)如何验证安全协议的安全性是一项非常重要的工作.提出了一种基于有色Petri网的安全协议形式化描述与安全性仿真验证方法.给出协议的有色Petri网模型,分析协议运行过程中可能出现的不安全状态,利用Petri网的状态可达性判断这些不安全状态是否可达从而验证协议的安全性.针对Diffie-Hellman协议给出了具体的仿真分析过程,证明了这种方法的有效性.4.期刊论文刘道斌.郭莉.白硕基于Petri网的安全协议形式化分析-电子学报2004,32(11)本文提出了一种基于Petri网的安全协议形式化描述和安全性验证的方法.该方法的特点是,利用逆向状态分析判定协议运行过程中可能出现的不安全状态,利用Petri网的状态可达性分析判断这些不安全状态是否可达.通过实例,我们证明了这种方法的有效性.5.会议论文林松.戴宗坤电子支付安全协议的Petri网模型及分析2005通过对电子支付安全协议的研究,利用Petri网描述了电子支付安全协议处理流程;根据可达树分析了电子支付协议Petri网模型的正确性、安全性、公平性、可达性和活性.基于Petri网理论研究电子支付安全协议的工作,对于指导电子支付相关安全项目的研究以及解决实际安全问题具有一定的理论价值和实践意义.6.会议论文黎波涛.罗军舟不可否认协议形式化分析的Petri网方法2005Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用,但目前还没有人使用Petri网来分析不可否认协议.本文以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其它形式化方法无法描述的协议性质.使用该方法分析J.Zhou和D.Gollmann的公平不可否认协议发现了它议的一个许多其它形式化方法不能发现的已知缺陷.7.学位论文关展鹏基于Petri网的安全协议分析与验证技术2006在一个分布式的网络环境中，人们通过安全协议实现安全共享网络资源的需求，因此安全协议的安全性逐渐成为网络安全的关键。传统的安全协议分析技术包括传统的基于推理结构性方法，基于攻击结构性方法以及基于证明结构性方法三大类。Petri网原本是用于并行系统分析的工具，但随着关注安全协议的学者不断实践，使用Petri网方法实现对安全协议的分析验证已经初露端倪。继[ALMU03]对STS协议的成功分析之后，[GULO05l和[DRES05]也分别成功地对3GPPAKA协议和SAP无线协议进行分析，其中[GULO05]的工作是本文的重点内容。BAN逻辑是基于推理结构性方法的经典，但是它本身具有一定的缺陷，尤其是对重放攻击的检测能力十分弱。3GPPAKA协议设计者使用BAN逻辑进行分析，声称协议的安全目标已经达到[3GTS33]。然而，本文使用Petri网的分析将会得到不同的结果。一个认证协议可以看成在其执行过程中通信实体信仰不断变化的过程，因此对一个认证协议的分析可视为对主体信仰的评估。KG逻辑正是基于信仰变化的逻辑。本文将使用KG逻辑对设计者的BAN逻辑分析工作进行改进，得到与Petri网一致的结果。8.期刊论文林松.戴宗坤.LINSong.DAIZong-kun电子支付安全协议的Petri网模型及分析-大连理工大学学报2005,45(z1)通过对电子支付安全协议的研究,利用Petri网描述了电子支付安全协议处理流程;根据可达树分析了电子支付协议Petri网模型的正确性、安全性、公平性、可达性和活性.基于Petri网理论研究电子支付安全协议的工作,对于指导电子支付相关安全项目的研究以及解决实际安全问题具有一定的理论价值和实践意义.9.学位论文曾杰安全协议的形式化描述与验证2004该论文主要讨论了安全协议的形式分析方法,作者主要研究内容如下:1)简要介绍了BAN逻辑为主的形式逻辑在对协议的描述与验证;2)采用有穷自动机对安全协议进行分析,并简介了自动机分析协议的一般方法;3)采用Petri网描述和分析了某工商局单向认证协议,并用SML协议形式描述语言描述该协议;4)着重使用Petri网的关联矩阵、状态方程求解的方法分析TMN密码协议,并验证TMN协议的安全缺陷,最终说明利用Petri分析安全协议是可行的;5)用Petri网表示BAN-Yahalom协议的重放攻击.分析方法有待后续工作.10.期刊论文洪志国.王永滨.石民勇.HONGZhi-guo.WANGYong-bin.SHIMin-yongLEO卫星网络中安全协议的建模与性能分析-计算机工程2009,35(7)在分析低轨(LEO)卫星网络的通信过程和几何特性的基础上,建立LEO卫星网络在全双工通信模式下的随机Petri网(SPN)模型,采用SPNP6.0软件,针对2种安全协议IKE和ISAKMP的野蛮交换模式,以及空间通信协议规范SCPS-SP,分析卫星网络的平均时延并进行了模型仿真.本文链接：授权使用：上海海事大学(wflshyxy)，授权号：a02dde93-f3d3-4b51-b899-9e08014fac95下载时间：2010年10月7日