安全協(xié)議的Athena方法研究.pdf

1、Athena方法是安全協(xié)議分析領(lǐng)域中的一種新的形式化分析方法。本文首先對其進(jìn)行了深入分析,然后針對安全協(xié)議形式化分析領(lǐng)域中的兩個重要問題——類型缺陷攻擊問題、組合協(xié)議猜測攻擊問題及 Athena方法在分析這兩個問題中遇到的困難,對該方法進(jìn)行了擴(kuò)展。取得的主要成果如下:
　　(1)對Athena方法進(jìn)行了深入研究,分析了Athena方法對串空間模型所做的擴(kuò)展,對 Athena方法的邏輯和驗證算法進(jìn)行了深入分析,并通過實驗說明其分析協(xié)

2、議的有效性和高效性。
　　(2) Athena方法建立在強類型抽象假設(shè)的基礎(chǔ)上,但在協(xié)議的實際執(zhí)行過程中,這樣的假設(shè)并不現(xiàn)實。因此本文去除這一假設(shè),對原有的 Athena方法進(jìn)行了相應(yīng)的擴(kuò)展,引入了組合項,增加了攻擊者強制類型轉(zhuǎn)換的能力,同時擴(kuò)展了Athena方法中的內(nèi)在項、目標(biāo)及目標(biāo)綁定等概念,并對相關(guān)內(nèi)容進(jìn)行修改。用擴(kuò)展后的方法對NSL協(xié)議進(jìn)行分析,發(fā)現(xiàn)了一處在APV中無法發(fā)現(xiàn)的類型缺陷攻擊。
　　(3)針對組合協(xié)議猜測