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
- Date
- Monday, June 29 2009 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.