Verified Certificate Checking for Counting Votes

Milad K. Ghale*, Dirk Pattinson, Ramana Kumar, Michael Norrish

*Corresponding author for this work

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

    5 Citations (Scopus)

    Abstract

    We introduce a new framework for verifying electronic vote counting results that are based on the Single Transferable Vote scheme (STV). Our approach frames electronic vote counting as certified computation where each execution of the counting algorithm is accompanied by a certificate that witnesses the correctness of the output. These certificates are then checked for correctness independently of how they are produced. We advocate verification of the verifier rather than the software used to produce the result. We use the theorem prover HOL4 to formalise the STV vote counting scheme, and obtain a fully verified certificate checker. By connecting HOL4 to the verified CakeML compiler, we then extract an executable that is guaranteed to behave correctly with respect to the formal specification of the protocol down to machine level. We demonstrate that our verifier can check certificates of real-size elections efficiently. Our encoding is modular, so repeating the same process for another different STV scheme would require a minimal amount of additional work.

    Original languageEnglish
    Title of host publicationVerified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers
    EditorsRuzica Piskac, Philipp Rümmer
    PublisherSpringer Verlag
    Pages69-87
    Number of pages19
    ISBN (Print)9783030035914
    DOIs
    Publication statusPublished - 2018
    Event10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018 - Oxford, United Kingdom
    Duration: 18 Jul 201819 Jul 2018

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume11294 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018
    Country/TerritoryUnited Kingdom
    CityOxford
    Period18/07/1819/07/18

    Fingerprint

    Dive into the research topics of 'Verified Certificate Checking for Counting Votes'. Together they form a unique fingerprint.

    Cite this