Challenging an E-Voting System in Court - An Experience Report
Abstract: The Swiss political system is decentralized, and this includes voting operations. Several cantons have implemented Internet-based e-voting systems. The system used until recently in Geneva was a simple Internet voting system which assumed that the voter’s personal computer had not been compromised. This was considered risky already at the time and various counter-measures were considered. The one that was implemented in practice was to limit the proportion of voters that could vote via Internet. At present, there is consensus amongst experts that such systems are unsafe and should be improved, in particular by implementing verification. In order to stimulate improvements in the system, the author challenged the use of the Geneva system in court, arguing that it was not compliant with constitutional principles and cantonal law on voting rights. At the end of a long and complex legal process, the Swiss Federal Tribunal (supreme court) ruled that the complaints could not be heard on their merits, because they did not allege that weaknesses had actually been exploited in a specific vote. This decision differs from those taken in other jurisdictions and highlights the difficulties of bringing scientific arguments into the court system.
Sven Heiberg, Arnis Parsovs, Jan Willemson
Log Analysis of Estonian Internet Voting 2013-2014
Abstract: This paper presents analysis of Internet voting system logs of 2013 local municipal and 2014 European Parliament elections in Estonia. We study both sociodemographic characteristics of voters and technical aspects of voting. Special attention is paid to voting and verification sessions that can be considered irregular (e.g. inability to cast a valid vote or failed verifications). We observe several interesting phenomena, e.g. that older people are generally faster Internet voters and that women use the vote verification option significantly less than men.
Juan Ignacio Toledo, Jordi Cucurull, Jordi Puiggali, Alicia Fornes, Josep Llados
Document Analysis Techniques for Automatic Electoral Document Processing: A Survey
Abstract: In this paper, we will discuss the most common challenges in electoral document processing and study the different solutions from the document analysis community that can be applied in each case. We will cover Optical Mark Recognition techniques to detect voter selections in the Australian Ballot, handwritten number recognition for preferential elections and handwriting recognition for write-in areas. We will also propose some particular adjustments that can be made to those general techniques in the specific context of electoral documents.
Oksana Kulyk, Vanessa Teague, Melanie Volkamer
Extending Helios Towards Private Eligibility Verifiability
Abstract: We show how to extend the Helios voting system to provide eligibility verifiability without revealing who voted which we call private eligibility verifiability. The main idea is that real votes are hidden in a crowd of null votes that are cast by others but are indistinguishable from those of the eligible voter. This extended Helios scheme also improves Helios towards receipt-freeness.
Yvo Desmedt, Stelios Erotokritou
Making Code Voting Secure against Insider Threats using Unconditionally Secure MIX Schemes and Human PSMT Protocols
Abstract: It is clear to the public that when it comes to privacy, computers and “secure” communication over the Internet cannot fully be trusted. Chaum introduced code voting as a solution for using a possibly infected-by-malware device to cast a vote in an electronic voting application. He trusted the mail system. However, a conspiracy between the mail system and the recipient of the cast ballots breaks privacy. Considering a t-bounded passive adversary, we remove the trust in the mail. We propose both single and multi-seat elections, using PSMT protocols (SCN 2012) where with the help of visual aids, humans can carry out mod10 addition correctly with a 99% degree of accuracy. We introduce an unconditionally secure MIX based on the combinatorics of set systems.
David Galindo, Sandra Guasch and Jordi Puiggali
2015 Neuchatel’s Cast-as-Intended Verification Mechanism
Abstract: Cast-as-intended verification seeks to prove to a voter that their vote was cast according to their intent. In case ballot casting is made remotely through a voting client, one of the most important dangers a designer faces are malicious voting clients (e.g. infected by a malware), which may change the voter’s selections. A previous approach for achieving cast-as-intended verification in this setting uses the so-called Return Codes. These allow a voter to check whether their voting options were correctly received by the ballot server, while keeping these choices private. An essential ingredient of this approach is a mechanism that allows a voter to discard a vote that does not represent their intent. This is usually solved using multiple voting, namely, if the return codes received by the voter do not match their choices, they cast a new vote. However, what happens if voters are not allowed to cast more than one ballot (aka single vote casting)? In this paper we propose a simple ballot casting protocol, using return codes, for allowing a voter to verify votes in a single vote casting election. We do so without significantly impacting the number of operations in the client side. This voting protocol has been implemented in a binding election in the Swiss canton of Neuchâtel in March 2015, and will be the canton’s new voting platform.
Pedro Bibiloni, Alex Escala, and Paz Morillo
Vote Validatability in Mix-Net-Based eVoting
Abstract: One way to build secure electronic voting systems is to use Mix-Nets, which break any correlation between voters and their votes. One of the characteristics of Mix-Net-based eVoting is that ballots are usually decrypted individually and, as a consequence, invalid votes can be detected during the tallying of the election. In particular, this means that the ballot does not need to contain a proof of the vote being valid. However, allowing for invalid votes to be detected only during the tallying of the election can have bad consequences on the reputation of the election. First, casting a ballot for an invalid vote might be considered as an attack against the eVoting system by non-technical people, who might expect that the system does not accept such ballots. Besides, it would be impossible to track the attacker due to the anonymity provided by the Mix-Net. Second, if a ballot for an invalid vote is produced by a software bug, it might be only detected after the election period has finished. In particular, voters would not be able to cast a valid vote again. In this work we formalize the concept of having a system that detects invalid votes during the election period. In addition, we give a general construction of an eVoting system satisfying such property and an efficient concrete instantiation based on well-studied assumptions.
Philipp Locher, Rolf Haenni
Verifiable Internet Elections with Everlasting Privacy and Minimal Trust
Abstract: This paper presents a new cryptographic Internet voting protocol based on a set membership proof and a proof of knowledge of the representation of a committed value. When casting a vote, the voter provides a zero-knowledge proof of knowledge of the representation of one of the registered voter credentials. In this way, votes are anonymized without the need of trusted authorities. The absence of such authorities reduces the trust assumptions to a minimum and makes our protocol remarkably simple. Since computational intractability assumptions are only necessary to prevent the creation of invalid votes during the voting period, but not to protect the secrecy of the vote, the protocol even offers a solution to the everlasting privacy problem.
Jeremy Dawson, Rajeev Gore and Thomas Meumann
Formal Reasoning About Complex Voting Schemes Using Higher-order Logic
Abstract: We describe how we first formally encoded the English-language Parliamentary Act for the Hare-Clark Single Transferable Vote-counting scheme used in the Australian state of Tasmania into higher-order logic, producing SPECHOL. Based on this logical specification, we then encoded an SML program to count ballots according to this specification inside the interactive theorem prover HOL4, giving us IMPHOL. We then manually transliterated the program as a real SML program IMP. We are currently verifying that the formalisation of the implementation implies the formalisation of the specification: that is, we are using the HOL4 interactive theorem prover to prove the implication IMPHOL → SPECHOL.
J. Alex Halderman and Vanessa Teague
The New South Wales iVote System: Security Failures and Verification Flaws in a Live Online Election
Abstract: In the world’s largest-ever deployment of online voting, the iVote Internet voting system was trusted for the return of 280,000 ballots in the 2015 state election in New South Wales, Australia. During the election, we performed an independent security analysis of parts of the live iVote system and uncovered severe vulnerabilities that could be leveraged to manipulate votes, violate ballot privacy, and subvert the verification mechanism. These vulnerabilities do not seem to have been detected by the election authorities before we disclosed them, despite a pre-election security review and despite the system having run in a live state election for five days. One vulnerability, the result of including analytics software from an insecure external server, exposed some votes to complete compromise of privacy and integrity. At least one parliamentary seat was decided by a margin much smaller than the number of votes taken while the system was vulnerable. We also found protocol flaws, including vote verification that was itself susceptible to manipulation. This incident underscores the difficulty of conducting secure elections online and carries lessons for voters, election officials, and the e-voting research community.