The authentication logic of Burrows, Abadi and Needham (BAN) provided an important step towards rigorous analysis of authentication protocols, and has motivated several subsequent refinements. We propose extensions to BAN-like logics which facilitate, for the first time, examination of public-key based authenticated key establishment protocols in which both parties 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.

Additional Metadata
Conference Proceedings of the 1st ACM Conference on Computer and Communications Security
Van Oorschot, P. (1993). Extending cryptographic logics of belief to key agreement protocols. In 1st ACM Conference on Computer and Communications Security (pp. 232–243).