Specification of Anonymity as a Secrecy Property in the ADM Logic - Homomorphic-Based Voting Protocols

Nowadays, it is a well-known fact that only formal methods can provide a proof that a given system meets its requirements. Their use become mandatory for critical systems such as electronic voting which must satisfy several and complex properties (receipt-freeness, verifiability). Among these properties, anonymity is probably the most desirable one. Formally, this property was mainly specified using the concept of indistinguishability which implies complex definitions (in terms of equivalence relations). In this paper, we give an alternative and simpler specification of anonymity property in the ADM logic. We specify anonymity as a secrecy property which represents the oldest and most understood property of security protocols. Our specification is specific to homomorphic-based voting schemes since in this case, voter´s anonymity rely on the secrecy of his vote.