Machine-Checking the Universal Verifiability of ElectionGuard

Thomas Haines, Rajeev Gore, Jack Stodart

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Citation (Scopus)

    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 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.
    Original languageEnglish
    Title of host publicationSecure IT Systems
    EditorsMikael Asplund, Simin Nadjm-Tehrani
    Place of PublicationSwitzerland
    PublisherSpringer Nature
    Pages57–73
    ISBN (Print)978-3-030-70851-1
    DOIs
    Publication statusPublished - 2021
    Event25th Nordic Conference Secure IT Systems - Virtual Event
    Duration: 1 Jan 2020 → …

    Conference

    Conference25th Nordic Conference Secure IT Systems
    Period1/01/20 → …
    OtherNovember 23–24, 2020

    Fingerprint

    Dive into the research topics of 'Machine-Checking the Universal Verifiability of ElectionGuard'. Together they form a unique fingerprint.

    Cite this