Conference Paper/Proceeding/Abstract 32 views
Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
Thomas Haines,
Rajeev Goré,
Mukesh Tiwari
SEC '23: Proceedings of the 32nd USENIX Conference on Security Symposium
Swansea University Author: Mukesh Tiwari
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 ballo...
| Published in: | SEC '23: Proceedings of the 32nd USENIX Conference on Security Symposium |
|---|---|
| ISBN: | 978-1-939133-37-3 |
| Published: |
ACM
2023
|
| Online Access: |
https://dl.acm.org/doi/10.5555/3620237.3620599 |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa65926 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| 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. |
|---|---|
| Item Description: |
https://dl.acm.org/doi/10.5555/3620237.3620599 |
| College: |
Faculty of Science and Engineering |
| Funders: |
Wewould like to thank the shepherd and reviewers for their excellent feedback. Thomas Haines is the recipient of an Australian Research Council Australian Discovery Early Career Award (project number DE220100595). Rajeev Goré supported by FWF project P 33548 and the National Centre for Research and Development, Poland (NCBR), and the Luxembourg National Research Fund (FNR),under the PolLux/FNRCOREproject STV (POLLUX-VII/1/2019). |