Formal analysis of vote privacy using computationally complete symbolic attacker

Abstract

We analyze the FOO electronic voting protocol in the provable security model using the technique of Computationally Complete Symbolic Attacker (CCSA). The protocol uses commitments, blind signatures and anonymous channels to achieve vote privacy. Unlike the Dolev-Yao analyses of the protocol, we assume neither perfect cryptography nor existence of perfectly anonymous channels. 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 in the sense that switching votes of two honest voters is undetectable to the attacker. Our techniques demonstrate effectiveness of the CCSA technique for both attack detection and verification.