Cryptology ePrint Archive: Report 2018/624

Formal Analysis of Vote Privacy using Computationally Complete Symbolic Attacker

Gergei Bana and 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.

Category / Keywords: cryptographic protocols / Provable security, Computationally complete symbolic attacke, Vote privacy

Date: received 20 Jun 2018

Contact author: ae266 at mail missouri edu

Available format(s): PDF | BibTeX Citation

Version: 20180622:150037 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]