In this paper, we present a formal analysis of EDHOC in an enhanced symbolic Dolev-Yao model using the Tamarin tool. We show that not all EDHOC methods satisfy the authentication notion injective of agreement, but that they all do satisfy a notion of implicit authentication, as well as Perfect Forward Secrecy (PFS) of the session key material. We identify other weaknesses to which we propose improvements. For example, a party may intend to establish a session key with a certain peer, but end up establishing it with another, trusted but compromised, peer. We communicated our findings and proposals to the IETF, which has incorporated some of these in newer versions of the IETF specification.
Authors:
Karl Norrman – Ericsson Research and KTH Royal Institute of Technology
Vaishnavi Sundararajan – University of California, Santa Cruz
Alessandro Bruni – IT University of Copenhagen
Presented at the 18th International Conference on Security and Cryptography (SECRYPT 2021), 6-8 July, 2021.