Formal Analysis Process

As a working group in the Security area of the Internet Engineering Task Force (IETF), LAKE is particularly attentive to inputs coming from the formal analysis community. The group requests and welcomes formal analysis to be performed on the documents that introduce cryptographically-relevant changes or additions to the EDHOC protocol.

The goal of the formal analysis on a protocol is to understand the security properties it provides. Specifically in the context of LAKE, we would like to ensure:

• Preservation of the security properties already proven for EDHOC, discussed in Section 9.1 of RFC9528.

• Assurance that the extensions to EDHOC satisfy new security goals.

History of Formal Analysis in LAKE

Different versions of EDHOC underwent formal analysis studies. The main bulk of this process happened between November 2021 and May 2022, when the EDHOC specification was declared ready for formal analysis and "frozen" from changes. Authors of studies were invited to present their findings to the working group during the IETF 113 and IETF 114 meetings. Each study contributed to the EDHOC specification, which was later updated to mitigate the vulnerabilities found, resulting in RFC9528, published in March 2024.

Process

The working group follows the formal analysis process it established during the standardization of the base EDHOC protocol, also for EDHOC extensions. Only adopted working group documents are concerned. In coordination with the document authors, the working group chairs trigger the call for formal analysis on a document by sending an email to the working group mailing list, announcing the period during which authors are asked to withhold any changes to the Internet Draft. This is to make sure that the authors of the formal study work on the latest version of the specification. In parallel, the chairs will typically reach out to the already established list of contributors soliciting formal analysis.

Contact

If you are interested in contributing to the formal analysis process of some of the LAKE documents, please express interest by sending an email to lake-chairs@ietf.org.

Resources

See Resources

Past Contributors

(in alphabetic order)

• Alessandro Bruni

• Baptiste Cottier

• Felix Günther

• Marc Ilunga

• Charlie Jacomme

• Thorvald Sahl Jørgensen

• Elise Klein

• Steve Kremer

• Karl Norrman

• David Pointcheval

• Maïwenn Racouchot

• Carsten Schürmann

• Vaishnavi Sundararajan