Functional Verification and Information Flow Analysis of an Electronic Voting System

Buchkapitel

Autor(en):Daniel Grahl und Christoph Scheben
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:10001
Kapitel:18
Jahr:2016
Seiten:593-607
DOI:10.1007/978-3-319-49812-6_18

Abstract

Electronic voting (e-voting) systems that are used in public elections need to fulfill a broad range of strong requirements concerning both safety and security. Among those requirements are reliability, robustness, privacy of votes, coercion resistance, and universal verifiability. Bugs in or manipulations of an e-voting system can have considerable influence on society. Therefore, e-voting systems are an obvious target for software verification. This case study proves the preservation of privacy of votes for a basic electronic voting system. Altogether the considered code comprises eight classes and thirteen methods in about 150 lines of code of a rich fragment of Java.

BibTeX

@incollection{GrahlScheben2016,
  author    = {Daniel Grahl and Christoph Scheben},
  title     = {Functional Verification and Information Flow Analysis of an Electronic Voting System},
  booktitle = {Deductive Software Verification - The \KeY Book: From Theory to Practice},
  year      = {2016},
  publisher = {Springer},
  pages     = {593--607},
  chapter   = {18},
  doi       = {10.1007/978-3-319-49812-6_18},
  series    = {Lecture Notes in Computer Science},
  volume    = {10001},
  month     = dec,
  abstract  = {Electronic voting (e-voting) systems that are used in public elections need to fulfill
               a broad range of strong requirements concerning both safety and security. Among those
               requirements are reliability, robustness, privacy of votes, coercion resistance, and
               universal verifiability. Bugs in or manipulations of an e-voting system can have
               considerable influence on society. Therefore, e-voting systems are an obvious target
               for software verification. This case study proves the preservation of privacy of votes
               for a basic electronic voting system. Altogether the considered code comprises eight
               classes and thirteen methods in about 150 lines of code of a rich fragment of Java.}
}