Machine-Checked Proofs of Accountability: How to sElect who is to Blame
Résumé
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.
Domaines
Informatique [cs]Origine | Fichiers produits par l'(les) auteur(s) |
---|