Abstract
The encryption of ballots is crucial to maintaining integrity and anonymity in electronic voting schemes. It enables, amongst other things, each voter to verify that their encrypted ballot has been recorded as cast, by checking their ballot against a bulletin board. We present a verifiable homomorphic tallying scheme for the Schulze method that allows verification of the correctness of the counton the basis of encrypted ballotsthat only reveals the final tally. We achieve verifiability by using zero knowledge proofs for ballot validity and honest decryption of the final tally. Our formalisation takes places inside the Coq theorem prover and is based on an axiomatisation of cryptogtaphic primitives, and our main result is the correctness of homomorphic tallying. We then instantiate these primitives using an external library and show the feasibility of our approach by means of case studies
| Original language | English |
|---|---|
| Title of host publication | Verified Software. Theories, Tools, and Experiments |
| Editors | Supratik Chakraborty, Jorge A. Navas |
| Place of Publication | USA |
| Publisher | Springer Cham |
| Pages | 36-53 |
| Edition | 1 |
| ISBN (Print) | 978-3-030-41600-3 |
| DOIs | |
| Publication status | Published - 2020 |
| Event | 11th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019) - New York City Duration: 1 Jan 2019 → … https://doi.org/10.1007/978-3-030-41600-3 |
Conference
| Conference | 11th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019) |
|---|---|
| Period | 1/01/19 → … |
| Other | July 1314 |
| Internet address |