Stéphanie Delaune, ERC Starting Grant 2016

Pour assurer la sécurité des échanges de nos informations, les systèmes s’appuient sur des protocoles de sécurité, censés satisfaire un certain nombre de paramètres : authentification, non traçabilité, anonymat… Mais ces protocoles ne sont pas adaptés aux spécificités des systèmes sans contact (voir Le paiement sans contact n’est pas sans risque). En effet, la distance physique, et les notions de temps et de distance sont essentielles dans les échanges avec du matériel sans contact, pour s’assurer que les informations sont bien adressées à la personne qui leur est destinée, et non à un autre dispositif alentour ! 

Jusqu’à maintenant, pour mesurer la distance entre deux éléments qui échangent, un message est envoyé et on estime le temps dans lequel on doit normalement recevoir une réponse. La seule parade proposée est ainsi le « time out » : une réponse arrivée trop tardivement pourrait indiquer que le dispositif avec lequel on échange n’est pas à proximité, et donc peut-être pas le bon. Mais cela laisse donc toute une marge de manœuvre pour un attaquant s’il se trouve à proximité, et si son matériel est suffisamment rapide.

Pour y remédier, Stéphanie Delaune travaille sur la vérification des protocoles cryptographiques pour les systèmes sans contact. À l’heure actuelle, les protocoles classiques décrivent uniquement les différentes actions des participants du protocole. Il est donc possible pour un attaquant de se substituer à un participant s’il fournit les bonnes réponses dans les délais impartis. Un premier travail est donc nécessaire pour réaliser une représentation plus fine des particularités du sans contact, et notamment des notions de temps et de distance. 

Mais le cœur du travail de la chercheuse, c’est la vérification, c’est-à-dire réaliser la preuve formelle, mathématique, du fonctionnement adéquat du protocole de sécurité. De la même façon que les protocoles ont besoin d’être particuliers pour s’adapter au sans contact, les outils de vérification de ces protocoles ont également besoin d’être adaptés. En effet, on ne peut pas tolérer un protocole qui fonctionne dans 99% des cas, car s’il y a une faille et qu’elle est découverte par un attaquant, il l’exploitera au maximum. Les failles peuvent parfois sembler minimes et même ne pas dévoiler directement des informations, mais cela constitue déjà une fragilité dans le système qui n’est pas acceptable (voir Passeport : la petite précision qui vous perdra). Il est donc nécessaire de modéliser le programme et de réaliser la preuve rigoureuse que le protocole assure bien le niveau de sécurité demandé en présence de tel ou tel attaquant. 

Ainsi, pour pouvoir prouver qu’un protocole est sûr, une technique consiste à représenter toutes les exécutions possibles du protocole (y compris en présence d’un attaquant). Comme si on déroulait un arbre de possibilités, un modèle mathématique va recenser l’ensemble des exécutions potentielles du protocole. Cet univers gigantesque de possibilités est représenté sous la forme d’un graphe pour vérifier que n’importe laquelle de ces exécutions couvre bien les paramètres attendus. 

Mais pour manipuler ces protocoles, plus complexes que pour les échanges standards, il est nécessaire de simplifier. Tout d’abord, il est utile de définir les éléments qui sont perceptibles par un attaquant, et ceux qui ne le sont pas et peuvent donc être supprimés. Est-ce important de faire l’analyse du protocole en estimant que plusieurs attaquants placés à différents endroits du réseau peuvent intervenir, ou un seul attaquant peut-il suffire ? Vérifier l’infinité des cas est impossible en terme de calcul, il est donc nécessaire de calculer le pire cas réaliste en fonction de chaque protocole. Cela permet ainsi de déterminer quelle est la situation la plus facile à étudier et qui ne rate pas d’attaque. 

Pour modéliser des propriétés du type respect de la vie privée (anonymat, non-traçabilité…), l’arbre des possibilités de toutes les exécutions possibles ne suffit pas. Il est nécessaire de le comparer à l’univers des possibles d’une situation idéale, en employant des équivalences. Pour s’assurer par exemple de la non-traçabilité d’un passeport, on compare la situation réelle (un passeport que j’utilise plein de fois) à une situation idéale pour vérifier ma propriété (un passeport à usage unique, et donc non traçable). Si les deux univers des possibles sont équivalents, c’est-à-dire indistinguable du point de vue de l’attaquant, alors la situation réelle est indistinguable de la situation idéale, et la propriété est vérifiée. La vérification des équivalences pour différentes propriétés selon les configurations est essentielle, mais le domaine est encore balbutiant. 

Enfin, au-delà de la conception, une part non négligeable du travail de Stéphanie Delaune se tourne également dans l’implémentation de ces découvertes. Elle souhaite ainsi proposer des principes généraux pour que les protocoles soient mieux conçus, mais aussi des correctifs aux protocoles défectueux. À partir de ces découvertes d’attaques et de vulnérabilités sur des objets sans contact, elle diffusera des bonnes pratiques à adopter pour avoir toutes les chances de concevoir un système sûr.