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

關(guān)鍵詞：安全協(xié)議；BAN邏輯；進(jìn)化規(guī)劃；自動生成

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 引 言

安全協(xié)議是以密碼學(xué)為基礎(chǔ)的協(xié)議，它在網(wǎng)絡(luò)和分布式系統(tǒng)中提供各種各樣的安全服務(wù)，在信息系統(tǒng)安全中占據(jù)重要的地位。近些年來，伴隨著 Internet 在全世界的飛速發(fā)展，大量網(wǎng)絡(luò)通信方面的應(yīng)用不斷產(chǎn)生，針對不同的應(yīng)用需求，均需要為之設(shè)計相應(yīng)的安全協(xié)議。但實(shí)踐證明，既便是一個簡單的協(xié)議，其設(shè)計和分析也是不容易的。

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

2 安全協(xié)議生成系統(tǒng)

本文提出的安全協(xié)議生成系統(tǒng)如圖1所示。

系統(tǒng)的輸入是安全協(xié)議的形式化需求規(guī)范，輸出是安全協(xié)議，生成模塊、驗證模塊和優(yōu)化模塊是系統(tǒng)的三個主要模塊。根據(jù)算法的染色體編碼方式，構(gòu)造出安全協(xié)議狀態(tài)空間，生成模塊的作用就是在安全協(xié)議空間中進(jìn)行搜索。生成模塊輸出的候選協(xié)議，驗證模塊對其進(jìn)行評估，主要是安全協(xié)議的安全性、效率和冗余度等因素。其中，安全協(xié)議的安全性評估是關(guān)鍵，通常是檢查協(xié)議是否達(dá)到了安全目標(biāo)。同時，對于驗證模塊出來的安全協(xié)議一定是達(dá)到了安全目標(biāo)的，但不一定是無冗余的，因此需要通過優(yōu)化模塊刪除里面不必要的消息體和信念。如果生成系統(tǒng)產(chǎn)生的候選協(xié)議通過了驗證，則進(jìn)入優(yōu)化模塊優(yōu)化輸出安全協(xié)議；否則繼續(xù)轉(zhuǎn)到生成模塊，繼續(xù)在狀態(tài)空間中進(jìn)行搜索。

3 安全協(xié)議的驗證方法

安全協(xié)議的驗證是安全協(xié)議自動生成的基礎(chǔ)，信念邏輯方法嚴(yán)謹(jǐn)且易于自動化，是一個比較合適的選擇。本文采用BAN邏輯來進(jìn)行安全協(xié)議的驗證。

BAN邏輯是一種基于信念的模態(tài)邏輯，在應(yīng)用BAN邏輯時，首先需要將協(xié)議理想化為邏輯公式，由邏輯的推理規(guī)則根據(jù)理想化協(xié)議和假設(shè)進(jìn)行推理，推斷協(xié)議能否完成預(yù)期的目標(biāo)。因此BAN邏輯不僅可以用來對于協(xié)議進(jìn)行分析，還可以在協(xié)議自動生成中作為協(xié)議的評估標(biāo)準(zhǔn)。