Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)

  • Alessandro BruniEmail author
  • Thorvald Sahl Jørgensen
  • Theis Grønbech Petersen
  • Carsten Schürmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11322)


Ephemeral Diffie-Hellman over COSE (EDHOC) [1] is an authentication protocol that aims to replace TLS for resource constrained Internet of Things (IoT) devices using a selection of lightweight ciphers and formats. It is inspired by the newest Internet Draft of TLS 1.3 [2] and includes reduced round-trip modes. Unlike TLS 1.3, EDHOC is designed from scratch, and does not have to support legacy versions of the protocol. As the protocol is neither well-known nor has been used in practice it has not been scrutinized to the extent it should be.

The objective of this paper is to verify security properties of the protocol, including integrity, secrecy, and perfect forward secrecy properties. We use ProVerif [3] to analyze these properties formally. We describe violations of specific security properties for the reduced round-trip modes. The flaws were reported to the authors of the EDHOC protocol.


  1. 1.
    Selander, G., Mattsson, J., Palombini, F.: Ephemeral Diffie-Hellman over cose (EDHOC) (2018). Accessed 10 May 2018
  2. 2.
    Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.3. Internet-Draft draft-ietf-tls-tls13-28, Internet Engineering Task Force (2018, Work in Progress)Google Scholar
  3. 3.
    Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: Proverif 2.00: automatic cryptographic protocol verifier, user manual and tutorial (2018)Google Scholar
  4. 4.
    Selander, G., Mattsson, J., Palombini, F., Seitz, L.: Object Security for Constrained RESTful Environments (OSCORE). Internet-Draft draft-ietf-core-object-security-13, Internet Engineering Task Force (2018, Work in Progress)Google Scholar
  5. 5.
    Krawczyk, H.: SIGMA: the ‘SIGn-and-MAc’ approach to authenticated Diffie-Hellman and its use in the IKE protocols. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 400–425. Springer, Heidelberg (2003). Scholar
  6. 6.
    Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy (SP), pp. 483–502. IEEE (2017)Google Scholar
  7. 7.
    Blanchet, B.: Cryptoverif: Computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl seminar Formal Protocol Verification Applied, vol. 117 (2007)Google Scholar
  8. 8.
    Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1773–1788. ACM (2017)Google Scholar
  9. 9.
    Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). Scholar
  10. 10.
    Meadows, C.: Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy, pp. 216–231. IEEE (1999)Google Scholar
  11. 11.
    Canetti, R., Krawczyk, H.: Security analysis of IKE’s signature-based key-exchange protocol. In: Yung, M. (ed.) CRYPTO 2002. LNCS, vol. 2442, pp. 143–161. Springer, Heidelberg (2002). Scholar
  12. 12.
    Jim Schaad, A.C.: CBOR object signing and encryption (COSE) (2010). Accessed 10 May 2018
  13. 13.
    Bormann, C.: Concise binary object representation (CBOR) (2013). Accessed 10 May 2018
  14. 14.
    Krawczyk, D.H., Eronen, P.: HMAC-based Extract-and-Expand Key Derivation Function (HKDF). RFC 5869 (2010)Google Scholar
  15. 15.
    Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: mobile values, new names, and secure communication. J. ACM 65, 1:1–1:41 (2018)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends Priv. Secur. 1, 1–135 (2016)CrossRefGoogle Scholar
  18. 18.
    Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), pp. 78–94. IEEE (2012)Google Scholar
  19. 19.
    Selander, G., Mattsson, J., Palombini, F.: Ephemeral Diffie-Hellman Over COSE (EDHOC). Internet-Draft draft-selander-ace-cose-ecdhe-09, Internet Engineering Task Force (2018, Work in Progress)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Alessandro Bruni
    • 1
    Email author
  • Thorvald Sahl Jørgensen
    • 1
  • Theis Grønbech Petersen
    • 1
  • Carsten Schürmann
    • 1
  1. 1.IT University of CopenhagenCopenhagenDenmark

Personalised recommendations