Machine-Checked Proofs of Privacy for Electronic Voting Protocols

This course teaches learners how to create machine-checked proofs of privacy-related properties for electronic voting protocols, specifically focusing on the Helios family of voting protocols. The course aims to provide the skills needed to identify appropriate levels of abstractions for simplifying and reusing proof steps across various variations of the voting scheme. The teaching method involves demonstrating the process of formalizing security proofs for different variants of the Helios protocol. This course is intended for individuals interested in cryptography, electronic voting systems, and formal verification methods.