https://www.dagstuhl.de/01391

23. – 28. September 2001, Dagstuhl-Seminar 01391

Specification and Analysis of Secure Cryptographic Protocols

Organisatoren

David Basin (ETH Zürich, CH)
Grit Denker (SRI – Menlo Park, US)
Gavin Lowe (University of Oxford, GB)
Jonathan K. Millen (SRI – Menlo Park, US)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team

Dokumente

Teilnehmerliste
Dagstuhl-Seminar-Report 321

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)?

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.