Machine-Checked Proofs of Accountability: How to sElect who is to Blame

Constantin Catalin Dragan (1) , François Dupressoir (2) , Kristian Gjøsteen (3) , Thomas Haines (4) , Peter Rønne (5) , Morten Rotvold Solberg (3)

1 UNIS - University of Surrey
2 University of Bristol [Bristol]
3 NTNU - Norwegian University of Science and Technology
4 ANU - Australian National University
5 PESTO - Proof techniques for security protocols

Accountability is a critical requirement of any deployed voting system as it allows unequivocal identification of misbehaving parties, including authorities. In this paper, we propose the first game-based definition of accountability and demonstrate its usefulness by applying it to the sElect voting system (Küsters et al., 2016)-a voting system that relies on no other cryptographic primitives than digital signatures and public key encryption. We strengthen our contribution by proving accountability for sElect in the EasyCrypt proof assistant. As part of this, we identify a few errors in the proof for sElect as presented by Küsters et al. (2016) for their definition of accountability. Finally, we reinforce the known relation between accountability and verifiability, and show that it is still maintained by our new game-based definition of accountability.

Domains: Computer Science [cs]

Constantin Catalin Dragan, François Dupressoir, Kristian Gjøsteen, Thomas Haines, Peter Rønne, et al.. Machine-Checked Proofs of Accountability: How to sElect who is to Blame. ESORICS 2023, Sep 2023, The Hague, The Netherlands, Netherlands. ⟨10.1007/978-3-031-51479-1_24⟩. ⟨hal-04216243⟩