Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Explore a groundbreaking presentation on machine-checked proofs of privacy for electronic voting protocols, delivered at the 2017 IEEE Symposium on Security & Privacy. Delve into the first-ever machine-checked proof of privacy-related properties, including ballot privacy, for the Helios family of voting protocols in the computational model. Discover the appropriate levels of abstractions identified to simplify and reuse proof steps across numerous variations of the voting scheme. Learn about the resulting framework that enables machine-checked security proofs for hundreds of Helios variants, serving as a foundation for analyzing future iterations. Gain insights into the challenges and lessons learned when bridging the gap between traditional pen-and-paper proofs and machine-checked proofs. Understand the experience of formalizing security protocols at this scale, providing valuable knowledge for researchers and practitioners in the field of electronic voting security.