串空間模型的拓展和應(yīng)用.pdf

1、隨著Internet技術(shù)的發(fā)展，安全協(xié)議在電子商務(wù)和電子政務(wù)中的應(yīng)用越來越多。與此相應(yīng)的就是人們對協(xié)議的安全性更加關(guān)注，隨之涌現(xiàn)出各種安全協(xié)議的形式化分析方法。本文簡要介紹了串空間模型的符號系統(tǒng)及其基本概念和理論，分析了基于串空間模型的極小元、理想與誠實、認(rèn)證測試方法這三個分支的原理和應(yīng)用場合，并體現(xiàn)了串空間模型的特點及優(yōu)勢。 在此基礎(chǔ)上，本文以廣義的挑戰(zhàn)-應(yīng)答協(xié)議和網(wǎng)絡(luò)上廣泛使用的SSL/TLS握手協(xié)議為例，用串空間模型中的相

2、關(guān)符號和叢圖對協(xié)議進(jìn)行建模，并在此基礎(chǔ)上用認(rèn)證測試方法分別對廣義和實際協(xié)議進(jìn)行分析找到了協(xié)議的漏洞及具體攻擊路徑，在對相關(guān)協(xié)議改進(jìn)的同時還歸納出對稱和非對稱密碼體制下協(xié)議分析和設(shè)計的一套指導(dǎo)原則，利用這些原則去分析相應(yīng)的網(wǎng)絡(luò)協(xié)議，能夠得到較好的結(jié)果，這進(jìn)一步擴(kuò)充了串空間模型在協(xié)議分析領(lǐng)域中的應(yīng)用，并很大程度上地證明了串空間模型的理論及實踐價值。 另外，串空間模型的基本概念和理論及其在協(xié)議分析上的應(yīng)用尚存在一些局限和缺陷。本研究從

3、串空間模型對各類密碼操作和安全特性的表示出發(fā)，對其符號系統(tǒng)、基本假設(shè)、攻擊者能力、消息格式及串空間的各個分支（特別是認(rèn)證測試方法）等各方面進(jìn)行了一定程度上的改進(jìn)和拓展。據(jù)此本文還用Yahalom協(xié)議驗證了拓展的認(rèn)證測試方法在分析協(xié)議及其各種安全特性上的能力和優(yōu)勢，證明它能作為一種指導(dǎo)協(xié)議設(shè)計的有效工具。 此外，憑借串空間模型的符號和叢圖對認(rèn)證協(xié)議進(jìn)行建模，汲取邏輯推理和模型檢測等各類形式化分析方法的優(yōu)勢，本文定義了一套全新的協(xié)議

4、分析方法--基于消息匹配的認(rèn)證協(xié)議分析方法，并詳細(xì)解釋了該方法的原理和概念，闡述了具體的分析步驟。此方法通過在攻擊者扮演不同角色的情況下，用常量或變量在各個階段對協(xié)議的基本元素進(jìn)行描述，并在分析過程中給變量逐步賦值，同時讓協(xié)議主體通過匹配消息的格式來尋找協(xié)議的漏洞。本文以Needham-Schroeder protocol為例，介紹了如何在實際協(xié)議分析中運(yùn)用此方法找出協(xié)議的攻擊路徑及相應(yīng)的改進(jìn)方法，最后還結(jié)合串空間的其他分支進(jìn)一步簡化了