[發明專利]一種基于IPv6下的安全協議的形式化驗證方法

在審

• 申請號: 202010693695.1
• 申請日: 2020-07-17
• 公開（公告）號: CN111885039A
• 公開（公告）日: 2020-11-03
• 發明（設計）人: 何道敬;葉籽蘭;鄧智;宋銘辰
• 申請（專利權）人: 華東師范大學
• 主分類號: H04L29/06
• 分類號: H04L29/06;H04L12/24
• 代理公司: 上海藍迪專利商標事務所(普通合伙) 31215
• 代理人: 徐筱梅;張翔

本發明公開了一種基于IPv6下的安全協議的形式化驗證方法，涉及Ipv6網絡安全領域，具體為一種針對安全協議的形式化驗證方法，包括如下步驟：1）安全協議分析階段提取安全協議所涉及的數據；2）安全協議簡化階段對提取的安全協議數據進行簡化；3）安全協議形式化建模階段使用Pi演算語法表示安全協議數據，進行形式化建模；4）自動化工具驗證階段使用Prolog編程語言描述形式化模型，使用ProVerif工具進行自動化驗證，得到ProVerif工具輸出的驗證結果；5）可視化結果階段對輸出驗證結果進行可視化顯示，顯示是否滿足相應的安全目標。本發明主要應用于信息交換安全場合，針對IPv6網絡環境安全，以SPFP協議為例進行形式化驗證，有利于提高IPv6的移動網絡環境的安全性。

技術領域

本發明屬于Ipv6網絡安全領域，特別涉及一種基于IPv6下的安全協議的形式化驗證方法。

背景技術

計算機網絡中，安全協議為通信雙方的信息交互提供安全保證，是計算機網絡安全的基礎。而當安全協議中存在安全漏洞時，會對信息安全產生重大威脅， 造成數據泄露、身份被冒用等危害。因此，對于安全協議安全性的研究，歷來都屬于安全領域的重要研究方向。互聯網經過幾十年的飛速發展，IPv4的地址已經耗盡，我國在2014年至2015年也逐步停止了向新用戶和應用分配IPv4地址，同時全面開始商用部署IPv6。

IPv6的引進帶來了更大的地址空間，同時也帶來了新的風險。因為部分協議新特性未配備適當的安全機制，可能引發擴展頭攻擊、NDP攻擊、DAD攻擊、前綴欺騙攻擊、MLD攻擊甚至新型網絡攻擊。在IPv4向IPv6的過渡期，還需要考慮各種過渡技術與方案的安全隱患。過渡期IPv4網絡與IPv6網絡同時存在且需要互通，需要滿足來自兩種不同IP協議網絡的威脅不能夠交叉感染。IPv6建設中將和IPv4長期并存，通常采用雙棧機制、隧道機制、翻譯機制等過渡機制實現IPv4向IPv6網絡的平穩升級。但部分過渡機制自身存在安全缺陷或將引入新的安全隱患。所以IPv6的安全協議是否存在問題也就需要進行形式化驗證的分析。

IPv6安全協議類型三大類型：

（1）密鑰交換協議：該類協議一般為通信雙方或多方之間協商一個會話密鑰。該會話密鑰一般通過主密鑰來產生。

（2）認證協議：該類協議主要目的是確定通信過程中某些信息，這些信息包括通信對方的身份、消息的目的等。主要用來防止偽造、篡改和否認等攻擊。

（3）認證及密鑰交換協議：該協議結合了上述兩種協議的目的，首先進行認證確定身份等信息，通過認證后進行密鑰交換來確定會話密鑰。目前互聯網中的安全協議大部分是該類協議。

驗證協議是否存在安全漏洞，對協議的安全性進行形式化分析是一種重要途徑。形式化分析方法的理論體系大致可分為三類：模態邏輯技術、模型檢測技術和定理證明技術。模態邏輯分析方法主要包括信仰邏輯方法和知識邏輯方法，用于分析協議執行過程中主體知識和信念的演化過程，比較有名的就是BAN邏輯，但BAN自身的缺陷決定了BAN發現的漏洞一定是漏洞，但是BAN證明是安全的協議未必是安全的。定理證明與模態邏輯技術很相似，其基本思想是將協議過程用公理系統來描述，同樣，也用目標定理表示安全目標，然后借助于數學方法對公理系統進行證明，看能否推出目標定理。

模型檢驗是并發系統驗證的主要形式化方法之一，與前兩種相比，其最大的優勢在于實現系統的自動化驗證。模型檢測技術分析有三個步驟：定義系統有限狀態機模型、定義系統屬性、系統模型驗證。這類方法本身都是從協議的初始狀態開始，對合法主體和一個攻擊者的所有可能的執行路徑進行窮盡搜索以期找到協議可能存在的錯誤。ProVerif工具是由法國人Bruno Blanchet提出并開發的，基于Dolev-Yao模型的主要用于安全密碼協議的自動形式化驗證分析工具，其基本原理是利Horn子句抽象相應的密碼協議并實施分析。相比較BAN邏輯，Proverif工具給出的結論無論是明確的true還是明確的false都是可以保證的結論的正確性的。

發明內容