基于應(yīng)用PI演算的遠(yuǎn)程網(wǎng)絡(luò)投票協(xié)議安全性自動(dòng)化證明.pdf

1、投票是人們使用自己選舉權(quán)力來表達(dá)自己對(duì)某一問題的觀點(diǎn)的一種方式。隨著計(jì)算機(jī)技術(shù)和通信技術(shù)的不斷發(fā)展，人們利用計(jì)算機(jī)在任何地方通過網(wǎng)絡(luò)投票系統(tǒng)進(jìn)行投票成為現(xiàn)實(shí)。
　　 網(wǎng)絡(luò)投票協(xié)議是實(shí)施網(wǎng)絡(luò)投票系統(tǒng)的基礎(chǔ)。安全實(shí)用的遠(yuǎn)程網(wǎng)絡(luò)投票協(xié)議應(yīng)該具有的安全屬性有秘密性、完全性、正確性、不可重用性、公平性、適任性、確定性、抗拒絕服務(wù)攻擊性、普遍驗(yàn)證性、沒有收條、抗威脅性。形式化方法是分析與驗(yàn)證安全協(xié)議的安全屬性的強(qiáng)有力的工具。按照分析方法，可

2、以分為手工分析和自動(dòng)分析。前者依賴于專家的經(jīng)驗(yàn)，不僅效率低、易出錯(cuò)、難推廣，而且很難應(yīng)用于對(duì)復(fù)雜的協(xié)議進(jìn)行分析，如網(wǎng)絡(luò)投票協(xié)議。因此，安全協(xié)議的自動(dòng)化分析與驗(yàn)證成為了信息安全領(lǐng)域中的熱點(diǎn)研究課題。
　　 本文以遠(yuǎn)程網(wǎng)絡(luò)投票協(xié)議作為研究對(duì)象，以基于定理證明的安全協(xié)議形式化分析與驗(yàn)證技術(shù)為工具，對(duì)遠(yuǎn)程網(wǎng)絡(luò)投票協(xié)議安全屬性自動(dòng)化證明技術(shù)進(jìn)行了深入研究。
　　 本文的主要工作和貢獻(xiàn)如下：
　　 1.對(duì)基于定理證明的一階定

3、理證明器ProVerif 進(jìn)行了深入研究。首先對(duì)ProVerif 輸入語言應(yīng)用PI 演算的項(xiàng)、進(jìn)程以及進(jìn)程間等價(jià)關(guān)系與Horn 子句進(jìn)行了深入研究，然后分析了ProVerif的系統(tǒng)結(jié)構(gòu)、基礎(chǔ)理論與其所能夠證明的安全屬性。
　　 2.對(duì)遠(yuǎn)程網(wǎng)絡(luò)投票協(xié)議的抗拒絕服務(wù)攻擊性的自動(dòng)化證明方法進(jìn)行了研究，提出一個(gè)基于定理證明的抗拒絕服務(wù)攻擊性自動(dòng)化證明模型。首先從攻擊者上下文與進(jìn)程表達(dá)式兩個(gè)方面對(duì)標(biāo)準(zhǔn)應(yīng)用PI 演算進(jìn)行擴(kuò)展，然后從協(xié)議狀態(tài)

4、的角度，應(yīng)用擴(kuò)展后的應(yīng)用PI 演算對(duì)抗拒絕服務(wù)攻擊性進(jìn)行建模，提出了一個(gè)基于定理證明的支持一階定理證明器ProVerif的抗拒絕服務(wù)攻擊性自動(dòng)化證明模型，最后分析了Acquisti協(xié)議和802.11四步握手協(xié)議的抗拒絕服務(wù)攻擊性。
　　 3.研究遠(yuǎn)程網(wǎng)絡(luò)投票協(xié)議無收據(jù)性與抗威脅性的自動(dòng)化證明方法，重點(diǎn)研究了支持正確性、無收據(jù)性與抗威脅性自動(dòng)化驗(yàn)證的Backes 模型，然后應(yīng)用Backes 模型，分析與驗(yàn)證Acquisti協(xié)議和M