Extended Formal Analysis of the EDHOC Protocol in Tamarin

Alessandro Bruni, Karl Normann, Vaishnavi Sundararajan

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


Given how common IoT devices that use constrained resources are becoming today, the need of the hour is communication protocols which can operate securely under such limitations. For a few years, the Internet Engineering Task Force (IETF) has been working to standardize EDHOC, an authenticated key establishment protocol for such constrained IoT devices. The first version of EDHOC was proposed in 2016. In 2018, Bruni et al. [3] used the ProVerif tool [2] to formally analyze an early version of EDHOC, which had only two key establishment methods. By 2021, the protocol had been fleshed out much more, with multiple new key establishment methods, and this version was formally analyzed using the Tamarin prover [15] in [17]. In this paper, we build on that work, by modifying the model, analyzing some new properties, and discussing some aspects of the latest EDHOC specification. In particular, we extend the modeling in [17] with trusted execution environments (TEEs), modify the way we model XOR encryption, and in addition to the properties verified in [17], we verify weak post-compromise security (PCS) as well as the secrecy and integrity of some additional data used as part of the protocol.
Original languageEnglish
Title of host publicationExtended Formal Analysis of the EDHOC Protocol in Tamarin
Publication date2023
ISBN (Print)978-3-031-36839-4
ISBN (Electronic)978-3-031-36840-0
Publication statusPublished - 2023


  • Authenticated key establishment
  • Formal verification
  • Symbolic dolev-yao model
  • Protocols
  • IoT
  • Tamarin


Dive into the research topics of 'Extended Formal Analysis of the EDHOC Protocol in Tamarin'. Together they form a unique fingerprint.

Cite this