基于串空間的安全協(xié)議Athena分析方法的研究.pdf

1、在眾多的安全協(xié)議分析方法中,基于串空間的形式化分析方法是當(dāng)前的研究熱點(diǎn)之一。串空間理論發(fā)展過程中有兩個(gè)重要事件:其一是Guttman提出的串空間模型認(rèn)證測試方法;其二是Song在串空間模型上提出的Athena方法。
　　本文對 Athena方法進(jìn)行了深入分析,針對目前安全協(xié)議分析領(lǐng)域中公開的“開端”問題以及 Athena方法自身的局限性,對該方法進(jìn)行了擴(kuò)展。取得的主要成果如下:
　　(1)對Athena方法進(jìn)行了系統(tǒng)的分析,

2、介紹了Athena的假設(shè)條件,給出了Athena的語法和語義,分析了該邏輯的優(yōu)點(diǎn)和局限性。在此基礎(chǔ)上,分析了 Athena的核心算法,討論了 Athena算法自動高效的原因,以及該算法如何避免狀態(tài)空間爆炸的技術(shù),指出了該算法的缺陷,形成原因以及解決的一般方法。最后,以Andrew協(xié)議為例,使用 Athena方法,對其進(jìn)行了分析和改進(jìn),消除其所存在的漏洞;以 NS協(xié)議為例,分別使用Athena方法與模型檢驗(yàn)工具SMV進(jìn)行了分析,并對分析結(jié)

3、果進(jìn)行了比較。
　　(2)Athena分析方法由于沒有抽象更多的密碼學(xué)原語,因此不能分析較復(fù)雜的安全協(xié)議。本文針對互聯(lián)網(wǎng)密鑰交換協(xié)議(IKEv2),對Athena方法進(jìn)行了擴(kuò)展。修改消息項(xiàng)結(jié)構(gòu),擴(kuò)展密碼學(xué)原語,使其能分析DH(Diffie-Hellman)密鑰協(xié)商問題;修改內(nèi)在項(xiàng)關(guān)系,使其能應(yīng)對更復(fù)雜的消息構(gòu)造情況;給出并證明了一個(gè)新的消減規(guī)則,并對相關(guān)命題和定理進(jìn)行了擴(kuò)展。
　　(3)開端協(xié)議(Open-Ended Pro