基于進化規劃的網絡安全協議的自動生成

摘 要：提出了基于進化規劃的安全協議生成方法，并用BAN邏輯來描述和驗證協議，為進一步提高協議生成效率，降低協議消息的冗余度，加入了協議優化模塊。該方法具有較高的擴展性，對于不同的需求，可以生成不同的安全協議。實驗表明，本文方法能夠成功、高效地生成安全協議，保證所生成協議的安全性。

關鍵詞：安全協議；BAN邏輯；進化規劃；自動生成

Automatic Generation of Cryptographic Protocol Based on BAN Logic

SUN Wanghua，SHEN Pubing，YANG Jin

(Xi′an Communication Institute，Xi′an，710106，China)

Abstract：An automatic generating approach cryptographic protocol is presented.Evolutionary programming is used as the core generating algorithm.BAN logic is used to describe and verify the protocol.Optimization system is used to increase the efficiency and reduce the redundancy of the generated protocols.The experimental results show that this approach is effective and of high efficiency.

Keywords：security protocol;BAN logic;evolutionary programming;automatic generating



1 引 言

安全協議是以密碼學為基礎的協議，它在網絡和分布式系統中提供各種各樣的安全服務，在信息系統安全中占據重要的地位。近些年來，伴隨著 Internet 在全世界的飛速發展，大量網絡通信方面的應用不斷產生，針對不同的應用需求，均需要為之設計相應的安全協議。但實踐證明，既便是一個簡單的協議，其設計和分析也是不容易的。

安全協議的自動生成與驗證研究是目前安全協議研究領域中的熱點之一^［1］，它為安全協議設計提供了一個新途徑。目前，針對安全協議自動驗證的研究比較多，而將安全協議的自動生成和驗證結合起來，進行安全協議自動綜合的研究則還很少。國外這方面的研究較多，而國內剛剛起步。國際上，Ho Randy^［2］采用人工智能規劃算法來生成安全協議，并用基于知識邏輯的方法來進行驗證；Perrig和Song^［3］采用迭代深化搜索算法來生成安全協議，并用模型檢測器Athena來進行驗證；John和Jeremy^［4］采用遺傳算法來生成安全協議，并用BAN類邏輯來進行驗證。國內，毛晨曉博士^［5］在其畢業論文中采用遺傳策略來生成安全協議，將協議結構作為安全協議知識庫的啟發式信息直接給出，而僅僅考慮了消息內容的自動生成問題。這種方法由于協議結構直接給出，消息內容基本不會有太大的變動，可擴展性不強，協議形式較單一，不能充分體現協議自動生成的動態性和多樣性。鑒于此，本文提出了基于進化規劃的安全協議生成方法，并用BAN邏輯來描述和驗證協議，為進一步提高協議生成效率，降低協議消息的冗余度，加入了協議優化模塊。實驗表明，本文方法能夠成功、高效地生成安全協議，保證所生成協議的安全性。

2 安全協議生成系統

本文提出的安全協議生成系統如圖1所示。

系統的輸入是安全協議的形式化需求規范，輸出是安全協議，生成模塊、驗證模塊和優化模塊是系統的三個主要模塊。根據算法的染色體編碼方式，構造出安全協議狀態空間，生成模塊的作用就是在安全協議空間中進行搜索。生成模塊輸出的候選協議，驗證模塊對其進行評估，主要是安全協議的安全性、效率和冗余度等因素。其中，安全協議的安全性評估是關鍵，通常是檢查協議是否達到了安全目標。同時，對于驗證模塊出來的安全協議一定是達到了安全目標的，但不一定是無冗余的，因此需要通過優化模塊刪除里面不必要的消息體和信念。如果生成系統產生的候選協議通過了驗證，則進入優化模塊優化輸出安全協議；否則繼續轉到生成模塊，繼續在狀態空間中進行搜索。

3 安全協議的驗證方法

安全協議的驗證是安全協議自動生成的基礎，信念邏輯方法嚴謹且易于自動化，是一個比較合適的選擇。本文采用BAN邏輯來進行安全協議的驗證。

BAN邏輯是一種基于信念的模態邏輯，在應用BAN邏輯時，首先需要將協議理想化為邏輯公式，由邏輯的推理規則根據理想化協議和假設進行推理，推斷協議能否完成預期的目標。因此BAN邏輯不僅可以用來對于協議進行分析，還可以在協議自動生成中作為協議的評估標準。