Skip to Main content Skip to Navigation
Conference papers

Specification of Electronic Voting Protocol Properties Using ADM Logic : FOO Case Study

Mehdi Talbi 1 Benjamin Morin 1 Valérie Viet Triem Tong 1 Adel Bouhoula 2, 3 Mohammed Mejri 4
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 : It is a well known fact that only formal methods can provide a proof that a given system meets its requirements. For critical systems (e.g. nuclear reactors, aircraft), the use of these methods becomes mandatory. Electronic voting is also one of these critical systems since the stakes are important: democracy. In this context, we propose in this paper, the use of the ADM logic in order to specify security properties (fairness, eligibility, individual verifiability and universal verifiability) of electronic voting protocols. These properties are first specified in a general form, and then adapted to the FOO protocol as a case study. Our goal is to verify these properties against a trace-based model. The choice of the ADM logic is motivated by the fact that it offers several features that are useful for trace analysis. Moreover, the logic is endowed with a tableau-based proof system that leads to a local model checking which enables an efficient implementation.
Document type :
Conference papers
Complete list of metadatas
Contributor : Myriam Andrieux <>
Submitted on : Monday, January 5, 2009 - 11:13:50 AM
Last modification on : Tuesday, August 18, 2020 - 1:54:04 PM


  • HAL Id : hal-00349880, version 1



Mehdi Talbi, Benjamin Morin, Valérie Viet Triem Tong, Adel Bouhoula, Mohammed Mejri. Specification of Electronic Voting Protocol Properties Using ADM Logic : FOO Case Study. ICICS 08, Oct 2008, Birmingham, United Kingdom. ⟨hal-00349880⟩



Record views