Félicitations à Yannick Chevalier pour le LICS Test-of-Time Award 2023
Yannick Chevalier, Maître de Conférences UT3 au département IA – équipe LILaC, a reçu le LICS Test-of-Time Award 2023 pour l’article “An NP Decision Procedure for Protocol Insecurity with XOR“. Cette publication a été co-signée avec Ralf Küsters de l’Université de Stuttgart, Michaël Rusinowitch et Mathieu Turuani (Loria, INRIA). Ce prix a été remis conjointement à l’article “Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or” d’Hubert Comon-Lundh et Vitaly Shmatikov sur le même thème, ainsi qu’à l’article “Tractable conservative Constraint Satisfaction Problems” d’Andrei Bulatov.
La conférence LICS — Logic in Computer Science est le plus prestigieux forum annuel sur des sujets théoriques et pratiques en informatique liés à la logique au sens large. Le prix LICS Test-of-Time Award récompense un petit nombre d’articles tirés des actes du LICS des vingt dernières années qui ont le mieux résisté à “l’épreuve du temps”. C’est-à-dire que l’article en question date du LICS 2002 et a été pris en considération cette année. En sélectionnant ces articles, le comité d’attribution tient compte de l’influence qu’ils ont eue depuis leur publication. En raison de la nature fondamentale des travaux de la LICS, l’impact n’est souvent pas ressenti immédiatement, d’où la perspective de vingt ans.
Résumé de la publication :
Nous proposons une méthode pour déterminer l’insécurité des protocoles cryptographiques en présence de l’intrus standard de Dolev-Yao (avec un nombre fini de sessions) étendu avec des règles dites d’oracle, c’est-à-dire des règles de déduction qui satisfont à certaines conditions. Comme exemple de ce cadre général, nous obtenons que l’insécurité des protocoles est dans NP pour un intrus qui peut exploiter les propriétés de l’opérateur XOR. Cet opérateur est fréquemment utilisé dans les protocoles cryptographiques mais ne peut pas être traité dans la plupart des modèles de protocole. Nous appliquons également notre cadre à un intrus qui exploite les propriétés de certains modes de chiffrement tels que le chaînage de blocs de chiffrement (CBC).