Paper 2025/461
Machine-checking Multi-Round Proofs of Shuffle: Terelius-Wikstrom and Bayer-Groth
Abstract
Shuffles are used in electronic voting in much the same way physical ballot boxes are used in paper systems: (encrypted) ballots are input into the shuffle and (encrypted) ballots are output in a random order, thereby breaking the link between voter identities and ballots. To guarantee that no ballots are added, omitted or altered, zero-knowledge proofs, called proofs of shuffle, are used to provide publicly verifiable transcripts that prove that the outputs are a re-encrypted permutation of the inputs. The most prominent proofs of shuffle, in practice, are those due to Terelius and Wikström (TW), and Bayer and Groth (BG). TW is simpler whereas BG is more efficient, both in terms of bandwidth and computation. Security for the simpler (TW) proof of shuffle has already been machine-checked but several prominent vendors insist on using the more complicated BG proof of shuffle. Here, we machine-check the security of the Bayer-Groth proof of shuffle via the Coq proof-assistant. We then extract the verifier (software) required to check the transcripts produced by Bayer-Groth implementations and use it to check transcripts from the Swiss Post evoting system under development for national elections in Switzerland.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Minor revision. USENIX Security 2023
- Contact author(s)
- thomas haines @ anu edu au
- History
- 2025-03-12: approved
- 2025-03-11: received
- See all versions
- Short URL
- https://ia.cr/2025/461
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2025/461,
author = {Thomas Haines and Rajeev Goré and Mukesh Tiwari},
title = {Machine-checking Multi-Round Proofs of Shuffle: Terelius-Wikstrom and Bayer-Groth},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/461},
year = {2025},
url = {https://eprint.iacr.org/2025/461}
}
