Machine-aided analysis of vote privacy using computationally complete symbolic attacker

Security protocols employ cryptographic primitives such as encryption and digital signatures to provide security guarantees of confidentiality and authenticity in the presence of malicious attackers. Due to the complexities of cryptographic primitives, subtle nature of the security guarantees and asymmetry of communication over the internet, their design tends to be error-prone. Thus, formal methods are often used to establish whether the protocols actually achieve their guarantees. The analysis can be either carried out in the Dolev-Yao model, where the cryptographic primitives are assumed to be perfect, and the attacker tries to exploit the logical errors to compromise the security of the protocols or in the provable security model, where the attacker can, in addition, break the cryptographic primitives with negligible probability. The provable security model provides better guarantees. We consider formalizing and verifying the security property of vote privacy for electronic voting protocols in the provable security model. As an example, we consider analyzing the FOO electronic voting protocol introduced by Fujioka, Okamoto, and Ohta. Several automated analyses have been carried for the FOO protocol in the Dolev-Yao model, and the protocol is secure in the Dolev-Yao model. The protocol uses commitments, blind signatures, and anonymous channels to achieve vote privacy. The Dolev-Yao analyses also assume the existence of perfectly anonymous channels. We carried out the analysis of the security protocol using the Computationally Complete Symbolic Attacker (CCSA) technique, which allows the establishment of proofs of security guarantees using deduction in first-order logic. Unlike the Dolev Yao analyses of the protocol, we assume neither perfect cryptography nor existence of perfectly anonymous channels. We model the anonymous communication using a mix-net server who is responsible for checking if the received messages are distinct and outputting the decrypted messages in a lexicographic order. 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 a Dolev-Yao style attack that arises due to the modeling of the anonymous communication as a mix-net server. With additional assumptions and modifications of the protocol, 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. In order to achieve higher assurances, we mechanized the CCSA technique in Coq, an interactive theorem-prover [BC04, PdAC+17] developed using the specification language Gallina. We demonstrate the effectiveness of our mechanization with the verification of authentication and secrecy guarantees of the Authenticated Die Hellman key exchange protocol. Finally, we prove the key lemmas of the proof of voter privacy for the FOO protocol in Coq.