Denis Lugiez (CMI), Symbolic Constraint Solving for Cryptographic Protocols

The verification of cryptographic protocols in the formal approach - the so-called Dolev-Yao model-, relies on the resolution of a particular notion of deducibility constraints. This successful approach has been enriched by adding several axioms which aim at a better modelization of the cryptographic primitives. In this talk, we show how to solve the deducibilty constraints in the case of an exclusive or operation (widely used in cryptographic protocols) combined with a homomorphism operation (that can model en encryption mechanism). We show how an algebraic notion like independence of vectors is the key to the solution of the problem and provides a clean tool for solving the complex deducibility constraints that arise in the problem. Joint work with S. Delaune, P. Lafourcade and R. Treinen (LSV, Ens Cachan)