Computer Science Department
School of Computer Science, Carnegie Mellon University
Deriving Key Distribution Protocols
Iliano Cervesato*, Catherine Meadows**, Dusko Pavlovic***
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.
*Qatar Campus, Carnegie Mellon University