Steve Kremer: Private votes on untrusted platforms: models, attacks and provable scheme

Private votes on untrusted platforms: models, attacks and provable scheme

Sergiu Bursuc, Constantin-Cătălin Drăgan, and Steve Kremer. Private votes on untrusted platforms: models, attacks and provable scheme. In Proceedings of the 4th IEEE European Symposium on Security and Privacy (EuroS&P'19), IEEE Computer Society Press, Stockholm, Sweden, June 2019.
doi:10.1109/EuroSP.2019.00050

Download

[PDF] [HTML]

Abstract

Modern e-voting systems deploy cryptographic protocols on a complex infrastructure involving different computing platforms and agents. It is crucial to have appropriate specification and evaluation methods to perform rigorous analysis of such systems, taking into account the corruption and computational capabilities of a potential attacker. In particular, the platform used for voting may be corrupted, e.g. infected by malware, and we need to ensure privacy and integrity of votes even in that case.
We propose a new definition of vote privacy, formalized as a computational indistinguishability game, that allows to take into account such refined attacker models; we show that the definition captures both known and novel attacks against several voting schemes; and we propose a scheme that is provably secure in this setting. We moreover formalize and machine-check the proof in the EasyCrypt theorem prover.

BibTeX

@inproceedings{BDK-eurosp19,
  abstract =	 {Modern e-voting systems deploy cryptographic
                  protocols on a complex infrastructure involving
                  different computing platforms and agents. It is
                  crucial to have appropriate specification and
                  evaluation methods to perform rigorous analysis of
                  such systems, taking into account the corruption and
                  computational capabilities of a potential
                  attacker. In particular, the platform used for
                  voting may be corrupted, e.g. infected by malware,
                  and we need to ensure privacy and integrity of votes
                  even in that case. \par We propose a new definition
                  of vote privacy, formalized as a computational
                  indistinguishability game, that allows to take into
                  account such refined attacker models; we show that
                  the definition captures both known and novel attacks
                  against several voting schemes; and we propose a
                  scheme that is provably secure in this setting. We
                  moreover formalize and machine-check the proof in
                  the EasyCrypt theorem prover. },
  address =	 {Stockholm, Sweden},
  author =	 {Bursuc, Sergiu and Constantin-C\u{a}t\u{a}lin
                  Dr\u{a}gan and Kremer, Steve},
  booktitle =	 {{P}roceedings of the 4th IEEE European Symposium on
                  Security and Privacy (EuroS\&P'19)},
  month =	 jun,
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {Private votes on untrusted platforms: models,
                  attacks and provable scheme},
  year =	 2019,
  acronym =	 {{EuroS\&P}'19},
  nmonth =	 6,
  doi =		 {10.1109/EuroSP.2019.00050},
  url =		 {https://ieeexplore.ieee.org/document/8806713},
}