Penn Arts & Sciences Logo

Tuesday, November 11, 2003 - 12:15pm

Ralf Kuesters

Stanford

Location

University of Pennsylvania

315 Levine

Operators such as XOR and Diffie-Hellman exponentiation are frequently used in cryptographic protocols. However, most formal methods for analyzing cryptographic protocols cannot handle these operators. In particular, up until recently deciding the security of protocols in presence of XOR and Diffie-Hellman exponentiation has been an open problem. In this talk, I first provide a brief overview of the various approaches for the analysis of cryptographic protocols and introduce the standard Dolev-Yao model---the protocol and intruder model most methods for the (semi-)automatic analysis of protocols are based on. I then extend the Dolev-Yao model to include XOR and Diffie-Hellman exponentiation, respectively, and illustrate that within the resulting models new attacks on realistic protocols can be found. Finally, I present the main result which says that deciding the insecurity of protocols in these models is NP-complete. The talk is based on joint work with Yannick Chevalier, Michael Rusinowitch, and Mathieu Turuani (INRIA, France) published in LICS 2003 and FSTTCS 2003.