Congratulations to Yannick Chevalier on winning the LICS Test-of-Time Award 2023

Logo de la conférence LICS (Logic in Computer Science)

Yannick Chevalier, UT3 Senior Lecturer in the AI Department – LILaC team, has received the LICS Test-of-Time Award 2023 for his paper “An NP Decision Procedure for Protocol Insecurity with XOR”. This publication was co-authored with Ralf Küsters from the University of Stuttgart, Michaël Rusinowitch and Mathieu Turuani (Loria, INRIA). This prize was awarded jointly to the article “Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or” by Hubert Comon-Lundh and Vitaly Shmatikov on the same theme, and to the article “Tractable conservative Constraint Satisfaction Problems” by Andrei Bulatov.

The LICS – Logic in Computer Science conference is the most prestigious annual forum on theoretical and practical topics in computer science related to logic in the broadest sense. The LICS Test-of-Time Award honours a small number of papers from the LICS proceedings of the last twenty years that have best stood the “test of time”. That is, the article in question dates from LICS 2002 and was considered this year. In selecting these papers, the Awards Committee takes into account the influence they have had since their publication. Because of the fundamental nature of LICS work, the impact is often not felt immediately, hence the twenty-year perspective.

 

Résumé en anglais de la publication : 

We provide a method for deciding the insecurity of cryptographic protocols in presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we obtain that protocol insecurity is in NP for an intruder that can exploit the properties of the XOR operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).