Machine-checking the universal verifiability of ElectionGuard

Thomas Haines; Rajeev Gore; Jack Stodart

Paper 2020/1477

Machine-checking the universal verifiability of ElectionGuard

Thomas Haines, Rajeev Gore, and Jack Stodart

Abstract

ElectionGuard is an open source set of software components and specifications from Microsoft designed to allow the modification of a number of different e-voting protocols and products to produce public evidence (transcripts) which anyone can verify. The software uses ElGamal, homomorphic tallying and sigma protocols to enable public scrutiny without adversely affecting privacy. Some components have been formally verified (machine-checked) to be free of certain software bugs but there was no formal verification of their cryptographic security. Here, we present a machine-checked proof of the verifiability guarantees of the transcripts produced and verified according to the ElectionGuard specification. We have also extracted an executable version of the verifier specification, which we proved to be secure, and used it to verify election transcripts produced by ElectionGuard. Our results show that our implementation is of similar efficiency to existing implementations.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. The 25th Nordic Conference on Secure IT Systems (Nordsec 2020)
Keywords: secure voting machine checked
Contact author(s): haines3163 @ yahoo com au
History: 2020-11-24: received
Short URL: https://ia.cr/2020/1477
License: CC BY

BibTeX

@misc{cryptoeprint:2020/1477,
      author = {Thomas Haines and Rajeev Gore and Jack Stodart},
      title = {Machine-checking the universal verifiability of {ElectionGuard}},
      howpublished = {Cryptology {ePrint} Archive, Paper 2020/1477},
      year = {2020},
      url = {https://eprint.iacr.org/2020/1477}
}