安全協(xié)議的形式化分析方法及驗(yàn)證技術(shù)研究.pdf

1、計(jì)算機(jī)網(wǎng)絡(luò)安全問(wèn)題日益引起人們的重視。安全協(xié)議是用來(lái)保證網(wǎng)絡(luò)通信安全的重要工具。但研究證明安全協(xié)議大多數(shù)都有安全漏洞。作為信息安全的一項(xiàng)重要研究?jī)?nèi)容，安全協(xié)議的分析具有極為重要的理論意義和實(shí)際價(jià)值。論文以形式化分析方法為核心，對(duì)BAN邏輯與串空間理論以及模型自動(dòng)校驗(yàn)工具SPIN進(jìn)行了深入研究，并在此基礎(chǔ)上提出了一種邏輯性更加嚴(yán)密，實(shí)用性更強(qiáng)的形式化分析方法。
　　 本文了BAN邏輯與串空間理論的基本概念、主要推理規(guī)則以及分析方法

2、，并用兩種方法分別對(duì)Helsinki協(xié)議進(jìn)行了分析，驗(yàn)證了Helsinki協(xié)議存在的安全漏洞。并藉此對(duì)BAN邏輯與串空間理論進(jìn)行了對(duì)比分析，對(duì)二者的不足進(jìn)行了歸納總結(jié)。理論方法對(duì)于安全協(xié)議的分析固然有效，但模型自動(dòng)校驗(yàn)工具能夠模擬協(xié)議執(zhí)行的實(shí)際環(huán)境，從而使得對(duì)協(xié)議安全性的分析變得相當(dāng)直觀。對(duì)Promela語(yǔ)言的關(guān)鍵技術(shù)作了全面論述，介紹了利用SPIN構(gòu)造及驗(yàn)證Promela語(yǔ)言描述的系統(tǒng)模型的基本步驟，并以Helsinki協(xié)議作為分析實(shí)