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

摘要

随着无线传感网领域和工业控制领域的不断发展，网络空间中的新兴领域不断产生，网络通信机制也日益复杂。安全协议作为保障各类新兴领域数据与服务资源的关键技术之一，近年来得到普遍关注。安全协议数量的激增，协议运行环境的差异，协议复杂度的提高，与设计分析人员主观联系密切等特点，导致安全协议的设计与分析成为极具挑战性的课题。 安全协议的形式化分析方法近年来取得了巨大进步，在模态逻辑、定理证明以及模型检测等几大分支都具有颇具影响力的代表方法。与之相对应，基于计算模型的计算复杂性方法也在同步发展。该方法具有严谨的数学理论作为支撑，使用结构复杂，对研究人员要求极高；此外，由于研究人员对协议的不同理解，在分析同种协议时，可能得到不同结果。与计算复杂性方法相比，基于符号模型的形式化分析方法由于自身的符号性和离散性，具有更简单清晰的结构，在与分布式计算机工程领域相结合方面，具备天生优势。并且，随着业界安全协议数量的规模化，协议的自动化分析势必成为协议安全性分析领域的重要趋势。 着色Petri网作为分布式异步并发系统分析中的最重要工具之一，具有二元性、图形化以及代数表示性的特点，既有清晰的结构又有严谨的数学基础；着色Petri网的辅助建模工具同时集成了自动化状态空间分析的功能，通过补充修改，即可用于分析安全协议。本文正是利用其在分布式系统建模领域的优势，结合时态逻辑语句的状态空间判决以及Dolev-Yao模型下的协议运行环境，提出一种基于着色Petri网的安全协议分析方法。该方法从攻击者模型构造出发，引入消息推理规则，形成了Dolev-Yao模型下使用着色Petri网建模分析协议安全性的理论。最后，本文以CPN Tools形式化建模工具为基础，结合上述理论方法，实现了一套基于着色Petri网的安全协议分析原型系统。通过与业界主流安全协议自动化分析工具AVISPA的对比，结果表明，本文所提方法具有较强的可行性；并且攻击者能力模型扩展后，能够用于分析多数安全协议。

目录

第一个书签之前