We apply the derivational method of protocol verification to key distribution protocols. This method assembles the security properties of a protocol by composing the guarantees offered by embedded fragments and patterns. It has shed light on fundamental notions such as challenge-response and fed a growing taxonomy of protocols. Here, we similarly capture the essence of key distribution, authentication timestamps and key confirmation. With these building blocks, we derive the authentication properties of the Needham-Schroeder shared-key and the Denning-Sacco protocols, and of the cores of Kerberos 4 and 5.

The main results of this research were obtained in 2003-04 and appeared at CSFW-18. The present document collects proofs omitted for space reasons and unpublished background material.

44 pages

*Qatar Campus, Carnegie Mellon University
**Naval Research Laboratory, Code 5543, Washington, DC 20375
***Kestrel Institute, 3260 Hillview Avenue, Palo Alto, CA 94304

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu