Computer Science Colloquium
Justifying FormalMethod Abstractions of Cryptography  A provably secure DolevYao model
Birgit Pfitzmann
Intel Corporation
Friday, February 13, 2004 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 100121185
Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html
Hosts:
Yevgeniy Dodis dodis@cs.nyu.edu, (212) 9983084
Abstract
Many practically relevant cryptographic protocols like SSL/TLS use cryptographic primitives like signature schemes or encryption in a blackbox way, while adding many noncryptographic 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 DolevYao 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 noncryptographic aspects of such proofs are tedious and errorprone.
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 DolevYao 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 webmaster@cs.nyu.edu
