Proving e-voting mixnets in the CCSA model: zero-knowledge proofs and rewinding

Links:   Paper

Mixnets are crucial components of electronic voting protocols, used to mix the ballot box before the tally. Mixnets should ensure two somewhat antithetic properties: preservation of the list of ballots, and privacy. Unfortunately, proving that mixnets ensure the desired properties requires both complex cryptographic primitives (zero-knowledge proofs, commitments schemes) and proof techniques (mainly rewinding). Hence, such proofs are at the same time highly desirable but quite complex to get. In order to achieve such complex formal proofs, we focus on the quite recent Computationally Complete Symbolic Attacker logics, which handles computational security proofs with first-order logic, abstracting most probabilities and explicit reductions. Said differently, it provides precise and subtle computational reasoning, while not requiring too much expertise from the user who setup the proof. In the present work, we enrich the logic to be able to deal with zero-knowledge proofs and rewinding techniques, and provide the first complete formal proof of the Terelius-Wikström mixnet protocol.