Automated Validation of Security Protocols

The AVASP'05 tutorial aims to provide an introduction to the development and application of automated reasoning techniques and tools for the formal specification and analysis of Internet security protocols. To that end, the tutorial will consist of two main modules.

The first module will be devoted to the introduction to Internet security protocols. This module will introduce the terminology and the basic concepts of security and cryptography and of security protocols. We will discuss simple security protocols, which provide the basis for the running examples considered throughout the tutorial, but we will also present some recent and current standardization discussions and efforts at the IETF and 3GPP to secure the new requirements for the Internet, such as IKE (Internet Key Exchange), Kerberos, Mobile-IP Security, UMTS AKA (Authenticated Key Agreement), and Multicast Streaming (for instance, continuous authentication of radio and TV Internet broadcasts).

The second module will survey the most significant automated reasoning techniques and tools for security protocol analysis. In particular, we will discuss the main techniques underlying model-checking and theorem proving approaches to the formal specification and analysis of security protocols. We will also briefly discuss complexity and (un)decidability results.

Presenters:

Date and Time: Sunday, April 3rd, 2005, all day

URL: http://www.avispa-project.org/avasp/avasp05-index.html