基于着色Petri网的安全协议漏洞挖掘方法

摘要

本发明公开了一种基于着色Petri网的安全协议漏洞挖掘方法，其实现步骤为：基于着色Petri网CPN建模安全协议，设计安全协议模型解析工具，基于安全协议模型解析工具生成安全协议CPN模型，生成安全协议CPN模型的状态空间，获取安全协议漏洞挖掘结果。本发明通过着色Petri网CPN建模安全协议，使得在构建复杂安全协议模型的情况下，模型结构清晰且易于理解，并在安全协议CPN建模阶段引入了安全协议模型解析工具，实现了安全协议CPN模型的自动化生成，相比于现有手动CPN建模的方案，精简了安全协议CPN模型建模的步骤，极大地降低了安全协议漏洞挖掘的门槛，并且能够正确实现安全协议漏洞的挖掘。

说明书

技术领域

本发明属于网络空间安全技术领域，更进一步涉及一种基于着色Petri网的安全协议漏洞挖掘方法，可用于金融系统等领域。

背景技术

安全协议也被称之为密码学协议，它的目标是通过应用密码学基件在不安全的网络环境中提供安全的通信服务。安全协议被设计用于保障开放网络和分布系统中秘密信息的安全处理和传输，在金融系统、军事系统等诸多领域提供安全服务，不同的安全协议在设计之初都有其对应的安全目标，也被称之为安全协议的安全属性。

安全协议的漏洞指的是可能允许攻击者以他人的身份进行身份验证，或者获得不应该被披露的信息，从而破坏安全协议设计之初的安全属性的不安全因素。安全协议的海量、复杂、易错等特点，导致安全协议自动化漏洞挖掘的需求与日俱增。

模型检测技术是一类主流的安全协议漏洞挖掘方法，该类方法的优点是自动化能力强，可计算出安全协议的不安全反例。其实现过程为：首先提取安全协议模型M

(1)采集和存储通过公共通道交换的所有信息。

(2)转发、重路由和阻塞消息。

(3)使用存储、随机生成和过时的数据和加密技术进行伪造消息的生成。

(4)如果入侵者有匹配的密钥，则解密加密。

(5)入侵者具有正常主体的能力，可以像正常主体一样发送接收消息。

着色Petri网即Color Petri Net，简称CPN，作为一种通用的基于模型检测原理实现的建模工具，适合于描述异步的、并发的计算机系统模型，同时，因其状态空间分析能力强大且通俗易懂，使其在安全协议的自动化漏洞挖掘领域具备很好的应用前景。一个着色Petri网模型是一个九元组{P,T,A,∑,V,C,G,E,I}，其中，P是一个库所集合，T是一个变迁集合，A是一个有向弧集合，∑是一个非空颜色集集合，V是一个变量集合，C是一个颜色集设置函数，为每个库所P分配一个颜色集，G是一个守卫函数集合，为每个变迁T赋一个守卫函数，E是一个弧表达式函数集合，为每个有向弧A赋一个弧表达式，I是一个初始化函数，为每个库所P赋值一个初始化表达式。CPN模型本质上是一个XML文件，CPN模型中的任意基本对象在XML文件中都有相应的标签与之对应。

CPN Tools是一种可用于CPN模型搭建和分析的工具，该工具不仅实现了计算机上的CPN模型可视化建模，还提供了CPN模型全部状态空间的自动计算以及生成状态空间报告的功能，同时，集成的SML(standard meta language)语言可以辅助完成安全协议漏洞挖掘所需要的不安全状态检索和攻击路径搜索功能。

电子科技大学在其申请的专利文献“基于多反例的安全协议漏洞挖掘方法”(公开日：20190903，申请公布号：CN110198319A)中公开了基于多反例的安全协议漏洞挖掘方法，包括以下步骤：S1、使用promela语言对需要验证的安全协议进行建模，并保存为.pml文件格式；S2、规约协议的安全性质，并以LTL形式表达；S3、通过查找反例的方式对安全协议进行验证；S4、消除相似反例：使用编辑距离法度量反例的权重序列，消除相似反例；随后使用对比攻击路径图的方法进一步消除相似反例；S5、使用统计方法对步骤S4剩余的反例集合进行处理。

该方法存在的不足之处是，由于该方法使用promela语言对需要验证的安全协议进行建模，在安全协议较为复杂的场景下，安全协议建模过程复杂，构建的安全协议模型不够直观，解释说明性不够，不便于与非专业的跨域人士进行合作交流，从而降低了安全协议漏洞挖掘的效率。

发明内容

