Machine-Checked Proofs of Accountability: How to sElect who is to Blame - Université de Lorraine
Communication Dans Un Congrès Année : 2023

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.
Fichier principal
Vignette du fichier
main-lncs.pdf (426.45 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04216243 , version 1 (24-09-2023)

Licence

Identifiants

Citer

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⟩
114 Consultations
160 Téléchargements

Altmetric

Partager

More