October 14 – 19 , 2007, Dagstuhl Seminar 07421

Formal Protocol Verification Applied


Liqun Chen (HP Lab – Bristol, GB)
Steve Kremer (ENS – Cachan, FR)
Mark D. Ryan (University of Birmingham, GB)

The Dagstuhl Foundation gratefully acknowledges the donation from:

  •   Microsoft Research, Cambridge, UK

For support, please contact

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
List of Participants


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.


  • Security / Cryptography
  • Semantics / Formal Methods
  • Verification / Logic


  • Security protocols
  • Formal verification
  • Trusted computing
  • Biometrics
  • Security of mobile computing
  • Electronic voting
  • Payment systems


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.