[發明專利]一種網絡安全協議的自動形式化驗證方法

有效

• 申請號: 202211083948.9
• 申請日: 2022-09-06
• 公開（公告）號: CN115460297B
• 公開（公告）日: 2023-06-30
• 發明（設計）人: 黃文超;熊焰;汪萬森;孟昭逸;蘇誠;熊峰;方賢進
• 申請（專利權）人: 中國科學技術大學
• 主分類號: H04L69/00
• 分類號: H04L69/00;H04L43/18;G06N20/00
• 代理公司: 安徽思沃達知識產權代理有限公司 34220
• 代理人: 王茜

本發明公開了一種網絡安全協議的自動形式化驗證方法，包括步驟：一、輸入協議模型；二、初始樹構建；已依據靜態策略路徑選擇執行六、否則執行三；三、依據靜態策略進行路徑選擇；四、依據靜態策略進行路徑檢查；路徑循環執行二；完整且正確輸出驗證結果；正確但不完整執行五；五、定理樹合并，已依據靜態策略路徑選擇執行六、否則執行三；六、依據動態策略進行路徑選擇；七、依據動態策略進行路徑檢查；路徑循環時訓練神經網絡優化證明策略再返回二；路徑完整且正確時輸出驗證結果；路徑正確但不完整時執行八；八、定理樹合并：定理樹合并，已依據靜態策略進行了路徑選擇執行六、否則執行三。本發明全過程都自動化，準確性高，效率高。

技術領域

本發明屬于計算機網絡協議安全分析技術領域，具體涉及一種網絡安全協議的自動形式化驗證方法。

背景技術

網絡安全協議的自動化驗證是形式化方法的重要目標，對于復雜的大型網絡安全協議，人工驗證的可行性較小，需要計算機進行輔助證明。因此，網絡安全協議的自動化分析就變得十分必要。

現如今，形式化驗證技術已在網絡安全協議的安全分析領域廣泛應用。ProVerif在Proceedings?of?the?14th?IEEE?Computer?Security?Foundations?Workshop(CSFW’14)發表的論文《B.Blanchet.An?efficient?cryptographic?protocol?verifier?basedon?Prolog?rules》中，基于邏輯編程語言Prolog規則，支持無限輪數協議的驗證。StatVerif在Proceedings?of?the?24th?IEEE?Computer?Security?FoundationsSymposium,CSF?2011發表的論文《Statverif:Verification?of?stateful?processes》中，擴展了ProVerif，支持全局狀態。它適用于狀態較少的簡單安全協議。Set-π在IEEE?28thComputer?Security?Foundations?Symposium,CSF?2015,Verona發表的論文《Setmembership?p-calculus》中，使用set-membership抽象來表示全局狀態，該工具基于ProVerif，并可以自動驗證簡單的狀態遷移協議。Maude-NPA在Computer?AidedVerification-25th?International?Conference發表的論文《Cryptographic?ProtocolAnalysis?Modulo?Equational?Propertie》中，支持無限會話模型,不僅可以實現攻擊和漏洞搜索，還可以實現安全性證明。Tamarin在Computer?Aided?Verification-25thInternational?Conference,CAV?2013發表的論文《The?TAMARIN?prover?for?thesymbolic?analysis?of?security?protocols》中，基于多重集合改寫規則描述協議流程，利用一階邏輯量化協議消息和時間節點,從而實現對協議屬性的描述，支持對具有復雜控制流的協議的驗證。

以上幾類工具雖然能夠實現部分協議的自動化驗證，但仍存在一個主要問題：驗證過程基于靜態策略，對于特定協議會由于狀態空間爆炸出現證明無法終止的情況。

目前，蘇誠在其博士論文《基于強化學習的網絡協議形式化驗證技術》中，提出了一種基于強化學習的網絡協議形式化驗證技術，通過動態策略解決狀態空間爆炸問題。但該技術還存在以下兩個問題：1)對于簡單協議也需要訓練強化學習網絡，相比靜態策略來說驗證效率較低；2)對不正確路徑的判斷方法是基于文本相似度的，存在準確性、通用性不足的問題，而錯誤的路徑判斷會導致部分協議無法完成自動驗證。

綜上所述，現有技術中的網絡安全協議自動形式化驗證方法，還無法很好地解決網絡安全協議的自動化驗證問題。

發明內容