基于应用PI演算的远程网络投票协议安全性自动化证明论文.docVIP

中南民族大学硕士学位论文 摘 要 投票是人们使用自己选举权力来表达自己对某一问题的观点的一 种方式。随着计算机技术和通信技术的不断发展，人们利用计算机在 任何地方通过网络投票系统进行投票成为现实。　 网络投票协议是实施网络投票系统的基础。安全实用的远程网络 投票协议应该具有的安全属性有秘密性、完全性、正确性、不可重用 性、公平性、适任性、确定性、抗拒绝服务攻击性、普遍验证性、没 有收条、抗威胁性。　 形式化方法是分析与验证安全协议的安全属性的强有力的工具。 按照分析方法，可以分为手工分析和自动分析。前者依赖于专家的经 验，不仅效率低、易出错、难推广，而且很难应用于对复杂的协议进 行分析，如网络投票协议。因此，安全协议的自动化分析与验证成为 了信息安全领域中的热点研究课题。　 本文以远程网络投票协议作为研究对象，以基于定理证明的安全 协议形式化分析与验证技术为工具，对远程网络投票协议安全属性自 动化证明技术进行了深入研究。　 本文的主要工作和贡献如下：　 １．　对基于定理证明的一阶定理证明器 ＰｒｏＶｅｒｉｆ 进行了深入研 究。首先对 ＰｒｏＶｅｒｉｆ 输入语言应用 ＰＩ 演算的项、进程以及进程间等 价关系与 Ｈｏｒｎ 子句进行了深入研究，然后分析了 ＰｒｏＶｅｒｉｆ 的系统结 构、基础理论与其所能够证明的安全属性。　 ２．　对远程网络投票协议的抗拒绝服务攻击性的自动化证明方法 进行了研究，提出一个基于定理证明的抗拒绝服务攻击性自动化证明 模型。首先从攻击者上下文与进程表达式两个方面对标准应用 ＰＩ 演算 进行扩展，然后从协议状态的角度，应用扩展后的应用 ＰＩ 演算对抗拒 绝服务攻击性进行建模，提出了一个基于定理证明的支持一阶定理证 明器 ＰｒｏＶｅｒｉｆ 的抗拒绝服务攻击性自动化证明模型，最后分析了 Ａｃｑｕｉｓｔｉ 协议和 ８０２．１１ 四步握手协议的抗拒绝服务攻击性。　 ３．　研究远程网络投票协议无收据性与抗威胁性的自动化证明方 法，重点研究了支持正确性、无收据性与抗威胁性自动化验证的　 Ｂａｃｋｅｓ 模型，然后应用Ｂａｃｋｅｓ模型，分析与验证Ａｃｑｕｉｓｔｉ 协议和Ｍｅｎｇ 协议的正确性、无收据性与抗威胁性。发现 Ｍｅｎｇ 协议不满足正确性， 并对 Ｍｅｎｇ 协议进行了改进，使其具有正确性。　 I 基于应用 PI 演算的远程网络投票协议安全性自动化证明 关键词：自动化证明，形式化，应用 PI 演算，ProVerif，抗拒绝服务 攻击性，抗威胁性　　 II 中南民族大学硕士学位论文 Abstract Voting is a way that people express their opinions on something using their right of election. With the development of the technology of computer and communication, it is come true that people vote through Internet voting system in anywhere with computer. Internet voting protocol is the base of the Internet voting system. A secure practical remote Internet voting protocol should include security properties: privacy, completeness, soundness, unreusability, fairness, eligibility, invariableness, DoS-resistance, universal verifiability, receipt-freeness and coercion-resistance. Formal method is a powerful tool of analysis and verification of security properties of security protocols. According to the analysis method, there are two ways: the manual analysis and the automatic analysis. The former relies on expert’s experience, not only low efficiency, easy to make a mistake, hard to promote, but also very difficult