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

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

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

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

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

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

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

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

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

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

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