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

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

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

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