Articles
Implementation-Level Analysis of E-Voting Systems (part of the RS3 project)
Summary
Systems for electronic voting (e-voting systems) are among the most challenging security-critical systems, with a rich set of intricate security requirements they have to fulfill. For example, besides keeping the votes of individual voters private (privacy of votes), they should also allow voters to check that their votes were counted correctly (verifiability), while at the same time prevent vote buying and voter coercion (coercion-resistance). These and other security requirements have been formalized and analyzed on the protocol design level of e-voting systems. However, ensuring such properties on the implementation-level of e-voting systems is still an open problem.
The goal of this project is therefore to devise general methods and techniques for the sound implementation-level analysis of e-voting systems and to demonstrate the applicability of these methods and techniques for concrete systems, including a prototypical implementation of an e-voting system provided as a case study within the project. In the project, techniques and methods for language-based information flow security, in particular language-based noninterference, will be combined with techniques and methods for cryptographic protocol analysis. This will advance research on language-based noninterference also beyond the domain of e-voting. Prototypes developed and results obtained within the project can serve as case studies for other projects within the Priority Programme.
Project members
- Prof. Dr. Ralf Küsters (principal investigator)
- Dr. Tomasz Truderung (researcher)
- Andreas Koch (student assistant)
Publications
- Ralf Küsters, Tomasz Truderung, and Jürgen Graf.
A Framework for the Cryptographic Verification of Java-like Programs.
In IEEE Computer Security Foundations Symposium, CSF 2012, IEEE Computer Society, 2012. To appear
BibTeX Download: [pdf] - Ralf Küsters, Tomasz Truderung, and Jürgen Graf.
A Framework for the Cryptographic Verification of Java-like Programs.
Cryptology ePrint Archive, Report 2012/153, 2012. http://eprint.iacr.org/2012/153
BibTeX Download: [pdf] - Bernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt, and Tomasz Truderung.
- The KeY Approach for the Cryptographic Verification of Java
- Programs: A Case Study,
- Ralf Küsters, Tomasz Truderung, and Andreas Vogt.
Clash Attacks on the Verifiability of E-Voting Systems.
In IEEE Symposium on Security and Privacy (S&P 2012), IEEE Computer Society, 2012. To appear.
BibTeX Abstract Download: [pdf] - Ralf Küsters, Tomasz Truderung, and Andreas Vogt.
Clash Attacks on the Verifiability of E-Voting Systems.
Technical Report 2012/116, Cryptology ePrint Archive, 2012. http://eprint.iacr.org/2012/116/
BibTeX Abstract Download: [pdf] - Ralf Küsters, Tomasz Truderung, and Andreas Vogt.
Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study.
In IEEE Symposium on Security and Privacy (S&P 2011), pp. 538–553, IEEE Computer Society, 2011.
BibTeX Abstract Download: [pdf] - Ralf Küsters, Tomasz Truderung, and Andreas Vogt.
Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study.
Technical Report 2011/517, Cryptology ePrint Archive, 2010. http://eprint.iacr.org/2011/517/
BibTeX Abstract Download: [pdf] - R. Küsters, T. Truderung, and A. Vogt.
Proving Coercion-Resistance of Scantegrity II.
In Proceedings of the 12th International Conference on Information and Communications Security (ICICS 2010), pp. 281–295, Lecture Notes in Computer Science 6476, Springer, 2010.
BibTeX Abstract Download: [pdf] - R. Küsters, T. Truderung, and A. Vogt.
Proving Coercion-Resistance of Scantegrity II.
Technical Report 2010/502, Cryptology ePrint Archive, 2010. http://eprint.iacr.org/2010/502/
BibTeX Abstract Download: [pdf]