Belenios with cast as intended

Belenios with cast as intended. Véronique Cortier, Alexandre Debant, Pierrick Gaudry, and Stéphane Glondu. In 8th Workshop on Advances in Secure Electronic Voting (Voting'23), Bol, Croatia, May 2023.

Download

[PDF]

Abstract

We propose the BeleniosCaI protocol, a variant of Belenios which brings the cast-as-intended property, in addition to other existing security properties. Our approach is based on a 2-part checksum that the voting device commits to, before being challenged to reveal one of them chosen at random by the voter. It requires only one device on the voter's side and does not rely on previously sent data like with return codes. Compared to the classical Benaloh audit-or-cast approach, we still have cast-as-intended with only some probability, but the voter's journey is more linear, and the audited ballot is really the one that is cast. We formally prove the security of BeleniosCaI w.r.t. end-to-end verifiability and privacy in a symbolic model, using the ProVerif tool.

BibTeX

@InProceedings{Voting23,
  author = 	 {V\'eronique Cortier and Alexandre Debant and Pierrick Gaudry and St\'ephane Glondu},
  title = 	 {Belenios with cast as intended},
  booktitle = {8th Workshop on Advances in Secure Electronic Voting (Voting'23)},
  year = 	 {2023},
  address = 	 {Bol, Croatia},
  month = 	 may,
  abstract = {We propose the BeleniosCaI protocol, a variant of Belenios which
    brings the cast-as-intended property, in addition to other existing
    security properties. Our approach is based on a 2-part checksum that
    the voting device commits to, before being challenged to reveal one
    of them chosen at random by the voter. It requires only one device on
    the voter's side and does not rely on previously sent data like with
    return codes. Compared to the classical Benaloh audit-or-cast
    approach, we still have cast-as-intended with only some probability, but the voter's
    journey is more linear, and the audited ballot is really the one that
    is cast.
    We formally prove the security of BeleniosCaI w.r.t. end-to-end verifiability and
     privacy in a symbolic model, using the ProVerif tool.},
}