Skip to Main content Skip to Navigation

Electronic Voting: Definitions and Analysis Techniques

Joseph Lallemand 1
1 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In this thesis we study several aspects of the security of remote electronic voting protocols. Such protocols describe how to securely organise elections over the Internet. They notably aim to guarantee vote privacy - ie, votes must remain secret -and verifiability - it must be possible to check that votes are correctly counted. Our contributions are on two aspects. First, we propose a new approach to automatically prove equivalence properties in the symbolic model. Many privacy properties can be expressed as equivalence properties, such as in particular vote privacy, but also anonymity or unlinkability. Our approach relies on typing: we design a type system that can typecheck two protocols to prove their equivalence. We show that our type system %, together with some additional conditions on the messages exchanged by the protocols, soundly implies trace equivalence, both for bounded and unbounded numbers of sessions. We compare a prototype implementation of our typechecker with other existing tools for symbolic equivalence, on a variety of protocols from the literature. This case study shows that our procedure is much more efficient than most other tools - at the price of losing precision (our tool may fail to prove some equivalences). Our second contribution is a study of the definitions of privacy and verifiability - more precisely, individual verifiability, a property that requires each voter to be able to check that their own vote is counted. We prove that, both in symbolic and computational models, privacy implies individual verifiability, contrary to intuition and related previous results that seem to indicate that these two properties are opposed. Our study also highlights a limitation of existing game-based definitions of privacy: they assume the ballot box is trusted, which makes for significantly weaker guarantees than what protocols aim for. Hence we propose a new game-based definition for vote privacy against a dishonest ballot box. We relate our definition to a simulation-based notion of privacy, to show that it provides meaningful guarantees, and conduct a case study on several voting schemes.
Document type :
Complete list of metadata

Cited literature [109 references]  Display  Hide  Download
Contributor : Joseph Lallemand <>
Submitted on : Friday, December 6, 2019 - 11:28:29 AM
Last modification on : Tuesday, February 18, 2020 - 3:17:30 PM
Long-term archiving on: : Saturday, March 7, 2020 - 2:54:44 PM


Files produced by the author(s)


  • HAL Id : tel-02396851, version 1


Joseph Lallemand. Electronic Voting: Definitions and Analysis Techniques. Cryptography and Security [cs.CR]. Université de Lorraine, 2019. English. ⟨NNT : 2019LORR0135⟩. ⟨tel-02396851⟩



Record views


Files downloads