@inproceedings{ae3bffbc53e64563a3d416b20aaaab3d,
title = "Verified verifiers for verifying elections",
abstract = "The security and trustworthiness of elections is critical to democracy; alas, securing elections is notoriously hard. Powerful cryptographic techniques for verifying the integrity of electronic voting have been developed and are in increasingly common use. The claimed security guarantees of most of these techniques have been formally proved. However, implementing the cryptographic verifiers which utilise these techniques is a technical and error prone process, and often leads to critical errors appearing in the gap between the implementation and the formally verified design. We significantly reduce the gap between theory and practice by using machine checked proofs coupled with code extraction to produce cryptographic verifiers that are themselves formally verified. We demonstrate the feasibility of our technique by producing a formally verified verifier which we use to check the 2018 International Association for Cryptologic Research (IACR) directors election.",
keywords = "Code extraction, Interactive theorem provers, Verifiable e-voting",
author = "Thomas Haines and Rajeev Gor{\'e} and Mukesh Tiwari",
note = "Publisher Copyright: {\textcopyright} 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.; 26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019 ; Conference date: 11-11-2019 Through 15-11-2019",
year = "2019",
month = nov,
day = "6",
doi = "10.1145/3319535.3354247",
language = "English",
series = "Proceedings of the ACM Conference on Computer and Communications Security",
publisher = "Association for Computing Machinery (ACM)",
pages = "685--702",
booktitle = "CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security",
address = "United States",
}