基于串空間模型的安全協(xié)議分析與驗證方法的研究.pdf

1、安全協(xié)議是網(wǎng)絡安全的保障，網(wǎng)絡中實體間通信的實現(xiàn)都是經(jīng)過安全協(xié)議來協(xié)助完成的，然而由于網(wǎng)絡處在復雜的環(huán)境之中以及安全協(xié)議本身所具有的缺陷，使得攻擊者能夠借助這些缺陷來對協(xié)議進行各種各樣的攻擊，從而達到對網(wǎng)絡安全進行破壞的目的，所以，在網(wǎng)絡安全中對安全協(xié)議進行正確的分析發(fā)揮著極其重要的作用。
　　 形式化分析方法是分析安全協(xié)議一種最重要的方法，認證測試方法的提出和Athena自動化方法的提出是串空間模型發(fā)展過程中兩個最大的成就，本

2、文在對安全協(xié)議分析和驗證方法進行深入研究的基礎上，所做的主要工作和創(chuàng)新點主要體現(xiàn)在以下幾個方面：
　　 第一，在對協(xié)議分析方法進行充分理解的基礎上，深入研究和探討了串空間模型分析協(xié)議的特點，并能夠用此種形式化的分析方法對安全協(xié)議進行分析和驗證；
　　 第二，掌握了認證測試方法分析協(xié)議的特點，并針對該方法在分析協(xié)議時存在的缺陷，對原有的認證測試方法進行了改進，擴大了其分析范圍。并用改進后的方法對TLS協(xié)議進行了分析，分析結

3、果表明改進后的認證測試方法的可行性；
　　 第三，提出了一種新的安全協(xié)議自動化分析方法，給出了相應的模型設計，并提出了實現(xiàn)該模型所需的一系列算法，介紹了其分析協(xié)議的基本過程和特點；
　　 第四，通過實驗實現(xiàn)了本文所提出的模型的基本功能，并用所提出的模型對改進前后的Helsinki協(xié)議進行了分析驗證，實驗結果表明所提出的協(xié)議分析方法的正確性和高效性；
　　 安全協(xié)議的自動化分析方法是形式化分析領域里一個前沿的方向，