Subject: [Lake] EDHOC is ready for formal analysis

From: Mališa Vučinić <[email-masked]>
Date: Tue, 23 Nov 2021 17:00:00 +0100

Dear all,

(At IETF 112, we discussed kicking off a process that we hope will produce security analyses of EDHOC over the coming months. This mail describes that in a form suitable for people less familiar with the details of the working group.)

Back in October 2019, the IETF LAKE working group was chartered to work on a lightweight authenticated key exchange protocol for constrained Internet of Things environments. A deliverable of this standardization process, the EDHOC specification, underwent multiple revisions as an official IETF working group document. Different versions of the specification were implemented through 7 independent and interop-tested implementations, including those that specifically target low-end microcontrollers.

The EDHOC protocol is based on a well-studied SIGMA-I core. However, the additional static Diffie-Hellman authentication methods depart from the original SIGMA design. Based on the study in the symbolic model on an early version of the specification, we have good reason to believe that these additional methods are still secure. But before publishing a document as an Internet Standard, it is important to further raise the confidence of the community on its formal security aspects, which also includes the proofs in the computational model. Based on the discussion during the IETF 112 meeting, we believe that the version -12 of the specification is “ready for formal analysis” and we are launching a call to the teams and individuals outside of the working group to formally study the specification. In that sense, we are now “freezing” the specification at -12 and requesting the authors to withhold from publishing new versions of the draft until further notice.

In order to facilitate this process, Mališa has worked with the authors on an EDHOC primer published in the form of a preprint [1], which summarizes EDHOC and its expected security properties. The document also outlines the research questions we would like to have answers to. While the document is formally not a working group document, we would be happy to incorporate any feedback you might have in the next version.

Mališa and Stephen

[1] https://hal.inria.fr/hal-03434293/document <https://hal.inria.fr/hal-03434293/document>