實例化空間邏輯在安全協(xié)議驗證中的語義研究與應用.pdf

1、安全協(xié)議是在開放網(wǎng)絡中借助密碼體制達到密鑰分配、身份認證、信息保密等特定目標的通信規(guī)范，其正確性對網(wǎng)絡應用的安全至關重要。安全協(xié)議的手工分析十分困難，容易出錯，因此，使用嚴謹?shù)男问交炞C方法和高效可靠的自動驗證工具來分析協(xié)議是當前安全協(xié)議研究的熱點。從協(xié)議驗證的目的劃分,安全協(xié)議的形式化驗證方法可分為證偽法和證真法：前者的目標在于尋找協(xié)議的漏洞和潛在攻擊的路徑；后者用于驗證協(xié)議是否能夠滿足某些安全性質(zhì)以及證明協(xié)議的正確性。
　　

2、 實例化空間邏輯(ISL)是一個在Dolev-Yao攻擊者模型下對安全協(xié)議進行形式化驗證的證真法。ISL以實例化空間為語義模型，擁有一組盡可能完備的一階邏輯公理集，能夠驗證工業(yè)級復雜協(xié)議的認證性、秘密性等相關安全性質(zhì)。但是，ISL的普適性還有待理論上的驗證.ISL的公理集在算法上是可實現(xiàn)的，其相應的自動化驗證工具為SPV(Security ProtocolVerifier).SPV能夠處理包含公鑰、私鑰、共享密鑰和hash密鑰嵌套加密的

3、復雜消息格式。該工具使用知識推理方法，調(diào)用SAT求解器，能夠高效驗證安全協(xié)議是否滿足CAPSL(Common Authentication Protocol Specification Language)協(xié)議規(guī)范及單層、多層認知規(guī)范。
　　 協(xié)議的驗證是個不可判問題，因此，無法直接對一個安全協(xié)議驗證邏輯公理系統(tǒng)進行嚴格的完備性證明，只能通過實驗或其它的方式對其普適性進行檢驗。為了對實例化空間邏輯ISL的語義表達能力給出理論上和實

4、踐上的衡量與評價，本文對ISL的語義及其應用進行了研究.目前，對安全協(xié)議形式化驗證邏輯語義方面的研究工作為數(shù)不多，因此該工作在一定程度上填補了這方面研究的空白.我們通過在實例化空間語義模型下解釋其它主流安全協(xié)議驗證邏輯的方法，說明了ISL具有較強的語義表達能力.ISL較強的語義表達能力使其具有實用性：在不同應用領域下，我們給出了一些重要工業(yè)級協(xié)議的合理簡化模型和轉(zhuǎn)換方法，利用SPV對這些協(xié)議進行完全自動化的證明，針對協(xié)議驗證結(jié)果的不足，

5、對協(xié)議進行了某些改進.我們還對原有的ISL理論進行擴展，使其能夠驗證更多類型的協(xié)議，這體現(xiàn)了ISL的語義可擴展性.原有的ISL語義與應用都是基于Dolev-Yao模型的，為使ISL適用于計算能力更強、更貼近協(xié)議實際運行的Computational攻擊者模型，我們還定義了ISL的計算語義，為ISL理論實現(xiàn)攻擊者模型的轉(zhuǎn)換打下了重要基礎。
　　 本文的主要工作如下：
　　 ⑴原有的ISL理論將Diffie-Hellman密鑰

6、抽象為共享密鑰，未討論DH密鑰本身的性質(zhì)，也未描述異或算子XOR的性質(zhì)。我們基于擴展的加密消息交換模型、擴展的安全協(xié)議形式化描述和擴展的實例化空間，對ISL的公理系統(tǒng)進行補充，增加了與DH密鑰假設相關的核心公理和與異或相關的主要公理.在不影響原有公式和公理的前提下，擴展的ISL具有更強的表達能力，足以驗證包含DH密鑰加密消息和帶異或算子的安全協(xié)議。
　　 ⑵為了從理論上衡量ISL的普適性，我們選擇另一種實用的基于證真的安全協(xié)議驗

7、證法組合協(xié)議邏輯PCL，對ISL和PCL之間的關系進行了分析。在此基礎上，將PCL的語義模型轉(zhuǎn)換為ISL的實例化空間語義模型，在實例化空間下對PCL的主要公式、定理、推導規(guī)則做了語義解釋。研究表明，實例化空間能夠完全表示PCL的語義，且ISL的語義表達能力強于PCL.新的模型解釋使PCL更易于擴展，且使得用PCL理論驗證的協(xié)議能夠利用SPV自動。
　　 ⑶電子商務領域中的安全電子交易(SET)協(xié)議是目前最復雜的工業(yè)級協(xié)議之一，其

8、原始文檔有上千頁，簡化過程相當困難，相關研究較少，已有的一些簡化模型也不夠完整。我們在花費大量時間研究SET協(xié)議原始文檔的基礎上，為該協(xié)議提出了合理的化簡規(guī)則，給出了比以往更貼近原協(xié)議的簡化模型，利用ISL的自動化驗證工具SPV實現(xiàn)了對SET協(xié)議秘密性、認證性等安全性質(zhì)的自動化驗證，并對協(xié)議進行了改進.該工作充分說明了ISL和SPV足以處理復雜的工業(yè)級協(xié)議。
　　 ⑷由于Web服務安全(WS-Security)協(xié)議與傳統(tǒng)網(wǎng)絡安全

9、協(xié)議的描述方式不同，因此無法直接使用原有的安全協(xié)議驗證技術對WS-Security協(xié)議進行形式化驗證。實際上，到目前為止，仍無完整、實用的理論和方法可以證明WS-Security協(xié)議的安全性質(zhì)是否能在協(xié)議的任意無窮會話中被滿足.我們提出了一個對WS-Security協(xié)議的認證性進行自動化驗證的方法：我們在一些自動化工具的支持下將WS-Security協(xié)議轉(zhuǎn)換為傳統(tǒng)協(xié)議消息格式，利用ISL理論將該協(xié)議的認證性描述為認知規(guī)范，最后使用SPV

10、實現(xiàn)了對WS-Security協(xié)議的認證性進行自動化驗證，并根據(jù)驗證結(jié)果討論了協(xié)議的安全性.該工作從一個新的角度研究了Web服務安全，也為WS-Security協(xié)議的設計與改進提供了幫助。
　　 ⑸ISL原先的語義是基于Dolev-Yao模型的，較為抽象和符號化。我們基于Computational模型，引入概率隨機性，為ISL構(gòu)建新的語義模型，定義新的計算語義。計算語義具有不同于符號化層面的一些新特性(例如Computation