The Computer Journal Advance Access published online on June 14, 2007
The Computer Journal, doi:10.1093/comjnl/bxm019
| ||||||||||||||||||||||||||||||||||||||||||||||||||
A Proof of Revised Yahalom Protocol In the Bellare and Rogaway (1993) Model1
Australian Institute of Criminology, GPO Box 2944 Canberra, ACT 2601, Australia
* Corresponding author: raymond.choo{at}aic.gov.au
Received 23 June 2006; revised 24 January 2007
Although the Yahalom protocol, proposed by Burrows, Abadi, and Needham in 1990, is one of the most prominent key establishment protocols analysed by researchers from the computer security community (using automated proof tools), a simplified version of the protocol is only recently proven secure by Backes and Pfitzmann [(2006) On the Cryptographic Key Secrecy of the Strengthened Yahalom Protocol. Proc. IFIP SEC 2006] in their cryptographic library framework. We present a protocol for key establishment that is closely based on the Yahalom protocol. We then present a security proof in the Bellare, M. and Rogaway, P. [(1993a). Entity Authentication and Key Distribution. Proc. of CRYPTO 1993, Santa Barbara, CA, August 2226, LNCS, Vol. 773, pp. 110125. Springer-Verlag, Berlin] model and the random oracle model. We also observe that no partnering mechanism is specified within the Yahalom protocol. We then present a brief discussion on the role and the possible construct of session identifiers (SIDs) as a form of partnering mechanism, which allows the right session key to be identified in concurrent protocol executions. We then recommend that SIDs should be included within protocol specification rather than consider SIDs as artefacts in protocol proof.
Key Words: Key establishment protocol provable security cryptographic protocol