Proof of Correctness of Homomorphic Voting Rules with Isabelle/HOL
| Forschungsthema: | Computational Social Choice |
|---|---|
| Typ: | BA |
| Datum: | 2024-07-01 |
| Betreuer: | Michael Kirsten |
| Aushang: |
Abstract
In the modern digital world, electronic voting systems are playing an increasingly important role, increasing the need for their verifiable security.
This thesis investigates formal game-based proofs of homomorphic encryption for voting procedures using the Isabelle theorem prover and the CryptHOL framework. Homomorphic encryption allows computations on encrypted data, ensuring the confidentiality and security of voting processes. The analysis focuses on three specific voting procedures: the majority, Borda and Black's voting procedure.
Literature
- "Formalising ∑-Protocols and Commitment Schemes Using CryptHOL" in Journal of Automated Reasoning 65, 521–567 (2021)
- "Verified Construction of Fair Voting Rules" in 29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019)