投票是人们使用自己选举权力来表达自己对某一问题的观点的一种方式。随着计算机技术和通信技术的不断发展,人们利用计算机在任何地方通过网络投票系统进行投票成为现实。网络投票协议是实施网络投票系统的基础。安全实用的远程网络投票协议应该具有的安全属性有秘密性、完全性、正确性、不可重用性、公平性、适任性、确定性、抗拒绝服务攻击性、普遍验证性、没有收条、抗威胁性。形式化方法是分析与验证安全协议的安全属性的强有力的工具。按照分析方法,可以分为手工分析和自动分析。前者依赖于专家的经验,不仅效率低、易出错、难推广,而且很难应用于对复杂的协议进行分析,如网络投票协议。因此,安全协议的自动化分析与验证成为了信息安全领域中的热点研究课题。本文以远程网络投票协议作为研究对象,以基于定理证明的安全协议形式化分析与验证技术为工具,对远程网络投票协议安全属性自动化证明技术进行了深入研究。本文的主要工作和贡献如下:1.对基于定理证明的一阶定理证明器ProVerif进行了深入研究。首先对ProVerif输入语言应用PI演算的项、进程以及进程间等价关系与Horn子句进行了深入研究,然后分析了ProVerif的系统结构、基础理论与其所能够证明的安全属性。2.对远程网络投票协议的抗拒绝服务攻击性的自动化证明方法进行了研究,提出一个基于定理证明的抗拒绝服务攻击性自动化证明模型。首先从攻击者上下文与进程表达式两个方面对标准应用PI演算进行扩展,然后从协议状态的角度,应用扩展后的应用PI演算对抗拒绝服务攻击性进行建模,提出了一个基于定理证明的支持一阶定理证明器ProVerif的抗拒绝服务攻击性自动化证明模型,最后分析了Acquisti协议和802.11四步握手协议的抗拒绝服务攻击性。3.研究远程网络投票协议无收据性与抗威胁性的自动化证明方法,重点研究了支持正确性、无收据性与抗威胁性自动化验证的Backes模型,然后应用Backes模型,分析与验证Acquisti协议和Meng协议的正确性、无收据性与抗威胁性。发现Meng协议不满足正确性,并对Meng协议进行了改进,使其具有正确性。