本发明公开了一种基于着色Petri网的安全协议漏洞挖掘方法，其实现步骤为：基于着色Petri网CPN建模安全协议，设计安全协议模型解析工具，基于安全协议模型解析工具生成安全协议CPN模型，生成安全协议CPN模型的状态空间，获取安全协议漏洞挖掘结果。本发明通过着色Petri网CPN建模安全协议，使得在构建复杂安全协议模型的情况下，模型结构清晰且易于理解，并在安全协议CPN建模阶段引入了安全协议模型解析工具，实现了安全协议CPN模型的自动化生成，相比于现有手动CPN建模的方案，精简了安全协议CPN模型建模的步骤，极大地降低了安全协议漏洞挖掘的门槛，并且能够正确实现安全协议漏洞的挖掘。
基于着色Petri网的安全协议漏洞挖掘方法
技术领域
[0001] 本发明属于网络空间安全技术领域，更进一步涉及一种基于着色Petri网的安全协议漏洞挖掘方法，可用于金融系统等领域。
背景技术
[0002] 安全协议也被称之为密码学协议，它的目标是通过应用密码学基件在不安全的网络环境中提供安全的通信服务。安全协议被设计用于保障开放网络和分布系统中秘密信息的安全处理和传输，在金融系统、军事系统等诸多领域提供安全服务，不同的安全协议在设计之初都有其对应的安全目标，也被称之为安全协议的安全属性。
[0003] 安全协议的漏洞指的是可能允许攻击者以他人的身份进行身份验证，或者获得不应该被披露的信息，从而破坏安全协议设计之初的安全属性的不安全因素。安全协议的海量、复杂、易错等特点，导致安全协议自动化漏洞挖掘的需求与日俱增。
[0004] 模型检测技术是一类主流的安全协议漏洞挖掘方法，该类方法的优点是自动化能力强，可计算出安全协议的不安全反例。其实现过程为：首先提取安全协议模型Mt，定制安全协议的安全性质Pt，检查Pt是否能在Mt的任何状态下都成立。当安全协议模型Mt的某个状态不满足性质P时，即在模型Mt的状态空间中存在不安全状态时，模型检测器就会把这条通往不安全状态的路径返回，从而实现安全协议漏洞的挖掘。通过模型检测技术在对安全协议漏洞进行挖掘时，必须尽可能考虑想破坏安全协议安全属性的攻击者可能采取的所有行动。Dolev‑Yao模型是所有对安全协议进行漏洞挖掘的基础攻击者模型，作为传统的攻击者模型极其具有代表性。Dolev‑Yao攻击者的能力描述如下：
[0005] (1)采集和存储通过公共通道交换的所有信息。
[0006] (2)转发、重路由和阻塞消息。
[0007] (3)使用存储、随机生成和过时的数据和加密技术进行伪造消息的生成。
[0008] (4)如果入侵者有匹配的密钥，则解密加密。
[0009] (5)入侵者具有正常主体的能力，可以像正常主体一样发送接收消息。
[0010] 着色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文件中都有相应的标签与之对应。
[0011] CPN Tools是一种可用于CPN模型搭建和分析的工具，该工具不仅实现了计算机上的CPN模型可视化建模，还提供了CPN模型全部状态空间的自动计算以及生成状态空间报告的功能，同时，集成的SML(standard meta language)语言可以辅助完成安全协议漏洞挖掘所需要的不安全状态检索和攻击路径搜索功能。
[0012] 电子科技大学在其申请的专利文献“基于多反例的安全协议漏洞挖掘方法”(公开日：20190903，申请公布号：CN110198319A)中公开了基于多反例的安全协议漏洞挖掘方法，包括以下步骤：S1、使用promela语言对需要验证的安全协议进行建模，并保存为.pml文件格式；S2、规约协议的安全性质，并以LTL形式表达；S3、通过查找反例的方式对安全协议进行验证；S4、消除相似反例：使用编辑距离法度量反例的权重序列，消除相似反例；随后使用对比攻击路径图的方法进一步消除相似反例；S5、使用统计方法对步骤S4剩余的反例集合进行处理。
[0013] 该方法存在的不足之处是，由于该方法使用promela语言对需要验证的安全协议进行建模，在安全协议较为复杂的场景下，安全协议建模过程复杂，构建的安全协议模型不够直观，解释说明性不够，不便于与非专业的跨域人士进行合作交流，从而降低了安全协议漏洞挖掘的效率。
发明内容
[0014] 本发明的目的是针对上述现有技术存在的不足，提出了一种基于着色Petri网的安全协议漏洞挖掘方法，用于解决安全协议漏洞挖掘过程中由于安全协议建模过程复杂、模型描述不够直观、解释说明性不够等造成的安全协议漏洞挖掘效率低的问题。
[0015] 为实现上述目的，本发明采取的技术方案为：基于着色Petri网CPN建模安全协议；设计安全协议模型解析工具；基于安全协议模型解析工具生成安全协议CPN模型；生成安全协议CPN模型的状态空间；获取安全协议漏洞挖掘结果。
[0016] 本发明实现的具体步骤包括如下：
[0017] (1)基于着色Petri网CPN建模安全协议：
[0018] 将CPN划分为简单颜色集、复合颜色集、变量、常量、函数、库所、弧和变迁8种类型的基本对象，将安全协议划分为基本元素E＝{E1,E2,...,En,...,EN}和事件A＝{A1,A2,...,Am,...,AM}，其中，N≥1，M≥1，En表示第n个基本元素，可以是原子消息、复合消息、固定值或密码学操作，Am表示第m个事件，建模基本元素E和A；
[0019] (1a)建模基本元素E：
[0020] 按照简单颜色集、复合颜色集、常量、函数分别建模原子消息、复合消息、固定值、密码学操作的方式，将E中的每个元素En建模为 得到基本元素模型其中，两个相邻的基本元素模型 和 通过回车符分隔；
[0021] (1b)建模事件A：
[0022] 按照格式：[库所名:库所类型:初始值:弧的方向:弧铭文]‑‑>变迁名:变迁执行条件‑‑>[库所名:库所类型:初始值:弧的方向:变量名]建模每个事件Am，得到事件模型其中，库所名为自定义的任意字符串，库所类型为步骤(1a)定义的简单颜色集或复合颜色集，初始值为步骤(1a)定义的常量，弧的方向取值可为PtoT、BOTHDIR、TtoP分别表示库所指向变迁、双向、变迁指向库所，弧铭文用于标识库所与变迁之间传递的数据，变迁名是自定义的任意字符串，执行条件为变迁的守卫函数，事件Am不需执行条件时，变迁执行条件省略不写，在两个相邻的事件模型 和 之间添加一个空行，其中， 之前和 之后的事件模型分别建模一条协议会话消息，设”end”字符串为事件建模结束的标志；
[0023] (2)设计安全协议模型解析工具：
[0024] (2a)设计安全协议模型解析工具的UI：
[0025] 利用python编程语言的pyside2库新建一个UI，向UI中添加两个文本框Text1、\ \Text2和一个按钮Button1，其中，Text1和Text2分别用于输入基本元素模型E和事件模型A，Button1执行安全协议模型解析并生成安全协议CPN模型的功能；
[0026] (2b)定义API生成CPN基本对象对应的XML标签：
[0027] 新建一个空白CPN模型Model1，模型Model1中存在的XML标签集合XModel1＝{X1,X2,...,Xp,...,XP}，向模型Model1中逐个添加单种CPN基本对象Oi(i＝1,...,8)后得到CPN模型设为Model1_1，模型Model1_1中存在的XML标签集合XModel1_1＝{X1,X2,...,Xp,...,XP,Xq}，得到Xq为CPN基本对象Oi对应的XML标签，并基于此，利用python编程语言的xml.dom.minidom库定义API生成CPN基本对象Oi对应的XML标签；
[0028] (2c)定义按钮Button1的功能：
[0029] 新建一个空白CPN模型Model2，加载模型Model2为Document对象，解析Text1和\ \Text2文本框中的基本元素模型E 和事件模型A ，基于步骤(2b)定义的API生成 和 对应的XML标签并将XML标签添加至Document对象，构建Dolev‑Yao攻击者CPN模型ModelI并将模型ModelI添加至Document对象，保存Document对象为XML文件；
[0030] (3)基于安全协议模型解析工具生成安全协议CPN模型：
[0031] 将步骤1建模的安全协议基本元素模型E\和事件模型A\分别输入至Text1和Text2文本框中，点击Button1按钮执行安全协议模型解析并生成安全协议CPN模型；
[0032] (4)生成安全协议CPN模型的状态空间：
[0033] 依据安全协议需要满足的安全要求定制安全协议安全性评估规则R＝{R1,R2,...,Rk,...,RK}，其中，K≥1，并以SML语言描述每条评估规则Rk，设置CPN Tools状态空间计算工具的predicatestop参数为评估规则Rk，在此基础上，利用状态空间计算工具生成安全协议CPN模型的状态空间S＝{S1,S2,...,Sl,...,SL}，其中，L≥1；
[0034] (5)获取安全协议漏洞挖掘结果：
[0035] 利用SearchNodes函数检索状态空间S中是否存在不符合步骤(4)所描述的评估规则Rk的不安全状态St，若是，说明安全协议在当前构建的Dolev‑Yao攻击者模型下安全协议是不安全的，进一步通过ArcsInPath函数获取从初始状态S1至不安全状态St的攻击路径，挖掘安全协议漏洞，否则，说明在当前构建的Dolev‑Yao攻击者模型下安全协议是安全的。
[0036] 本发明与现有技术相比具有以下优点：
[0037] 本发明基于CPN建模安全协议，构建的安全协议CPN模型具备通俗易懂的图形形式，易于理解，便于与非专业的跨域人士进行合作交流，并在安全协议CPN建模阶段引入安全协议模型解析工具，实现了安全协议CPN的自动化生成。与现有技术相比，本发明精简了安全协议CPN模型建模的步骤，减少人工参与的工作量，提升了安全协议漏洞挖掘的效率。
附图说明
[0038] 图1是本发明的流程图；
[0039] 图2是本发明实施例中Andrew Secure RPC协议会话示意图；
[0040] 图3是本发明实施例中Andrew Secure RPC协议基本元素建模示意图；
[0041] 图4是本发明实施例中Andrew Secure RPC协议事件建模示意图；
[0042] 图5是本发明实施例中设计的安全协议解析工具UI示意图；
[0043] 图6是本发明实施例中分析的CPN模型XML标签结构示意图；
[0044] 图7是本发明实施例中构建安全协议解析工具的流程图；
[0045] 图8是本发明实施例中生成的Andrew Secure RPC协议顶层CPN模型示意图；
[0046] 图9是本发明实施例中生成的C_Send1子页面CPN模型示意图；
[0047] 图10是本发明实施例中构建的Intruder1子页面CPN模型示意图；
[0048] 图11是本发明实施例中获取的Andrew Secure RPC协议漏洞示意图。
具体实施方式
[0049] 下面结合附图和实施例对本发明的技术方案和效果做进一步的详细描述，实施例仅用于说明本发明，并不构成对本发明的任何限制。
[0050] 本实施例分析的对象是经典的Andrew Secure RPC协议，该协议基于对称加密机制实现通信双方的身份认证并建立新的共享对称密钥SK。
[0051] 参照附图1，对本发明的具体实现步骤做进一步的详细描述。
[0052] (1)基于着色Petri网CPN建模安全协议：
[0053] 将CPN划分为简单颜色集、复合颜色集、变量、常量、函数、库所、弧和变迁8种类型的基本对象，将安全协议划分为基本元素E＝{E1,E2,...,En,...,EN}和事件A＝{A1,A2,...,Am,...,AM}，其中，N≥1，M≥1，En表示第n个基本元素，可以是原子消息、复合消息、固定值或密码学操作，Am表示第m个事件，建模基本元素E和A；
[0054] 参照附图2，本实施例中N＝17，M＝12，E＝{E1,E2,...,E17}，A＝{A1,A2,...,A12}。其中，E1,E2,E3、E4,E5和E6,E7分别表示构建Andrew Secure RPC协议第一条会话消息所需要的原子消息、复合消息和固定值，E8、E9和E10分别表示构建该协议第二条会话消息所需要的原子消息、密码学操作和复合消息，E11表示构建该协议第三条会话消息所需要的复合消息，E12,E13和E14分别表示构建该协议第四条会话消息所需要的原子消息和复合消息，E15、E16和E17分别表示建模验证HKC、验证Xr和验证Yr事件时所需要的变量。A1,A2,A3、A4,A5,A6、A7,A8、A9,A10,A11和A12表示客户端或服务器发送或接收第一、二、三、四条消息时需要执行的事件。
[0055] (1a)建模基本元素E：
[0056] 按照简单颜色集、复合颜色集、常量、函数分别建模原子消息、复合消息、固定值、密码学操作的方式，将E中的每个元素En建模为 得到基本元素模型其中，相邻的两个基本元素模型 和 通过回车符分隔；
[0057] 参照附图3，本实施例中N＝17， E中的每个元素En被建模为例如，原子消息E1被建模为with类型的简单颜色集，复合消息E4被建模为product类型的复合颜色集，固定值E7被建模为常量，密码学操作E9被建模为函数GetKey。
[0058] (1b)建模事件A：
[0059] 按照格式：[库所名:库所类型:初始值:弧的方向:弧铭文]‑‑>变迁名:变迁执行条件‑‑>[库所名:库所类型:初始值:弧的方向:变量名]建模每个事件Am，得到事件模型其中，库所名为自定义的任意字符串，库所类型为步骤(1a)定义的简单颜色集或复合颜色集，初始值为步骤(1a)定义的常量，弧的方向取值可为PtoT、BOTHDIR、TtoP分别表示库所指向变迁、双向、变迁指向库所，弧铭文用于标识库所与变迁之间传递的数据，变迁名是自定义的任意字符串，执行条件为变迁的守卫函数，事件Am不需执行条件时，变迁执行条件省略不写，在两个相邻的事件模型 和 之间添加一个空行，其中， 之前和 之后的事件模型分别建模一条协议会话消息，设”end”字符串为事件建模结束的标志；
[0060] 参照附图4，本实施例中M＝12， A中的每个元素Am被建模为例如，第一个空行之前的内容建模客户端发送第一条消息时需要执行的事件A1,A2,A3，C_Send1表示客户端发送第一条消息的标识，事件模型 建模事件A1，表示执行一个不需要执行条件的ChoandGen的事件，一个库所类型为HKC的库所p1为该事件的输入库所，库所p1的初始值为C_InitHkc，库所p1和变迁ChoandGen之间的连接弧为双向弧，传递的数据为变量hkc所绑定的值，库所p2和库所p3为该事件的输出库所。
[0061] (2)设计安全协议模型解析工具：
[0062] (2a)设计安全协议模型解析工具的UI：
[0063] 利用python编程语言的pyside2库新建一个UI，向UI中添加两个文本框Text1、\ \Text2和一个按钮Button1，其中，Text1和Text2分别用于输入基本元素模型E和事件模型A，Button1执行安全协议模型解析并生成安全协议CPN模型的功能；
[0064] 参照附图5，本实施例中文本框Text1和Text2分别为文本框1和文本框2，按钮Button1为CPN模型生成按钮。
[0065] (2b)定义API生成CPN基本对象对应的XML标签：
[0066] 新建一个空白CPN模型Model1，模型Model1中存在的XML标签集合XModel1＝{X1,X2,...,Xp,...,XP}，向模型Model1中逐个添加单种CPN基本对象Oi(i＝1,...,8)后得到CPN模型设为Model1_1，模型Model1_1中存在的XML标签集合XModel1_1＝{X1,X2,...,Xp,...,XP,Xq}，得到Xq为CPN基本对象Oi对应的XML标签，并基于此，利用python编程语言的xml.dom.minidom库定义API生成CPN基本对象Oi对应的XML标签；
[0067] 参照附图6，本实施例中P＝16，XModel1＝{X1,X2,...,X16}，向模型Model1中添加一个颜色集之后，得到q＝17，Xq＝X17，XModel1_1＝{X1,X2,...,X16,X17}，＜color＞＜/color＞为颜色集对应的XML标签，＜color＞＜/color＞标签的具体内容如下：
[0068]
[0069] a
[0070]
[0071] colset a＝int；
[0072]
[0073] 其中，id＝"ID3"表示＜color＞＜/color＞标签的编号，a表示该颜色集的名称为a，表示该颜色集为int类型，colset a＝int；表示该颜色集的申明语法为colset a＝int；；
[0074] 利用python编程语言的xml.dom.minidom库定义API生成int类型颜色集对应的，API的具体内容如下：
[0075] def create_int_colset(id,declaration):
[0076] color＝create_color(id)
[0077] id＝id+1
[0078] chars＝declaration.split("")
[0079] color_id＝create_id(chars[1])
[0080] color_int＝DOMTree.createElement("int")
[0081] layout＝create_layout(declaration)
[0082] color.appendChild(color_id)
[0083] color.appendChild(color_int)
[0084] color.appendChild(layout)
[0085] return id,color
[0086] 其中，id参数为int类型颜色集的编号，declaration参数为int类型颜色集标签的文本内容，API的返回结果为id和color，其中color为int类型颜色集对应的＜color＞＜/color＞标签。
[0087] (2c)定义按钮Button1的功能：
[0088] 新建一个空白CPN模型Model2，加载模型Model2为Document对象，解析Text1和\ \Text2文本框中的基本元素模型E 和事件模型A ，基于步骤(2b)定义的API生成 和 对应的XML标签并将XML标签添加至Document对象，构建Dolev‑Yao攻击者CPN模型ModelI并将模型ModelI添加至Document对象，保存Document对象为XML文件；
[0089] 参照附图7，本实施例中，具体步骤如下：
[0090] 第一步，通过python编程语言的xml.dom.minidom库将模型Model2加载为Document对象；
[0091] 第二步，解析Text1文本框中的内容，判断 是否为简单颜色集或复合颜色集，若是，则生成一个 颜色集对应的变量 并基于步骤(2b)定义的API生成 和 对应的XML标签Xi和Xi1，并将XML标签Xi和Xi1添加至Document对象中，否则，则基于步骤(2b)定义的API生成 对应的XML标签Xi，并将XML标签Xi添加至Document对象中；
[0092] 本实施例中， colset Xr＝int；为int类型的简单颜色集，因此需生成一个对应的变量 varxr:Xr；，并基于步骤(2b)定义的API生成 和 对应的XML标签，并将XML标签Xi和Xi1添加至Document对象中， 和 对应的XML标签的具体内容如下；
[0093]
[0094] 其中，和分别为 和对应的XML标签。
[0095] 第三步，统计Text2文本框中空行的数量count，基于count创建Ctrl_I颜色集并基于步骤(2b)定义的API生成Ctrl_I颜色集对应的XML标签XI，创建一个fusion标签并设置name属性为Fusion_I，得到一个不包含任何元素的Fusion_I融合集，将XML标签XI和Fusion_I融合集对应的XML标签添加至Document对象中；
[0096] 本实施例中，count＝5，创建的Ctrl_I颜色集包含count‑1个元素，为colset Ctrl_I＝with I1|I2|I3|I4；，对应的XML标签具体内容如下：
[0097]
[0098] 第四步，解析Text2文本框中的内容，判断 是否为“end”字符串，若是，则跳过步骤(2c4)和步骤(2c5)，执行步骤(2c6)，否则，在模型Model2中添加一个变迁T和一个库所P，设库所P为变迁T的输出库所，基于层次化建模的方式将变迁T移动到子页面PageT1，将事件所描述的内容添加至子页面PageT1；
[0099] 参照附图8，本实施例中，针对第一个空行之前的事件模型 和 在模型Model2中添加的变迁T为C_Send1，库所P为In1，针对第二个空行之前的事件模型 和在模型Model2中添加的变迁T为S_Receive1_Send1，库所P为In2，针对第三个空行之前的事件模型 和 在模型Model2中添加的变迁T为C_Receive1_Send2，库所P为In3，针对第四个空行之前的事件模型 和 在模型Model2中添加的变迁T为S_Receive2_
Send2，库所P为In4，针对第五个空行之前的事件 在模型Model2中添加的变迁T为C_Receive2，事件 为最后一个事件，因此不存在输出库所。
[0100] 参照附图9，本实施例中，模型Model2中添加的变迁C_Send1关联的子页面PageT1为C_Send1子页面，其中，C_Send1子页面中的变迁ChoandGen、Cret_D1_1和Cret_D1_1分别是事件模型 和 对应的CPN模型。
[0101] 第五步，在模型Model2中添加一个攻击者变迁TI和一个库所PI，设库所PI为变迁TI的输出库所，将步骤(2c4)模型Model2添加的库所P设为变迁TI的输入库所，基于层次化建模的方式将变迁TI移动到子页面PageTI，其中，库所P和库所PI在子页面PageTI中分别为库所In和库所Out；向子页面PageTI中添加一个库所Data和一个库所I，将Data库所的库所类型设为库所In的库所类型，将库所I的类型设为Ctrl_I颜色集并将库所I添加至Fusion_I融合集，依据Dolev‑Yao攻击者模型给出的敌手能力的描述，在子页面PageTI中添加五个变迁来表示五种敌手能力：拦截、窃听、重放、分解、重构，拦截变迁的输入库所和输出库所分别设为库所In和库所Data，窃听变迁的输入库所和输出变迁分别设为库所In和库所Out，重放变迁的输入库所和输出变迁分别设为库所Data和库所Out，分解变迁的输入库所设为库所Data并对库所Data输入的数据进行拆分得到分解变迁的输出库所，重构变迁的输入库所和输出变迁分别设为分解变迁的输出库所和库所Out，将库所I设为拦截变迁和分解变迁的输出库所、窃听变迁、重放变迁和重构变迁的输入库所，返回步骤(2c4)；
[0102] 参照附图8，本实施例中，模型Model2中添加的攻击者变迁TI和库所PI分别为TI＝{Intruder1,Intruder2,Intruder3,Intruder4}和PI＝{Out1,Out2,Out3,Out4}。
[0103] 参照附图10，本实施例中，Intruder1的具体内容包括7个库所、5个变迁和18条弧，其中库所包括一个库所In、一个库所Out、一个库所Data、一个库所I和拆分第一条协议消息得到的三个库所Clientid、Xr和Hkc，变迁包括Intercept、Eavesdrop、SendData、Decomposite和Composite分别表示拦截、窃听、重放、分解、重构这五种敌手能力，变迁和库所之间的弧表示的库所中数据流动关系。
[0104] 第六步，将Document对象保存为XML文件，该XML文件即安全协议CPN模型。
[0105] (3)基于安全协议模型解析工具生成安全协议CPN模型：
[0106] 将步骤1建模的安全协议基本元素模型E\和事件模型A\分别输入至Text1和Text2文本框中，点击Button1按钮执行安全协议模型解析并生成安全协议CPN模型；
[0107] (4)生成安全协议CPN模型的状态空间：
[0108] 依据安全协议需要满足的安全要求定制安全协议安全性评估规则R＝{R1,R2,...,Rk,...,RK}，其中，K≥1，并以SML语言描述每条评估规则Rk，设置CPN Tools状态空间计算工具的predicatestop参数为评估规则Rk，在此基础上，利用状态空间计算工具生成安全协议CPN模型的状态空间S＝{S1,S2,...,Sl,...,SL}，其中，L≥1；
[0109] 本实施例中K＝3，R＝{R1,R2,R3}，其中，评估规则R3为：Client和Server交换密钥SK和初始化序列号N0成功，然而获取到的SK和N0并不是本次会话中产生的，SML语言描述评估规则R3，具体内容如下：
[0110] fn n＝>
[0111] let
[0112] val sk＝Mark.C_Receive2'p19 1n
[0113] val sk1＝remdupl sk
[0114] in
[0115] if(length sk)＝(length sk1)
[0116] then false
[0117] else true
[0118] end
[0119] 将状态空间计算工具的predicatestop参数设置为该SML表达式描述的评估规则，生成安全协议CPN模型的状态空间S＝{S1,S2,...,S1529}。
[0120] (5)获取安全协议漏洞挖掘结果：
[0121] 利用SearchNodes函数检索状态空间S中是否存在不符合步骤(4)所描述的评估规则Rk的不安全状态St，若是，说明安全协议在当前构建的Dolev‑Yao攻击者模型下安全协议是不安全的，进一步通过ArcsInPath函数获取从初始状态S1至不安全状态St的攻击路径，挖掘安全协议漏洞，否则，说明在当前构建的Dolev‑Yao攻击者模型下安全协议是安全的。
[0122] 本实施例中SearchNodes函数的具体描述如下：
[0123] SearchNodes(EntireGraph,
[0124] fn n＝>
[0125] let
[0126] val sk＝Mark.C_Receive2'p19 1n
[0127] val sk1＝remdupl sk
[0128] in
[0129] if(length sk)＝(length sk1)
[0130] then false
[0131] else true
[0132] end,
[0133] 1,
[0134] fn n＝>n,
[0135] [],
[0136] op::)
[0137] 参照附图11，本实施例中SearchNodes函数的返回值为1379，说明状态空间S中存在不符合评估规则R3的不安全状态S1379，进一步通过ArcsInPath函数获取从初始状态S1至不安全状态S1379的攻击路径，挖掘安全协议漏洞，ArcsInPath函数的具体描述如下：
[0138] fun Arc(item)＝
[0139] print(ArcDescriptor(item)^"\n")；
[0140] val node＝1379
[0141] val arcs＝ArcsInPath(1,node)
[0142] val it＝map Arc arcs
[0143] 其中，Arc函数实现对攻击路径中每条边的描述。val arcs＝ArcsInPath(1,node)表示获取从初始状态S1至不安全状态S1379的攻击路径，val it＝map Arc arcs表示对arcs中的每个元素执行函数Arc的功能，并返回一个包含所有结果的列表，列表中的每一行是对一条弧的详细描述，例如，1:1‑>2C_Send1'ChoandGen 1:{hkc＝Kcs}表示弧的编号为1，表示C_Send1子页面中变迁ChoandGen执行时弧铭文hkc绑定的数值为Kcs，变迁ChoandGen执行后由状态S1转变到了状态S2。
[0144] 以上描述仅是本发明的一个具体实例，显然对于本领域的专业人员来说，在了解了本发明内容和原理后，都可能在不背离本发明原理、结构的情况下，进行形式和细节上的各种修正和改变，但是这些基于本发明思想的修正和改变仍在本发明的权利要求保护范围之内。
