基于串空間模型的安全協(xié)議形式化驗(yàn)證方法的研究.pdf

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

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

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

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

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

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

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