Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 07421

Formal Protocol Verification Applied

( Oct 14 – Oct 19, 2007 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



The Dagstuhl Foundation gratefully acknowledges the donation from


Security protocols are a core part of distributed computing systems, and are part of our everyday life since they are used in web servers, email, mobile phones, bank transactions, etc. However, security protocols are notoriously difficult to get right. There are many cases of protocols which are proposed and considered secure for many years, but later found to have security flaws. Formal methods offer a promising way for automated security analysis of protocols. While there have been considerable advances in this area, most techniques have only been applied to academic case studies and security properties such as secrecy and authentication. The seminar brought together researchers deploying security protocols in new application areas, cryptographers, and researchers from formal methods who analyse security protocols. The interaction between researchers from these different communities aims to open new research topics, e.g., identify new security properties that need verification and refine abstractions of the abstract models of crytpographic primitives.

Because of the multi-disciplinary nature of the workshop, not all of the participants knew each other in advance. We devoted the first morning to five-minute introductions of ourselves and our areas of research, given by each participant (including those who did not later give a full talk). Additionally, we scheduled some tutorial talks on the first day in order to enable all of the participants to understand the relevant foundations. We had four tutorials from internationally renouned speakers, as follows:

  • Kenny Paterson: Introduction to Provable Security
  • Hubert Comon-Lundh: Introduction to Formal Methods Approach to Protocol Verification
  • Catuscia Palamidessi: Overview of Formal Approaches to Information-hiding
  • Ahmad-Reza Sadeghi: Tutorial on Security Protocols on Trusted Platforms

The seminar was sponsored by Microsoft Research Cambridge. A special dinner was held on Thursday evening to note this contribution.

The seminar has led to much extensive discussion among the participants during and after the event. Quite a few of the papers presented have now been published.

  • Frederik Armknecht (Ruhr-Universität Bochum, DE) [dblp]
  • Michael Backes (Universität des Saarlandes, DE) [dblp]
  • Karthikeyan Bhargavan (Microsoft Research UK - Cambridge, GB) [dblp]
  • Bruno Blanchet (ENS - Paris, FR) [dblp]
  • Rohit Chadha (University of Illinois - Urbana-Champaign, US)
  • Kostas Chatzikokolakis (Ecole Polytechnique - Palaiseau, FR)
  • Liqun Chen (HP Lab - Bristol, GB)
  • Hubert Comon-Lundh (AIST - Tokyo, JP)
  • Ricardo Corin (INRIA-MSR - Orsay, FR)
  • Cas Cremers (ETH Zürich, CH) [dblp]
  • Sandro Etalle (University of Twente, NL)
  • Cédric Fournet (Microsoft Research UK - Cambridge, GB) [dblp]
  • Andrew D. Gordon (Microsoft Research UK - Cambridge, GB) [dblp]
  • Francis Klay (France Telecom - Lannion, FR)
  • Steve Kremer (ENS - Cachan, FR) [dblp]
  • Ralf Küsters (Disney Research - Zürich, CH) [dblp]
  • Hans Löhr (Ruhr-Universität Bochum, DE)
  • Matteo Maffei (Universität des Saarlandes, DE) [dblp]
  • Antoine Mercier (ENS - Cachan, FR)
  • Sebastian Mödersheim (IBM Research - Zürich, CH)
  • Catuscia Palamidessi (Ecole Polytechnique - Palaiseau, FR) [dblp]
  • Kenneth G. Paterson (Royal Holloway University of London, GB) [dblp]
  • Eike Ritter (University of Birmingham, GB)
  • Carsten Rudolph (Fraunhofer SIT - Darmstadt, DE) [dblp]
  • Mark D. Ryan (University of Birmingham, GB) [dblp]
  • Peter Y. A. Ryan (Newcastle University, GB) [dblp]
  • Ahmad-Reza Sadeghi (Ruhr-Universität Bochum, DE) [dblp]
  • Pierre-Yves Schobbens (University of Namur, BE)
  • Matt Smart (University of Birmingham, GB)
  • Ben Smyth (University of Birmingham, GB)
  • Joe-Kai Tsay (University of Pennsylvania - Philadelphia, US)
  • Laurent Vigneron (LORIA & INRIA Nancy, FR)
  • Eugen Zalinescu (LORIA & INRIA Nancy, FR)

  • security / cryptography
  • semantics / formal methods
  • verification / logic

  • security protocols
  • formal verification
  • trusted computing
  • biometrics
  • security of mobile computing
  • electronic voting
  • payment systems