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

Sergiu Bursuc 1 Constantin-Catalin Dragan 2 Steve Kremer 1
1 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [55 references]  Display  Hide  Download

https://hal.inria.fr/hal-02099434
Contributor : Steve Kremer <>
Submitted on : Monday, April 15, 2019 - 8:51:56 AM
Last modification on : Tuesday, May 7, 2019 - 2:53:40 PM

File

sp.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02099434, version 1

Collections

Citation

Sergiu Bursuc, Constantin-Catalin Dragan, Steve Kremer. Private votes on untrusted platforms: models, attacks and provable scheme. EuroS&P 2019 - 4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden. ⟨hal-02099434⟩

Share

Metrics

Record views

93

Files downloads

143