本发明的目的是针对上述现有技术存在的不足，提出了一种基于着色Petri网的安全协议漏洞挖掘方法，用于解决安全协议漏洞挖掘过程中由于安全协议建模过程复杂、模型描述不够直观、解释说明性不够等造成的安全协议漏洞挖掘效率低的问题。

为实现上述目的，本发明采取的技术方案为：基于着色Petri网CPN建模安全协议；设计安全协议模型解析工具；基于安全协议模型解析工具生成安全协议CPN模型；生成安全协议CPN模型的状态空间；获取安全协议漏洞挖掘结果。

本发明实现的具体步骤包括如下：

(1)基于着色Petri网CPN建模安全协议：

将CPN划分为简单颜色集、复合颜色集、变量、常量、函数、库所、弧和变迁8种类型的基本对象，将安全协议划分为基本元素E＝{E

(1a)建模基本元素E：

按照简单颜色集、复合颜色集、常量、函数分别建模原子消息、复合消息、固定值、密码学操作的方式，将E中的每个元素E

(1b)建模事件A：

按照格式：[库所名:库所类型:初始值:弧的方向:弧铭文]-->变迁名:变迁执行条件-->[库所名:库所类型:初始值:弧的方向:变量名]建模每个事件A

(2)设计安全协议模型解析工具：

(2a)设计安全协议模型解析工具的UI：

利用python编程语言的pyside2库新建一个UI，向UI中添加两个文本框Text

(2b)定义API生成CPN基本对象对应的XML标签：

新建一个空白CPN模型Model1，模型Model1中存在的XML标签集合X

(2c)定义按钮Button

新建一个空白CPN模型Model2，加载模型Model2为Document对象，解析Text

(3)基于安全协议模型解析工具生成安全协议CPN模型：

将步骤1建模的安全协议基本元素模型E

(4)生成安全协议CPN模型的状态空间：

依据安全协议需要满足的安全要求定制安全协议安全性评估规则R＝{R

(5)获取安全协议漏洞挖掘结果：

利用SearchNodes函数检索状态空间S中是否存在不符合步骤(4)所描述的评估规则R

本发明与现有技术相比具有以下优点：

本发明基于CPN建模安全协议，构建的安全协议CPN模型具备通俗易懂的图形形式，易于理解，便于与非专业的跨域人士进行合作交流，并在安全协议CPN建模阶段引入安全协议模型解析工具，实现了安全协议CPN的自动化生成。与现有技术相比，本发明精简了安全协议CPN模型建模的步骤，减少人工参与的工作量，提升了安全协议漏洞挖掘的效率。

附图说明

图1是本发明的流程图；

图2是本发明实施例中Andrew Secure RPC协议会话示意图；

图3是本发明实施例中Andrew Secure RPC协议基本元素建模示意图；

图4是本发明实施例中Andrew Secure RPC协议事件建模示意图；

图5是本发明实施例中设计的安全协议解析工具UI示意图；

图6是本发明实施例中分析的CPN模型XML标签结构示意图；

图7是本发明实施例中构建安全协议解析工具的流程图；

图8是本发明实施例中生成的Andrew Secure RPC协议顶层CPN模型示意图；

图9是本发明实施例中生成的C_Send1子页面CPN模型示意图；

图10是本发明实施例中构建的Intruder1子页面CPN模型示意图；

图11是本发明实施例中获取的Andrew Secure RPC协议漏洞示意图。

具体实施方式

下面结合附图和实施例对本发明的技术方案和效果做进一步的详细描述，实施例仅用于说明本发明，并不构成对本发明的任何限制。

本实施例分析的对象是经典的Andrew Secure RPC协议，该协议基于对称加密机制实现通信双方的身份认证并建立新的共享对称密钥SK。

参照附图1，对本发明的具体实现步骤做进一步的详细描述。

(1)基于着色Petri网CPN建模安全协议：

将CPN划分为简单颜色集、复合颜色集、变量、常量、函数、库所、弧和变迁8种类型的基本对象，将安全协议划分为基本元素E＝{E

参照附图2，本实施例中N＝17，M＝12，E＝{E

(1a)建模基本元素E：

按照简单颜色集、复合颜色集、常量、函数分别建模原子消息、复合消息、固定值、密码学操作的方式，将E中的每个元素E

参照附图3，本实施例中N＝17，

(1b)建模事件A：

按照格式：[库所名:库所类型:初始值:弧的方向:弧铭文]-->变迁名:变迁执行条件-->[库所名:库所类型:初始值:弧的方向:变量名]建模每个事件A

参照附图4，本实施例中M＝12，

(2)设计安全协议模型解析工具：

(2a)设计安全协议模型解析工具的UI：

利用python编程语言的pyside2库新建一个UI，向UI中添加两个文本框Text

参照附图5，本实施例中文本框Text

(2b)定义API生成CPN基本对象对应的XML标签：

新建一个空白CPN模型Model1，模型Model1中存在的XML标签集合X

参照附图6，本实施例中P＝16，X

a

colset a＝int；

其中，id＝"ID3"表示＜color＞＜/color＞标签的编号，a表示该颜色集的名称为a，表示该颜色集为int类型，colset a＝int；表示该颜色集的申明语法为colset a＝int；；

利用python编程语言的xml.dom.minidom库定义API生成int类型颜色集对应的，API的具体内容如下：

def create_int_colset(id,declaration):

color＝create_color(id)

id＝id+1

chars＝declaration.split("")

color_id＝create_id(chars[1])

color_int＝DOMTree.createElement("int")

layout＝create_layout(declaration)

color.appendChild(color_id)

color.appendChild(color_int)

color.appendChild(layout)

return id,color

其中，id参数为int类型颜色集的编号，declaration参数为int类型颜色集标签的文本内容，API的返回结果为id和color，其中color为int类型颜色集对应的＜color＞＜/color＞标签。

(2c)定义按钮Button

新建一个空白CPN模型Model2，加载模型Model2为Document对象，解析Text

参照附图7，本实施例中，具体步骤如下：

第一步，通过python编程语言的xml.dom.minidom库将模型Model2加载为Document对象；

第二步，解析Text

本实施例中，

其中，和分别为

第三步，统计Text

本实施例中，count＝5，创建的Ctrl_I颜色集包含count-1个元素，为colsetCtrl_I＝with I1|I2|I3|I4；，对应的XML标签具体内容如下：

第四步，解析Text

参照附图8，本实施例中，针对第一个空行之前的事件模型

参照附图9，本实施例中，模型Model2中添加的变迁C_Send1关联的子页面Page

第五步，在模型Model2中添加一个攻击者变迁T

参照附图8，本实施例中，模型Model2中添加的攻击者变迁T

参照附图10，本实施例中，Intruder1的具体内容包括7个库所、5个变迁和18条弧，其中库所包括一个库所In、一个库所Out、一个库所Data、一个库所I和拆分第一条协议消息得到的三个库所Clientid、Xr和Hkc，变迁包括Intercept、Eavesdrop、SendData、Decomposite和Composite分别表示拦截、窃听、重放、分解、重构这五种敌手能力，变迁和库所之间的弧表示的库所中数据流动关系。

第六步，将Document对象保存为XML文件，该XML文件即安全协议CPN模型。

(3)基于安全协议模型解析工具生成安全协议CPN模型：

将步骤1建模的安全协议基本元素模型E

(4)生成安全协议CPN模型的状态空间：

依据安全协议需要满足的安全要求定制安全协议安全性评估规则R＝{R

本实施例中K＝3，R＝{R

fn n＝>

let

val sk＝Mark.C_Receive2'p19 1n

val sk1＝remdupl sk

in

if(length sk)＝(length sk1)

then false

else true

end

将状态空间计算工具的predicatestop参数设置为该SML表达式描述的评估规则，生成安全协议CPN模型的状态空间S＝{S

(5)获取安全协议漏洞挖掘结果：

利用SearchNodes函数检索状态空间S中是否存在不符合步骤(4)所描述的评估规则R

本实施例中SearchNodes函数的具体描述如下：

SearchNodes(EntireGraph,

fn n＝>

let

val sk＝Mark.C_Receive2'p19 1n

val sk1＝remdupl sk

in

if(length sk)＝(length sk1)

then false

else true

end,

1,

fn n＝>n,

[],

op::)

参照附图11，本实施例中SearchNodes函数的返回值为1379，说明状态空间S中存在不符合评估规则R

fun Arc(item)＝

print(ArcDescriptor(item)^"\n")；

val node＝1379

val arcs＝ArcsInPath(1,node)

val it＝map Arc arcs

其中，Arc函数实现对攻击路径中每条边的描述。val arcs＝ArcsInPath(1,node)表示获取从初始状态S

以上描述仅是本发明的一个具体实例，显然对于本领域的专业人员来说，在了解了本发明内容和原理后，都可能在不背离本发明原理、结构的情况下，进行形式和细节上的各种修正和改变，但是这些基于本发明思想的修正和改变仍在本发明的权利要求保护范围之内。