Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC) | springerprofessional.de

Register Login

Springer Professional

JAVASCRIPT NEEDED

Please enable JavaScript on your browser, so that you can use all features of this website.

window.dataLayer = window.dataLayer || []; window.dataLayer.push({ 'event': 'track', 'eventCategory': 'flash_warning', 'eventAction': 'Javascript needed', 'eventLabel': 'Please enable JavaScript on your browser, so that you can use all features of this website.' });

Top

Hint

Swipe to navigate through the chapters of this book

Published in:

Read chapter Read first chapter

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

Login to get access

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.

Advertisement

previous chapter hacspec: Towards Verifiable Crypto Standards

next chapter Experimental Evaluation of Attacks on TESLA-Secured Time Synchronization Protocols

See also Figures 1 and 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.

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.

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].

1.

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

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)

3.

Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: Proverif 2.00: automatic cryptographic protocol verifier, user manual and tutorial (2018)

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)

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). https://doi.org/10.1007/978-3-540-45146-4_24 CrossRef

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)

7.

Blanchet, B.: Cryptoverif: Computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl seminar Formal Protocol Verification Applied, vol. 117 (2007)

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)

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). https://doi.org/10.1007/978-3-642-39799-8_48 CrossRef

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)

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). https://doi.org/10.1007/3-540-45708-9_10 CrossRef

12.

Jim Schaad, A.C.: CBOR object signing and encryption (COSE) (2010). https://tools.ietf.org/html/rfc8152. Accessed 10 May 2018

13.

Bormann, C.: Concise binary object representation (CBOR) (2013). https://tools.ietf.org/html/rfc7049. Accessed 10 May 2018

14.

Krawczyk, D.H., Eronen, P.: HMAC-based Extract-and-Expand Key Derivation Function (HKDF). RFC 5869 (2010)

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) MathSciNetMATH

16.

Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983) MathSciNetCrossRef

17.

Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends Priv. Secur. 1, 1–135 (2016) CrossRef

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)

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)

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
Publisher: Springer International Publishing
Book: Security Standardisation Research
Print ISBN: 978-3-030-04761-0

Electronic ISBN: 978-3-030-04762-7

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-04762-7_2

Premium Partner

Version: 0.2014.0