基于着色Petri网的安全协议形式化分析理论与技术研究

《基于着色Petri网的安全协议形式化分析理论与技术研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、硕士学位论文Ｉ基于着色Ｐｅｔｒｉ网的安全协议形式化分析理论与技术研究作者姓名马瑞洁指导教师姓名、职称马卓副教授？申请学位类别工学硕士基于着色Petri网的安全协议形式化分析理论与技术研究作者姓名马瑞洁指导教师姓名、职称马卓副教授申请学位类别工学硕士学校代码10701学号1503121520分类号TP39密级公开西安电子科技大学硕士学位论文基于着色Petri网的安全协议形式化分析理论与技术研究作者姓名：马瑞洁一级学科：计算机科学与技术二级学科：计算机系统结构学位类别：工学硕士指导教师

2、姓名、职称：马卓副教授学院：计算机学院提交日期：2018年4月OntheFormalDescriptionandAnalysisofSecurityProtocolsUsingColoredPetriNetsA thesissubmitted toXIDIAN UNIVERSITYin partial fulfillment of the requirementsfor the degreeof Masterin Computer System ArchitectureByMa RuijieSupervi

3、sor: Ma ZhuoTitle:Associate ProfessorApril 2018西安电子科技大学学位论文独创性（或创新性）声明秉承学校严谨的学风和优良的科学道德，本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成果也不包含；为获得西安电子科技大学或其它教育机构的学位或证书而使用过的材料一。与我同工作的同事对本研宄所做的任何贡献均已在论文中作了明确的说

4、明并表示了谢意。一学位论文若有不实之处，本人承担切法律责任。本人签名？＾秦主：日期：西安电子科技大学关于论文使用授权的说明？本人完全了解西安电子科技大学＾：关保留和使用学位论文的规定，即研宄生在一校攻读学位期间论文工作的知识产权属于西安电子科技大学。学校有权保留送交论文的复印件，允许查阅、借阅论文；学校可以公布论文的全部或部分内容，允许采用影印、缩印或其它复制手段保存论文。同时本人保证，结合学位论文研宄成果完成的论文、发明专利等成果，署名单位为西安电子科技大学。

5、■＾傘客导师签名本人签名：：日期：ｇ日期：專ｑ认曰摘要摘要随着无线传感网领域和工业控制领域的不断发展，网络空间中的新兴领域不断产生，网络通信机制也日益复杂。安全协议作为保障各类新兴领域数据与服务资源的关键技术之一，近年来得到普遍关注。安全协议数量的激增，协议运行环境的差异，协议复杂度的提高，与设计分析人员主观联系密切等特点，导致安全协议的设计与分析成为极具挑战性的课题。安全协议的形式化分析方法近年来取得了巨大进步，在模态逻辑、定理证明以及模型检测等几大分支都具有颇具影响力的代表方法。与

6、之相对应，基于计算模型的计算复杂性方法也在同步发展。该方法具有严谨的数学理论作为支撑，使用结构复杂，对研究人员要求极高；此外，由于研究人员对协议的不同理解，在分析同种协议时，可能得到不同结果。与计算复杂性方法相比，基于符号模型的形式化分析方法由于自身的符号性和离散性，具有更简单清晰的结构，在与分布式计算机工程领域相结合方面，具备天生优势。并且，随着业界安全协议数量的规模化，协议的自动化分析势必成为协议安全性分析领域的重要趋势。着色Petri网作为分布式异步并发系统分析中的最重要工具之一，具有二元性、图形化

7、以及代数表示性的特点，既有清晰的结构又有严谨的数学基础；着色Petri网的辅助建模工具同时集成了自动化状态空间分析的功能，通过补充修改，即可用于分析安全协议。本文正是利用其在分布式系统建模领域的优势，结合时态逻辑语句的状态空间判决以及Dolev-Yao模型下的协议运行环境，提出一种基于着色Petri网的安全协议分析方法。该方法从攻击者模型构造出发，引入消息推理规则，形成了Dolev-Yao模型下使用着色Petri网建模分析协议安全性的理论。最后，本文以CPN Tools形式化建模工具为基础，结合上述理论方

8、法，实现了一套基于着色Petri网的安全协议分析原型系统。通过与业界主流安全协议自动化分析工具AVISPA的对比，结果表明，本文所提方法具有较强的可行性；并且攻击者能力模型扩展后，能够用于分析多数安全协议。关键词：安全协议，着色Petri网，CPN Tools，模型检测，自动化IABSTRACTABSTRACTWith the continuous development of wireless sensor network