串空間模型的拓展和應用.pdf

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

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

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

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