基于形式化方法的安全協(xié)議自動化驗證算法的研究.pdf

1、作為網(wǎng)絡(luò)通信的安全保障,安全協(xié)議是整個信息系統(tǒng)架構(gòu)的安全基礎(chǔ)。為了保證安全協(xié)議的正確性,研究人員提出了一系列基于形式化方法的自動化驗證算法來對安全協(xié)議進行分析驗證,并已經(jīng)成功地發(fā)現(xiàn)很多安全協(xié)議中存在的漏洞和攻擊,但這些算法只能指出協(xié)議中的漏洞和攻擊,不能自動生成改進協(xié)議,而且這些算法還存在驗證效率低、使用難度大的問題。鑒于此,本文以串空間模型和認證測試方法為理論基礎(chǔ),對以上問題進行深入研究,研究內(nèi)容主要包括以下幾個方面：
　　

2、首先,在深入研究形式化方法的基礎(chǔ)上,詳細分析了幾種應(yīng)用較為廣泛的自動化驗證算法,并針對現(xiàn)有算法的不足,提出了IVAP算法(Intelligent Validator for Authentication Protocols)。IVAP算法不僅能自動地完成協(xié)議的驗證,而且還能根據(jù)不安全屬性逆向搜索主體串樹,自動生成改進協(xié)議并繼續(xù)完成改進協(xié)議的驗證。
　　 然后,詳細設(shè)計并開發(fā)了基于IVAP算法的安全協(xié)議自動化驗證原型系統(tǒng),原型系統(tǒng)

3、采用B/S架構(gòu),由安全協(xié)議圖形轉(zhuǎn)換接口模塊、安全協(xié)議形式化描述接口模塊、安全協(xié)議驗證模塊和改進協(xié)議生成模塊四個功能模塊組成。
　　 最后,用原型系統(tǒng)對一系列經(jīng)典認證協(xié)議進行了實驗驗證,分析了在協(xié)議驗證過程中所需的時間復(fù)雜度和空間復(fù)雜度,并把實驗數(shù)據(jù)與其它同類算法作了詳盡的比較分析。通過實驗結(jié)果表明了IVAP算法的有效性和高效性。
　　 本文的創(chuàng)新工作有以下兩點：
　　 1.提出了基于串空間的IVAP算法,在協(xié)議驗