"Security protocols are three-line programs that people still manage to get wrong." This famous quote by the late Roger Needham clearly expresses that the design of security protocols is an error-prone activity. A security protocol is a communication protocol that establishes security properties, such as confidentiality and authentication. In current open communication environments like the Internet, such properties are a prerequisite for proper operation and trusted services. The purpose of the tutorial is to explain the basics of security protocol design and analysis.

We will discuss security protocols in their most abstract form and even take an abstract view on the underlying cryptographic primitives. This is called the "black box" approach to security protocols.

The tutorial aims at a wide audience, such as computer science students with an interest in security, scientific researchers who want to broaden their scope, researchers and developers from industry with responsibilities in the field of security. We don't presume particular initial knowledge of the audience. However, some prior exposure to specification languages and their formalization and to formal verification would be an advantage. The tutorial will not address topics from the field of cryptography.

The tutorial concentrates on the following questions: What is a (black box) security protocol? What does it mean for a security protocol to be correct? What is the underlying security model? Which possible attacks apply to security protocols? How to model an intruder? How can we verify correctness of security protocols? Which computer tools provide support in design and validation of security protocols? The tutorial mixes both formal and informal reasoning, with an emphasis on explaining the notions by means of examples. We will use Message Sequence Charts to express both security protocols and attacks on security protocols.

The tutorial day is divided into four sessions. Each session consists of a lecture (of about 60 to 90 minutes) and an exercise (taking about 15 to 30 minutes). There will be both pencil-and-paper exercises and computer-based exercises. Attendants will receive a set of handouts.

Session A. Security Protocol Basics

Session B. A Security Model

Session C. Security Protocol Verification

Session D. Formal models

• Exercise: simple verification by hand
  
• Choice of: BAN logic, strand spaces, operational semantics, process algebra
  
  

Sjouke Mauw (1961) is associate professor at the Eindhoven University of Technology (the Netherlands) and head of the Eindhoven Computer Science Security group. This is a small but rapidly expanding group performing research in the application of formal methods to computer security. He received his Master's degree in mathematics and his PhD degree in computer science from the University of Amsterdam. Sjouke Mauw has authored over 50 refereed research papers on the following topics: process algebra, algebraic specifications, Message Sequence Charts, distributed algorithms, testing, model checking, and security, which is his current research focus. He was member of a number of program committees and associate rapporteur for ITU study group 10 (now 17).

Cas Cremers received his MsC in Computer Science at the Eindhoven University of Technology. After graduation, he continued working as a PhD student at the university with Sjouke Mauw, as member of the recently formed ECSS group, which uses formal methods to reason about security problems. His current research focusses on semantics and model checking techniques for security protocols.

This tutorial will be held at the University of Ottawa, in the SITE building, on Tuesday, June 1st, 9:00-17:00. The registration form is available on-line. It is not necessary to register to the SAM'04 workshop in order to attend this tutorial.