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

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

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