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

在審

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

1.一種基于IPv6下的安全協(xié)議的形式化驗證方法，其特征在于，該方法包括如下步驟：

步驟S1，安全協(xié)議分析階段

提取安全協(xié)議所涉及的數(shù)據(jù)，包括安全協(xié)議的通信主體、通信信道、通信交互消息、通信交互過程和協(xié)議安全目標；

步驟S2，安全協(xié)議簡化階段

對步驟S1提取的安全協(xié)議所涉及的數(shù)據(jù)進行簡化；

步驟S3，安全協(xié)議形式化建模階段

對步驟S2簡化后的安全協(xié)議所涉及的數(shù)據(jù)進行形式化建模得到形式化模型，該形式化模型能被自動化工具進行自動化驗證；

步驟S4，自動化工具驗證階段

使用自動化工具提供的語法規(guī)則描述形式化模型，然后使用自動化工具進行自動化驗證，得到自動化工具輸出的驗證結果；

步驟S5，可視化結果階段

對步驟S4輸出的驗證結果進行判斷，對每一個要驗證的安全目標自動化驗證工具會輸出唯一的驗證結果并進行可視化輸出。

2.根據(jù)權利要求1所述的基于IPv6下的安全協(xié)議的形式化驗證方法，其特征在于，步驟S1所述通信交互過程是指通信主體在通信信道上發(fā)送或接收通信交互消息的過程。

3.根據(jù)權利要求1所述的基于IPv6下的安全協(xié)議的形式化驗證方法，其特征在于，步驟S2所述的數(shù)據(jù)進行簡化為刪除數(shù)據(jù)中起中轉作用的通信主體及與該通信主體對應的所有的通信交互消息和通信交互過程。

4.根據(jù)權利要求1所述的基于IPv6下的安全協(xié)議的形式化驗證方法，其特征在于，步驟S3所述對步驟S2簡化后的安全協(xié)議所涉及的數(shù)據(jù)進行建模是使用Pi演算語法對安全協(xié)議所涉及的數(shù)據(jù)進行形式化建模。

5.根據(jù)權利要求1所述的基于IPv6下的安全協(xié)議的形式化驗證方法，其特征在于，步驟S4所述的自動化工具為ProVerif工具；所述語法規(guī)則為Prolog編程語言規(guī)則；所述描述形式化模型為使用Prolog編程語言描述步驟S3得到的形式化模型。

6.根據(jù)權利要求1所述的基于IPv6下的安全協(xié)議的形式化驗證方法，其特征在于：步驟S5所述的驗證結果進行判斷，具體為：對每一個要驗證的安全目標ProVerif工具會輸出唯一的驗證結果并進行可視化輸出，其中，唯一的驗證結果為下述的A或B：

A.所驗證安全目標得到true的結果，則證明該安全目標成立，即協(xié)議滿足該安全目標；

B.所驗證的安全目標得到false的結果，則證明該安全目標不成立，即協(xié)議不滿足該安全目標，即該協(xié)議存在該安全目標對應的漏洞。