1、安全協(xié)議是構(gòu)建網(wǎng)絡(luò)安全環(huán)境的基石,是網(wǎng)絡(luò)安全通信系統(tǒng)的核心技術(shù),它正確性對整個網(wǎng)絡(luò)環(huán)境的安全起著至關(guān)重要的作用.然而如何保證安全協(xié)議的全性,如何使協(xié)議的設(shè)計能夠滿足安全性的要求,如何提高安全協(xié)議自動化驗的效率等,都是安全協(xié)議研究領(lǐng)域不斷探索的問題.為了保證安全協(xié)議的安全研究人員提出了形式化的方法.雖然形式化方法已經(jīng)成功地發(fā)現(xiàn)了許多安全協(xié)議的漏洞和攻擊,但是這些方法仍然存在很多問題.一些形式化的方法本身并完善,因此無法適用于某些安全協(xié)議的

2、驗證；一些理論完善的形式化方法由于雜而缺乏自動化工具的支持；現(xiàn)有的自動化協(xié)議驗證工具資源占用量大, 要求高.鑒于此,本文以串空間模型理論和認證測試方法為基礎(chǔ),針對上上方面的問題進行了深入的研究,并且提出了有效的解決方案,取得了一定的科研成果.論文的研究內(nèi)容主要包括以下三個方面: 首先,對于串空間模型和認證測試方法理論在典型安全協(xié)議驗證中的應(yīng)用進行了深入的研究,通過形式化的驗證指出協(xié)議中存在的安全漏洞,構(gòu)造可能的攻擊方式,并以理論分析結(jié)果

3、為指導(dǎo)提出對這些協(xié)議的改進方案,最后使用理論方法驗證改進協(xié)議的安全性.本文還以認證測試方法為理論基礎(chǔ),對通用安全協(xié)議的設(shè)計方法進行了研究.以Needham-Schroeder協(xié)議為例,使用基于認證測試的通用安全協(xié)議設(shè)計方法指導(dǎo)該協(xié)議的重新設(shè)計,并對重新設(shè)計后的協(xié)議應(yīng)用形式化的理論方法證明其安全性. 其次,在對認證測試方法深入研究的基礎(chǔ)上,指出該方法在對稱密鑰協(xié)議驗證中存在無法確定消息項初始產(chǎn)生主體的問題,以及由此可能引起的消息重

4、放攻擊和類型攻擊.通過引入消息類型對認證測試方法進行了改進,提出了基于消息類型檢測的改進認證測試方法,并通過對認證協(xié)議的驗證表明了改進的認證測試方法能夠有效地發(fā)現(xiàn)原有認證測試方法沒有發(fā)現(xiàn)的類型攻擊.與此同時,還將改進的認證測試方法應(yīng)用于無線認證協(xié)議的驗證,證明了改進的認證測試方法對無線認證協(xié)議安全性驗證的有效性.然后,以改進的認證測試方法為基礎(chǔ),提出了安全協(xié)議的認證屬性中不僅要滿足一致性屬性,還要滿足測試分量的唯一性屬性.通過定義測試分

5、量唯一性,排除由于消息重放而引起攻擊的可能性.并提出了安全協(xié)議自動化驗證算法--AAAP (Automatic Analyzer of Authentication Protocols),AAAP算法在多種認證協(xié)議證明中的應(yīng)用說明了該算法能夠有效發(fā)現(xiàn)協(xié)議中存在的漏洞并及時終止算法的運行；而與類似算法相比,AAAP算法在協(xié)議驗證中具有遍歷狀態(tài)空間少、運行效率高的優(yōu)點. 最后,基于AAAP算法開發(fā)了安全協(xié)議自動化驗證原型系統(tǒng),并通過

6、對多個經(jīng)典認證協(xié)議的實驗驗證說明該原型系統(tǒng)的有效性. 本文創(chuàng)新性的工作主要有:1. 改進了認證測試方法,使之能夠為對稱密鑰協(xié)議提供更為完善的驗證.通過引入消息類型的概念,提出了基于消息類型檢測的改進認證測試方法,用于檢測協(xié)議中是否存在由消息重放而引起的攻擊,解決了原有認證測試方法無法發(fā)現(xiàn)重放攻擊的問題,在理論上具有創(chuàng)新性.2. 提出了測試分量唯一性屬性,完善了協(xié)議認證屬性的描述.通過對測試分量唯一性的證明,驗證協(xié)議抵抗重放攻擊和

7、類型攻擊的能力,在理論上具有創(chuàng)新性.3. 提出了基于改進認證測試方法的AAAP算法.通過對協(xié)議一致性屬性和唯一性屬性的自動化證明,驗證協(xié)議能夠達到的安全目標(biāo).AAAP算法對多種認證協(xié)議的驗證說明該算法能夠及時發(fā)現(xiàn)協(xié)議中存在的漏洞并終止協(xié)議運行,與同類型算法相比資源耗費小,在理論的應(yīng)用上具有創(chuàng)新的特點.4. 開發(fā)了基于AAAP算法的安全協(xié)議自動化驗證原型系統(tǒng),將理論模型應(yīng)用于實際的安全協(xié)議驗證.應(yīng)用該原型系統(tǒng)驗證了 Needham-Sch