Paper 2018/624

Formal Analysis of Vote Privacy using Computationally Complete Symbolic Attacker

Gergei Bana, Rohit Chadha, and Ajay Kumar Eeralla

Abstract

We analyze the FOO electronic voting protocol in the provable secu- rity model using the technique of Computationally Complete Symbolic Attacker (CCSA). The protocol uses commitments, blind signatures and anonymous chan- nels to achieve vote privacy. Unlike the Dolev-Yao analyses of the protocol, we assume neither perfect cryptography nor existence of perfectly anonymous chan- nels. Our analysis reveals new attacks on vote privacy, including an attack that arises due to the inadequacy of the blindness property of blind signatures and not due to a specific implementation of anonymous channels. With additional assumptions and modifications, we were able to show that the protocol satisfies vote privacy. Our techniques demonstrate effectiveness of the CCSA technique for both attack detection and verification.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Preprint. MINOR revision.
Keywords
Provable securityComputationally complete symbolic attackeVote privacy
Contact author(s)
ae266 @ mail missouri edu
History
2018-06-22: received
Short URL
https://ia.cr/2018/624
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2018/624,
      author = {Gergei Bana and Rohit Chadha and Ajay Kumar Eeralla},
      title = {Formal Analysis of Vote Privacy using Computationally Complete Symbolic Attacker},
      howpublished = {Cryptology ePrint Archive, Paper 2018/624},
      year = {2018},
      note = {\url{https://eprint.iacr.org/2018/624}},
      url = {https://eprint.iacr.org/2018/624}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.