The faithfulness of abstract protocol analysis: message authentication

Dolev and Yao initiated an approach to studying crypto-graphic protocols which abstracts from possible problems with the cryptography so as to focus on the structural as-pects of the protocol. Recent work in this framework has developed easily applicable methods to determine many se-curity properties of protocols. A separate line of work, initi-ated by Bellare and Rogaway, analyzes the way specic cryp-tographic primitives are used in protocols. It gives asymp-totic bounds on the risk of failures of secrecy or authentica-tion. 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 crypto-graphic primitives may diverge from the idealized model. We develop this method where the cryptographic primitives are based on Carter-Wegman universal classes of hash func-tions. This choice allows us to give specic quantitative bounds rather than simply asymptotic bounds. 1