# Formal Verification of Voting Schemes

#### Diplomarbeit

Autor(en):Michael Kirsten
Hochschule:ITI Beckert, Karlsruhe Institute of Technology
Jahr:2014
PDF:

## Abstract

Fundamental trust and credibility in democratic systems is commonly established through the existence and execution of democratic elections. The vote-counting of an election, usually formalised by a voting scheme, essentially boils down to a mechanism that aggregates individual preferences of the voters to reach a decision. For this matter, there are various differing voting schemes in use throughout the world, commonly based on high expectations and means to ensure a sensible democratic process. However, incidents such as the ruling by the German federal constitutional court which led to a change of the German legislation in 2013 manifest that it is difficult for a voting scheme to meet these legitimate expectations. In fact, there is no general notion of correctness for a voting scheme and thus no universal mechanism as shown in Kenneth J. Arrow’s Impossibility Theorem in 1951. As a consequence, designing a real-world voting scheme without flaws, which still gives significant democratic guarantees, is a difficult task as a trade-off between desirable properties is non-trivial and error-prone.
The approach in this thesis is based on the idea to tackle this issue by proposing an incremental and iterative development process for voting schemes based on automated formal reasoning methods using program verification. We analyse two different forms of verification considering their role in this development process in order to achieve formal correctness of voting schemes. We perform a comprehensive set of case studies by applying "medium-weight" and "light-weight" verification techniques. The "medium-weight" approach uses the annotation-based deductive verification tool VCC based on an auto-active methodology and the "light-weight" technique is performed with the bounded model checking tool LLBMC. Our analysis covers a set of well-known voting schemes combined with a set of prominent voting scheme criteria. In addition to giving precise formalisations for these criteria adapted to the specific voting schemes and tools used, we advance the efficiency of the "light-weight" approach by exploiting fundamental symmetric properties. Furthermore, we investigate on encountered challenges posed by the auto-active verification methodology, which lies in-between automatic and interactive verification methodologies, with respect to specific characteristics in voting schemes and also explore the potential of bounded verification techniques to produce precise counterexamples in order to enhance the capability of our envisioned development process to give early feedback. This thesis gives fundamental insights in general challenges and the potential of automated formal reasoning with the goal of correct voting schemes.

## BibTeX

@MastersThesis{KirstenDA2014,
author	= {Michael Kirsten},
title		= {Formal Verification of Voting Schemes},
school	= {ITI Beckert, Karlsruhe Institute of Technology},
month		= dec,
year		= {2014},
location      = {Karlsruhe, Germany},
abstract	= {Fundamental trust and credibility in democratic systems is commonly established
through the existence and execution of democratic elections. The vote-counting
of an election, usually formalised by a \emph{voting scheme}, essentially boils
down to a mechanism that aggregates individual preferences of the voters to
reach a decision.
For this matter, there are various differing voting schemes in use throughout
the world, commonly based on high expectations and means to ensure a sensible
democratic process.
However, incidents such as the ruling by the German federal constitutional court
which led to a change of the German legislation in 2013 manifest that it is
difficult for a voting scheme to meet these legitimate expectations.
In fact, there is no general notion of correctness for a voting scheme and thus
no universal mechanism as shown in Kenneth J. Arrow’s \emph{Impossibility Theorem}
in 1951.
As a consequence, designing a real-world voting scheme without flaws, which still
between desirable properties is non-trivial and error-prone.
\newline

The approach in this thesis is based on the idea to tackle this issue by proposing
an incremental and iterative development process for voting schemes based on
automated formal reasoning methods using program verification.
We analyse two different forms of verification considering their role in this
development process in order to achieve formal correctness of voting schemes.
We perform a comprehensive set of case studies by applying medium-weight'' and
light-weight'' verification techniques.
The medium-weight'' approach uses the annotation-based deductive verification
tool VCC based on an \emph{auto-active} methodology and the light-weight''
technique is performed with the bounded model checking tool LLBMC.
Our analysis covers a set of well-known voting schemes combined with a set of
prominent voting scheme criteria.
In addition to giving precise formalisations for these criteria adapted to the
specific voting schemes and tools used, we advance the efficiency of the
light-weight'' approach by exploiting fundamental symmetric properties.
Furthermore, we investigate on encountered challenges posed by the
\emph{auto-active} verification methodology, which lies in-between automatic
and interactive verification methodologies, with respect to specific
characteristics in voting schemes and also explore the potential of bounded
verification techniques to produce precise counterexamples in order to enhance
the capability of our envisioned development process to give early feedback.
This thesis gives fundamental insights in general challenges and the potential
of automated formal reasoning with the goal of correct voting schemes.},
language	= {english},
type		= {Diplomarbeit}
}