Formal Verification of an Electronic Voting System

@TechReport{Bruns14,
  author	= {Daniel Bruns},
  title		= {Formal Verification of an Electronic Voting System},
  year		= 2014,
  month		= aug,
  institution	= {Department of Informatics, Karlsruhe Institute of
		   Technology},
  language	= {english},
  number	= {2014-11},
  series	= {Karlsruhe Reports in Informatics},
  url		= {https://publikationen.bibliothek.kit.edu/1000042284},
  urn		= {urn:nbn:de:swb:90-422842},
  issn		= {2190-4782},
  license	= {https://creativecommons.org/licenses/by-nc-nd/3.0/},
  abstract	= {Electronic voting (e-voting) systems that are used in
		   public elections need to fulfil a broad range of strong
		   requirements concerning both safety and security. Among
		   these requirements are reliability, robustness, privacy of
		   votes, coercion resistance and universal verifiability.
		   Bugs in or manipulations of an e-voting system may have
		   considerable influence on the life of the humans living in
		   a country where such a system is used. Hence, e-voting
		   systems are an obvious target for software verification.
		   
		   In this paper, we report on an implementation of such a
		   system in Java and the formal verification of functional
		   properties thereof in the {\KeY} verification system. Even
		   though the actual components are clearly modularized, the
		   challenge lies in the fact that we need to prove a highly
		   nonlocal property: After all voters have cast their votes,
		   the server calculates the correct votes for each candidate
		   w.r.t.\ the original ballots. This kind of trace property
		   is difficult to prove with static techniques like
		   verification and typically yields a large specification
		   overhead.}
}