Skip to Main content Skip to Navigation
New interface
Conference papers

A comprehensive, formal and automated analysis of the EDHOC protocol

Charlie Jacomme 1 Elise Klein 2 Steve Kremer 2 Maïwenn Racouchot 2 
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : EDHOC is a key exchange proposed by IETF's Lightweight Authenticated Key Exchange (LAKE) Working Group (WG). Its design focuses on small message sizes to be suitable for constrained IoT communication technologies. In this paper we provide an in-depth formal analysis of EDHOC-draft version 12, taking into account the different proposed authentication methods and various options. For our analysis we use the SAPIC + protocol platform that allows to compile a single specification to 3 state-of-the-art protocol verification tools (PROVERIF, TAMARIN and DEEPSEC) and take advantage of the strengths of each of the tools. In our analysis we consider a large variety of compromise scenarios, and also exploit recent results that allow to model existing weaknesses in cryptographic primitives, relaxing the perfect cryptography assumption, common in symbolic analysis. While our analysis confirmed security for the most basic threat models, a number of weaknesses were uncovered in the current design when more advanced threat models were taken into account. These weaknesses have been acknowledged by the LAKE WG and the mitigations we propose (and prove secure) have been included in version 14 of the draft.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03810102
Contributor : Steve Kremer Connect in order to contact the contributor
Submitted on : Tuesday, October 11, 2022 - 10:29:30 AM
Last modification on : Tuesday, October 25, 2022 - 4:20:25 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03810102, version 1

Collections

Citation

Charlie Jacomme, Elise Klein, Steve Kremer, Maïwenn Racouchot. A comprehensive, formal and automated analysis of the EDHOC protocol. USENIX Security '23 - 32nd USENIX Security Symposium, Aug 2023, Anaheim, CA, United States. ⟨hal-03810102⟩

Share

Metrics

Record views

0

Files downloads

0