The faithfulness of abstract protocol analysis: Message authentication^*

Issue title: ACM Conference on Computer and Communications Security, 2001

Guest editors: Sabrina De Capitani di Vimercati

Article type: Research Article

Authors: Guttman, Joshua D.^a | Thayer, F. Javier^a | Zuck, Lenore D.^b

Affiliations: [a] The MITRE Corporation, Bedford MA, USA. E-mail: [email protected], [email protected] | [b] New York University, NY, USA. E-mail: [email protected]

Note: [*] This work supported by the National Security Agency.

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.

DOI: 10.3233/JCS-2004-12603

Journal: Journal of Computer Security, vol. 12, no. 6, pp. 865-891, 2004