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

1、計算機(jī)網(wǎng)絡(luò)的高速發(fā)展和網(wǎng)絡(luò)新應(yīng)用的不斷涌現(xiàn)給網(wǎng)絡(luò)安全帶來了很大的沖擊，網(wǎng)絡(luò)安全成為新的信息安全的熱點；安全協(xié)議作為計算機(jī)網(wǎng)絡(luò)安全體系的重要組成部分，也就變得越來越重要。然而，由于安全協(xié)議的復(fù)雜性，設(shè)計一個完美的安全協(xié)議是十分困難的，許多公開發(fā)表的安全協(xié)議中后來被發(fā)現(xiàn)它們存在各種各樣的安全漏洞。因此，以確保安全協(xié)議正確性為目的的安全協(xié)議分析成為一項重要的研究課題。安全協(xié)議分析可分為形式化分析和非形式化分析，其中，形式化分析方法是安全協(xié)議理

2、論研究的熱點之一。常見的形式化分析方法有BAN邏輯，Kailar邏輯，SPI演算，CSP方法，串空間模型等。
　　串空間模型理論是安全協(xié)議分析領(lǐng)域最新的研究成果，它是在1998年由Thayer，Herzog和Guttman提出的，具有高效、直觀、實用等特點，不僅可以用于證明安全協(xié)議的正確性，還可以用于構(gòu)造攻擊，揭示安全協(xié)議的內(nèi)在缺陷。該方法已經(jīng)成功地分析了Needham-Schroeder-Lowe協(xié)議，Otway-Rees協(xié)議，

3、Yahalom協(xié)議等諸多協(xié)議，被公認(rèn)為是一種先進(jìn)的高效的協(xié)議分析方法。
　　本文以串空間理論作為研究基礎(chǔ)，主要進(jìn)行了以下研究：
　　(1)深入研究串空間模型的基礎(chǔ)理論，應(yīng)用串空間模型分析了Natalia Miloslavskaya等人提出的一個雙向認(rèn)證協(xié)議，發(fā)現(xiàn)該協(xié)議在認(rèn)證方面存在缺陷，并對該協(xié)議進(jìn)行了改進(jìn)。
　　(2)對運用串空間理論分析不可否認(rèn)協(xié)議進(jìn)行研究，發(fā)現(xiàn)了以往運用串空間理論分析協(xié)議公平性的兩個問題，并給出了

4、解決方法。隨后對不可否認(rèn)協(xié)議中彈性信道、同步消息等特定假設(shè)條件，采用串空間理論的方式進(jìn)行形式化描述及推理，從而為串空間理論分析不可否認(rèn)協(xié)議掃除了障礙。然后以一個實例來說明如何運用串空間理論證明不可否認(rèn)協(xié)議的公平性，其中，關(guān)鍵之處是如何構(gòu)造正確的命題。
　　(3)分析TEENP不可否認(rèn)協(xié)議，發(fā)現(xiàn)它的安全缺陷，在此基礎(chǔ)上提出了一個新的不可否認(rèn)協(xié)議。同時，對另外兩個不可否認(rèn)協(xié)議進(jìn)行分析，發(fā)現(xiàn)以往文獻(xiàn)中未提及的新的漏洞。
　　(4)