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

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

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

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

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