Verifying privacy-type properties of electronic voting protocols
Verifying privacy-type properties of electronic voting protocols
复制标题
DOI：
10.3233/jcs-2009-0340
复制
发表时间：
2009-01-01
影响因子：
1.2
通讯作者：
Ryan, Mark
中科院分区：
文献类型：
--
作者：
Delaune, Stephanie;Kremer, Steve;Ryan, Mark
电子投票为在选举中记录和统计选票提供了方便、高效和安全的设施。最近突出的已实施系统的不足之处表明了正式核查底层投票协议的重要性。我们研究了电子投票协议的三个隐私型属性：从强度的高低依次为投票隐私性、可接受性和抗强制性。我们使用应用pi演算，这是一种非常适合对此类协议建模的形式，它具有基于易于理解的概念的优点。隐私型属性使用观察等价表示，我们根据直觉表明，强制抵抗意味着收据自由，这意味着投票隐私。我们从文献中阐述了我们对三种电子投票协议的定义。理想情况下，即使选举官员腐败，这三个属性也应该保持不变。然而，在腐败官员在场的情况下，旨在满足无收据或抗强制要求的协议可能无法做到这一点。我们的模型和定义允许我们指定并轻松更改哪些权威应该是值得信赖的。
Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receiptfreeness and coercion-resistance.We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy.We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.