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

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