Systems for electronic voting (e-voting systems), including systems for voting over the Internet and systems for voting in a voting booth, are employed in many countries. However, most of the systems used in practice today do not provide a sufficient level of security. For example, programming errors and malicious behavior easily go undetected. In fact, numerous problems with e-voting systems have been reported in various countries.

Therefore, in recent years modern e-voting systems have been designed that strive to achieve a rich set of fundamental but at the same time intricate and seemingly contradictory security requirements. For example, besides keeping the votes of individual voters private (privacy of votes), they allow voters to check that their votes were counted correctly, even if voting machines have programming errors or are outright malicious (verifiability/accountability). Some of these systems also try to prevent vote buying and voter coercion (coercion resistance).

In this course, we cover the above mentioned central security requirements of e-voting systems and how they can be formally defined and analyzed. While analysis is mostly done based on cryptographic models or even more abstract so-called Dolev-Yao models, we also discuss approaches to perform (cryptographic) analysis directly on the implementation-/language-level of a system.