兩種安全協(xié)議形式化理論的研究.pdf

1、在本文中，我們探討了有關(guān)兩種安全協(xié)議形式化理論的若干問題，其中，工作重點集中在對三方認(rèn)證密鑰交換協(xié)議的形式化分析上。 網(wǎng)絡(luò)技術(shù)具有快速實現(xiàn)信息共享的特點，這大大提高了人們通信的效率，給人們的生活、學(xué)習(xí)和工作帶來了巨大的改觀。但與此同時，人們對網(wǎng)絡(luò)本身具有的公開性和匿名性所帶來的日益嚴(yán)重的信息安全問題也深感不安。 為了解決網(wǎng)絡(luò)的信息安全問題，人們設(shè)計了許多用于開放網(wǎng)絡(luò)的安全協(xié)議來解決各種安全應(yīng)用問題。所謂安全協(xié)議，就是兩個

2、或兩個以上的參與者采取一系列步驟來完成某項特定的安全任務(wù)。它包含三層含義：1.協(xié)議需要至少兩個參與者。2.參與者之間執(zhí)行的是消息處理和消息交換交替進行的一系列步驟。3.通過協(xié)議執(zhí)行必須能夠完成某種安全任務(wù)。 由于每個安全協(xié)議都是為了某種安全應(yīng)用而精心設(shè)計的，協(xié)議中的各條消息間有著微妙的相互制約關(guān)系，因此若采用人工方式對協(xié)議進行安全性分析，往往不能發(fā)現(xiàn)協(xié)議存在的問題，所以必須借助于形式化的方法來完成。形式化方法是一種用于描述系統(tǒng)性

3、質(zhì)的數(shù)學(xué)方法，它主要用于發(fā)現(xiàn)一個系統(tǒng)中的歧義性、不一致性與不完備性。該系統(tǒng)可以大到一個企業(yè)級的軟硬件系統(tǒng)，也可以小到有若干條消息組成的協(xié)議。對安全協(xié)議使用形式化的方法，可挖掘出協(xié)議消息所表示的內(nèi)在含義，對協(xié)議的正確性進行驗證。通過驗證，不僅可證明協(xié)議是否符合預(yù)期的安全目標(biāo)，而且對不符合安全目標(biāo)的協(xié)議可分析其缺陷之所在，進而為協(xié)議的設(shè)計提供有力的支持。 目前在安全協(xié)議形式化的研究領(lǐng)域有兩種截然不同的理論：符號理論與計算理論：

4、 在符號理論的形式化中，協(xié)議各要素被抽象為賦予了特定含義的符號，然后通過對這些符號的形式化分析來考察協(xié)議的安全性。雖然符號理論為協(xié)議的驗證工作提供了強大的證明手段，但是這些證明手段都是在一定的假設(shè)下進行的，比如均假設(shè)協(xié)議所采用的算法是理想化的，敵手在進行密碼分析時得不到任何有用的信息。由于這些假設(shè)不僅高估了一些常見算法的強度，同時低估了敵手的攻擊能力，因此符號理論不具有計算可靠性。 在計算理論中，協(xié)議各要素被看成位串，協(xié)議所采

5、用的算法由函數(shù)表示。其安全性的證明通常是通過構(gòu)造一個“矛盾歸約”的證明得到，這里的矛盾指的是計算復(fù)雜性領(lǐng)域中人們普遍相信的困難問題出現(xiàn)了一個有效解。計算理論通過分析敵手的攻擊能力來考察協(xié)議的安全性，更具有實際意義。但是計算理論下的分析方法難以考察協(xié)議各要素的完備性，因此不適于分析協(xié)議的邏輯正確性。 在本文中，我們主要以認(rèn)證密鑰交換協(xié)議為載體，深入考察了符號理論與計算理論各自的優(yōu)缺點，然后提出了若干有關(guān)安全協(xié)議形式化的新思路，主要

