[發明專利]基于著色Petri網的安全協議漏洞挖掘方法

有效

• 申請號: 202210497259.6
• 申請日: 2022-05-09
• 公開（公告）號: CN114900358B
• 公開（公告）日: 2023-01-06
• 發明（設計）人: 馬卓;李湘;劉洋;劉心晶;楊易龍;張俊偉;李騰;馬建峰
• 申請（專利權）人: 西安電子科技大學
• 主分類號: H04L9/40
• 分類號: H04L9/40;G06F21/57
• 代理公司: 陜西電子工業專利中心 61205
• 代理人: 陳宏社;王品華

本發明公開了一種基于著色Petri網的安全協議漏洞挖掘方法，其實現步驟為：基于著色Petri網CPN建模安全協議，設計安全協議模型解析工具，基于安全協議模型解析工具生成安全協議CPN模型，生成安全協議CPN模型的狀態空間，獲取安全協議漏洞挖掘結果。本發明通過著色Petri網CPN建模安全協議，使得在構建復雜安全協議模型的情況下，模型結構清晰且易于理解，并在安全協議CPN建模階段引入了安全協議模型解析工具，實現了安全協議CPN模型的自動化生成，相比于現有手動CPN建模的方案，精簡了安全協議CPN模型建模的步驟，極大地降低了安全協議漏洞挖掘的門檻，并且能夠正確實現安全協議漏洞的挖掘。

技術領域

本發明屬于網絡空間安全技術領域，更進一步涉及一種基于著色Petri網的安全協議漏洞挖掘方法，可用于金融系統等領域。

背景技術

安全協議也被稱之為密碼學協議，它的目標是通過應用密碼學基件在不安全的網絡環境中提供安全的通信服務。安全協議被設計用于保障開放網絡和分布系統中秘密信息的安全處理和傳輸，在金融系統、軍事系統等諸多領域提供安全服務，不同的安全協議在設計之初都有其對應的安全目標，也被稱之為安全協議的安全屬性。

安全協議的漏洞指的是可能允許攻擊者以他人的身份進行身份驗證，或者獲得不應該被披露的信息，從而破壞安全協議設計之初的安全屬性的不安全因素。安全協議的海量、復雜、易錯等特點，導致安全協議自動化漏洞挖掘的需求與日俱增。

模型檢測技術是一類主流的安全協議漏洞挖掘方法，該類方法的優點是自動化能力強，可計算出安全協議的不安全反例。其實現過程為：首先提取安全協議模型M_t，定制安全協議的安全性質P_t，檢查P_t是否能在M_t的任何狀態下都成立。當安全協議模型M_t的某個狀態不滿足性質P時，即在模型M_t的狀態空間中存在不安全狀態時，模型檢測器就會把這條通往不安全狀態的路徑返回，從而實現安全協議漏洞的挖掘。通過模型檢測技術在對安全協議漏洞進行挖掘時，必須盡可能考慮想破壞安全協議安全屬性的攻擊者可能采取的所有行動。Dolev-Yao模型是所有對安全協議進行漏洞挖掘的基礎攻擊者模型，作為傳統的攻擊者模型極其具有代表性。Dolev-Yao攻擊者的能力描述如下：

(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)語言可以輔助完成安全協議漏洞挖掘所需要的不安全狀態檢索和攻擊路徑搜索功能。