TOP
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
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 01391

Specification and Analysis of Secure Cryptographic Protocols

( Sep 23 – Sep 28, 2001 )

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/01391

Organizers



Summary

Cryptographic protocols are the cornerstone of secure electronic communication, banking, and commerce. By providing functions like key management in distributed systems, individual and group authentication, anonymity, fair exchange, and policy negotiation, they support a spectrum of secure online activities such as financial account transactions, distributed sealed-bid auctions and their escrow services, voting, distributed and federated database access, and virtual private networks.

Designing cryptographic protocols is difficult. Cryptographic protocols are vulnerable to message modification attacks and it is surprisingly difficult to get even small protocols right. Moreover, their complexity is steadily increasing and it is nontrivial to compose or extend smaller protocols to more complex ones. Formal methods have proven helpful for both cryptographic protocol design and analysis. The use of formal languages, including state machines, epistemic logics, and process algebras, supports the rigorous formalization of protocol models and their properties. Moreover, they provide a basis for using tools such as model checkers and theorem-provers to prove protocols correct or uncover security flaws.

The goal of this seminar was to bring together experts from the formal methods and security communities to study and compare existing modeling and analysis techniques and tools for cryptographic protocols, focusing on the following topics:

  1. identifying and formalizing appropriate and practical security goals and security protocol analysis techniques,
  2. classifying and comparing existing modeling techniques and formalisms, and
  3. comparing existing tools, identifying the most urgent needs to integrate formal methods into real world protocol design, and suggesting future directions for tool design.

There are many questions and unresolved issues associated with each of these topics.

Regarding (1), security goals include message and entity authentication, secrecy, anonymity, integrity, non-repudiation, fair exchange, agreement, and denial of service resistance. There is currently no commonly accepted formal model of all of these and it is not even clear if this list is complete. Additional questions include: Which tool or analysis technique best supports which kind of goals? What is the relationship between formalizations of goals in different frameworks? Which protocol technique can handle "weak secrets," i.e., secrets that can be revealed by guessing? What security goals are essential in group communication applications? In this seminar we aim to identify commonly understood security goals and security protocol techniques and means to link goals with appropriate verification tools.

Regarding (2), currently many different techniques are used for modeling, e.g., event-based approaches using knowledge and belief logic abstractions, agent-based approaches modeling protocol processes using multiset rewriting, process algebra based approaches, and the strand space approach. How do these models differ? Natural candidates for a classification scheme are: synchronous versus asynchronous communication, complexity, decidability, practicability, which class of cryptographic protocols can be modeled (point-to-point, group communication, etc.), which cryptographic and other computations are supported, which analysis techniques are supported, and what is the scope, extensibility, and reusability of the modeling formalism. Heuristics and transformations play a role here too: how can protocols and their models be safely transformed to bring them within the reach of current tools (e.g., reduced to small finite-state programs that can be model checked)?

Regarding (3), more sophisticated tools are required if protocol designers are to use them for real world problems. To what extent can tools scale that are based on (potentially infinite) state enumeration, finite state model checking, or automated (or interactive) theorem proving? In automated approaches, heuristics often play an important role in incorporating domain knowledge about particular protocols into the search process. Tool design issues include: how can the performance of heuristics be enhanced by exploiting knowledge about the protocol, message formats or attacker behavior in a rigorous way? Can heuristics be designed in a general, reusable style but still amenable to optimization? Finally, how can model checkers and theorem provers fruitfully interact with each other (e.g., the use of theorem provers to verify abstractions for model checking)?


Participants
  • Rafael Accorsi (Universität Freiburg, DE) [dblp]
  • Roberto Amadio (University of Marseille, FR)
  • Alessandro Armando (University of Genova, IT) [dblp]
  • Tuomas Aura (Microsoft Research UK - Cambridge, GB)
  • David Basin (ETH Zürich, CH) [dblp]
  • Mike Bond (University of Cambridge, GB)
  • Iliano Cervesato (ITT Inc. - Alexandria, US) [dblp]
  • Ernie Cohen (Microsoft Corporation - Redmond, US) [dblp]
  • Jorge R. Cuéllar (Siemens AG - München, DE) [dblp]
  • Grit Denker (SRI - Menlo Park, US) [dblp]
  • Nancy Durgin (Stanford University, US)
  • Michael Goldsmith (Formal Systems Ltd. - Oxford, GB)
  • Dieter Gollmann (TU Hamburg-Harburg, DE) [dblp]
  • Dieter Hutter (DFKI - Saarbrücken, DE)
  • Bart Jacobs (Radboud University Nijmegen, NL) [dblp]
  • Peeter Laud (University of Tartu, EE)
  • Gavin Lowe (University of Oxford, GB)
  • Catherine Meadows (NRL - Washington, US)
  • Jonathan K. Millen (SRI - Menlo Park, US)
  • Sebastian Mödersheim (Universität Freiburg, DE)
  • David Monniaux (CNRS / ENS - Paris, FR) [dblp]
  • Lawrence Paulson (University of Cambridge, GB) [dblp]
  • Andreas Pfitzmann (TU Dresden, DE)
  • Michaël Rusinowitch (INRIA Lorraine - Nancy, FR)
  • André Scedrov (University of Pennsylvania - Philadelphia, US)
  • Vitaly Shmatikov (SRI - Menlo Park, US) [dblp]
  • Scott D. Stoller (SUNY - Stony Brook, US)
  • Carolyn L. Talcott (SRI - Menlo Park, US) [dblp]
  • Luca Vigano (ETH Zürich, CH) [dblp]
  • Dennis Volpano (Cranite Systems, Inc., US)
  • Christoph Walther (TU Darmstadt, DE)
  • Thomas Wilke (Universität Kiel, DE) [dblp]
  • Irfan Zakiuddin (DERA - Malvern, GB)