Designing secure key exchange protocols

  • Colin Boyd
  • Wenbo Mao
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 875)


Protocols for authentication and key exchange have proved difficult to develop correctly despite their apparent simplicity in terms of the length and number of messages involved. A number of formal techniques have been developed to help analyse such protocols and have been useful in detecting errors. Nevertheless it is still difficult to be certain that a particular protocol is correct.

This paper explores a different approach; instead of analysing existing protocols the aim is to design protocols to be secure in the first place. A methodology is developed for designing key exchange protocols in a restricted way such that they must be correct according to a defined security criterion. The protocols are defined abstractly with the cryptographic operations specified only according to their basic functions. This allows the protocols to be made concrete in a variety of ways. A number of concrete protocols are presented, some of which appear novel and, at the same time, efficient in comparison with existing ones.


Cryptographic protocols key management authentication 


  1. 1.
    C.A.Boyd, Security Architectures using Formal Methods, IEEE Journal on Selected Areas on Communications, June 1993, pp. 694–701.Google Scholar
  2. 2.
    C.A.Boyd and W.Mao, On a Limitation of BAN logic, Proceedings of Eurocrypt 93, Springer-Verlag 1993.Google Scholar
  3. 3.
    M.Burrows, M.Abadi, and R.Needham, A Logic of Authentication, ACM Transactions on Computer Systems, Vol 8,1, February 1990, pp 18–36.CrossRefGoogle Scholar
  4. 4.
    D.W.Davies and W.L.Price, Security for Computer Networks, John Wiley and Sons, 1989.Google Scholar
  5. 5.
    W.Diffie and M.E.Hellman, New Directions in Cryptography, IEEE Transaction on Information Theory, IT-22, pp. 644–654, 1976.CrossRefGoogle Scholar
  6. 6.
    W.Diffie, P.C.VanOorschot and M.Wiener, Authentication and Authenticated Key Exchanges, Designs, Codes and Cryptography, 2, pp. 107–125 (1992).Google Scholar
  7. 7.
    L.Gong, R.Needham & R.Yahalom, Reasoning about Belief in Cryptographic Protocols Proceedings of the 1990 IEEE Computer Society Symposium on Security and Privacy, pp. 234–248, IEEE Computer Society Press, 1990.Google Scholar
  8. 8.
    L.Gong, Variations on the Themes of Message Freshness and Replay, IEEE Security Foundations Workshop, pp. 131–136, 1993.Google Scholar
  9. 9.
    L.Gong, Increasing Availability and Security of an Authentication Service, IEEE Journal on Selected Areas on Communications, June 1993, pp. 657–662.Google Scholar
  10. 10.
    C.B.Jones, Systematic Software Development Using VDM, Prentice-Hall, 1986.Google Scholar
  11. 11.
    W.Mao and C.A.Boyd Towards Formal Analysis of Security Protocols, IEEE Security Foundations Workshop, pp. 147–158, IEEE Press, 1993.Google Scholar
  12. 12.
    W.Mao and C.A.Boyd, On the use of Encryption in Cryptographic Protocols, Proceedings of 4th IMA Conference on Coding and Cryptography, to appear.Google Scholar
  13. 13.
    C.Meadows, A System for the Specification and Analysis of Key Management Protocols, Proceedings of the 1991 IEEE Computer Society Symposium on Security and Privacy, pp. 182–195, IEEE Computer Society Press, 1991.Google Scholar
  14. 14.
    R.M.Needham & M.D.Schroeder, Using Encryption for Authentication in Large Networks of Computers, Communications of the ACM, 21,12, December 1978, 993–999.CrossRefGoogle Scholar
  15. 15.
    D.M.Nessett, A Critique of the Burrows, Abadi and Needham Logic, ACM Operating Systems Review, 24,2, pp. 35–38, 1990.CrossRefGoogle Scholar
  16. 16.
    Dave Otway & Owen Rees, Efficient and Timely Mutual Authentication ACM Operating Systems Review, 21,1, pp. 8–10, 1987.CrossRefGoogle Scholar
  17. 17.
    R.Rivest, A.Shamir & L.Adleman, A Method for Obtaining Digital Signatures and Public Key Cryptosystems, Communications of the ACM, 21, pp. 120–126, 1978.CrossRefGoogle Scholar
  18. 18.
    M.E.Smid and D.K.Branstad, The Data Encryption Standard: Past and Future, Proceedings of the IEEE, 76,5, pp. 550–559, 1988.CrossRefGoogle Scholar
  19. 19.
    R.L.Rivest, The MD4 Message Digest Algorithm, Advances in Cryptology-CRYPTO '90, Springer-Verlag, 1991.Google Scholar
  20. 20.
    C.E.Shannon, Communication Theory of Secrecy Systems, Bell Systems Technical Journal, pp. 656–715, 1949.Google Scholar
  21. 21.
    G.J.Simmons, A Survey of Information Authentication, in Contemporary Cryptology, G.J.Simmons Ed., pp. 379–419, IEEE Press, 1992.Google Scholar
  22. 22.
    E.Snekkenes, Exploring the BAN Approach to Protocol Analysis, Computer Security Foundations Workshop, pp. 171–181, IEEE Press, 1991.Google Scholar
  23. 23.
    P.Syverson, The Use of Logic in the Analysis of Cryptographic Protocols, IEEE Symposium on Security and Privacy, pp. 156–170, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Colin Boyd
    • 1
  • Wenbo Mao
    • 1
  1. 1.Communications Research Group, Electrical Engineering LaboratoriesUniversity of ManchesterManchesterUK

Personalised recommendations