Schulze voting as evidence carrying computation

Dirk Pattinson*, Mukesh Tiwari

*Corresponding author for this work

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

    6 Citations (Scopus)

    Abstract

    The correctness of vote counting in electronic election is one of the main pillars that engenders trust in electronic elections. However, the present state of the art in vote counting leaves much to be desired: while some jurisdictions publish the source code of vote counting code, others treat the code as commercial in confidence. None of the systems in use today applies any formal verification. In this paper, we formally specify the so-called Schulze method, a vote counting scheme that is gaining popularity on the open source community. The cornerstone of our formalisation is a (dependent, inductive) type that represents all correct executions of the vote counting scheme. Every inhabitant of this type not only gives a final result, but also all intermediate steps that lead to this result, and can so be externally verified. As a consequence, we do not even need to trust the execution of the (verified) algorithm: the correctness of a particular run of the vote counting code can be verified on the basis of the evidence for correctness that is produced along with determination of election winners.

    Original languageEnglish
    Title of host publicationInteractive Theorem Proving - 8th International Conference, ITP 2017,Proceedings
    EditorsCesar A. Munoz, Mauricio Ayala-Rincon
    PublisherSpringer Verlag
    Pages410-426
    Number of pages17
    ISBN (Print)9783319661063
    DOIs
    Publication statusPublished - 2017
    Event8th International Conference on Interactive Theorem Proving, ITP 2017 - Brasilia, Brazil
    Duration: 26 Sept 201729 Sept 2017

    Publication series

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

    Conference

    Conference8th International Conference on Interactive Theorem Proving, ITP 2017
    Country/TerritoryBrazil
    CityBrasilia
    Period26/09/1729/09/17

    Fingerprint

    Dive into the research topics of 'Schulze voting as evidence carrying computation'. Together they form a unique fingerprint.

    Cite this