Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices

The IETF is standardizing an authenticated key establishment (AKE) protocol named EDHOC for constrained IoT devices. In contrast to more powerful devices like web cameras and cars, which receive a lot of media attention, such devices operate under severe energy consumption and message size restrictions. EDHOC was first formally analyzed in 2018 by Bruni et al. Since then, the protocol has been significantly extended and now has three new key establishment methods. In this paper, we formally analyze all methods of EDHOC in a symbolic Dolev-Yao model, using the Tamarin verification tool. We show that the different methods provide sensible, but also rather heterogeneous security properties, and discuss various consequences of this. Our work has also led to improvements in the design and the specification of EDHOC.