随着计算机和Internet的不断普及,电子投票的应用也越来越广泛。同时,人们对电子投票的安全性要求也越来越高。一般来说,电子投票的安全性需求包括私密性,有效性,合法性,公平性以及广泛可验证性等。但是,目前已有的基于盲签名的电子投票方案都无法很好的满足这些安全需求。另外,对于电子投票方案中私密性,尤其是匿名性的分析,目前绝大多数还是采用非形式化的经验性分析或是形式化的手动分析方法,缺乏一个对电子投票方案匿名性进行建模和自动化分析的框架。针对以上问题,本文主要做了如下的工作:首先,我们对基于盲签名的电子投票方案进行研究,分析了近十几年来基于盲签名的电子投票方案的发展过程,提出了一种新的电子投票方案。与以往的方案相比,我们的方案在安全性上有了明显提高。它不仅能够成功地抵抗所有针对现有方案的攻击,还是第一个真正地实现了广泛可验证性的电子投票方案。其次,本文使用了GSPML语言对我们提出的电子投票方案进行了可视化建模,然后,基于Schneider等提出的强弱匿名性定义,我们新构建了一个使用通信顺序进程CSP分析电子投票方案匿名性的框架,并使用故障分歧提炼工具FDR2对我们的电子投票方案的匿名性编写程序进行了自动分析。结果表明,我们的电子投票方案是满足匿名性目标的。同时,我们构建的这个建模和分析的框架也可以稍作修改从而应用于同类型的其他电子投票方案匿名性的分析上。