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

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

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

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

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

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

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

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

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

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

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

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