No Cover Image

Conference Paper/Proceeding/Abstract 39 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...

Full description

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!
first_indexed 2024-04-03T10:22:51Z
last_indexed 2024-04-03T10:22:51Z
id cronfa65926
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>65926</id><entry>2024-03-28</entry><title>Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth</title><swanseaauthors><author><sid>4b6a02f9e2ebffd1dd1b7151116dd8aa</sid><firstname>Mukesh</firstname><surname>Tiwari</surname><name>Mukesh Tiwari</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2024-03-28</date><deptcode>SCS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>SEC '23: Proceedings of the 32nd USENIX Conference on Security Symposium</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>ACM</publisher><placeOfPublication/><isbnPrint/><isbnElectronic>978-1-939133-37-3</isbnElectronic><issnPrint/><issnElectronic/><keywords/><publishedDay>9</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-08-09</publishedDate><doi/><url>https://dl.acm.org/doi/10.5555/3620237.3620599</url><notes>https://dl.acm.org/doi/10.5555/3620237.3620599</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><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).</funders><projectreference/><lastEdited>2024-04-23T15:02:10.0740076</lastEdited><Created>2024-03-28T07:15:29.5809281</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Thomas</firstname><surname>Haines</surname><order>1</order></author><author><firstname>Rajeev</firstname><surname>Goré</surname><order>2</order></author><author><firstname>Mukesh</firstname><surname>Tiwari</surname><order>3</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling v2 65926 2024-03-28 Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth 4b6a02f9e2ebffd1dd1b7151116dd8aa Mukesh Tiwari Mukesh Tiwari true false 2024-03-28 SCS 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. Conference Paper/Proceeding/Abstract SEC '23: Proceedings of the 32nd USENIX Conference on Security Symposium ACM 978-1-939133-37-3 9 8 2023 2023-08-09 https://dl.acm.org/doi/10.5555/3620237.3620599 https://dl.acm.org/doi/10.5555/3620237.3620599 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 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). 2024-04-23T15:02:10.0740076 2024-03-28T07:15:29.5809281 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Thomas Haines 1 Rajeev Goré 2 Mukesh Tiwari 3
title Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
spellingShingle Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
Mukesh Tiwari
title_short Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
title_full Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
title_fullStr Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
title_full_unstemmed Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
title_sort Machine-checking multi-round proofs of shuffle: Terelius-Wikstrom and Bayer-Groth
author_id_str_mv 4b6a02f9e2ebffd1dd1b7151116dd8aa
author_id_fullname_str_mv 4b6a02f9e2ebffd1dd1b7151116dd8aa_***_Mukesh Tiwari
author Mukesh Tiwari
author2 Thomas Haines
Rajeev Goré
Mukesh Tiwari
format Conference Paper/Proceeding/Abstract
container_title SEC '23: Proceedings of the 32nd USENIX Conference on Security Symposium
publishDate 2023
institution Swansea University
isbn 978-1-939133-37-3
publisher ACM
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url https://dl.acm.org/doi/10.5555/3620237.3620599
document_store_str 0
active_str 0
description 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.
published_date 2023-08-09T15:02:06Z
_version_ 1797134406838648832
score 11.012656

Similar Items