現(xiàn)代密碼協(xié)議的形式化方法研究.pdf

1、現(xiàn)代密碼協(xié)議作為網(wǎng)絡(luò)安全通信系統(tǒng)的核心技術(shù)，其重要性不言而喻。然而，如何分析密碼協(xié)議的安全性，從而證明密碼協(xié)議的有效性?如何設(shè)計密碼協(xié)議，從而確保所設(shè)計協(xié)議的安全性?這些則都是需由密碼協(xié)議形式化方法來解決的問題。密碼協(xié)議的形式化方法作為密碼協(xié)議分析和設(shè)計的理論基礎(chǔ)，自Dolev和Yao的開創(chuàng)性工作以來，目前已有了較大的發(fā)展，形成了兩大流派，其中典型的有StrandSpace模型理論和預(yù)言機模型理論等。然而，在如何應(yīng)用抽象的形式化理論或方

2、法來研究現(xiàn)行通信系統(tǒng)中大型、復(fù)雜并行系統(tǒng)的密碼協(xié)議，發(fā)現(xiàn)其安全缺陷或證明其安全性?在如何擴展現(xiàn)有形式化理論，使之能夠解決網(wǎng)絡(luò)中出現(xiàn)的新的威脅?以及在如何應(yīng)用形式化理論指導(dǎo)密碼協(xié)議的設(shè)計等幾個方面還有待進一步的研究。鑒于此，本文基于StrandSpace模型理論和預(yù)言機模型理論，針對上述三個方面的問題進行了深入的研究，并提出了一些有效的解決方案，得到了一些研究成果。論文的研究內(nèi)容主要包括以下三個方面： 首先，研究了如何應(yīng)用Stra

3、ndSpace模型理論和預(yù)言機模型理論分析現(xiàn)行復(fù)雜系統(tǒng)中的密碼協(xié)議，指出了這些密碼協(xié)議存在的安全缺陷，并基于形式化理論分析的結(jié)果提出了對這些協(xié)議的改進方案，最后基于形式化理論論證了這些改進方案的安全性。本文所研究的密碼協(xié)議具有普遍的理論意義和現(xiàn)實的應(yīng)用意義。其中對于CCITTX.509認證協(xié)議及簡單認證密鑰交換算法(Diffie-Hellman密鑰交換算法的一個變種)的研究具有普遍的理論意義。而對于基于SmartCard的密碼認證協(xié)議及

4、高效匿名拍賣協(xié)議的研究，則解決了網(wǎng)絡(luò)中最新的電子商務(wù)應(yīng)用問題，具有現(xiàn)實的應(yīng)用意義。 第一，本文基于StrandSpace模型，在協(xié)議的保密性和協(xié)議的認證性兩方面，對CCITTX.509認證協(xié)議進行了形式化分析，得出了BAN邏輯沒有得到的協(xié)議保密性缺陷和相同的協(xié)議認證正確性缺陷，并給出了相應(yīng)的攻擊方法。在此基礎(chǔ)上提出了一種改進的X.509認證協(xié)議，并采用StrandSpace模型形式化證明了該改進X.509協(xié)議的保密性和認證正確性

5、。 第二，基于StrandSpace模型及AuthenticationTest方法形式化分析了基于SmartCard的密碼認證協(xié)議，指出了該協(xié)議存在的安全缺陷，給出了相應(yīng)的協(xié)議攻擊手段。在此基礎(chǔ)上提出了對該協(xié)議的改進方案，并基于AuthenticationTest方法形式化分析了改進方案，證明了改進方案的認證正確性。 第三，基于AuthenticationTest方法形式化分析了高效匿名拍賣協(xié)議的初始化階段，指出了該協(xié)議

6、初始化階段存在的安全缺陷，并給出了對于協(xié)議初始化階段的攻擊手段，該攻擊將使得后續(xù)的拍賣協(xié)議失效。在此基礎(chǔ)上提出了一種改進的初始化協(xié)議以防止類似的攻擊，并且基于StrandSpace模型理論及AuthenticationTest方法形式化分析了改進的初始化拍賣協(xié)議，證明了該改進的初始化協(xié)議中竟拍者和拍賣人之間的安全認證特性，從而保證了整個高效匿名拍賣協(xié)議的安全有效性。 第四，簡單認證密鑰交換算法作為Diffie-Hellman密鑰

7、交換算法的一個變種，通過增加兩消息來防止中間人攻擊，從而保證通信雙方可靠地協(xié)商秘密會話密鑰。然而，該算法卻存在著一些安全缺陷。本文在分析該算法及相關(guān)改進算法的基礎(chǔ)上，提出了一種新型增強簡單認證密鑰交換算法以克服這些安全缺陷。同時在已有預(yù)言機模型的基礎(chǔ)上，給出了增強的語言機模型，并基于該增強的預(yù)言機模型，形式化分析了新型簡單認證密鑰交換算法，證明了該新型增強算法具備抗密碼猜測攻擊的能力，并具有完美的前向機密性。 其次，對于網(wǎng)絡(luò)中新

8、出現(xiàn)的協(xié)議攻擊——拒絕服務(wù)攻擊，目前為止還沒有一種有效的形式化分析方法可以用來分析安全通信協(xié)議中的該類攻擊。本文提出了一種新型形式化方法用以分析密碼協(xié)議的拒絕服務(wù)攻擊，以確定通信協(xié)議是否具有抵抗拒絕服務(wù)攻擊的能力。本文首先應(yīng)用賦權(quán)圖的概念擴展StrandSpace模型，接著引入fail-stop協(xié)議的概念，由此提出兩類DOStests(拒絕服務(wù)測試)方法，并基于兩類DOStests提出了密碼協(xié)議拒絕服務(wù)分析的新型形式化方法。最后，選取四

9、個具有普遍意義的示例協(xié)議，即TCP三次握手協(xié)議，Intemet密鑰交換協(xié)議(IKE)，高效抗DOS攻擊安全密鑰交換協(xié)議(JFK)和抗DOS攻擊IKE協(xié)議，應(yīng)用本文提出的新型形式化方法進行了協(xié)議分析，從而證明前兩個協(xié)議易受DOS攻擊，而后兩個協(xié)議具備抗DOS攻擊的能力。 最后，基于AuthenticationTest方法研究了密碼協(xié)議的形式化設(shè)計方法，設(shè)計出了高效安全Internet密鑰交換(ESIKE)協(xié)議。首先鑒于IKE協(xié)議中

10、存在的一些安全缺陷，確定了ESIKE協(xié)議的安全目標。然后根據(jù)協(xié)議所需實現(xiàn)的安全目標，基于AuthenticationTest方法一步一步地完成了整個協(xié)議的設(shè)計。最后基于StrandSpace模型理論和AuthenticationTest方法形式化證明了ESIKE達到了所需的安全設(shè)計目標。ESIKE協(xié)議克服了IKE協(xié)議中存在的安全缺陷，同時提供對于會話密鑰及安全關(guān)聯(lián)SA的安全協(xié)商，提供了對于通信端點的身份保護，并且實現(xiàn)了協(xié)議發(fā)起者和響應(yīng)者