Conception et analyse formelle de protocoles de sécurité, une application au vote électronique et au paiement mobile

Les “smart-devices” tels les smartphones, tablettes et meme les montres ont ete largement democratises au cours de la derniere decennie. Dans nos societes occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arriere de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limites, en termes d’utilisation, a de la simple communication par SMS ou bien telephone, on se fie a eux pour stocker nos photos et donnees personnelles, ces dernieres parfois aussi critiques que des donnees de paiement bancaires, on gere nos contacts et finances, se connecte a notre boite mail ou un site marchand depuis eux. . . Des exemples recents nous fournissent d’ailleurs un apercu des tâches de plus en plus complexes que l’on confie a ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la societe Transport for London a lance sa propre application autorisant l’emulation d’une Oyster card et son rechargement pour emprunter son reseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordee par les groupes industriels et les utilisateurs grandit. Nous nous interessons ici aux protocoles cryptographiques qui definissent les echanges entre les outils et entites qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de securite (authentification mutuelle des agent, integrite des messages circulant, secret d’une valeur critique…). Moult exemples de la litterature et de la vie courante ont demontre que leur elaboration etait hautement vulnerable a des erreurs de design. Heureusement, des annees de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les methodes formelles font partie de ceux-la. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des donnees et primitives cryptographiques elles aussi modelisees comme des termes et fonctions abstraites. On met le protocole a l’epreuve face a un attaquant actif et on peut specifier mathematiquement les proprietes de securite qu’il est cense garantir. Ces preuves de securite peuvent etre automatisees grâce a des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultes lorsque l’on cherche a concevoir et prouver formellement la securite d’un protocole de niveau industriel reside dans le fait que ce genre de protocole est generalement tres long et doit satisfaire des proprietes de securite plus complexes que certains protocoles universitaires. Au cours de cette these, nous avons souhaite etudier deux cas d’usage : le vote electronique et le paiement mobile. Dans les deux cas, nous avons concu et prouve la securite d’un protocole repondant aux problematiques specifiques a chacun des cas d’usage. Dans le cadre du vote electronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous definissons l’ecosysteme dans lequel le protocole est execute et prouvons sa securite grâce a ProVerif. Belenios VS garantit la confidentialite du vote et le fait qu’un utilisateur puisse verifier que son vote a bien fait parti du resultat final de l’election, tout cela meme si l’outil utilise par le votant est sous le controle d’un attaquant. Dans le cadre du paiement, nous avons propose la premiere specification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter a l’ecosysteme de paiement deja existant pour etre largement deployable et que les couts de gestion, de developpement et de maintenance de la securite devait etre optimises