| Symbolic verification of distance-bounding protocols : application to payment protocols (Vérification symbolique de protocoles de sécurité : le cas des protocoles délimiteurs de distance : application aux protocoles de paiement) Debant, Alexandre - (2020-11-17) / Universite de Rennes 1 - Symbolic verification of distance-bounding protocols : application to payment protocols
| |||
Langue : Anglais Directeur(s) de thèse: Delaune, Stéphanie Discipline : Informatique Laboratoire : IRISA Ecole Doctorale : MATHSTIC Classification : Informatique Mots-clés : Protocoles de sécurité, Méthodes formelles, Vérification automatique, protocoles délimiteurs de distance, protocole de paiement
| |||
Résumé : 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 carte 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 protocole cryptographique, protocole de paiement 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 parti- culières aux protocoles de paiement sans contact. Abstract : The rise of new technologies, and in particular Near Field Communication (NFC) tags, offers new applications such as contactless payments, key-less entry systems, transport ticketing... Due to their security concerns, new security protocols, called distance-bounding protocols, have been developed to ensure the physical proximity of the de- vices during a session. In order to prevent flaws and attacks, these protocols require formal verification. In this manuscript, we present several techniques that allow for an automatic verification of such protocols. To this aim, we first present a symbolic model which faithfully models time and locations. Then we develop two approaches : either ba- sed on a new verification procedure, or leveraging existing tools like Proverif. Along this manuscript, we pay a particular attention to apply our results to contactless payment protocols. | |||