TR-241: Extending Cryptographic Logics of Belief to Key Agreement Protocols

Abstract

The authentication logic of Burrows, Abadi and Needham (BAN) provided an important step towards rigourous analysis of authentication protocols, and has motivated several subsequent refinements. We propose extensions to BAN-like log­ics which facilitate, for the first time, examination of public-key based authenticated key establishment protocols in which both par­ties contribute to the derived key (i.e. key agreement protocols). Attention is focussed on six distinct generic goals for authenticated key establishment protocols. The extended logic is used to analyze three Diffie-Hellman based key agreement protocols, facilitating direct comparison of these protocols with respect to formal goals reached and formal assumptions required.