[發(fā)明專利]一種網(wǎng)絡(luò)安全協(xié)議的自動(dòng)形式化驗(yàn)證方法

有效

• 申請?zhí)枺?/td>: 202211083948.9
• 申請日: 2022-09-06
• 公開（公告）號: CN115460297B
• 公開（公告）日: 2023-06-30
• 發(fā)明（設(shè)計(jì)）人: 黃文超;熊焰;汪萬森;孟昭逸;蘇誠;熊峰;方賢進(jìn)
• 申請（專利權(quán)）人: 中國科學(xué)技術(shù)大學(xué)
• 主分類號: H04L69/00
• 分類號: H04L69/00;H04L43/18;G06N20/00
• 代理公司: 安徽思沃達(dá)知識(shí)產(chǎn)權(quán)代理有限公司 34220
• 代理人: 王茜

1.一種網(wǎng)絡(luò)安全協(xié)議的自動(dòng)形式化驗(yàn)證方法，其特征在于，該方法包括以下步驟：

步驟一、輸入?yún)f(xié)議模型：輸入網(wǎng)絡(luò)安全協(xié)議形式化模型；

步驟二、初始樹構(gòu)建：構(gòu)建形式化驗(yàn)證的底層框架，自動(dòng)提取網(wǎng)絡(luò)安全協(xié)議形式化模型中的證明目標(biāo)，構(gòu)建初始定理樹；判斷是否已依據(jù)靜態(tài)策略進(jìn)行了路徑選擇，是就執(zhí)行步驟六、否則執(zhí)行步驟三；

步驟三、依據(jù)靜態(tài)策略進(jìn)行路徑選擇：根據(jù)預(yù)設(shè)的靜態(tài)策略進(jìn)行證明路徑的選擇；

步驟三中所述預(yù)設(shè)的靜態(tài)策略包括以下任意一種：

第一種、按照約束引入的先后順序進(jìn)行證明路徑節(jié)點(diǎn)選擇，優(yōu)先選擇先引入的約束對應(yīng)的證明路徑節(jié)點(diǎn)；

第二種、按照約束類型進(jìn)行證明路徑節(jié)點(diǎn)選擇，優(yōu)先選擇鏈型約束對應(yīng)的證明路徑節(jié)點(diǎn)，次優(yōu)選擇析取約束對應(yīng)的證明路徑節(jié)點(diǎn)，再次之選擇事實(shí)約束或動(dòng)作約束對應(yīng)的證明路徑節(jié)點(diǎn)，攻擊者相關(guān)約束的證明路徑節(jié)點(diǎn)最后選擇；

第三種、優(yōu)先選擇鏈型約束對應(yīng)的證明路徑節(jié)點(diǎn)，次優(yōu)選擇析取約束對應(yīng)的證明路徑節(jié)點(diǎn)，剩下幾個(gè)類型的約束對應(yīng)的證明路徑節(jié)點(diǎn)處于同等優(yōu)先級，按照引入約束的順序進(jìn)行選擇；

步驟四、依據(jù)靜態(tài)策略進(jìn)行路徑檢查：使用循環(huán)檢測算法判斷證明路徑的完整性和正確性；當(dāng)證明路徑中存在循環(huán)時(shí)，返回執(zhí)行步驟二；當(dāng)證明路徑完整且正確時(shí)，網(wǎng)絡(luò)安全協(xié)議成功完成驗(yàn)證，系統(tǒng)自動(dòng)終止，輸出驗(yàn)證結(jié)果；當(dāng)證明路徑正確但不完整時(shí)，執(zhí)行步驟五；

步驟五、定理樹合并：根據(jù)當(dāng)前證明路徑，使用信息獲取模塊進(jìn)一步構(gòu)建新的定理子樹，并與之前輪次的定理樹合并，對定理樹進(jìn)行擴(kuò)展；擴(kuò)展完成后，判斷是否已依據(jù)靜態(tài)策略進(jìn)行了路徑選擇，是就執(zhí)行步驟六、否則返回執(zhí)行步驟三；

步驟六、依據(jù)動(dòng)態(tài)策略進(jìn)行路徑選擇：根據(jù)預(yù)設(shè)的動(dòng)態(tài)策略進(jìn)行證明路徑的選擇；

