Top

previous chapter hacspec: Towards Verifiable Crypto Standards

next chapter Experimental Evaluation of Attacks on TESLA-Sec...

Hint

Swipe to navigate through the chapters of this book

2018 | OriginalPaper | Chapter

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

Read first chapter

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

Publisher: Springer International Publishing

Published in: Security Standardisation Research

» Get access to the full-text

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.

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

inform now

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 CrossRef

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

Book

Security Standardisation Research

Print ISBN: 978-3-030-04761-0

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

https://doi.org/10.1007/978-3-030-04762-7

DOI

https://doi.org/10.1007/978-3-030-04762-7_2

Authors:

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

Publisher

Springer International Publishing

Sequence number

Premium Partner

Image Credits