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

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

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

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