Extended Formal Analysis of the EDHOC Protocol in Tamarin

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.