From Secure to Usable and Verifiable Voting Schemes

Elections are the foundations of democracy. To uphold democratic principles, researchers have proposed systems that ensure the integrity of elections. It is a highly interdisciplinary field, as it can be studied from a technical, legal or societal points of view. While lawyers give a legal framework to the voting procedures, security researchers translate these rules into technical properties that operational voting systems must satisfy, notably privacy and verifiability. If Privacy aims to protect vote-secrecy and provide coercion-resistance to the protocol, Verifiability allows voters to check that their vote has been taken into account in the general outcome, contributing to the assurance of the integrity of the elections. To satisfy both properties in a voting system, we rely on cryptographic primitives such as encryption, signatures, commitments schemes, or zero-knowledge proofs, etc. Many protocols, paper-based or electronic-based, have been designed to satisfy these properties. Although the security of some protocols, and their limits, have been analysed from a technical perspective, the usability has often been shown to have very low rates of effectiveness. The necessary cryptographic interactions have already shown to be one contributor to this problem, but the design of the interface could also contribute by misleading voters. As elections typically rarely happen, voters must be able to understand the system they use quickly and mostly without training, which brings the user experience at the forefront of the designed protocols. In this thesis, the first contribution is to redefine privacy and verifiability in the context of tracker-based verifiable schemes. These schemes, using a so-called tracking number for individual verification, need additional user steps that must be considered in the security evaluation. These security definitions are applied to the boardroom voting protocol F2FV used by the CNRS, and the e-voting protocol Selene, both use a tracker-based procedure for individual verifiability. We provide proofs of security in the symbolic model using the Tamarin prover. The second contribution is an implementation of the Selene protocol as a mobile and a web application, tested in several user studies. The goal is to evaluate the usability and the overall user experience of the verifiability features, as well as their understanding of the system through the evaluation of mental models. The third contribution concerns the evaluation of the voters' understanding of the coercion mitigation mechanism provided by Selene, through a unique study design using game theory for the evaluation of voters. Finally, the fourth contribution is about the design of a new voting scheme, Electryo, that is based on the Selene verification mechanisms but provides a user experience close to the standard paper-based voting protocols