Description du sujet de thèse

Les façons de voter sont multiples. De nos jours cohabitent aussi bien les méthodes traditionnelles comme le vote postal ou le vote à l'urne tel qu'on le pratique en France, que des méthodes utilisant au moins en partie des ordinateurs, comme le vote par Internet ou bien les machines à voter. Les contraintes pratiques, mais aussi les habitudes, dictent quels types de vote seront acceptés en fonction du contexte.
Si le vote à l'urne présente de nombreux avantages, dont des propriétés de sécurité très satisfaisantes, le vote postal laisse à désirer en terme de transparence et de secret du vote. De même, les systèmes électroniques déployés en pratique sont souvent imparfaits.
Une des raisons de cet état des lieux est que le déploiement d'un système de vote, quel qu'il soit, est composé de multiples facettes, chacune comportant des détails pouvant nuire à la sécurité. Ces détails ne sont pas ou peu abordés dans les articles académiques présentant et analysant des protocoles théoriques. Ces dernières années, de plus en plus de systèmes de vote électronique déployés fournissent des données publiques permettant de les analyser, que ce soit des spécifications précises ou même le code source. Ceux-ci deviennent donc des objets d'étude, posant des défis pour les personnes souhaitant les analyser, de part leur grande complexité.

L'objectif de cette thèse est de se confronter à la réalité terrain du vote à distance, tout en mobilisant les ressources théoriques nécessaires à l'analyse. Les deux cibles principales seront le vote postal et le vote par Internet.
En ce qui concerne le vote postal, les mécanismes de sécurité restent souvent “opérationnels” (double, voire triple enveloppe, par exemple), et nécessitent une forte confiance tout au long de la chaîne de traitement du bulletin. L'objectif sera d'être force de proposition pour concevoir un protocole apportant des garanties supplémentaires de sécurité, sans perdre les avantages du vote postal : des personnes ne disposant pas ou ne souhaitant pas utiliser d'ordinateur ou de smartphone doivent pouvoir tout de même voter, quitte à ne pas profiter des améliorations de sécurité. Cette conception devra nécessairement s'accompagner de preuves de sécurité, qui seront effectuées dans le cadre des méthodes formelles, à l'aide de l'outil ProVerif ou Tamarin. Une des difficultés sera de modéliser des canaux de communications et des acteurs inhabituels par rapport aux études classiques en vote électronique. Au-delà des nouvelles propriétés de sécurité apportées, un des critères de succès sera la simplicité du protocole obtenu, aussi bien pour les électeurs que pour les organisateurs de l'élection.
Pour le vote par Internet, il s'agira de faire une analyse de sécurité du célèbre système de vote de la Poste Suisse, qui a été rendu public depuis bientôt 2 ans, et qui sera utilisé pour des élections politiques dans certains Cantons à partir de cet été. Ce système jouit d'une très bonne réputation en terme de qualité de la description de son fonctionnement. La spécification est complète et publique, ainsi que le code source de la plupart des composants. Des preuves de sécurité ont été effectuées, afin d'entrer en conformité avec la réglementation fédérale suisse qui est très exigeante. Toutefois, ces preuves s'appuient sur la spécification. Or la mise en œuvre dans le code est nécessairement différente. Un objectif de la thèse sera de proposer une analyse de sécurité en partant directement du code. Les défis seront de plusieurs ordres. Tout d'abord il s'agira de décider à quel point la modélisation peut se faire automatiquement ou du moins semi-automatiquement. Un autre souci sera d'utiliser les outils de preuves formelles comme ProVerif dans un contexte inhabituel, où un très grand nombre de processus vont être en concurrence, pour rendre compte de la complexité du code. Une dernière contrainte sera de rendre ce travail facilement adaptable aux évolutions du protocole, car celui-ci est encore récent et risque de beaucoup bouger dans les années à venir. Il est important de pouvoir refaire l'analyse de sécurité sur les versions ultérieures.
Il est attendu que ces deux travaux, vote postal et analyse du système Suisse, ouvrent de nouvelles perspectives et le sujet de thèse sera adapté en fonction de celles-ci, ainsi que de l'évolution du contexte des recherches. Par exemple, une piste que l'on gardera en tête est la possibilité de mener une analyse similaire à celle effectuée pour le système Suisse, appliquée à d'autres systèmes dont le code source deviendrait ouvert afin de se conformer à des exigences de transparence.

Contexte de travail

La thèse sera effectuée au sein des équipes Pesto et Caramba du LORIA. Les encadrants ont étudié de nombreux systèmes de vote en France (contrats industriels avec les leaders du marché) ou à l'étranger (systèmes du canton de Genève, de l'entreprise Scytl, de la ville de Moscou, de la Poste Suisse), aussi bien sur des aspects théoriques (prouver les bonnes propriétés ; découvrir des failles), que pratiques (compromis entre faisabilité pratique et élégance académique).

Le poste se situe dans un secteur relevant de la protection du potentiel scientifique et technique (PPST), et nécessite donc, conformément à la réglementation, que votre arrivée soit autorisée par l'autorité compétente du MESR.

Contraintes et risques

ras