6、的工作有以下幾個方面： 第一，提出了CS邏輯及其改進方案的不足之處，對CS邏輯重新進行了擴展。CS邏輯在公理方面存在一些不足，比如違背了公鑰的公開性原則，知識與信念的轉(zhuǎn)化是通過非形式化的手段得到的等等，而已有改進方案中有關(guān)時間單調(diào)性與消息新鮮性的公理不能正確反映現(xiàn)實。我們通過對邏輯公理的改進與擴展實現(xiàn)了：1．更準(zhǔn)確地描述了有關(guān)知識和信念與時間有關(guān)的單調(diào)性概念。2．對發(fā)送和接收有關(guān)密文的知識和信念進行了描述，優(yōu)化了原有的推理過程。

7、3．改進后的推理公理描述了知識與信念之間的轉(zhuǎn)化關(guān)系，更客觀地反映了人類的認(rèn)知能力。4．可分析協(xié)議要素在一定時間段內(nèi)的安全需求，為深入了解協(xié)議消息的性質(zhì)以及設(shè)計更優(yōu)質(zhì)的安全協(xié)議提供了強有力的幫助。 第二，針對BAN類邏輯的不足，構(gòu)造了一個新的形式化分析工具-MBL邏輯。該邏輯的特點在于：1．克服了BAN類邏輯缺乏有效證明機制的不足，具有嚴(yán)格的證明體系，可證明在給出的語義模型下推理規(guī)則的正確性，說明了邏輯系統(tǒng)的合理性。2．對協(xié)議進行

8、簡單的處理便可進行安全性分析，不需進行理想化處理，降低了分析者分析協(xié)議的難度。3．可分析協(xié)議消息的保密性，使得主體不必過分依靠可信中心，主要根據(jù)自己的判斷來確定秘密是與哪個主體共享的，從而能彌補BAN類邏輯不能發(fā)現(xiàn)由于敵手欺騙可信中心所造成攻擊的不足。此外，我們基于MBL邏輯并采用Prolog語言實現(xiàn)了一個協(xié)議的自動化分析工具，可以大大提高分析協(xié)議安全性的效率。 第三，發(fā)現(xiàn)了敵手針對認(rèn)證密鑰交換協(xié)議的一種新型攻擊：敵手利用針對協(xié)

9、議的某種看似“無用”的攻擊過程，能夠完成另一種嚴(yán)重的攻擊，即敵手能夠延續(xù)對協(xié)議的攻擊效果從而實現(xiàn)另一種攻擊。由于目前所普遍使用的Dolev-Yao敵手模型無法具體涵蓋該類型的攻擊，所以我們對Dolev-Yao敵手模型進行了補充。 第四，分析了設(shè)計認(rèn)證密鑰交換協(xié)議所需注意的事項，指出設(shè)計安全的協(xié)議不僅要保證具備必要的協(xié)議要素，還要保證采用正確的密碼算法，由此引出了在計算方法下討論協(xié)議安全性的初衷。然后通過兩個攻擊游戲模型化了敵手攻

10、擊認(rèn)證協(xié)議的行為，進而通過主體在游戲中的成功概率給出了敵手在實施有關(guān)密碼分析的攻擊時認(rèn)證密鑰交換協(xié)議認(rèn)證性的定義。該定義充分考慮了敵手實施主動攻擊時協(xié)議的安全性，具有實際意義。 第五，結(jié)合符號理論中的模態(tài)邏輯法與計算理論下的矛盾歸約法，提出了一種安全協(xié)議的調(diào)和分析法。該方法與符號理論下的方法相比，克服了它們總假設(shè)密碼體制是完善的，并且僅考慮敵手的被動攻擊的不足，可有效地分析在面對敵手實施有關(guān)密碼分析的主動攻擊時協(xié)議的安全性；與計

11、算理論下的方法相比，該方法能考察協(xié)議各要素的完備性，能有效發(fā)現(xiàn)協(xié)議在面對重放攻擊、平行穿插攻擊等非密碼分析的攻擊時是否存在漏洞。最后我們給出了采用該方法分析協(xié)議的一個實例。 下一步的工作包括：建立一種設(shè)計安全協(xié)議的邏輯方法，然后利用prolog語言建立該邏輯方法的自動化方案，并實現(xiàn)由協(xié)議目標(biāo)來自動定位協(xié)議的缺陷；研究在各種攻擊模型下對稱鑰體制的安全性，以便提出更好的用于安全協(xié)議的對稱鑰加密方案，以及更全面地分析加密方案的安全性。