Computer Science Colloquium

Justifying Formal-Method Abstractions of Cryptography - A provably secure Dolev-Yao model

Birgit Pfitzmann
Intel Corporation

Friday, February 13, 2004 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Colloquium Information:


Yevgeniy Dodis, (212) 998-3084


Many practically relevant cryptographic protocols like SSL/TLS use cryptographic primitives like signature schemes or encryption in a black-box way, while adding many non-cryptographic features. Such protocols are tricky; even seemingly very simple variants often turn out to be wrong. In the past, there were two entirely separate approaches at proving such protocols:

  • Formal methods offer the advantage of precise protocol descriptions and automatic tools for protocol analysis. However, they used unfounded idealizations of the real cryptographic primitives as term algebras, the Dolev-Yao model(s).
  • Cryptographic reduction proofs show that if one can break the protocol, then one can also break an underlying primitive with respect to its real cryptographic definition. This, however, had to be done by hand, and the non-cryptographic aspects of such proofs are tedious and error-prone.

It is clearly desirable to combine the advantages of these two approaches, i.e., tool support and cryptographic soundness. We show how we can cryptographically justify a variant of the Dolev-Yao model. It contains a significant set of different operators, and the correctness result holds under arbitrary attacks, in arbitrary surrounding protocols, and for arbitrary desired security properties.

top | contact