20 years after publication, the paper "An NP Decision Procedure for Protocol Insecurity with XOR" has now been awarded a Test-of-Time Award at the ACM/IEEE Symposium on Logic in Computer Science (LICS 2023). The authors of the work, which was honoured on 29 June 2023 in Boston, include Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch and Mathieu Turuani.
The decision was based on progress made by the researchers in protocol verification with additional operators, in particular XOR, which is widely used in practical applications. The researchers shared the Test-of-Time Award with the thematically similar paper "Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or" by Hubert Comon-Lundh and Vitaly Shmatikov.
According to the jury, both papers have not only definitively settled the complexity issues under consideration. In addition, the lasting value of this line of work was demonstrated by mature verification tools such as ProVerif, Tamarin, Maude-NPA, and CPSA.
