Work in this direction initially started in the security community but
recently there has been a tremendous progress thanks to contributions
from different automated reasoning communities, such as model checking,
resolution, planning, rewriting/narrowing, and higher-order theorem
proving. Moreover, there has been another wave of progress due to
research in applying non-classical logics, such as epistemic and belief
logics, to analyze protocols and their properties.
Based on this progress, a large number of formal methods and tools have
been developed that have been quite successful in determining strengths
and weaknesses of many protocols, i.e. in proving the correctness of the
protocols or in identifying attacks on them.
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.
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 techniques and
tools for automated 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.
Description
Context
Experience over the last twenty years has shown that, even assuming
perfect cryptography, the design of security protocols (or cryptographic
protocols, as they are sometimes called) is highly error-prone and that
conventional validation techniques based on informal arguments and/or
testing are not up to the task. It is now widely recognized that only
formal analysis can provide the level of assurance required by both the
developers and the users of the protocols. This is especially true not
only when one considers the simple academic protocols that have been
proposed as example applications for automated reasoning techniques and
tools (such as the Needham-Schroeder Public Key Protocol and the like),
but also when one tries to scale up these techniques and tools to
industrial-strength Internet security protocols (like Kerberos and IKE).
Outline
The tutorial aims to provide an introduction to the development and
application of automated techniques and tools for the formal
specification and analysis of Internet security protocols. To that end,
the tutorial will consist of two main modules.
Intended Audience
The tutorial aims to provide an introduction to the development and
application of automated techniques and tools for the formal
specification and analysis of Internet security protocols. Hence, no
prerequisite knowledge on computer security will be assumed.
There is no limitation to participation: the tutorial will be open to
all interested persons.
Presenters
Slides
Last modified: Thu Apr 7 14:15:45 CEST 2005