in Proceedings of 21st IFIP International Information Security Conference (SEC), pp. 233-245, May 2006.
Symbolic secrecy of exchanged keys is arguably one of the most important notions of secrecy shown with automated proof tools. It means that an adversary restricted to symbolic operations on terms can never get the entire key into its knowledge set. Cryptographic key secrecy essentially means computational indistinguishability between the real key and a random one, given the view of a much more general adversary. We analyze the cryptographic key secrecy for the strengthened Yahalom protocol, which constitutes one of the most prominent key exchange protocols analyzed symbolically by means of automated proof tools. We show that the strengthened Yahalom protocol does not guarantee cryptographic key secrecy. We further show that cryptographic key secrecy can be proven for a slight simplification of the protocol by exploiting recent results on linking symbolic and cryptographic key secrecy in order to perform a symbolic proof of secrecy for the simplified Yahalom protocol in a specific setting that allows us to derive the desired cryptographic key secrecy from the symbolic proof. The proof holds in the presence of arbitrary active attacks provided that the protocol is relying on standard provably secure cryptographic primitives.
This publication is accompanied by links to downloadable versions of this publication. These documents do not necessarily correspond exactly to the cited version. Instead, in most cases full or updated versions are provided. For access to the official version, follow the "Official version" link to the publishers site.