A comprehensive, formal and automated analysis of the EDHOC protocol

EDHOC is a key exchange proposed by IETF's Lightweight Authenticated Key Exchange (LAKE) Working Group (WG). Its design focuses on small message sizes to be suitable for constrained IoT communication technologies. In this paper we provide an in-depth formal analysis of EDHOC-draft version 12, taking into account the different proposed authentication methods and various options. For our analysis we use the SAPIC + protocol platform that allows to compile a single specification to 3 state-of-the-art protocol verification tools (PROVERIF, TAMARIN and DEEPSEC) and take advantage of the strengths of each of the tools. In our analysis we consider a large variety of compromise scenarios, and also exploit recent results that allow to model existing weaknesses in cryptographic primitives, relaxing the perfect cryptography assumption, common in symbolic analysis. While our analysis confirmed security for the most basic threat models, a number of weaknesses were uncovered in the current design when more advanced threat models were taken into account. These weaknesses have been acknowledged by the LAKE WG and the mitigations we propose (and prove secure) have been included in version 14 of the draft.

• This work was partly done while Charlie Jacomme was at the CISPA Helmholtz Center for Information Security.

then several drafts have been released and version 12 of the draft [21] was issued in October 2021. EDHOC is a publickey based authenticated Diffie Hellman (DH) key exchange protocol. It allows for different authentication methods, either based on signatures or static long-term DH keys. It also supports a specific version aiming at Post-Quantum security, replacing the DH key derivation by a Key Encapsulation Mechanism (KEM).

Automated, symbolic protocol analysis is a successful approach for finding attacks or proving their absence. The approach can be traced back to the seminal work of Dolev and Yao [12] at the beginning of the 80's. In the so-called Dolev-Yao model the attacker has complete control over the network and can eavesdrop, intercept and inject any messages. Cryptography is however treated in a rather abstract way, sometimes referred to as the perfect cryptography assumption, but this abstraction significantly eases automation of the verification. State-of-the-art verification tools, such as PROVERIF [6] and TAMARIN [20], are indeed able today to scale up to industrial-size, deployed protocols. They have in particular been used successfully to find weaknesses in early versions of the 5G standard [2] and actively assisted the standardization process of TLS 1.3 [4,10]. Following these successes of formal analysis, Vučinić et al. invite the formal analysis community to study the protocol and contribute the results in both the symbolic and the computational model in a short paper which summarizes the design of EDHOC [23].

Contributions. In this paper, we present a comprehensive formal analysis of the EDHOC protocol: we provide a detailed model of version 12 and perform an analysis that combines several recent developments in formal methods.

• Detailed models of the protocol, properties and primitives (Section 3). We provide a detailed formal specification of version 12 of EDHOC. Our models include the 4 possible authentication methods, the KEM based version, and several optional checks. We also formally state the security properties claimed by the designers, see How each PRK is computed is method dependent and summarized in Table 2. Meth. PRK 2e PRK 3e2m PRK 4x3m 0 kdf(G XY ) PRK 2e PRK 3e2m