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

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

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

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

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