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

Mehdi Talbi 1 Valérie Viet Triem Tong 1 Adel Bouhoula 2, 3
3 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

https://hal-supelec.archives-ouvertes.fr/hal-00349878
Contributor : Myriam Andrieux <>
Submitted on : Monday, January 5, 2009 - 11:05:12 AM
Last modification on : Thursday, December 13, 2018 - 8:06:02 PM

Identifiers

  • HAL Id : hal-00349878, version 1

Collections

Citation

Mehdi Talbi, Valérie Viet Triem Tong, Adel Bouhoula. Specification of Anonymity as a Secrecy Property in the ADM Logic – Homomorphic-based Voting Protocols. International Conference on Availability, Reliability and Security, Mar 2009, Fukuoka, Japan. ⟨hal-00349878⟩

Share

Metrics

Record views

315