Modélisation des propriétés d'anonymat dans le pi-calcul appliqué

Auteur: Stéphanie Delaune (LORIA, projet INRIA Cassis)

delaune@lsv.ens-cachan.fr

Travaux réalisés avec S. Kremer (LSV - ENS de Cachan) et M. Ryan (Université de Birmingham)

Le but du vote électronique est de se rapprocher du vote réel (et pourquoi pas de faire mieux) en transposant dans un environnement informatique cette manière de s'exprimer anonymement. Ces protocoles sont déjà très largement déployés bien qu'aucune vérification formelle d'un protocole de vote n'a été aujourd'hui complètement réalisée.

Un protocole de vote pour être utilisable en pratique doit satisfaire un certain nombre de propriétés parmi lesquelles :

- l'anonymat: personne ne doit être capable de faire le rapprochement entre un électeur et son vote,

- l'absence de reçu et la résistance à la coercition : aucun électeur ne doit être capable de prouver la manière dont il a voté afin d'éviter l'achat de vote et la coercition.

Des définitions informelles de ces propriétés existent dans la littérature, mais elles ne sont pas suffisamment précises pour permettre de réaliser une analyse formelle. Nous avons donc proposé, en utilisant l'équivalence observationnelle du pi-calcul appliqué, une modélisation élégante de ces propriétés. Je vous présenterai cette modélisation et je les illustrerai sur quelques protocoles issus de la littérature.