步驟七、依據(jù)動(dòng)態(tài)策略進(jìn)行路徑檢查：使用循環(huán)檢測算法判斷證明路徑的完整性和正確性；當(dāng)證明路徑中存在循環(huán)時(shí)，可能導(dǎo)致協(xié)議驗(yàn)證過程無法終止，給予該證明路徑神經(jīng)網(wǎng)絡(luò)反饋，并訓(xùn)練神經(jīng)網(wǎng)絡(luò)優(yōu)化證明策略，再返回執(zhí)行步驟二；當(dāng)證明路徑完整且正確時(shí)，網(wǎng)絡(luò)安全協(xié)議成功完成驗(yàn)證，系統(tǒng)自動(dòng)終止，輸出驗(yàn)證結(jié)果；當(dāng)證明路徑正確但不完整時(shí)，執(zhí)行步驟八；

步驟八、定理樹合并：根據(jù)當(dāng)前證明路徑，使用信息獲取模塊進(jìn)一步構(gòu)建新的定理子樹，并與之前輪次的定理樹合并，對定理樹進(jìn)行擴(kuò)展；擴(kuò)展完成后，判斷是否已依據(jù)靜態(tài)策略進(jìn)行了路徑選擇，是就執(zhí)行步驟六、否則返回執(zhí)行步驟三。

2.按照權(quán)利要求1所述的一種網(wǎng)絡(luò)安全協(xié)議的自動(dòng)形式化驗(yàn)證方法，其特征在于：步驟一中所述網(wǎng)絡(luò)安全協(xié)議形式化模型使用多重集合復(fù)寫規(guī)則表示。

3.按照權(quán)利要求1所述的一種網(wǎng)絡(luò)安全協(xié)議的自動(dòng)形式化驗(yàn)證方法，其特征在于：步驟六中所述預(yù)設(shè)的動(dòng)態(tài)策略為DQN強(qiáng)化學(xué)習(xí)網(wǎng)絡(luò)、DDQN強(qiáng)化學(xué)習(xí)網(wǎng)絡(luò)或DuelingDQN強(qiáng)化學(xué)習(xí)網(wǎng)絡(luò)，步驟六中所述根據(jù)預(yù)設(shè)的動(dòng)態(tài)策略進(jìn)行證明路徑的選擇時(shí)，根據(jù)DQN強(qiáng)化學(xué)習(xí)網(wǎng)絡(luò)、DDQN強(qiáng)化學(xué)習(xí)網(wǎng)絡(luò)或DuelingDQN強(qiáng)化學(xué)習(xí)網(wǎng)絡(luò)評估定理樹各節(jié)點(diǎn)成功完成驗(yàn)證的概率，并根據(jù)評估結(jié)果自動(dòng)選擇出證明路徑。

4.按照權(quán)利要求1所述的一種網(wǎng)絡(luò)安全協(xié)議的自動(dòng)形式化驗(yàn)證方法，其特征在于：步驟四和步驟七中所述循環(huán)檢測算法為基于約束含義的循環(huán)檢測算法，采用該循環(huán)檢測算法判斷證明路徑的完整性和正確性時(shí)的方法為：去除約束中的時(shí)間點(diǎn)編號和項(xiàng)編號，得到簡化后的約束；并略過即使簡化形式相同也可能存在不同的含義的特殊約束；當(dāng)兩個(gè)約束簡化形式相同時(shí)，判斷為兩個(gè)約束的含義是相同的，對證明過程的影響也是相似的；當(dāng)這樣的約束在某條證明路徑中出現(xiàn)過多次時(shí)，判斷為證明路徑中存在循環(huán)。

5.按照權(quán)利要求4所述的一種網(wǎng)絡(luò)安全協(xié)議的自動(dòng)形式化驗(yàn)證方法，其特征在于：所述即使簡化形式相同也可能存在不同的含義的特殊約束包括攻擊者相關(guān)約束、時(shí)間點(diǎn)比較約束和時(shí)間點(diǎn)引入約束。

6.按照權(quán)利要求4所述的一種網(wǎng)絡(luò)安全協(xié)議的自動(dòng)形式化驗(yàn)證方法，其特征在于：所述當(dāng)這樣的約束在某條證明路徑中出現(xiàn)過多次時(shí)，判斷為證明路徑中存在循環(huán)，其中，多次為三次以上。