文档介绍：中南民族大学
硕士学位论文
基于应用PI演算的远程网络投票协议安全性自动化证明
姓名:黄伟
申请学位级别:硕士
专业:计算机应用技术
指导教师:孟博
2011-05-03
中南民族大学硕士学位论文
摘要
投票是人们使用自己选举权力来表达自己对某一问题的观点的一
种方式。随着计算机技术和通信技术的不断发展,人们利用计算机在
任何地方通过网络投票系统进行投票成为现实。
网络投票协议是实施网络投票系统的基础。安全实用的远程网络
投票协议应该具有的安全属性有秘密性、完全性、正确性、不可重用
性、公平性、适任性、确定性、抗拒绝服务攻击性、普遍验证性、没
有收条、抗威胁性。
形式化方法是分析与验证安全协议的安全属性的强有力的工具。
按照分析方法,可以分为手工分析和自动分析。前者依赖于专家的经
验,不仅效率低、易出错、难推广,而且很难应用于对复杂的协议进
行分析,如网络投票协议。因此,安全协议的自动化分析与验证成为
了信息安全领域中的热点研究课题。
本文以远程网络投票协议作为研究对象,以基于定理证明的安全
协议形式化分析与验证技术为工具,对远程网络投票协议安全属性自
动化证明技术进行了深入研究。
本文的主要工作和贡献如下:
对基于定理证明的一阶定理证明器进行了深入研
究。首先对输入语言应用演算的项、进程以及进程间等
价关系与子句进行了深入研究,然后分析了的系统结
构、基础理论与其所能够证明的安全属性。
对远程网络投票协议的抗拒绝服务攻击性的自动化证明方法
进行了研究,提出一个基于定理证明的抗拒绝服务攻击性自动化证明
模型。首先从攻击者上下文与进程表达式两个方面对标准应用演算
进行扩展,然后从协议状态的角度,应用扩展后的应用演算对抗拒
绝服务攻击性进行建模,提出了一个基于定理证明的支持一阶定理证
明器的抗拒绝服务攻击性自动化证明模型,最后分析了
协议和四步握手协议的抗拒绝服务攻击性。
研究远程网络投票协议无收据性与抗威胁性的自动化证明方
法,重点研究了支持正确性、无收据性与抗威胁性自动化验证的
模型,然后应用模型,分析与验证协议和
协议的正确性、无收据性与抗威胁性。发现协议不满足正确性,
并对协议进行了改进,使其具有正确性。
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 munication, it e true that people vote through
voting system in anywhere puter.
voting protocol is the base of the voting system. A
secure practical remote 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 to a