|
The Faithfulness of Abstract Protocol Analysis: Message Authentication
2004 Award Winner
Joshua D. Guttman, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
Lenore D. Zuck
ABSTRACT
Dolev and Yao initiated an approach to studying cryptographic protocols
which abstracts from possible problems with the cryptography
so as to focus on the structural aspects of the protocol. Recent work in
this framework has developed easily applicable methods to determine
many security properties of protocols. A separate line of work, initiated
by Bellare and Rogaway, analyzes the way specific cryptographic
primitives are used in protocols. It gives asymptotic bounds on the
risk of failures of secrecy or authentication.
In this paper we show how the Dolev-Yao model may be used for
protocol analysis, while a further analysis gives a quantitative bound
on the extent to which real cryptographic primitives may diverge from
the idealized model. We illustrate this method where the cryptographic
primitives are based on Carter-Wegman universal classes of hash functions.
This choice allows us to give specific quantitative bounds rather
than simply asymptotic bounds.
» Download Paper [PDF, 296KB]
Publication
Copyright ©2004. Reprinted from Journal of Computer Security, Vol. 12, pp. 865–891, with permission from IOS Press.
Additional Search Keywords
n/a
|
