安全協(xié)議代數(shù)證明方法研究.pdf

1、安全協(xié)議是網(wǎng)絡(luò)通信和安全應(yīng)用的基礎(chǔ)，是安全基礎(chǔ)設(shè)施的重要組成部分。安全協(xié)議的設(shè)計(jì)和分析是協(xié)議工程領(lǐng)域主要的研究內(nèi)容，在設(shè)計(jì)、建模、驗(yàn)證、性能分析、實(shí)現(xiàn)、測試和維護(hù)等協(xié)議工程的各個(gè)環(huán)節(jié)中，協(xié)議驗(yàn)證是最為關(guān)鍵的一個(gè)環(huán)節(jié)。 自20世紀(jì)70年代以來，人們提出多種協(xié)議分析、驗(yàn)證的形式化方法，它們可以大致劃分為四種：基于BAN類邏輯的模態(tài)邏輯方法，基于有限狀態(tài)機(jī)理論的模型檢驗(yàn)方法，基于安全代數(shù)模型的定理證明方法和程序分析技術(shù)。在這些方法中，

2、定理證明方法能夠給出協(xié)議的安全性證明，因此也是密碼協(xié)議分析的主要研究內(nèi)容。 由于密碼協(xié)議本身安全目標(biāo)定義的微妙性，運(yùn)行環(huán)境的復(fù)雜性，攻擊者能力的不確定性和協(xié)議執(zhí)行的高并發(fā)性，使得安全協(xié)議的驗(yàn)證存在一系列困難，因此協(xié)議分析也采用了一些特殊的技術(shù)，如：狀態(tài)檢測、不變集技術(shù)、等價(jià)驗(yàn)證技術(shù)等。 本文對(duì)基于定理證明的安全協(xié)議形式化驗(yàn)證方法進(jìn)行了詳細(xì)的分析，其中主要研究了基于π演算密碼協(xié)議分析方法，包括spi演算，應(yīng)用pi演算和協(xié)議

3、驗(yàn)證的框架互模擬方法，其中主要的工作和貢獻(xiàn)如下： (1)對(duì)spi演算進(jìn)行詳細(xì)的分析，包括其協(xié)議驗(yàn)證思想，系統(tǒng)框架、操作語意以及進(jìn)程等價(jià)證明方法，并使用spi演算對(duì)Otway-Rees變體協(xié)議的安全性進(jìn)行分析，證明其不能滿足安全性。 (2)spi演算通過對(duì)π演算中的項(xiàng)和進(jìn)程進(jìn)行擴(kuò)展，使其能夠表示基本的密碼操作進(jìn)而對(duì)協(xié)議建模，但是spi忽略了密碼操作的安全意義，限制了它在協(xié)議分析中的應(yīng)用。本文通過引入消息起源的標(biāo)準(zhǔn)測試證明了

4、ZG非可否認(rèn)協(xié)議的非可否認(rèn)性和公平性，擴(kuò)展了spi演算在協(xié)議分析中的應(yīng)用范圍。 (3)框架互模擬是證明協(xié)議滿足觀察等價(jià)的有效手段，其中用框架、理論偶表示協(xié)議運(yùn)行環(huán)境的信息，通過證明規(guī)范進(jìn)程與協(xié)議進(jìn)程的框架互模擬關(guān)系驗(yàn)證協(xié)議的安全性。本文對(duì)其語法，操作語意，驗(yàn)證方法以及主要結(jié)論進(jìn)行了簡要的總結(jié)。 (4)應(yīng)用pi演算是Abadi等將π演算對(duì)協(xié)議進(jìn)行特化而建立的協(xié)議驗(yàn)證方法：其中使用函數(shù)應(yīng)用建模密碼操作，大大增強(qiáng)了對(duì)攻擊者能力