Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices.

IETF is standardizing a key establishment protocol named EDHOC for constrained IoT devices. In contrast to more powerful IoT devices, such as web cameras and cars, which receive most attention from media, constrained devices often have severe restrictions on energy consumption. Additionally, they often use specialized wireless communication links with demanding constraints on message sizes, which may also vary between messages. EDHOC was first formally analyzed by Bruni et. al. Since then, the protocol has been significantly extended and is now a framework with a number of cryptographic cores, called methods. The initial version of EDHOC contained only two out of the current five 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 consequences of this.