[發明專利]針對安全協議的形式化建模及驗證方法

有效

• 申請號: 201310152401.4
• 申請日: 2013-04-27
• 公開（公告）號: CN103259788A
• 公開（公告）日: 2013-08-21
• 發明（設計）人: 李曉紅;沈崗;胡靜;韓卓兵;謝肖飛;張程偉
• 申請（專利權）人: 天津大學
• 主分類號: H04L29/06
• 分類號: H04L29/06
• 代理公司: 天津市北洋有限責任專利代理事務所 12201
• 代理人: 劉國威

1.一種針對安全協議的形式化建模及驗證方法，其特征是，包括如下步驟：

1)、對安全協議進行總結和分析，提取出安全協議所涉及的資源、協議參與者交互過程和安全屬性，使用Pi演算對這些信息進行描述，獲得安全協議的形式化模型；

2)、根據得到的安全協議形式化模型作為輸入，使用Proverif工具進行自動化驗證，對驗證的結果進行細化分塊，并將發現的攻擊路徑進行圖形化；

3)、將細化分塊后的驗證結果和圖形化的攻擊路徑整合，最終得到一份完整的協議驗證結果報表，使其能幫助安全協議研究人員較快的發現并修復安全協議存在的缺陷。

2.根據權利要求1所述的針對安全協議的形式化建模及驗證方法，其特征是，對安全協議進行總結和分析即安全協議形式化建模分析及驗證主要包括三個部分：安全協議知識抽取，安全協議形式化建模，驗證結果細化分塊及攻擊路徑圖形化，整個框架的輸入是安全協議知識，輸出是針對該安全協議相應安全屬性的驗證結果；

安全協議形式化建模是通過對安全協議知識進行整理、提煉和抽象，并使用Pi演算對安全協議知識進行描述，通過Pi演算來定義協議的資源、安全屬性和協議參與者的交互過程，最后完成安全協議的整體建模，使該模型能被Proverif工具進行自動化驗證；

驗證結果細化分塊主要是根據Proverif幫助文檔對驗證結果的具體結構進行分析，從而得到源碼經編譯后的主程序，驗證的屬性個數，驗證屬性的假設和結果，如果驗證結果不滿足相關的安全屬性，則會給出相應的反例，反例中主要包含對應的目標反例、攻擊路徑和相應的攻擊跟蹤，而攻擊路徑圖形化則是先將相應的攻擊軌跡轉化成易于理解的信息交互過程，并將該信息交互過程以信息交互圖的形式進行顯示，最終生成驗證結果報表。

3.根據權利要求2所述的針對安全協議的形式化建模及驗證方法，其特征是，安全協議知識主要包括協議資源、參與者交互過程和安全屬性，安全協議知識是協議進行形式化建模的數據源，主要是安全協議的相關聲明以及實現這些安全協議的應用，安全協議知識是建模和驗證的數據基礎。