Abstract
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.
This work was funded in part through the Danish Council for Strategic Research, Programme Comission on Strategic Growth Technologies under grant 10-092309. This publication was also made possible by NPRP grant NPRP 7-988-1-178 from the Qatar National Research Fund (a member of Qatar Foundation). The statements made herein are solely the responsibility of the authors.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
The original SIGMA-I protocol uses a message authentication code (MAC), and then encrypts the signature and the authentication code with a symmetric encryption scheme for identity protection and binding: the use of authenticated encryption here serves this combined purpose.
- 3.
As discussed in Sect. 2.2, draft 08 warns against the reuse of \( KID \), but does not prescribe a standard mechanism to avoid such reuse.
- 4.
The use of \(\mathbf {phase}\) is a ProVerif-specific extension to the Applied Pi-calculus, which intuitively disables a process in a later phase to interact with processes from previous phases, though the attacker’s information is carried through phases. For a more detailed description of how phases work, we refer to the ProVerif manual [3].
References
Selander, G., Mattsson, J., Palombini, F.: Ephemeral Diffie-Hellman over cose (EDHOC) (2018). https://tools.ietf.org/html/draft-selander-ace-cose-ecdhe-08. Accessed 10 May 2018
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)
Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: Proverif 2.00: automatic cryptographic protocol verifier, user manual and tutorial (2018)
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)
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). https://doi.org/10.1007/978-3-540-45146-4_24
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)
Blanchet, B.: Cryptoverif: Computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl seminar Formal Protocol Verification Applied, vol. 117 (2007)
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)
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). https://doi.org/10.1007/978-3-642-39799-8_48
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)
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). https://doi.org/10.1007/3-540-45708-9_10
Jim Schaad, A.C.: CBOR object signing and encryption (COSE) (2010). https://tools.ietf.org/html/rfc8152. Accessed 10 May 2018
Bormann, C.: Concise binary object representation (CBOR) (2013). https://tools.ietf.org/html/rfc7049. Accessed 10 May 2018
Krawczyk, D.H., Eronen, P.: HMAC-based Extract-and-Expand Key Derivation Function (HKDF). RFC 5869 (2010)
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)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983)
Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends Priv. Secur. 1, 1–135 (2016)
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)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Bruni, A., Sahl Jørgensen, T., Grønbech Petersen, T., Schürmann, C. (2018). Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC). In: Cremers, C., Lehmann, A. (eds) Security Standardisation Research. SSR 2018. Lecture Notes in Computer Science(), vol 11322. Springer, Cham. https://doi.org/10.1007/978-3-030-04762-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-04762-7_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-04761-0
Online ISBN: 978-3-030-04762-7
eBook Packages: Computer ScienceComputer Science (R0)