Formal Methods for Trustworthy Voting Systems

@PhDThesis{KirstenDiss2022,
  author     = {Michael Kirsten},
  year       = {2022},
  title      = {Formal Methods for Trustworthy Voting Systems},
  school     = {Karlsruhe Institute of Technology (KIT)},
  month      = jan,
  doi        = {10.5445/IR/1000155115},
  abstract   = {Voting is prominently an important part of democratic
                societies, and its outcome may have a dramatic and broad
                impact on societal progress. Therefore, it is paramount
                that such a society has extensive trust in the electoral
                process, such that the system’s functioning is reliable
                and stable with respect to the expectations within
                society. Yet, with or without the use of modern
                technology, voting is full of algorithmic and security
                challenges, and the failure to address these challenges
                in a controlled manner may produce fundamental flaws in
                the voting system and potentially undermine critical
                societal aspects.
                In this thesis, we argue for a development process of
                voting systems that is rooted in and assisted by formal
                methods that produce transparently checkable evidence
                for the guarantees that the final system should provide
                so that it can be deemed trustworthy. The goal of this
                thesis is to advance the state of the art in formal
                methods that allow to systematically develop trustworthy
                voting systems that can be provenly verified. In the
                literature, voting systems are modeled in the following
                four comparatively separable and distinguishable layers:
                (1) the physical layer, (2) the computational layer,
                (3) the election layer, and (4) the human layer. Current
                research usually either mostly stays within one of those
                layers or lacks machine-checkable evidence, and
                consequently, trusted and understandable criteria often
                lack formally proven and checkable guarantees on
                software-level and vice versa.
                The contributions in this work are formal methods that
                fill in the trust gap between the principal election
                layer and the computational layer by a reliable
                translation of trusted and understandable criteria
                into trustworthy software. Thereby, we enable that
                executable procedures can be formally traced back and
                understood by election experts without the need for
                inspection on code level, and trust can be preserved
                to the trustworthy system.
                \newline

                The works in this thesis all contribute to this end and
                consist in five distinct contributions, which are the
                following:

                (I) a method for the generation of secure card-based
                    communication schemes,
                (II) a method for the synthesis of reliable tallying
                    procedures,
                (III) a method for the efficient verification of
                    reliable tallying procedures,
                (IV) a method for the computation of dependable election
                    margins for reliable audits,
                (V) a case study about the security verification of the
                    GI voter-anonymization software.
                \newline

                These contributions span formal methods on illustrative
                examples for each of the three principal components,
                (1) voter-ballot box communication, (2) election method,
                and (3) election management, between the election layer
                and the computational layer. Within the first component,
                the voter-ballot box communication channel, we build a
                bridge from the communication channel to the
                cryptography scheme by automatically generating secure
                card-based schemes from a small formal model with a
                parameterization of the desired security requirements.
                For the second component, the election method, we build
                a bridge from the election method to the tallying
                procedure by (1) automatically synthesizing a runnable
                tallying procedure from the desired requirements given
                as properties that capture the desired intuitions or
                regulations of fairness considerations,
                (2) automatically generating either comprehensible
                arguments or bounded proofs to compare tallying
                procedures based on user-definable fairness properties,
                and (3) automatically computing concrete election
                margins for a given tallying procedure, the collected
                ballots, and the computed election result, that enable
                efficient election audits. Finally, for the third and
                final component, the election management system, we
                perform a case study and apply state-of-the-art
                verification technology to a real-world e-voting
                system that has been used for the annual elections of
                the German Informatics Society (GI – “Gesellschaft für
                Informatik”) in 2019. The case study consists in the
                formal implementation-level security verification that
                the voter identities are securely anonymized and the
                voters’ passwords cannot be leaked.
                \newline

                The presented methods assist the systematic development
                and verification of provenly trustworthy voting systems
                across traditional layers, i.e., from the election layer
                to the computational layer. They all pursue the goal of
                making voting systems trustworthy by reliable and
                explainable formal requirements. We evaluate the devised
                methods on minimal card-based protocols that compute a
                secure AND function for two different decks of cards, a
                classical knock-out tournament and several Condorcet
                rules, various plurality, scoring, and Condorcet rules
                from the literature, the Danish national parliamentary
                elections in 2015, and a state-of-the-art electronic
                voting system that is used for the German Informatics
                Society’s annual elections in 2019 and following.}
}