Individual Verifiability for E-Voting, From Formal Verification To Machine Learning

The cornerstone of secure electronic voting protocols lies in the principle of individual verifiability. This thesis delves into the intricate task of harmonizing this principle with two other crucial aspects: ballot privacy and coercion-resistance. In the realm of electronic voting, individual verifiability serves as a critical safeguard. It empowers each voter with the ability to confirm that their vote has been accurately recorded and counted in the final tally. This thesis explores the intricate balance between this pivotal aspect of electronic voting and the equally important facets of ballot privacy and coercion-resistance. Ballot privacy, or the assurance that a voter's choice remains confidential, is a fundamental right in democratic processes. It ensures that voters can express their political preferences without fear of retribution or discrimination. On the other hand, coercion-resistance refers to the system's resilience against attempts to influence or manipulate a voter's choice. Furthermore, this thesis also ventures into an empirical analysis of the effectiveness of individual voter checks in ensuring a correct election outcome. It considers a scenario where an adversary possesses additional knowledge about the individual voters and can strategically decide which voters to target. The study aims to estimate the degree to which these checks can still guarantee the accuracy of the election results under such circumstances. In essence, this thesis embarks on a comprehensive exploration of the dynamics between individual verifiability, ballot privacy, and coercion-resistance in secure electronic voting protocols. It also seeks to quantify the effectiveness of individual voter checks in maintaining the integrity of election outcomes, particularly when faced with a knowledgeable and capable adversary. The first contribution of this thesis is revisiting the seminal coercion-resistant e-voting protocol by Juels, Catalano, and Jakobsson (JCJ), examining its usability and practicality. It discusses the credential handling system proposed by Neumann et al., which uses a smart card to unlock or fake credentials via a PIN code. The thesis identifies several security concerns with the JCJ protocol, including an attack on coercion-resistance due to information leakage from the removal of duplicate ballots. It also addresses the issues of PIN errors and the single point of failure associated with the smart card. To mitigate these vulnerabilities, we propose hardware-flexible protocols that allow credentials to be stored by ordinary means while still being PIN-based and providing PIN error resilience. One of these protocols features a linear tally complexity, ensuring efficiency and scalability for large-scale electronic voting systems. The second contribution of this thesis pertains to the exploration and validation of the ballot privacy definition proposed by Cortier et. al., particularly in the context of an adversarial presence. Our exploration involves both the Selene and the MiniVoting abstract scheme. We apply Cortier's definition of ballot privacy to this scheme, investigating how it holds up under this framework. To ensure the validity of our findings, we employ the use of tools for machine-checked proof. This method provides a rigorous and reliable means of verifying our results, ensuring that our conclusions are both accurate and trustworthy. The final contribution of this thesis is a detailed examination and analysis of the Estonian election results. This analysis is conducted in several phases, each contributing to a comprehensive understanding of the election process. The first phase involves a comprehensive marginal analysis of the Estonian election results. We compute upper bounds for several margins, providing a detailed statistical overview of the election outcome. This analysis allows us to identify key trends and patterns in the voting data, laying the groundwork for the subsequent phase of our research. We then train multiple binary classifiers to predict whether a voter is likely to verify their vote. This predictive modeling enables an adversary to gain insights into voter behavior and the factors that may influence their decision to verify their vote. With the insights gained from the previous phases, an adversarial classification algorithm for verifying voters is trained. The likelihood of such an adversary is calculated using various machine learning models, providing a more robust assessment of potential threats to the election process