Vérification formelle des protocoles délimiteurs de distance - Application aux protocoles de paiement

Type de soutenance
Thèse
Date de début
Lieu
IRISA Rennes
Salle
Métivier (restreint)
Orateur
Alexandre DEBANT (EMSEC)
Sujet

L’essor des nouvelles technologies, et en particulier la Communication en Champ Proche (NFC), a permis l’apparition de nouvelles applications. Á ce titre, nous pouvons mentionner le paiement sans contact, les clefs mains libres ou encore les cartes d’abonnement dans les transports en commun. Afin de sécuriser l’ensemble de ces applications, des protocoles de sécurité, appelés protocoles délimiteurs de distance on été développés. Ces protocoles ont pour objectif d’assurer la proximité physique des appareils mis en jeu afin de limiter le risque d’attaque. Dans ce manuscrit, nous présentons diverses approches permettant une analyse formelle de ces protocoles. Dans ce but, nous proposons un modèle symbolique permettant une modélisation précise du temps ainsi que des positions dans l’espace de chaque participant. Nous proposons ensuite deux approches : la première développant une nouvelle procédure de vérification, la seconde permettant la ré-utilisation d’outils existants tels que Proverif. Tout au long de ce manuscrit, nous porterons une attention particulières aux protocoles de paiement sans contact.

Mot clés : méthode formelle, modèle symbolique, protocole cryptographique, protocole de paiement

Composition du jury
Bruno Blanchet, Directeur de recherche Inria, Paris, France (rapporteur)
Ioana Boureanu, Lecturer, University of Surrey, Royaume-Uni
Cas Cremers, Professeur, CISPA, Allemagne
Sjouke Mauw, Professeur, University of Luxembourg, Luxembourg (rapporteur)
David Pichardie, Professeur, École normale supérieure de Rennes, France
Stéphanie Delaune, Directrice de recherche CNRS, Rennes, France (encadrante)