Deriving Key Distribution Protocols and their Security Properties

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