In recent years, a new approach has been developed for ver- ifying security protocols with the aim of combining the benefits of sym- bolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [1]. The BC technique has the advantage that it is syntactically simple and standard computational security notions can be translated to it in a straightforward matter. In this work, we further develop the BC framework for indistinguishability properties first introduced in [1] by formulating axioms and mechanizing security proofs in Coq, an inter- active theorem-prover. In Coq, we proved the vote privacy of the voting protocol proposed by Fujioka et al. in the paper [2]. We assume that there are at least two honest voters and an honest administrator, and the collector is an adversary. We model the anonymous channel using Mixnets in tandem with encryptions. We also plan to analyze the vote privacy in the presence of a dishonest administrator.