TY - GEN
T1 - Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices
AU - Normann, Karl
AU - Sundararajan, Vaishnavi
AU - Bruni, Alessandro
PY - 2021
Y1 - 2021
N2 - Constrained IoT devices are becoming ubiquitous in society and there is a need for secure communication protocols that respect the constraints under which these devices operate. EDHOC is an authenticated key establishment protocol for constrained IoT devices, currently being standardized by the Internet Engineering Task Force (IETF). A rudimentary version of EDHOC with only two key establishment methods was formally analyzed in 2018. Since then, the protocol has evolved significantly and several new key establishment methods have been added. In this paper, we present a formal analysis of all EDHOC methods in an enhanced symbolic Dolev-Yao model using the Tamarin tool. We show that not all 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 standard.
AB - Constrained IoT devices are becoming ubiquitous in society and there is a need for secure communication protocols that respect the constraints under which these devices operate. EDHOC is an authenticated key establishment protocol for constrained IoT devices, currently being standardized by the Internet Engineering Task Force (IETF). A rudimentary version of EDHOC with only two key establishment methods was formally analyzed in 2018. Since then, the protocol has evolved significantly and several new key establishment methods have been added. In this paper, we present a formal analysis of all EDHOC methods in an enhanced symbolic Dolev-Yao model using the Tamarin tool. We show that not all 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 standard.
KW - Constrained IoT devices
KW - Secure communication protocols
KW - EDHOC
KW - Authenticated key establishment
KW - Tamarin tool
KW - Symbolic Dolev-Yao model
KW - Injective agreement
KW - Implicit authentication
KW - Perfect Forward Secrecy (PFS)
KW - IETF standardization
KW - Constrained IoT devices
KW - Secure communication protocols
KW - EDHOC
KW - Authenticated key establishment
KW - Tamarin tool
KW - Symbolic Dolev-Yao model
KW - Injective agreement
KW - Implicit authentication
KW - Perfect Forward Secrecy (PFS)
KW - IETF standardization
UR - https://arxiv.org/pdf/2007.11427.pdf
U2 - 10.48550/arXiv.2007.11427
DO - 10.48550/arXiv.2007.11427
M3 - Article in proceedings
BT - Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices
ER -