Automatic verification of unbounded security protocols

Yassine Lakhnech
VERIMAG, Grenoble
Friday, 21 February, 2003 (All day)

At the heart of any computer security system are security protocols, also called cryptographic protocols. The design and implementation of these protocols is an error prone activity. Moreover, most of the errors are not due to weakness in the cryptographic system but rather in the logic underlying the protocol. In other words, most of the errors remain even when assuming idealized cryptographic primitives. Defining a semantic model for security protocols and formally defining what "secrecy", " authentification" etc.. mean is a difficult task. Moreover, these protocols are infinite state systems: the intruder knowledge is unbounded, the number of sessions is unbounded, the size of messages is unbounded, the number of principals is unbounded, etc... In this talk, we will survey the main results concerning the modeling and verification of security protocols. In particular, we will explain a new automatic verification method for security protocols that is applicable to unbounded protocols.