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

Abstract

<div> Mixnet protocols are used in electronic voting protocols to mix the ballot box before the tally, to preserve ballots privacy and unlinkabiliy. Whereas proving security properties of the other components of the electronic voting protocols has globally already been done in several logical frameworks and tools, proofs of mixnets remain a real challenge to handle. In this paper we focus on the quite recent CCSA logic, which enables handling of computational security proofs with first-order logics facilities. We enrich the logic to be able to deal with zero-knowledge proofs and rewinding techniques, and provide the first complete proof of Terelius-Wikström mixnet protocol. </div>