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.
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
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.