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

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

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

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