Verification of E-Voting Algorithms in Dafny
By: Robert Büttner , Fabian Franz Dießl , Patrick Janoschek and more
Electronic voting procedures are implementations of electoral systems, making it possible to conduct polls or elections with the help of computers. This paper reports on the development of an open-source library of electronic voting procedures, which currently covers Score Voting, Instant-Runoff Voting, Borda Count, and Single Transferable Vote. The four procedures, of which two are discussed in detail, have been implemented in Dafny, formally verifying the consistency with functional specifications and key correctness properties. Using code extraction from the Dafny implementation, the library has been used to set up a voting web service.
Similar Papers
A Post-Quantum Secure End-to-End Verifiable E-Voting Protocol Based on Multivariate Polynomials
Cryptography and Security
Makes online voting safe from future computers.
A Quantum-Secure and Blockchain-Integrated E-Voting Framework with Identity Validation
Cryptography and Security
Secures online votes against future computer threats.
Verified VCG and Verified Compiler for Dafny
Programming Languages
Proves computer programs are correct, even complex ones.