Security in E-Voting (Poster)
Daniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico
Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, and
Richard Gay
We consider the verification of security properties of Java programs that use
cryptographic operations. Our motivating objective is to provide cryptographic
guarantees on the code level for a Java implementation of a realistic, usable
electronic-voting system, called sElect1.
While tools for verification of Java programs are available, including tools
for checking noninterference properties, they cannot deal with cryptography:
guarantees for cryptographic primitives are based complexity arguments and
therefore these primitives do not provide absolute security against unbounded
adversaries (which is the adversary model employed in these tools).
We propose a framework that allows the existing tools for checking
noninterference to verify cryptographic properties, such as cryptographic
indistinguishability, of Java programs. We applied our framework to several
case studies, using the Joana and KeY tools. The integration of these tools in
our framework led to interesting insights and motivated us to improve the
existing techniques and develop new techniques for proving noninterference.