LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

Using ProVerif to Analyze Protocols with XOR and Diffie-Hellman Exponentiation

 Ralf Küsters
Monday, June 29 2009 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Ralf Küsters (University of Trier, Germany)

ProVerif is one of the most successful tools for cryptographic protocol analysis. However, dealing with algebraic properties of operators such as the exclusive OR (XOR) and Diffie-Hellman exponentiation has been problematic.

In this talk, I will present an approach which enables ProVerif, and related tools, to analyze a large class of protocols that employ the XOR operator and Diffie-Hellman exponentiation.

The core of our approach is to reduce the derivation problem for Horn theories modulo algebraic properties of XOR/Diffie-Hellman exponentiation to a purely syntactical derivation problem for Horn theories. The latter problem can then be solved by tools such as ProVerif. Our reduction works for a large class of Horn theories, allowing to model a wide range of intruder capabilities and protocols. We implemented our reduction and, in combination with ProVerif, applied it in the automatic analysis of several state-of-the-art protocols that use XOR or Diffie-Hellman exponentiation.

This talk is based on joint work with Tomasz Truderung, published at CCS 2008 and CSF 2009.

About LSV