安全協議的Athena方法研究.pdf

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

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