Spécification Formelle des propriétés des Protocoles de Vote au moyen de la Logique ADM - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

Spécification Formelle des propriétés des Protocoles de Vote au moyen de la Logique ADM

Résumé

L'usage des méthodes formelles dans le cadre de la vérification des protocoles cryptographiques n'est plus à démontrer. Ceci est d'autant plus important dans le cas particulier des protocoles de vote électronique étant donné les enjeux impliqués par les élections. Dans ce contexte là, nous proposons dans cet article d'utiliser la logique ADM afin de spécifier quatre propriétés des protocoles de vote électronique : équité, éligibilité, vérifiabilité individuelle et vérifiabilité universelle. Elles sont exprimées en premier lieu d'une manière générale, puis adaptées aus cas particulier du protocole FOO. L'objectif étant de vérifier ces propriétés par rapport à une trace représentant l'exécution d'un protocole. Le choix de la logique ADM est motivé par la fait qu'elle offre un certain nombre de modalités intéressantes pour l'analyse des traces. De plus, elle est accompagnée d'une sémantique opérationnelle définie sous forme d'un ensemble de règles, ce qui permet l'implémentation d'un outil automatisant la tache de la vérification formelle des propriétés
Fichier non déposé

Dates et versions

hal-00349883 , version 1 (05-01-2009)

Identifiants

  • HAL Id : hal-00349883 , version 1

Citer

Mehdi Talbi, Benjamin Morin, Valérie Viet Triem Tong, Adel Bouhoula, Mohammed Mejri. Spécification Formelle des propriétés des Protocoles de Vote au moyen de la Logique ADM. Conférence sur la sécurité des Architectures Réseaux et des Systèmes d'Information, Oct 2008, Loctudy, France. ⟨hal-00349883⟩
197 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More