Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

2018 | OriginalPaper | Chapter

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

Authors: Alessandro Bruni, Thorvald Sahl Jørgensen, Theis Grønbech Petersen, Carsten Schürmann

Published in: Security Standardisation Research

Publisher: Springer International Publishing

share
SHARE

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.
Footnotes
1
See also Figures 1 and 2.
 
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].
 
Literature
2.
go back to reference 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) 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)
3.
go back to reference Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: Proverif 2.00: automatic cryptographic protocol verifier, user manual and tutorial (2018) Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: Proverif 2.00: automatic cryptographic protocol verifier, user manual and tutorial (2018)
4.
go back to reference 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) 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)
6.
go back to reference 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) 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)
7.
go back to reference Blanchet, B.: Cryptoverif: Computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl seminar Formal Protocol Verification Applied, vol. 117 (2007) Blanchet, B.: Cryptoverif: Computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl seminar Formal Protocol Verification Applied, vol. 117 (2007)
8.
go back to reference 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) 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)
10.
go back to reference 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) 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)
14.
go back to reference Krawczyk, D.H., Eronen, P.: HMAC-based Extract-and-Expand Key Derivation Function (HKDF). RFC 5869 (2010) Krawczyk, D.H., Eronen, P.: HMAC-based Extract-and-Expand Key Derivation Function (HKDF). RFC 5869 (2010)
15.
go back to reference 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) MathSciNetMATH 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) MathSciNetMATH
16.
17.
go back to reference Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends Priv. Secur. 1, 1–135 (2016) CrossRef Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends Priv. Secur. 1, 1–135 (2016) CrossRef
18.
go back to reference 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) 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)
19.
go back to reference 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) 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)
Metadata
Title
Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)
Authors
Alessandro Bruni
Thorvald Sahl Jørgensen
Theis Grønbech Petersen
Carsten Schürmann
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-04762-7_2

Premium Partner