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

发布时间：2021-06-26 14:45

　　随着无线传感网领域和工业控制领域的不断发展,网络空间中的新兴领域不断产生,网络通信机制也日益复杂。安全协议作为保障各类新兴领域数据与服务资源的关键技术之一,近年来得到普遍关注。安全协议数量的激增,协议运行环境的差异,协议复杂度的提高,与设计分析人员主观联系密切等特点,导致安全协议的设计与分析成为极具挑战性的课题。安全协议的形式化分析方法近年来取得了巨大进步,在模态逻辑、定理证明以及模型检测等几大分支都具有颇具影响力的代表方法。与之相对应,基于计算模型的计算复杂性方法也在同步发展。该方法具有严谨的数学理论作为支撑,使用结构复杂,对研究人员要求极高;此外,由于研究人员对协议的不同理解,在分析同种协议时,可能得到不同结果。与计算复杂性方法相比,基于符号模型的形式化分析方法由于自身的符号性和离散性,具有更简单清晰的结构,在与分布式计算机工程领域相结合方面,具备天生优势。并且,随着业界安全协议数量的规模化,协议的自动化分析势必成为协议安全性分析领域的重要趋势。着色Petri网作为分布式异步并发系统分析中的最重要工具之一,具有二元性、图形化以及代数表示性的特点,既有清晰的结构又有严谨的数学基础;着... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：89 页

【学位级别】：硕士

【部分图文】：

HelloWorld1模型图，初始标记0M

图3.2 变迁激发示例图，标记1M 有向弧，用于连接库所和变迁，并指示出变迁激发的条件，条件使用有向弧注入式（arc inscription）来表示，如示例图中箭头上的变量“s”即为一个有向弧表达式。因为有向弧不需要名字，只用来表示变迁需要和输出的数据类型或嵌入其他 CPN ML语句，所以有向弧注入式又被称为有向弧表达式（arc expression）。CPN 网络中的有向弧可以是单向也可以是双向，但是每个有向弧上表达式的类型必须是单一的。 由于 CPN 使用 ML 语言作为其内部机制，故而，值和表达式以及递归构成了语言的关键机制。在标准元语言 SML 中

图3.3 结束状态2 deadM（ M ） 在 CPN Tools 中，库所内令牌由系统初始标记0M 到系统结束标记2M 的流动过程，以及过程中变量绑定的变化，即为 CPN 模型 HelloWorld 的仿真。系统的仿真只能对模型进行有限步的执行，使用仿真可排除一些模型的与预设需求不相符的设计错误。总体来看，CPN 模型的运行遵循以下两条规律： 1）当库所中的多重集能为弧表达式中的变量提供合适的绑定时，变迁被激发，相应的多重集流入下一库所，为下一变迁提供绑定。 2）在网络模型中，变量的名字虽然不变，但随着多重集在库所中的流动，变量在不停地被重新绑定新的值。 在 CPN 的形式化定义中

【参考文献】：
期刊论文
[1]EGAKA:一种面向LTE-A机器类型通信的高效组认证与密钥协商协议[J]. 宋亚鹏,陈昕.  计算机科学. 2016(S1)
[2]一种基于CPN的协议测试序列生成方法[J]. 孙涛,叶新铭,刘靖,杨蒙.  解放军理工大学学报(自然科学版). 2012(02)



本文编号：3251537