Sciweavers

Share
WOTE
2010

Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster

8 years 3 months ago
Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster
Abstract. While electronic elections promise the possibility of convenient, efficient and secure facilities for recording and tallying votes, recent studies have highlighted inadequacies in implemented systems. These inadequacies provide additional motivation for applying formal methods to the validation of electronic voting protocols. In this paper we report on some of our recent efforts in using the applied pi calculus to model and analyse properties of electronic elections. We particularly focus on anonymity properties, namely vote-privacy and receipt-freeness. These properties are expressed using observational equivalence and we show in accordance with intuition that receipt-freeness implies vote-privacy. We illustrate our definitions on two electronic voting protocols from the literature. Ideally, these properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy privacy or receipt-freeness may not do so in the presence of cor...
Stéphanie Delaune, Steve Kremer, Mark Ryan
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Where WOTE
Authors Stéphanie Delaune, Steve Kremer, Mark Ryan
Comments (0)
books