Deriving Key Distribution Protocols and their Security Properties
Abstract
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 time stamps 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 in [3]. The present document collects proofs omitted for space reasons and unpublished background material.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 04, 2006
- Accession Number
- ADA462541
Entities
People
- Catherine Meadows
- Dusko Pavlovic
- Iliano Cervesato
Organizations
- Carnegie Mellon University