Sjouke Mauw (TU/e)

Operational semantics of security protocols

Starting point is the following observation by Roger Needham: "Security protocols are three-line programs that people still manage to get wrong." Therefore, it is imperative to use formal methods for the validation of security protocols. Throughout the last decade many tools and theories have been developed which support such formal validation. These tools have been applied successfully in showing deficiencies of protocols and proving protocols correct. However, we experienced that none of these theories supported us in full to rigorously proof properties of security protocols. This triggered our approach to define a formal (operational) semantics for security protocols, which is set up in such a way that it supports e.g. different intruder models.

After a short introduction to black-box security protocols, the presentation focuses on the modeling of a network of agents and an intruder. The behaviour of such a network is formally defined as a transition system. Properties of the protocol can be expressed formally as properties of the set of traces induced by the transition system.  

---

Last Version - $Revision: 1.1 $ / $Date: 2003/06/17 08:28:34 $
Maintained by Jaap-Henk Hoepman
Email: