Spécification Formelle des propriétés des Protocoles de Vote au moyen de la Logique ADM
Abstract
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