This repository contains the EasyCrypt code associated with the paper "Machine-checked proofs of privacy against malicious boards for Selene & Co". The main contribution of the paper is a new definition of ballot privacy for electronic voting systems, called delay-use malicious-ballotbox ballot privacy (or du-mb-bpriv), assuming a dishonest ballot box and allowing for delayed use of voter verification (i.e. voter verification can happen after the tally has been computed). As a case study, we prove that Selene, Labelled-MiniVoting and Belenios all satisfy this definition of ballot privacy.
In addition, we model the mb-bpriv ballot privacy definition in EasyCrypt, and prove that Labelled-MiniVoting and Belenios satisfy this definition.
- The
Corefolder contains files modelling labelled public key encryption systems (including a concrete model of the ElGamal PKE), zero-knowledge proof systems and hybrid arguments - The
du_mb_bprivfolder contains:- A definition of voting systems and the du-mb-bpriv security definition (
du_mb_bpriv/VotingDefinition) - A proof that the Selene voting protocol satisfies du-mb-bpriv (Selene with signatures in
du_mb_bpriv/Selene_with_signaturesand Selene without signatures indu_mb_bpriv/Selene) - Proofs that Labelled-MiniVoting and Belenios satisfy du-mb-bpriv (
du_mb_bpriv/Belenios_and_MiniVoting)
- A definition of voting systems and the du-mb-bpriv security definition (
- The
mb_bpriv_orignal_deffolder contains an EasyCrypt model of the mb-bpriv ballot privacy definition and proofs that Labelled-MiniVoting and Belenios satisfy this definition
We refer to https://github.com/EasyCrypt/easycrypt for instructions on how to install EasyCrypt.
This proof is known to check with EasyCrypt stable release r2022.04, using Z3 4.8.10, Alt-Ergo 2.4.0, and CVC4 1.8.