Refining Key Establishment

We use refinement to systematically develop a family of key establishment protocols using a theorem prover. Our development spans four levels of abstraction: abstract security properties, message-less guard protocols, protocols communicating over channels with security properties, and protocols secure with respect to a Dolev-Yao intruder. The protocols we develop are Needham-Schroeder Shared Key, the core of Kerberos 4 and 5, and Denning Sacco, and include realistic features such as key confirmation, replay caches, and encrypted tickets. Our development highlights that message-less guard protocols provide a fundamental abstraction for bridging the gap between security properties and message-based protocol descriptions. It also shows that the refinement approach presented in [SB10] can be applied, with minor adaption, to families of key establishment protocols and that it scales to protocols of nontrivial size and complexity.