Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
hacspec: Towards Verifiable Crypto Standards 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

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

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




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

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




Jetzt Wissensvorsprung sichern!

inform now
previous chapter hacspec: Towards Verifiable Crypto Standards
next chapter Experimental Evaluation of Attacks on TESLA-Secured Time Synchronization Protocols
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
1.
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.
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.
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.
12.
13.
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.
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)
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
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

    Image Credits