一种基于有色一种基于有色Petri网的安全协议分析方法研究网的安全协议分析方法研究
利用有色Petri网建模工具CPN tools中的查询函数对安全属性进行描述，搭建一个能够覆盖大部分安全性质的
CPN查询函数库，提出一种基于CPN的通用和规范的安全协议形式化分析语言，该语言可以像用面向对象编程
语言编程一样对安全协议进行建模。
摘摘 要：要： 利用
关键词：关键词： 有色Petri网；安全协议；形式化分析；面向对象编程语言
如何在一个无法确定的操作环境下，保证计算机间传送信息的安全性，从而确保通信双方主体之间的“信任”以及通信数据的
秘密和完整，其中安全协议对保障网络安全起到至关重要的作用。但一些著名的协议在使用了相当长的时间后，相继被发现存
在有若干安全漏洞。由于安全协议的运行是处于某种不安全的环境中，很难用人工识别的方法来分析其安全性，必须借助形式
化的分析方法或工具来完成。
关于安全协议的形式化分析，国内外学者基于不同的模型进行了不少有益的研究。如Yasinsac提出的通用安全协议分析语
言CPAL[1]、Millen开发的通用认证协议说明语言CAPSL[2]、李梦君等人用扩展Horn逻辑模型对安全协议进行分析和验证方法
[3]、怀进鹏等人用代数模型来研究协议的安全性[4]、WE等人基于有色Petri网CPN(Coloured Petri Net)提出一种集成的安全协
议分析模型[5]。
现有的方法大多针对个别协议进行分析，很少能够通用于大部分的安全协议，并且大部分的方法还停留在理论上，缺少自动
分析的工具[6]。
本文利用CPN tools建模语言(CPN ML)中的查询函数对安全属性进行描述，然后对CPN tools工具在规范协议描述、简化协
议建模、自动检测进行扩展三方面，搭建一个能够覆盖大部分安全性质的CPN查询函数库，提出一种基于CPN的通用和规范
的安全协议形式化分析语言，该语言可以像用面向对象编程语言编程一样对安全协议进行建模。
1 基于基于CPN的安全协议的安全协议
1.1 有色有色Petri网网(CPN)理论研究理论研究
Petri网是一种可用于多种系统的图形化、数学化建模工具，为描述和研究具有并行、异步、分布式和随机性等特征的复杂
系统提供了强有力的手段。
作为一种图形化工具，可以把Petri网看作与数据流图和网络相似的方法来描述系统模型；作为一种数学化工具，它可以用
来建立状态方程、代数方程和其他描述系统行为的数学模型。
在CPN模型中，有色标志表示系统中不同的资源，同时每个位置都与特定的颜色集绑定，表示该位置中只能存放相应颜色的
标志。在弧上和变迁上标注的条件表达式和运算函数是用于解释弧的权值、运算所用的颜色以及变迁触发的条件。
CPN tools是一个专用于有色Petri网编辑、模拟和分析的工具，除了有强大的CPN分析工具外，它还有简洁紧凑的CPN图形
编辑工具，几乎所有的CPN元素(除数据类型、变量申明外)都能在模型图中表示。
CPN是将Petri网具有相似性质的元素分类，用不同颜色区分不同类别，每一种颜色用一种标识符号来表示，将某种属性赋
予标记。
1.2 基于基于CPN的安全协议的安全协议
安全协议的形式化分析与验证是一个复杂的过程，首先都要用形式化方法的语义对安全协议进行描述与建模。然而，从协议
的非形式化描述，尤其是自然语言描述转变成形式化说明的过程可能会有错误发生，将直接导致后续分析的不确定性。同时一
些形式化方法的提出都是从个别安全协议出发来设计规范的术语，遇见了新的协议形式，再对原有规范加以扩展，这样的形式
化术语存在通用性差的问题。所以在进行安全协议的形式化描述与建模之前，需要采用通用的安全协议形式化说明加以规范。
为了使得通用安全协议说明更加适合于Petri网方法，本文在CAPSL的基础上抽象出通用安全协议的基本要素，在此基础上
建立与Petri网要素的一一对应，如表1所示。
资源评论
