# Scrutinizing the Vulnerability of Ephemeral Diffie–Hellman over COSE (EDHOC) for IoT Environment Using Formal Approaches

Authors: Jiyoon Kim; Daniel Gerbi Duguma; Sangmin Lee; Bonam Kim; JaeDeok Lim; Ilsun You
Journal: Mobile Information Systems
 (2021)

---

## Abstract

Most existing conventional security mechanisms are insufficient, mainly attributable to their requirements for heavy processing capacity, large protocol message size, and longer round trips, for resource-intensive devices operating in an Internet of Things (IoT) context. These devices necessitate efficient communication and security protocols that are cognizant of the severe resource restrictions regarding energy, computation, communication, and storage. To realize this, the IETF (Internet Engineering Task Force) is currently working towards standardizing an ephemeral key-based lightweight and authenticated key exchange protocol called EDHOC (Ephemeral Diffie–Hellman over COSE). The protocol’s primary purpose is to build an OSCORE (Object Security for Constrained RESTful Environments) security environment by supplying crucial security properties such as secure key exchange, mutual authentication, perfect forward secrecy, and identity protection. EDHOC will most likely dominate IoT security once it becomes a standard. It is, therefore, imperative to inspect the protocol for any security flaw. In this regard, two previous studies have shown different security vulnerabilities of the protocol using formal security verification methods. Yet, both missed the vital security flaws we found in this paper: resource exhaustion and privacy attacks. In finding these vulnerabilities, we leveraged BAN-Logic and AVISPA to formally verify both EDHOC protocol variants. Consequently, we described these security flaws together with the results of the related studies and put forward recommended solutions as part of our future work.


---

## Body

## 1. Introduction

IoT refers to a network environment in which all surrounding objects are connected to wired and wireless networks to interact and exchange information over the Internet. These objects (also referred to as “things”) can range from a simple soil moisture sensor in a field to a complex implanted device in a human body. With continuous developments in low-cost electronics (such as sensors), fast progress in mobile communication (especially with the introduction of 5G), and significant advances in data analytics (e.g., machine learning and lightweight deep learning), IoT has become one of the most demanded technologies in our time [1, 2]. Currently, IoT serves as an instrumental platform to host many applications in manufacturing, healthcare, energy, cities, and many more. In the next four years (by 2025) only, the total market share of IoT can stretch to reach up to 3 trillion USD [3], while the number of devices operating in an IoT environment can cross 42 billion with over 73 ZB of generated data [4].Despite the vast expansion of IoT-enabled devices and their widespread applications, IoT still has several challenges that needs to be tackled. Some of the issues are tightly related to the severe computing resource constraints concerning storage, processing, and communication [5–7]. Such tight requirements call for efficient mechanisms to enable devices operating within IoT environments to function through unstable channels with constrained bandwidth and varying topology [8]. To realize these stringent conditions, essential protocols, such as [9–11], have been standardized by IETF. In addition, because IoT devices transport several sensitive information, security problems can threaten the inability to provide services and the user's personal information. Some potential security attacks are device software malfunction, prying, malevolent code infusions, device tampering, and unauthorized access [12]. Furthermore, studies such as [13, 14] investigated the security issues of integrating LPWAN in the 5G ecosystem, as well as the practical evaluation of compression and fragmentation of standard protocols as applied to IoTs in LPWAN, respectively. Hence, IoT devices require more capable security schemes that work in tandem with the communication protocols to mitigate these security attacks.Even though IoT applications anticipate solid security assurance, securing IoT frameworks is challenging. It is mainly because of their intrinsic nature of resource constraint and absence of “security aware” design. Although there are various security solutions designed for conventional networks, such as IKEv2 [15], TLS [16], and DTLS [17], they are not suitable for the IoT environment due to their high degree of processing power and memory space. For instance, the footprint in bytes for a DTLS is six times heavier than the EDHOC + CoAP (Constrained Application Protocol) [8]. Fortunately, there are now efforts in designing standard security protocols mainly intended to serve in IoT environments. One such application layer security protocol is the OSCORE [18]. The protocol is efficient for severely constrained networks as it maintains the minor communication overhead possible. Using OSCORE, however, requires preshared keys to establish a security context. For this purpose, the IETF is in the process of standardizing an authenticated Diffie–Hellman key exchange protocol known as EDHOC [19]. The protocol is aforesaid to provide essential security properties such as mutual authentication, perfect forward secrecy, identity protection, and cipher suite negotiation.EDHOC will most certainly dominate IoT security once it becomes a standard, which is why it is critical to analyse it for security vulnerabilities thoroughly. Since its inception in March 2016, it passed through 26 different versions, among which only two of its versions ([20] in 2018 and [21] in 2020) were formally analysed by [22, 23] using ProVerif [24] and Tamarin [25], respectively. While these studies bring numerous essential security issues to light, there are still security flaws that they have not yet discovered. Furthermore, evaluating security protocols using several formal approaches increases our confidence in the protocols’ resilience to various security threats since one can compensate for the weakness of the other. Accordingly, in this paper, we formally analysed both the symmetric and asymmetric variants of the EDHOC protocol by using BAN (Burrows, Abadi, and Needham)-Logic [26] and AVISPA (Automated Validation of Internet Security Protocols and Applications) [27] to uncover other security issues. The formal verification results indicate that the protocols suffer from resource exhaustion and privacy attacks. While the former vulnerability is related to a class of attacks known as (distributed) denial-of-service attacks, where excessive and unnecessary requests deplete a node’s resource, the latter pertains to privacy violations due to ID_PSK and ID_CREDR (in symmetric and asymmetric variations, respectively). Both security issues are described in detail in Section 4 of the paper. The core contributions of this paper are summarized as follows:(i)
We carried out a formal security verification of the asymmetric and symmetric variants of the EDHOC protocol using two formal approaches: BAN-Logic and AVISPA(ii)
We pointed out two novel potential security vulnerabilities that may lead to resource exhaustion and privacy attacks(iii)
We described a concise summary of the principal security threats found by former related studies together with those identified by usThe remainder of the paper is organized as follows. Section2 describes the EDHOC protocol along with the related studies on its formal security analysis. The formal verification of the protocol and results, respectively, are presented in the subsequent two sections. Finally, Section 5 concludes the paper.


## 2. The EDHOC Protocol

### 2.1. Protocol Overview

The increasing usage of IoT devices in vertical applications, such as energy, smart factory, healthcare, and transportation, calls for more efficient approaches to power, communication, storage, and processing. Given their severe constraint concerning these requirements, it is not possible (or inefficient) to apply existing security protocols. The main reason is due to the heavy cryptography algorithms, message sizes, and total round trips involved with these schemes. Implementing security on the application layer of the IoT communication systems is especially beneficial when there is insufficient security at the transport layer or when considering the performance of the communication is required. To this point, there are fundamental advances in providing application-aware security solutions. Some of these schemes are the CoAP [9] and its lightweight extension to provide sufficient object security, OSCORE [18].Another vital protocol that serves as a lightweight authenticated key exchange mechanism for OSCORE is the EDHOC. The EDHOC protocol provides session key establishment while supporting fundamental security properties like perfect forward secrecy and mutual authentication [19]. The protocol involves essential components like Elliptic Curve Diffie–Hellman (ECDH) for key exchange, CBOR (Concise Binary Object Representation) [10] for data encoding, COSE (CBOR Object Signing and Encryption) [28] for protecting the CBOR encoded messages, and CoAP for message transportation. In summary, the primary intent of EDHOC is to leverage the OSCORE initiated security so that the message footprints and the round trips are small. Figure 1 shows the IoT protocol stack with the EDHOC protocol located in the application layer.Figure 1
IoT protocol stack.


### 2.2. Related Works

Formal security analysis of various authentication protocols has been performed to guarantee the resilience of different security schemes against numerous attacks. Concerning EDHOC, there are two significant studies that analysed the security of this protocol with a formal approach.In [22], the authors formally analysed both symmetric-key and asymmetric-key options of the EDHOC protocol using ProVerif [24]. This research inspected the protocol against various security characteristics like identity protection against an active attacker, application data confidentiality and perfect forward secrecy, and robust authentication. Consequently, the authors highlighted the risk of leaking the responder’s identity, although the initiator’s identity is secured. Furthermore, by utilizing the same preshared key identifier ID_PSK, an attacker may link several sessions and launch various assaults to the symmetric variant of the protocol. Concerning the application data (AD1 to AD3), the authors also showed that only AD3 (for both symmetric and asymmetric variants) satisfies secrecy, perfect forward secrecy, and integrity at both the time of message arrival and conclusion of the protocol.Another paper [23] that analysed the EDHOC security using the Tamarin prover [25] verification tool found various improvement points. The authors, among other issues, identified the following flaws by the time they analysed the protocol: absence of nonrepudiation security property and lack of verification of ID_CREDR of Msg2 by the initiator. The authors also showed that a security threat due to a prolonged metasession covering several sessions of the EDHOC protocol can happen when the responder rejects proposed cipher suites. The paper also recommended the use of a trusted execution environment (TEE) for security hardening.


### 2.3. Protocol Description

The initiator and responder of the EDHOC protocol can encrypt and protect the integrity of information communicated between them by following a similar construction as SIGMA-1 [29]. The initiator and responder exchange three messages to establish Diffie–Hellman’s shared secrets and perform encryption using Authenticated Encryption with Associated Data (AEAD) [30]. Unique to EDHOC, however, new parameters like connection identifiers, transcript hashes, methods, and others exist. Moreover, EDHOC protocol works in two modes: asymmetric-key-based authentication technique that provides mutual authenticity via Diffie–Hellman shared ciphers and symmetric-key-based authentication that relies on preshared symmetric keys. Table 1 shows the parameters used in the EDHOC protocol.Table 1
Symbols and notations used in the EDHOC protocol.
ComponentsDescriptionMethodOne of the four types of authentication methods agreed by the initiator and the responder.CorrOne of the four types of correlation mechanisms provided by the transport path.SUITES_I, SUITS_RList of cipher suites (in order of preference) supported by the initiator and the responder, respectively.x, yThe ECDH ephemeral private keys of the initiator and the responder, respectively.GX, GYThe ECDH ephemeral public keys of the initiator and the responder, respectively.pA prime number that states the size of the finite field.a, bThe coefficients of the elliptic curve equation.GThe generator (base point) of the subgroup.h, nThe cofactor and order of the subgroup, respectively.CI, CRConnection identifiers for the initiator and responder, respectively, that are used to facilitate the retrieval of the protocol state.ADApplication data (also known as external authorization data).CREDI, CREDRThe credentials containing the public authentication keys of the initiator and the responder, respectively.ID_CREDI, ID_CREDRThe identifiers for the credentialsCREDI and CREDR, respectively.THTranscript hashes used for key derivation and additional authenticated data.KSession key.PRKPseudorandom key.PSKPreshared key.AEAD (K; )Authenticated Encryption with Associated Data using a keyK.Sig (I; . ), Sig(R; . )Digital signatures made with the private authentication key of the initiator and the responder, respectively.


#### 2.3.1. Asymmetric-Key-Based EDHOC Protocol

The execution steps of an EDHOC protocol that uses asymmetric-keys are shown in Figure2. Furthermore, to better understand and visualize the operations of both variants of the EDHOC protocol, we presented a state diagram as shown in Figures 3 and 4 . Take note that the figures show one session connection between the initiator and the responder.Figure 2
Asymmetric-key-based EDHOC protocol.Figure 3
State diagram for the asymmetric-key-based EDHOC protocol.Figure 4
State diagram for the symmetric-key-based EDHOC protocol.(1) Initiator ⟶ Responder. Before the commencement of the protocol, the initiator I stores the domain parameters for the agreed elliptic curve, ID_CREDI, AD1, and AD2. Firstly, the caller generates a method that identifies the authentication method and the associated correlation (corr) of the transport mechanism. Here, “method” and “corr” take values from 0 to 3 as described in [19]. The initiator also chooses SUITESI from the list of cipher suites that an EDHOC protocol recognizes and select the connection identifier CI. It then picks a number x to serve as an ECDH private key. Once the preliminary information is ready, it computes the ECDH public key GX (=G.x) and TYPE (=4 ∗ method + corr). Finally, it constructs and sends Msg1 containing TYPE, SUITESI, GX, CI, and AD1 to the responder. Note that AD1, at this time, cannot guarantee security as it is transmitted in plaintext.(2) Responder ⟶ Initiator. Once it receives Msg1, the responder selects a cipher suite SUITESR and the connection identifier CR, and calculates the ECDH public key GY (=G.y) the same way the initiator calculated GX. It then calculates the ECDH shared key GXY (=GX.y). Subsequently, the transcript hash TH2 is computed by hashing the received message Msg1 and data2, where data2 consists of the session identifiers CI, CR, and the ECDH public GY. The responder uses TH2 for authentication. It then computes an encryption key K2 (HKDF (PRK, GXY)) from the pseudorandom key PRK (HKDF (“0x,” GXY)) and the transcript hash TH2. Next, the responder constructs Msg2 by concatenating CIPHERTEXT2 and data2.The former message is formed by first signing CREDR and TH2 with the responder’s private key, followed by encrypting the signature, ID_CREDR, and AD2 with K2. The latter message is simply the concatenation of CI, CR, and GY. Finally, the responder sends Msg2 to the initiator.(3) Initiator ⟶ Responder. When Msg2 reaches the initiator, it computes the ECDH shared key GXY (=GY.x), PRK, TH2, and K2, like the responder. Then, it uses K2 to decrypt CIPHERTEXT2 and retrieve ID_CREDI, the signature, and AD2. It then validates the signature, and if the result succeeds, it generates TH3 and K3. The former is constructed by first hashing CIPHERTEXT2 with TH2 and then rehashing the result with CR. The latter is computed by using HKDF (PRK, TH3). Finally, the initiator constructs a message CIPHERTEXT3 by signing CREDI and TH3 with its private key and encrypting it together with ID_CREDR and AD3 using the computed session key K3; it forms Msg3 by concatenating CR and CIPHERTEXT3 and sends it to the responder. The asymmetric-key-based EDHOC protocol concludes by removing the Diffie–Hellman key pairs used to generate the encryption keys K2 and K3 to support perfect forward secrecy.


#### 2.3.2. Symmetric-Key-Based EDHOC Protocol

The symmetric-key-based EDHOC protocol, shown in Figure5, is very similar to the asymmetric-key-based protocol, with the following exceptions:(1)
The public key identifiersID_CREDI and ID_CREDR are not used as part of the authenticated encryption(2)
Authentication happens via preshared keyPSK (identified by ID_PSK) rather than the digital signatures used in the previous protocol(3)
The protocol session keysK2 and K3 are derived based on Diffie–Hellman shared keys, transcript hashes, and preshared keys PSKFigure 5
Symmetric-key-based EDHOC protocol.


## 2.1. Protocol Overview

The increasing usage of IoT devices in vertical applications, such as energy, smart factory, healthcare, and transportation, calls for more efficient approaches to power, communication, storage, and processing. Given their severe constraint concerning these requirements, it is not possible (or inefficient) to apply existing security protocols. The main reason is due to the heavy cryptography algorithms, message sizes, and total round trips involved with these schemes. Implementing security on the application layer of the IoT communication systems is especially beneficial when there is insufficient security at the transport layer or when considering the performance of the communication is required. To this point, there are fundamental advances in providing application-aware security solutions. Some of these schemes are the CoAP [9] and its lightweight extension to provide sufficient object security, OSCORE [18].Another vital protocol that serves as a lightweight authenticated key exchange mechanism for OSCORE is the EDHOC. The EDHOC protocol provides session key establishment while supporting fundamental security properties like perfect forward secrecy and mutual authentication [19]. The protocol involves essential components like Elliptic Curve Diffie–Hellman (ECDH) for key exchange, CBOR (Concise Binary Object Representation) [10] for data encoding, COSE (CBOR Object Signing and Encryption) [28] for protecting the CBOR encoded messages, and CoAP for message transportation. In summary, the primary intent of EDHOC is to leverage the OSCORE initiated security so that the message footprints and the round trips are small. Figure 1 shows the IoT protocol stack with the EDHOC protocol located in the application layer.Figure 1
IoT protocol stack.


## 2.2. Related Works

Formal security analysis of various authentication protocols has been performed to guarantee the resilience of different security schemes against numerous attacks. Concerning EDHOC, there are two significant studies that analysed the security of this protocol with a formal approach.In [22], the authors formally analysed both symmetric-key and asymmetric-key options of the EDHOC protocol using ProVerif [24]. This research inspected the protocol against various security characteristics like identity protection against an active attacker, application data confidentiality and perfect forward secrecy, and robust authentication. Consequently, the authors highlighted the risk of leaking the responder’s identity, although the initiator’s identity is secured. Furthermore, by utilizing the same preshared key identifier ID_PSK, an attacker may link several sessions and launch various assaults to the symmetric variant of the protocol. Concerning the application data (AD1 to AD3), the authors also showed that only AD3 (for both symmetric and asymmetric variants) satisfies secrecy, perfect forward secrecy, and integrity at both the time of message arrival and conclusion of the protocol.Another paper [23] that analysed the EDHOC security using the Tamarin prover [25] verification tool found various improvement points. The authors, among other issues, identified the following flaws by the time they analysed the protocol: absence of nonrepudiation security property and lack of verification of ID_CREDR of Msg2 by the initiator. The authors also showed that a security threat due to a prolonged metasession covering several sessions of the EDHOC protocol can happen when the responder rejects proposed cipher suites. The paper also recommended the use of a trusted execution environment (TEE) for security hardening.


## 2.3. Protocol Description

The initiator and responder of the EDHOC protocol can encrypt and protect the integrity of information communicated between them by following a similar construction as SIGMA-1 [29]. The initiator and responder exchange three messages to establish Diffie–Hellman’s shared secrets and perform encryption using Authenticated Encryption with Associated Data (AEAD) [30]. Unique to EDHOC, however, new parameters like connection identifiers, transcript hashes, methods, and others exist. Moreover, EDHOC protocol works in two modes: asymmetric-key-based authentication technique that provides mutual authenticity via Diffie–Hellman shared ciphers and symmetric-key-based authentication that relies on preshared symmetric keys. Table 1 shows the parameters used in the EDHOC protocol.Table 1
Symbols and notations used in the EDHOC protocol.
ComponentsDescriptionMethodOne of the four types of authentication methods agreed by the initiator and the responder.CorrOne of the four types of correlation mechanisms provided by the transport path.SUITES_I, SUITS_RList of cipher suites (in order of preference) supported by the initiator and the responder, respectively.x, yThe ECDH ephemeral private keys of the initiator and the responder, respectively.GX, GYThe ECDH ephemeral public keys of the initiator and the responder, respectively.pA prime number that states the size of the finite field.a, bThe coefficients of the elliptic curve equation.GThe generator (base point) of the subgroup.h, nThe cofactor and order of the subgroup, respectively.CI, CRConnection identifiers for the initiator and responder, respectively, that are used to facilitate the retrieval of the protocol state.ADApplication data (also known as external authorization data).CREDI, CREDRThe credentials containing the public authentication keys of the initiator and the responder, respectively.ID_CREDI, ID_CREDRThe identifiers for the credentialsCREDI and CREDR, respectively.THTranscript hashes used for key derivation and additional authenticated data.KSession key.PRKPseudorandom key.PSKPreshared key.AEAD (K; )Authenticated Encryption with Associated Data using a keyK.Sig (I; . ), Sig(R; . )Digital signatures made with the private authentication key of the initiator and the responder, respectively.


### 2.3.1. Asymmetric-Key-Based EDHOC Protocol

The execution steps of an EDHOC protocol that uses asymmetric-keys are shown in Figure2. Furthermore, to better understand and visualize the operations of both variants of the EDHOC protocol, we presented a state diagram as shown in Figures 3 and 4 . Take note that the figures show one session connection between the initiator and the responder.Figure 2
Asymmetric-key-based EDHOC protocol.Figure 3
State diagram for the asymmetric-key-based EDHOC protocol.Figure 4
State diagram for the symmetric-key-based EDHOC protocol.(1) Initiator ⟶ Responder. Before the commencement of the protocol, the initiator I stores the domain parameters for the agreed elliptic curve, ID_CREDI, AD1, and AD2. Firstly, the caller generates a method that identifies the authentication method and the associated correlation (corr) of the transport mechanism. Here, “method” and “corr” take values from 0 to 3 as described in [19]. The initiator also chooses SUITESI from the list of cipher suites that an EDHOC protocol recognizes and select the connection identifier CI. It then picks a number x to serve as an ECDH private key. Once the preliminary information is ready, it computes the ECDH public key GX (=G.x) and TYPE (=4 ∗ method + corr). Finally, it constructs and sends Msg1 containing TYPE, SUITESI, GX, CI, and AD1 to the responder. Note that AD1, at this time, cannot guarantee security as it is transmitted in plaintext.(2) Responder ⟶ Initiator. Once it receives Msg1, the responder selects a cipher suite SUITESR and the connection identifier CR, and calculates the ECDH public key GY (=G.y) the same way the initiator calculated GX. It then calculates the ECDH shared key GXY (=GX.y). Subsequently, the transcript hash TH2 is computed by hashing the received message Msg1 and data2, where data2 consists of the session identifiers CI, CR, and the ECDH public GY. The responder uses TH2 for authentication. It then computes an encryption key K2 (HKDF (PRK, GXY)) from the pseudorandom key PRK (HKDF (“0x,” GXY)) and the transcript hash TH2. Next, the responder constructs Msg2 by concatenating CIPHERTEXT2 and data2.The former message is formed by first signing CREDR and TH2 with the responder’s private key, followed by encrypting the signature, ID_CREDR, and AD2 with K2. The latter message is simply the concatenation of CI, CR, and GY. Finally, the responder sends Msg2 to the initiator.(3) Initiator ⟶ Responder. When Msg2 reaches the initiator, it computes the ECDH shared key GXY (=GY.x), PRK, TH2, and K2, like the responder. Then, it uses K2 to decrypt CIPHERTEXT2 and retrieve ID_CREDI, the signature, and AD2. It then validates the signature, and if the result succeeds, it generates TH3 and K3. The former is constructed by first hashing CIPHERTEXT2 with TH2 and then rehashing the result with CR. The latter is computed by using HKDF (PRK, TH3). Finally, the initiator constructs a message CIPHERTEXT3 by signing CREDI and TH3 with its private key and encrypting it together with ID_CREDR and AD3 using the computed session key K3; it forms Msg3 by concatenating CR and CIPHERTEXT3 and sends it to the responder. The asymmetric-key-based EDHOC protocol concludes by removing the Diffie–Hellman key pairs used to generate the encryption keys K2 and K3 to support perfect forward secrecy.


### 2.3.2. Symmetric-Key-Based EDHOC Protocol

The symmetric-key-based EDHOC protocol, shown in Figure5, is very similar to the asymmetric-key-based protocol, with the following exceptions:(1)
The public key identifiersID_CREDI and ID_CREDR are not used as part of the authenticated encryption(2)
Authentication happens via preshared keyPSK (identified by ID_PSK) rather than the digital signatures used in the previous protocol(3)
The protocol session keysK2 and K3 are derived based on Diffie–Hellman shared keys, transcript hashes, and preshared keys PSKFigure 5
Symmetric-key-based EDHOC protocol.


## 2.3.1. Asymmetric-Key-Based EDHOC Protocol

The execution steps of an EDHOC protocol that uses asymmetric-keys are shown in Figure2. Furthermore, to better understand and visualize the operations of both variants of the EDHOC protocol, we presented a state diagram as shown in Figures 3 and 4 . Take note that the figures show one session connection between the initiator and the responder.Figure 2
Asymmetric-key-based EDHOC protocol.Figure 3
State diagram for the asymmetric-key-based EDHOC protocol.Figure 4
State diagram for the symmetric-key-based EDHOC protocol.(1) Initiator ⟶ Responder. Before the commencement of the protocol, the initiator I stores the domain parameters for the agreed elliptic curve, ID_CREDI, AD1, and AD2. Firstly, the caller generates a method that identifies the authentication method and the associated correlation (corr) of the transport mechanism. Here, “method” and “corr” take values from 0 to 3 as described in [19]. The initiator also chooses SUITESI from the list of cipher suites that an EDHOC protocol recognizes and select the connection identifier CI. It then picks a number x to serve as an ECDH private key. Once the preliminary information is ready, it computes the ECDH public key GX (=G.x) and TYPE (=4 ∗ method + corr). Finally, it constructs and sends Msg1 containing TYPE, SUITESI, GX, CI, and AD1 to the responder. Note that AD1, at this time, cannot guarantee security as it is transmitted in plaintext.(2) Responder ⟶ Initiator. Once it receives Msg1, the responder selects a cipher suite SUITESR and the connection identifier CR, and calculates the ECDH public key GY (=G.y) the same way the initiator calculated GX. It then calculates the ECDH shared key GXY (=GX.y). Subsequently, the transcript hash TH2 is computed by hashing the received message Msg1 and data2, where data2 consists of the session identifiers CI, CR, and the ECDH public GY. The responder uses TH2 for authentication. It then computes an encryption key K2 (HKDF (PRK, GXY)) from the pseudorandom key PRK (HKDF (“0x,” GXY)) and the transcript hash TH2. Next, the responder constructs Msg2 by concatenating CIPHERTEXT2 and data2.The former message is formed by first signing CREDR and TH2 with the responder’s private key, followed by encrypting the signature, ID_CREDR, and AD2 with K2. The latter message is simply the concatenation of CI, CR, and GY. Finally, the responder sends Msg2 to the initiator.(3) Initiator ⟶ Responder. When Msg2 reaches the initiator, it computes the ECDH shared key GXY (=GY.x), PRK, TH2, and K2, like the responder. Then, it uses K2 to decrypt CIPHERTEXT2 and retrieve ID_CREDI, the signature, and AD2. It then validates the signature, and if the result succeeds, it generates TH3 and K3. The former is constructed by first hashing CIPHERTEXT2 with TH2 and then rehashing the result with CR. The latter is computed by using HKDF (PRK, TH3). Finally, the initiator constructs a message CIPHERTEXT3 by signing CREDI and TH3 with its private key and encrypting it together with ID_CREDR and AD3 using the computed session key K3; it forms Msg3 by concatenating CR and CIPHERTEXT3 and sends it to the responder. The asymmetric-key-based EDHOC protocol concludes by removing the Diffie–Hellman key pairs used to generate the encryption keys K2 and K3 to support perfect forward secrecy.


## 2.3.2. Symmetric-Key-Based EDHOC Protocol

The symmetric-key-based EDHOC protocol, shown in Figure5, is very similar to the asymmetric-key-based protocol, with the following exceptions:(1)
The public key identifiersID_CREDI and ID_CREDR are not used as part of the authenticated encryption(2)
Authentication happens via preshared keyPSK (identified by ID_PSK) rather than the digital signatures used in the previous protocol(3)
The protocol session keysK2 and K3 are derived based on Diffie–Hellman shared keys, transcript hashes, and preshared keys PSKFigure 5
Symmetric-key-based EDHOC protocol.


## 3. Formal Security Verification for EDHOC Protocol

This section describes the formal security verification of both variants of the EDHOC protocol. First, we leverage BAN-Logic to analyse any security flaw that may exist in the protocol. Next, to further strengthen the verification result and complement the weakness of the first approach, we will use the AVISPA tool.


### 3.1. BAN-Logic-Based Formal Verification

BAN-Logic is a modal logic of beliefs (proposed by Burrows, Abadi, and Needham) used to verify authentication protocols in a formal manner [26, 31]. The formal description of the authentication process, participants’ knowledge, and beliefs serve as a foundation for analysing the changes at each level of the protocol. BAN-Logic is the most utilized approach for examining various security protocols due to its simplicity and robustness.Verification of security protocols using this method starts with converting the protocol into an idealized form through idealization. Here, only protected messages, traversing from one participant to another, are of interest. Then, realistic assumptions and security objectives that the protocol should guarantee proceed. Subsequently, the derivation of the security goals continues by applying different BAN-Logic rules, the premises, and the intermediate results of the derivation. Tables2 and 3 describe the symbols and formulas used in the BAN-Logic formalization process, respectively.Table 2
BAN-Logic notations.
NotationMeaningRbelievesMR believes that message M is trueRseesMR receives message M at any point in timeRsaidMR previously sent messageMRcontrolsMR has jurisdiction over MFreshMM is freshR↔SIS is a secret key shared between M and N⟶SRS is R’s public keyR⇔SIS is a secret that R and I shareMKM is a message encrypted with a key KM,VM is combined with VTable 3
BAN-Logic rules.
Rule nameRuleMessage meaning rule (MM)RbelievesR↔SI,RseesMS/RbelievesIsaidMRbelievesR⇔SI,RseesMS/RbelievesIsaidMRbelieves⟶SI,RseesMS−1/RbelievesIsaidMNonce verification (NV) ruleRbelieves#M,RbelievesIsaidM/RbelievesIbelievesMJurisdiction (JR) ruleRbelievesIcontrolsK,RbelievesIbelievesK/RbelievesKFreshness (FR) ruleRbelieves freshM/Rbelieves freshM,QDecomposition (DR) ruleRseesM,Q/RseesMBelief conjunction (BC) ruleRbelievesM,RbelievesQ/RbelievesM,QRbelievesIbelievesM,Q/RbelievesIbelievesMRbelievesIsaidM,Q/RbelievesIsaidMDiffie–Hellman (DH) ruleRbelievesIsaid⟶GMI,Rbelieves⟶GQR/RbelievesR↔gMQIRbelievesIsaid⟶GMI,Rbelieves⟶GQR/RbelievesR⇔GMQI


#### 3.1.1. The Asymmetric-Key Option

Idealization. An idealized version of the asymmetric form of the EDHOC protocol is shown below. Note that the idealized form only comprises encrypted (protected) communications, which is why Msg1 is left out.(1)R⟶I:ID_CREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2GXY,(2)I⟶R:ID_CREDI,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD3GXY.Goals. The following objectives are established for verifying mutual authentication and key exchange between I and R. Consequently, while the goals in (5) and (6) show the beliefs I has on R’s trust concerning its credential identity and the associated data (respectively), (9) and (10) show the opposite. About key exchange, the goals in (3) and (4) show I’s belief on the session key, and (7) and (8) assert R’s belief on the same key.(3)IbelievesI⟷GXYR,(4)IbelievesRbelievesI⟷GXYR,(5)IbelievesRbelievesAD2,(6)IbelievesRbelievesID_CREDR,(7)RbelievesI↔GXYR,(8)RbelievesIbelievesI↔GXYR,(9)RbelievesIbelievesAD3(10)RbelievesIbelievesID_CREDI.Assumptions. There are some assumptions and hypotheses we need to set to derive the above goals. Accordingly, the assumptions in (11), (15), and (16) show R’s belief in its ECDH public key, the long-term public key of I, and the freshness of its ECDH public key. On the other hand, while (12) and (14) point out I’s belief in its ECDH public key and its freshness, (13) indicates the belief “I” has in R’s long-term public key. Finally, the two hypotheses (17) and (18) imply that R trusts that I sent its ECDH public key and vice versa, respectively.(11)Rbelieves⟶GYR,(12)Ibelieves⟶GXI,(13)Ibelieves⟶PURR,(14)Ibelieves#⟶GXI,(15)Rbelieves⟶PUII,(16)Rbelieves#⟶GYR,(17)RbelievesIsaid⟶GXI,(18)IbelievesRsaid⟶GYR.Derivations. As a final step of the formal analysis, derivation of goals proceeds. To do so, we leverage the BAN-Logic rules (shown in Table 3), idealizations, assumptions, and the intermediate results of the derivation process. Therefore, if all goals can be derived, the target protocol is considered secure. Otherwise, the protocol may be vulnerable to threats.(19)RbelievesI↔GXYRby11,17,DH,(20)IbelievesI↔GXYRby12,18,DH,(21)IseesID_CREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2GXYfrom1,(22)IbelievesRsaidIDCREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2by20,21,MM,(23)IseesCREDR,⟶GYR,⟶GXI,I↔GXYRR−1by22,(24)IbelievesRsaidCREDR,⟶GYR,⟶GXI,I↔GXYRby23,13,MM,(25)IbelivesRbelievesCREDR,⟶GYR,⟶GXI,I↔GXYRby24,14,FR,NV,(26)IbelievesRbelievesI↔GXYRby25,BC,(27)IbelievesRbelieves⟶GYRby25,BC,(28)IbelievesRbelievesID_CREDRby22,14,FR,NV,BC,(29)IbelievesRbelievesAD2by22,14,FR,NV,BC,(30)RseesID_CREDI,CREDI,⟶GYR,⟶GXI,I↔GXYRR−1,AD3GXYfrom2,(31)RbelievesIsaidIDCREDI,CREDI,⟶GYR,⟶GXI,I↔GXYRI−1,AD3by19,30,MM,(32)RseesCREDI,⟶GYR,⟶GXI,I↔GXYRR−1by31,BC,(33)RbelievesIsaidCREDI,⟶GYR,⟶GXI,I↔GXYRby32,15,MM,(34)RbelievesIbelievesCREDI,⟶GYR,⟶GXI,I↔GXYRby33,16,FR,NV,(35)RbelievesIbelievesI↔GXYRby34,BC,(36)RbelievesIbelieves⟶GXIby34,BC,(37)RbelievesIbelievesID_CREDIby31,16,FR,NV,(38)RbelievesIbelievesAD3by31,16,FR,NV,Note that, without the two hypotheses in (17) and (18), this derivation should stop before (22). In other words, only if both hypotheses are true, the proposed protocol can achieve the goals in (3)∼(10). Unfortunately, they cannot hold because the two parties have no trust in each other’s ECDH public key. Therefore, we conclude that asymmetric-key option is not secure.


#### 3.1.2. The Symmetric-Key Option

Idealization. The idealization forms of the symmetric-key option of EDHOC protocol are shown as follows:(39)R⟶I:AD2,⟶GYR,⟶GXI,I↔GXYRGXY,(40)I⟶R:AD3,⟶GYR,⟶GXI,I↔GXYRGXY.Goals. In general, the goals involve the guarantee of secure key exchange and mutual authentication. In the former case, while (41) and (42) form the belief of I in the ECDH session key, (44) and (45) represent the same case for R. In the latter point, the goals in (43), (46), and (47) serve to verify the mutual authentication.(41)IbelievesI↔GXYR,(42)IbelievesRbelievesI↔GXYR,(43)IbelievesRbelievesAD2,(44)RbelievesI↔GXYR,(45)RbelievesIbelievesI↔GXYR,(46)RbelievesIbelievesAD3,(47)RbelievesIbelievesID_PSK.Assumptions. While the assumptions in (49) and (50) show I’s belief concerning its ECDH public key and its freshness (respectively), (48) and (51) do the same for R (respectively). Moreover, the symmetric-key option of the EDHOC protocol also requires the same additional hypotheses in (52) and (53) as the asymmetric-key option.(48)Rbelieves⟶GYR,(49)Ibelieves⟶GXI,(50)Ibelieves#⟶GXI,(51)Rbelieves#⟶GYR,(52)RbelievesIsaid⟶GXI,(53)IbelievesRsaid⟶GXR.Derivations. The derivations of this variant of the EDHOC protocol proceed as follows:(54)RbelievesI↔GXYRby48,52,DH,(55)IbelievesI↔GXYRby49,53,DH,(56)IseesAD2,⟶GYR,⟶GXI,I↔GXYRGXYfrom39,(57)IbelievesRsaidAD2,⟶GYR,⟶GXI,I↔GXYRby55,56,MM,(58)IbelievesRbelievesAD2,⟶GYR,⟶GXI,I↔GXYRby57,50,FR,NV,(59)IbelievesRbelievesI↔GXYRby58,BC,(60)IbelievesRbelievesAD2by58,BC,(61)RseesAD3,⟶GYR,⟶GXI,I↔GXYRGXYfrom40,(62)RbelievesIsaidAD3,⟶GYR,⟶GXI,I↔GXYRby54,61,MM,(63)RbelievesIbelievesAD3,⟶GYR,⟶GXI,I↔GXYRby62,51,FR,NV,(64)RbelievesIbelievesI↔GXYRby63,BC,(65)RbelievesIbelieves⟶GXIby63,BC,(66)RbelievesIbelievesAD3by63,BC,Similar to the asymmetric-key option, the symmetric-key option can achieve the goals in (41)∼(47) in the case that the two hypotheses in (52) and (53) are true. Thus, the hypotheses, which cannot be proved to be true, show that this option fails to satisfy the goals in (41)∼(47). On the other hand, the last goal (47) indicating the privacy property cannot be achieved because ID_PSK is sent without being encrypted in the first message as shown in Figure 5.To realize mutual authentication between “I” and “R,” the former must believe the latter’s ECDH public key, and it also must believe that the latter believes this key, and vice versa. That is, the derivations [(54), (55), (61), and (65)] of the asymmetric-key option and [(54), (55), (61), and (65)] of the symmetric-key option need to be satisfied. However, since all these derivations are entirely dependent on the fact that “I” (“R”) believes “R” (“I”) sent the ECDH public keys, it automatically follows that mutual authentication can only be fulfilled when these hypotheses are satisfied.Messages Msg2 and Msg3, as illustrated in the idealizations in (39) and (40), use the ECDH session key to derive the AEAD encryption keys K2 and K3. Consequently, this can only happen through the hypotheses in (52) and (53) and is illustrated in derivations (59) and (64). Consequently, it is impossible to conclude that the session key is successfully communicated in the present asymmetric-key form of the protocol. Similarly, the symmetric version of the EDHOC protocol also fails to successfully exchange the session key without the hypotheses in (52) and (53). Thus, the derivations in (54) and (55) for “I” and “R” to believe the session key, respectively, require the use of the hypotheses.Perfect forward secrecy is a characteristic of robust protocols because it protects previous sessions from future key compromise attempts. Accordingly, the asymmetric variant of the EDHOC protocol leverages the unique generation of ECDH private keys for each session of the protocol run to realize perfect forward secrecy. Likewise, in the symmetric-key option of the EDHOC protocol, the generation of the secret keysK2 and K3 uses the nonstatic Diffie–Hellman session key between “I” and “R.” Thus, the symmetric-key option of the EDHOC protocol also provides perfect forward secrecy.For both symmetric and asymmetric alternatives of EDHOC protocol to provide confidentiality and integrity, secure session key exchange must be in place. However, “I” and “R” may fail to transfer this key securely, as described earlier. As a result, the protocol cannot guarantee both confidentiality and integrity security properties.Finally, due to the absence of authentication for the initial message, the anonymity of the responder’s identifier for the public authentication keys (ID_CREDR, for asymmetric-key option) and preshared key (ID_PSK, for the symmetric-key option) can be exposed.Table4 summarizes the result of the BAN-Logic derivation process for both options of the EDHOC protocol. As illustrated in the table and explanation above, both options of the protocol are insecure.Table 4
Security property satisfaction.
No.Security propertiesAsymmetric-key optionSymmetric-key optionSP1Mutual authenticationXXSP2Secure key exchangeXXSP3Perfect forward secrecy✓✓SP4ConfidentialityXXSP5IntegrityXXSP6AnonymityXX


### 3.2. AVISPA-Based Formal Verification

AVISPA is an automation tool for modelling and analysing security protocols [27]. The description of the formal verification process using AVISPA proceeds as follows. First, we use a High-Level Protocol Specification Language (HLPSL) [32] to model the protocol. The HLPSL2IF component then converts the HLPSL-modelled protocols to Intermediate Format (IF). Finally, using the On-the-Fly Model-Checker (OFMC) [33], CL-based Attack Searcher (CL-AtSe) [34], SAT-based Model-Checker (SATMC) [35], and Tree-Automata-based Protocol Analyzer (TA4SP) [36], the IF is transformed to Output Format (OF). Figure 6 shows the general system architecture of the tool, highlighting the main processes from HLPSL to OF.Figure 6
AVISPA system structure.HLPSL is composed of different roles such as Basic Role, Session Role, and Environment Role:(i)
Basic Role. This is a role that models protocol participants in a function with parameters. It consists of steps such as header expression, local variable declaration, and initialization. Additionally, it identifies communication modelling, which specifies the channel for communication between the modelled participants and indicates real-world protocol behaviour. It also defines, together with these parameters, transitions that denote message reception and the corresponding reply of the agent.(ii)
Session Role. This function receives the agents and other parameters to activate the previous role. It is executed via a composition to instantiate the parts in a parallel manner. /\ represents such parallel execution of prior roles.(iii)
Environment Role. It is a role that comprises global constants with the agents and sessions defined in the above two roles. In addition, it outlines an attacker’s knowledge of the protocol’s communication. The intruder’s knowledge concerning the execution of the protocol is also defined. Like the Session Role, parallel execution of sessions executes with the intruder’s information considered. Once the Environment Role completes, the security goals follow, and their verification proceeds with OFMC and CL-AtSe submodules.


#### 3.2.1. The Asymmetric-Key Option

At first, the asymmetric-key option of EDHOC protocol is modelled in HLPSL code. The code specifies the initiator and the responder roles with their security goals, Session Role to activate the basic roles, and finally the Environment Role. The source code for the AVISPA verification for both asymmetric and symmetric variants can be found in the Supplementary Materials (availablehere), while the pseudocodes are presented in Figure 7 (for asymmetric variant) and Figure 8 (for symmetric variant). The obtained verification results for the asymmetric option based on OFMC module and CL-AtSe module are also shown in Figure 9. The attack simulation of the asymmetric-key option of EDHOC protocol is illustrated in Figure 10.Figure 7
A pseudocode for the AVISPA-based verification of asymmetric-key option of EDHOC protocol.Figure 8
A pseudocode for the AVISPA-based verification of symmetric-key option of EDHOC protocol.Figure 9
Verification result of the asymmetric-key option of EDHOC protocol.Figure 10
Attack simulation of the asymmetric-key option of EDHOC protocol.As shown in Figure10, the attack simulation shows the asymmetric-key option of EDHOC protocol is vulnerable due to the fact that the message is sent without any verification of the sender. In other words, when the intruder sends the message of step 2, the responder should generate and calculate all the elements for communication without any proof to the user. It seems to be able to induce resource exhaustion attacks in R due to Msg2 created or modified by the attacker.


#### 3.2.2. The Symmetric-Key Option

Like the previous case, once we translate the protocol into an HLPSL form, the AVISPA tool passes the code through the modules (such as CL-AtSe and OFMC) to check for any security flaws. Figure11 presents the outcome of this process. According to the verification result, the symmetric-key option of the EDHOC protocol is unsafe. Figure 12 shows the possible attack simulation for the identified security flaw.Figure 11
Verification result of symmetric-key option of EDHOC protocol.Figure 12
Attack simulation of the symmetric-key option of EDHOC protocol.In Figure12, when an intruder sends a message in step 2, the responder should create all the elements for communication without user authentication as Figure 10. This may deplete R’s resource due to responses to numerous authentication requests from unauthorized users.


## 3.1. BAN-Logic-Based Formal Verification

BAN-Logic is a modal logic of beliefs (proposed by Burrows, Abadi, and Needham) used to verify authentication protocols in a formal manner [26, 31]. The formal description of the authentication process, participants’ knowledge, and beliefs serve as a foundation for analysing the changes at each level of the protocol. BAN-Logic is the most utilized approach for examining various security protocols due to its simplicity and robustness.Verification of security protocols using this method starts with converting the protocol into an idealized form through idealization. Here, only protected messages, traversing from one participant to another, are of interest. Then, realistic assumptions and security objectives that the protocol should guarantee proceed. Subsequently, the derivation of the security goals continues by applying different BAN-Logic rules, the premises, and the intermediate results of the derivation. Tables2 and 3 describe the symbols and formulas used in the BAN-Logic formalization process, respectively.Table 2
BAN-Logic notations.
NotationMeaningRbelievesMR believes that message M is trueRseesMR receives message M at any point in timeRsaidMR previously sent messageMRcontrolsMR has jurisdiction over MFreshMM is freshR↔SIS is a secret key shared between M and N⟶SRS is R’s public keyR⇔SIS is a secret that R and I shareMKM is a message encrypted with a key KM,VM is combined with VTable 3
BAN-Logic rules.
Rule nameRuleMessage meaning rule (MM)RbelievesR↔SI,RseesMS/RbelievesIsaidMRbelievesR⇔SI,RseesMS/RbelievesIsaidMRbelieves⟶SI,RseesMS−1/RbelievesIsaidMNonce verification (NV) ruleRbelieves#M,RbelievesIsaidM/RbelievesIbelievesMJurisdiction (JR) ruleRbelievesIcontrolsK,RbelievesIbelievesK/RbelievesKFreshness (FR) ruleRbelieves freshM/Rbelieves freshM,QDecomposition (DR) ruleRseesM,Q/RseesMBelief conjunction (BC) ruleRbelievesM,RbelievesQ/RbelievesM,QRbelievesIbelievesM,Q/RbelievesIbelievesMRbelievesIsaidM,Q/RbelievesIsaidMDiffie–Hellman (DH) ruleRbelievesIsaid⟶GMI,Rbelieves⟶GQR/RbelievesR↔gMQIRbelievesIsaid⟶GMI,Rbelieves⟶GQR/RbelievesR⇔GMQI


### 3.1.1. The Asymmetric-Key Option

Idealization. An idealized version of the asymmetric form of the EDHOC protocol is shown below. Note that the idealized form only comprises encrypted (protected) communications, which is why Msg1 is left out.(1)R⟶I:ID_CREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2GXY,(2)I⟶R:ID_CREDI,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD3GXY.Goals. The following objectives are established for verifying mutual authentication and key exchange between I and R. Consequently, while the goals in (5) and (6) show the beliefs I has on R’s trust concerning its credential identity and the associated data (respectively), (9) and (10) show the opposite. About key exchange, the goals in (3) and (4) show I’s belief on the session key, and (7) and (8) assert R’s belief on the same key.(3)IbelievesI⟷GXYR,(4)IbelievesRbelievesI⟷GXYR,(5)IbelievesRbelievesAD2,(6)IbelievesRbelievesID_CREDR,(7)RbelievesI↔GXYR,(8)RbelievesIbelievesI↔GXYR,(9)RbelievesIbelievesAD3(10)RbelievesIbelievesID_CREDI.Assumptions. There are some assumptions and hypotheses we need to set to derive the above goals. Accordingly, the assumptions in (11), (15), and (16) show R’s belief in its ECDH public key, the long-term public key of I, and the freshness of its ECDH public key. On the other hand, while (12) and (14) point out I’s belief in its ECDH public key and its freshness, (13) indicates the belief “I” has in R’s long-term public key. Finally, the two hypotheses (17) and (18) imply that R trusts that I sent its ECDH public key and vice versa, respectively.(11)Rbelieves⟶GYR,(12)Ibelieves⟶GXI,(13)Ibelieves⟶PURR,(14)Ibelieves#⟶GXI,(15)Rbelieves⟶PUII,(16)Rbelieves#⟶GYR,(17)RbelievesIsaid⟶GXI,(18)IbelievesRsaid⟶GYR.Derivations. As a final step of the formal analysis, derivation of goals proceeds. To do so, we leverage the BAN-Logic rules (shown in Table 3), idealizations, assumptions, and the intermediate results of the derivation process. Therefore, if all goals can be derived, the target protocol is considered secure. Otherwise, the protocol may be vulnerable to threats.(19)RbelievesI↔GXYRby11,17,DH,(20)IbelievesI↔GXYRby12,18,DH,(21)IseesID_CREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2GXYfrom1,(22)IbelievesRsaidIDCREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2by20,21,MM,(23)IseesCREDR,⟶GYR,⟶GXI,I↔GXYRR−1by22,(24)IbelievesRsaidCREDR,⟶GYR,⟶GXI,I↔GXYRby23,13,MM,(25)IbelivesRbelievesCREDR,⟶GYR,⟶GXI,I↔GXYRby24,14,FR,NV,(26)IbelievesRbelievesI↔GXYRby25,BC,(27)IbelievesRbelieves⟶GYRby25,BC,(28)IbelievesRbelievesID_CREDRby22,14,FR,NV,BC,(29)IbelievesRbelievesAD2by22,14,FR,NV,BC,(30)RseesID_CREDI,CREDI,⟶GYR,⟶GXI,I↔GXYRR−1,AD3GXYfrom2,(31)RbelievesIsaidIDCREDI,CREDI,⟶GYR,⟶GXI,I↔GXYRI−1,AD3by19,30,MM,(32)RseesCREDI,⟶GYR,⟶GXI,I↔GXYRR−1by31,BC,(33)RbelievesIsaidCREDI,⟶GYR,⟶GXI,I↔GXYRby32,15,MM,(34)RbelievesIbelievesCREDI,⟶GYR,⟶GXI,I↔GXYRby33,16,FR,NV,(35)RbelievesIbelievesI↔GXYRby34,BC,(36)RbelievesIbelieves⟶GXIby34,BC,(37)RbelievesIbelievesID_CREDIby31,16,FR,NV,(38)RbelievesIbelievesAD3by31,16,FR,NV,Note that, without the two hypotheses in (17) and (18), this derivation should stop before (22). In other words, only if both hypotheses are true, the proposed protocol can achieve the goals in (3)∼(10). Unfortunately, they cannot hold because the two parties have no trust in each other’s ECDH public key. Therefore, we conclude that asymmetric-key option is not secure.


### 3.1.2. The Symmetric-Key Option

Idealization. The idealization forms of the symmetric-key option of EDHOC protocol are shown as follows:(39)R⟶I:AD2,⟶GYR,⟶GXI,I↔GXYRGXY,(40)I⟶R:AD3,⟶GYR,⟶GXI,I↔GXYRGXY.Goals. In general, the goals involve the guarantee of secure key exchange and mutual authentication. In the former case, while (41) and (42) form the belief of I in the ECDH session key, (44) and (45) represent the same case for R. In the latter point, the goals in (43), (46), and (47) serve to verify the mutual authentication.(41)IbelievesI↔GXYR,(42)IbelievesRbelievesI↔GXYR,(43)IbelievesRbelievesAD2,(44)RbelievesI↔GXYR,(45)RbelievesIbelievesI↔GXYR,(46)RbelievesIbelievesAD3,(47)RbelievesIbelievesID_PSK.Assumptions. While the assumptions in (49) and (50) show I’s belief concerning its ECDH public key and its freshness (respectively), (48) and (51) do the same for R (respectively). Moreover, the symmetric-key option of the EDHOC protocol also requires the same additional hypotheses in (52) and (53) as the asymmetric-key option.(48)Rbelieves⟶GYR,(49)Ibelieves⟶GXI,(50)Ibelieves#⟶GXI,(51)Rbelieves#⟶GYR,(52)RbelievesIsaid⟶GXI,(53)IbelievesRsaid⟶GXR.Derivations. The derivations of this variant of the EDHOC protocol proceed as follows:(54)RbelievesI↔GXYRby48,52,DH,(55)IbelievesI↔GXYRby49,53,DH,(56)IseesAD2,⟶GYR,⟶GXI,I↔GXYRGXYfrom39,(57)IbelievesRsaidAD2,⟶GYR,⟶GXI,I↔GXYRby55,56,MM,(58)IbelievesRbelievesAD2,⟶GYR,⟶GXI,I↔GXYRby57,50,FR,NV,(59)IbelievesRbelievesI↔GXYRby58,BC,(60)IbelievesRbelievesAD2by58,BC,(61)RseesAD3,⟶GYR,⟶GXI,I↔GXYRGXYfrom40,(62)RbelievesIsaidAD3,⟶GYR,⟶GXI,I↔GXYRby54,61,MM,(63)RbelievesIbelievesAD3,⟶GYR,⟶GXI,I↔GXYRby62,51,FR,NV,(64)RbelievesIbelievesI↔GXYRby63,BC,(65)RbelievesIbelieves⟶GXIby63,BC,(66)RbelievesIbelievesAD3by63,BC,Similar to the asymmetric-key option, the symmetric-key option can achieve the goals in (41)∼(47) in the case that the two hypotheses in (52) and (53) are true. Thus, the hypotheses, which cannot be proved to be true, show that this option fails to satisfy the goals in (41)∼(47). On the other hand, the last goal (47) indicating the privacy property cannot be achieved because ID_PSK is sent without being encrypted in the first message as shown in Figure 5.To realize mutual authentication between “I” and “R,” the former must believe the latter’s ECDH public key, and it also must believe that the latter believes this key, and vice versa. That is, the derivations [(54), (55), (61), and (65)] of the asymmetric-key option and [(54), (55), (61), and (65)] of the symmetric-key option need to be satisfied. However, since all these derivations are entirely dependent on the fact that “I” (“R”) believes “R” (“I”) sent the ECDH public keys, it automatically follows that mutual authentication can only be fulfilled when these hypotheses are satisfied.Messages Msg2 and Msg3, as illustrated in the idealizations in (39) and (40), use the ECDH session key to derive the AEAD encryption keys K2 and K3. Consequently, this can only happen through the hypotheses in (52) and (53) and is illustrated in derivations (59) and (64). Consequently, it is impossible to conclude that the session key is successfully communicated in the present asymmetric-key form of the protocol. Similarly, the symmetric version of the EDHOC protocol also fails to successfully exchange the session key without the hypotheses in (52) and (53). Thus, the derivations in (54) and (55) for “I” and “R” to believe the session key, respectively, require the use of the hypotheses.Perfect forward secrecy is a characteristic of robust protocols because it protects previous sessions from future key compromise attempts. Accordingly, the asymmetric variant of the EDHOC protocol leverages the unique generation of ECDH private keys for each session of the protocol run to realize perfect forward secrecy. Likewise, in the symmetric-key option of the EDHOC protocol, the generation of the secret keysK2 and K3 uses the nonstatic Diffie–Hellman session key between “I” and “R.” Thus, the symmetric-key option of the EDHOC protocol also provides perfect forward secrecy.For both symmetric and asymmetric alternatives of EDHOC protocol to provide confidentiality and integrity, secure session key exchange must be in place. However, “I” and “R” may fail to transfer this key securely, as described earlier. As a result, the protocol cannot guarantee both confidentiality and integrity security properties.Finally, due to the absence of authentication for the initial message, the anonymity of the responder’s identifier for the public authentication keys (ID_CREDR, for asymmetric-key option) and preshared key (ID_PSK, for the symmetric-key option) can be exposed.Table4 summarizes the result of the BAN-Logic derivation process for both options of the EDHOC protocol. As illustrated in the table and explanation above, both options of the protocol are insecure.Table 4
Security property satisfaction.
No.Security propertiesAsymmetric-key optionSymmetric-key optionSP1Mutual authenticationXXSP2Secure key exchangeXXSP3Perfect forward secrecy✓✓SP4ConfidentialityXXSP5IntegrityXXSP6AnonymityXX


## 3.1.1. The Asymmetric-Key Option

Idealization. An idealized version of the asymmetric form of the EDHOC protocol is shown below. Note that the idealized form only comprises encrypted (protected) communications, which is why Msg1 is left out.(1)R⟶I:ID_CREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2GXY,(2)I⟶R:ID_CREDI,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD3GXY.Goals. The following objectives are established for verifying mutual authentication and key exchange between I and R. Consequently, while the goals in (5) and (6) show the beliefs I has on R’s trust concerning its credential identity and the associated data (respectively), (9) and (10) show the opposite. About key exchange, the goals in (3) and (4) show I’s belief on the session key, and (7) and (8) assert R’s belief on the same key.(3)IbelievesI⟷GXYR,(4)IbelievesRbelievesI⟷GXYR,(5)IbelievesRbelievesAD2,(6)IbelievesRbelievesID_CREDR,(7)RbelievesI↔GXYR,(8)RbelievesIbelievesI↔GXYR,(9)RbelievesIbelievesAD3(10)RbelievesIbelievesID_CREDI.Assumptions. There are some assumptions and hypotheses we need to set to derive the above goals. Accordingly, the assumptions in (11), (15), and (16) show R’s belief in its ECDH public key, the long-term public key of I, and the freshness of its ECDH public key. On the other hand, while (12) and (14) point out I’s belief in its ECDH public key and its freshness, (13) indicates the belief “I” has in R’s long-term public key. Finally, the two hypotheses (17) and (18) imply that R trusts that I sent its ECDH public key and vice versa, respectively.(11)Rbelieves⟶GYR,(12)Ibelieves⟶GXI,(13)Ibelieves⟶PURR,(14)Ibelieves#⟶GXI,(15)Rbelieves⟶PUII,(16)Rbelieves#⟶GYR,(17)RbelievesIsaid⟶GXI,(18)IbelievesRsaid⟶GYR.Derivations. As a final step of the formal analysis, derivation of goals proceeds. To do so, we leverage the BAN-Logic rules (shown in Table 3), idealizations, assumptions, and the intermediate results of the derivation process. Therefore, if all goals can be derived, the target protocol is considered secure. Otherwise, the protocol may be vulnerable to threats.(19)RbelievesI↔GXYRby11,17,DH,(20)IbelievesI↔GXYRby12,18,DH,(21)IseesID_CREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2GXYfrom1,(22)IbelievesRsaidIDCREDR,CREDR,⟶GYR,⟶GXI,I↔GXYRR−1,AD2by20,21,MM,(23)IseesCREDR,⟶GYR,⟶GXI,I↔GXYRR−1by22,(24)IbelievesRsaidCREDR,⟶GYR,⟶GXI,I↔GXYRby23,13,MM,(25)IbelivesRbelievesCREDR,⟶GYR,⟶GXI,I↔GXYRby24,14,FR,NV,(26)IbelievesRbelievesI↔GXYRby25,BC,(27)IbelievesRbelieves⟶GYRby25,BC,(28)IbelievesRbelievesID_CREDRby22,14,FR,NV,BC,(29)IbelievesRbelievesAD2by22,14,FR,NV,BC,(30)RseesID_CREDI,CREDI,⟶GYR,⟶GXI,I↔GXYRR−1,AD3GXYfrom2,(31)RbelievesIsaidIDCREDI,CREDI,⟶GYR,⟶GXI,I↔GXYRI−1,AD3by19,30,MM,(32)RseesCREDI,⟶GYR,⟶GXI,I↔GXYRR−1by31,BC,(33)RbelievesIsaidCREDI,⟶GYR,⟶GXI,I↔GXYRby32,15,MM,(34)RbelievesIbelievesCREDI,⟶GYR,⟶GXI,I↔GXYRby33,16,FR,NV,(35)RbelievesIbelievesI↔GXYRby34,BC,(36)RbelievesIbelieves⟶GXIby34,BC,(37)RbelievesIbelievesID_CREDIby31,16,FR,NV,(38)RbelievesIbelievesAD3by31,16,FR,NV,Note that, without the two hypotheses in (17) and (18), this derivation should stop before (22). In other words, only if both hypotheses are true, the proposed protocol can achieve the goals in (3)∼(10). Unfortunately, they cannot hold because the two parties have no trust in each other’s ECDH public key. Therefore, we conclude that asymmetric-key option is not secure.


## 3.1.2. The Symmetric-Key Option

Idealization. The idealization forms of the symmetric-key option of EDHOC protocol are shown as follows:(39)R⟶I:AD2,⟶GYR,⟶GXI,I↔GXYRGXY,(40)I⟶R:AD3,⟶GYR,⟶GXI,I↔GXYRGXY.Goals. In general, the goals involve the guarantee of secure key exchange and mutual authentication. In the former case, while (41) and (42) form the belief of I in the ECDH session key, (44) and (45) represent the same case for R. In the latter point, the goals in (43), (46), and (47) serve to verify the mutual authentication.(41)IbelievesI↔GXYR,(42)IbelievesRbelievesI↔GXYR,(43)IbelievesRbelievesAD2,(44)RbelievesI↔GXYR,(45)RbelievesIbelievesI↔GXYR,(46)RbelievesIbelievesAD3,(47)RbelievesIbelievesID_PSK.Assumptions. While the assumptions in (49) and (50) show I’s belief concerning its ECDH public key and its freshness (respectively), (48) and (51) do the same for R (respectively). Moreover, the symmetric-key option of the EDHOC protocol also requires the same additional hypotheses in (52) and (53) as the asymmetric-key option.(48)Rbelieves⟶GYR,(49)Ibelieves⟶GXI,(50)Ibelieves#⟶GXI,(51)Rbelieves#⟶GYR,(52)RbelievesIsaid⟶GXI,(53)IbelievesRsaid⟶GXR.Derivations. The derivations of this variant of the EDHOC protocol proceed as follows:(54)RbelievesI↔GXYRby48,52,DH,(55)IbelievesI↔GXYRby49,53,DH,(56)IseesAD2,⟶GYR,⟶GXI,I↔GXYRGXYfrom39,(57)IbelievesRsaidAD2,⟶GYR,⟶GXI,I↔GXYRby55,56,MM,(58)IbelievesRbelievesAD2,⟶GYR,⟶GXI,I↔GXYRby57,50,FR,NV,(59)IbelievesRbelievesI↔GXYRby58,BC,(60)IbelievesRbelievesAD2by58,BC,(61)RseesAD3,⟶GYR,⟶GXI,I↔GXYRGXYfrom40,(62)RbelievesIsaidAD3,⟶GYR,⟶GXI,I↔GXYRby54,61,MM,(63)RbelievesIbelievesAD3,⟶GYR,⟶GXI,I↔GXYRby62,51,FR,NV,(64)RbelievesIbelievesI↔GXYRby63,BC,(65)RbelievesIbelieves⟶GXIby63,BC,(66)RbelievesIbelievesAD3by63,BC,Similar to the asymmetric-key option, the symmetric-key option can achieve the goals in (41)∼(47) in the case that the two hypotheses in (52) and (53) are true. Thus, the hypotheses, which cannot be proved to be true, show that this option fails to satisfy the goals in (41)∼(47). On the other hand, the last goal (47) indicating the privacy property cannot be achieved because ID_PSK is sent without being encrypted in the first message as shown in Figure 5.To realize mutual authentication between “I” and “R,” the former must believe the latter’s ECDH public key, and it also must believe that the latter believes this key, and vice versa. That is, the derivations [(54), (55), (61), and (65)] of the asymmetric-key option and [(54), (55), (61), and (65)] of the symmetric-key option need to be satisfied. However, since all these derivations are entirely dependent on the fact that “I” (“R”) believes “R” (“I”) sent the ECDH public keys, it automatically follows that mutual authentication can only be fulfilled when these hypotheses are satisfied.Messages Msg2 and Msg3, as illustrated in the idealizations in (39) and (40), use the ECDH session key to derive the AEAD encryption keys K2 and K3. Consequently, this can only happen through the hypotheses in (52) and (53) and is illustrated in derivations (59) and (64). Consequently, it is impossible to conclude that the session key is successfully communicated in the present asymmetric-key form of the protocol. Similarly, the symmetric version of the EDHOC protocol also fails to successfully exchange the session key without the hypotheses in (52) and (53). Thus, the derivations in (54) and (55) for “I” and “R” to believe the session key, respectively, require the use of the hypotheses.Perfect forward secrecy is a characteristic of robust protocols because it protects previous sessions from future key compromise attempts. Accordingly, the asymmetric variant of the EDHOC protocol leverages the unique generation of ECDH private keys for each session of the protocol run to realize perfect forward secrecy. Likewise, in the symmetric-key option of the EDHOC protocol, the generation of the secret keysK2 and K3 uses the nonstatic Diffie–Hellman session key between “I” and “R.” Thus, the symmetric-key option of the EDHOC protocol also provides perfect forward secrecy.For both symmetric and asymmetric alternatives of EDHOC protocol to provide confidentiality and integrity, secure session key exchange must be in place. However, “I” and “R” may fail to transfer this key securely, as described earlier. As a result, the protocol cannot guarantee both confidentiality and integrity security properties.Finally, due to the absence of authentication for the initial message, the anonymity of the responder’s identifier for the public authentication keys (ID_CREDR, for asymmetric-key option) and preshared key (ID_PSK, for the symmetric-key option) can be exposed.Table4 summarizes the result of the BAN-Logic derivation process for both options of the EDHOC protocol. As illustrated in the table and explanation above, both options of the protocol are insecure.Table 4
Security property satisfaction.
No.Security propertiesAsymmetric-key optionSymmetric-key optionSP1Mutual authenticationXXSP2Secure key exchangeXXSP3Perfect forward secrecy✓✓SP4ConfidentialityXXSP5IntegrityXXSP6AnonymityXX


## 3.2. AVISPA-Based Formal Verification

AVISPA is an automation tool for modelling and analysing security protocols [27]. The description of the formal verification process using AVISPA proceeds as follows. First, we use a High-Level Protocol Specification Language (HLPSL) [32] to model the protocol. The HLPSL2IF component then converts the HLPSL-modelled protocols to Intermediate Format (IF). Finally, using the On-the-Fly Model-Checker (OFMC) [33], CL-based Attack Searcher (CL-AtSe) [34], SAT-based Model-Checker (SATMC) [35], and Tree-Automata-based Protocol Analyzer (TA4SP) [36], the IF is transformed to Output Format (OF). Figure 6 shows the general system architecture of the tool, highlighting the main processes from HLPSL to OF.Figure 6
AVISPA system structure.HLPSL is composed of different roles such as Basic Role, Session Role, and Environment Role:(i)
Basic Role. This is a role that models protocol participants in a function with parameters. It consists of steps such as header expression, local variable declaration, and initialization. Additionally, it identifies communication modelling, which specifies the channel for communication between the modelled participants and indicates real-world protocol behaviour. It also defines, together with these parameters, transitions that denote message reception and the corresponding reply of the agent.(ii)
Session Role. This function receives the agents and other parameters to activate the previous role. It is executed via a composition to instantiate the parts in a parallel manner. /\ represents such parallel execution of prior roles.(iii)
Environment Role. It is a role that comprises global constants with the agents and sessions defined in the above two roles. In addition, it outlines an attacker’s knowledge of the protocol’s communication. The intruder’s knowledge concerning the execution of the protocol is also defined. Like the Session Role, parallel execution of sessions executes with the intruder’s information considered. Once the Environment Role completes, the security goals follow, and their verification proceeds with OFMC and CL-AtSe submodules.


### 3.2.1. The Asymmetric-Key Option

At first, the asymmetric-key option of EDHOC protocol is modelled in HLPSL code. The code specifies the initiator and the responder roles with their security goals, Session Role to activate the basic roles, and finally the Environment Role. The source code for the AVISPA verification for both asymmetric and symmetric variants can be found in the Supplementary Materials (availablehere), while the pseudocodes are presented in Figure 7 (for asymmetric variant) and Figure 8 (for symmetric variant). The obtained verification results for the asymmetric option based on OFMC module and CL-AtSe module are also shown in Figure 9. The attack simulation of the asymmetric-key option of EDHOC protocol is illustrated in Figure 10.Figure 7
A pseudocode for the AVISPA-based verification of asymmetric-key option of EDHOC protocol.Figure 8
A pseudocode for the AVISPA-based verification of symmetric-key option of EDHOC protocol.Figure 9
Verification result of the asymmetric-key option of EDHOC protocol.Figure 10
Attack simulation of the asymmetric-key option of EDHOC protocol.As shown in Figure10, the attack simulation shows the asymmetric-key option of EDHOC protocol is vulnerable due to the fact that the message is sent without any verification of the sender. In other words, when the intruder sends the message of step 2, the responder should generate and calculate all the elements for communication without any proof to the user. It seems to be able to induce resource exhaustion attacks in R due to Msg2 created or modified by the attacker.


### 3.2.2. The Symmetric-Key Option

Like the previous case, once we translate the protocol into an HLPSL form, the AVISPA tool passes the code through the modules (such as CL-AtSe and OFMC) to check for any security flaws. Figure11 presents the outcome of this process. According to the verification result, the symmetric-key option of the EDHOC protocol is unsafe. Figure 12 shows the possible attack simulation for the identified security flaw.Figure 11
Verification result of symmetric-key option of EDHOC protocol.Figure 12
Attack simulation of the symmetric-key option of EDHOC protocol.In Figure12, when an intruder sends a message in step 2, the responder should create all the elements for communication without user authentication as Figure 10. This may deplete R’s resource due to responses to numerous authentication requests from unauthorized users.


## 3.2.1. The Asymmetric-Key Option

At first, the asymmetric-key option of EDHOC protocol is modelled in HLPSL code. The code specifies the initiator and the responder roles with their security goals, Session Role to activate the basic roles, and finally the Environment Role. The source code for the AVISPA verification for both asymmetric and symmetric variants can be found in the Supplementary Materials (availablehere), while the pseudocodes are presented in Figure 7 (for asymmetric variant) and Figure 8 (for symmetric variant). The obtained verification results for the asymmetric option based on OFMC module and CL-AtSe module are also shown in Figure 9. The attack simulation of the asymmetric-key option of EDHOC protocol is illustrated in Figure 10.Figure 7
A pseudocode for the AVISPA-based verification of asymmetric-key option of EDHOC protocol.Figure 8
A pseudocode for the AVISPA-based verification of symmetric-key option of EDHOC protocol.Figure 9
Verification result of the asymmetric-key option of EDHOC protocol.Figure 10
Attack simulation of the asymmetric-key option of EDHOC protocol.As shown in Figure10, the attack simulation shows the asymmetric-key option of EDHOC protocol is vulnerable due to the fact that the message is sent without any verification of the sender. In other words, when the intruder sends the message of step 2, the responder should generate and calculate all the elements for communication without any proof to the user. It seems to be able to induce resource exhaustion attacks in R due to Msg2 created or modified by the attacker.


## 3.2.2. The Symmetric-Key Option

Like the previous case, once we translate the protocol into an HLPSL form, the AVISPA tool passes the code through the modules (such as CL-AtSe and OFMC) to check for any security flaws. Figure11 presents the outcome of this process. According to the verification result, the symmetric-key option of the EDHOC protocol is unsafe. Figure 12 shows the possible attack simulation for the identified security flaw.Figure 11
Verification result of symmetric-key option of EDHOC protocol.Figure 12
Attack simulation of the symmetric-key option of EDHOC protocol.In Figure12, when an intruder sends a message in step 2, the responder should create all the elements for communication without user authentication as Figure 10. This may deplete R’s resource due to responses to numerous authentication requests from unauthorized users.


## 4. Results and Discussion

The results of the formal security analysis of both variants of the EDHOC protocol show some security-related shortcomings. In this section, we discuss these flaws.The complete security analysis of the asymmetric-key EDHOC protocol depends on the assumption that the responder trusts the ephemeral ECDH public keyGX is from the initiator. Furthermore, the initiator also must believe that the responder sends the ephemeral ECDH public key GY. As shown in the BAN-Logic analysis, the hypotheses in (17) and (18) represent these two claims, respectively. Without these assumptions, mainly hypothesis (17), it is impossible to derive the goals we set. Moreover, it is worth mentioning that both hypotheses are merely there to complete the proof. Hence, it is crucial to realize them to guarantee the evidence.Similarly, the AVISPA results for both asymmetric and symmetric variants of the protocol also show that an attack can happen (Figures10 and 12). The responder’s failure to ensure the integrity of Msg1 and the difficulty of the initiator in validating Msg2 are the significant reasons for this attack. Especially for the latter point, given that the generation of the secret key K2 depends on the ECDH session key GXY, the initiator has no option but to trust the responder’s ECDH public key GY transmitted in plaintext to verify Msg2.Another critical security threat refers to the denial-of-service attacks (more specifically, the resource exhaustion attack). Given the IoT devices’ severe resource limitations concerning computation, storage, and communication, an attacker can send a significant amount of Msg1 to the responder. The responder then performs expensive operations such as encryption, signature, and key derivation functions for each of these messages before authenticating the initiator. Consequently, the responder can get easily overwhelmed by the traffic, deplete its energy, and finally cease communicating with the other end.A second serious threat with the asymmetric-key-based EDHOC protocol, which we referred to as a partial privacy attack, is related to the privacy ofID_CREDR. The access of the credentials containing the public authentication keys of both initiator and responder is via their identities. These identities (ID_CREDI and ID_CREDR), although they do not have any cryptographic purpose in the protocol, serve an essential purpose by facilitating the retrieval of the public authentication keys. Moreover, according to the standard, their privacy is protected by the session key computed by the initiator and responder. Thus, an attacker can easily break the privacy of ID_CREDR as it can establish the session key K2 with the responder. Therefore, it implies a privacy disclosure of one of the two identities, hence a partial privacy attack. Concerning the symmetric variant, a clear violation of privacy also happens as ID_PSK in Msg1 is transmitted in plain text.It is important to note that if an attacker exploits these vulnerabilities, the results might be disastrous. For example, a medical IoT device attempting to obtain a remote service, perhaps for remote diagnostics, may fail owing to a resource depletion assault on the other end. Moreover, in cases where the responder is a sensitive medical IoT device, its identity (the identity of the credentials containing the public authentication keys) can be traced by an attacker that he/she may use to track and localize the patient eventually. Both resource exhaustion and privacy attacks (as part of transporting EDHOC via CoAP message exchanges) are shown in Figure13. In addition, Table 5 summarizes the security issues identified by the related works together with the ones we identified.Figure 13
Attack simulation of the symmetric-key option of EDHOC protocol.Table 5
Summary of related works.
PapersIdentified security issuesEDHOC versionAnalysis tools used[22](i) Disclosure of the responders identity in the asymmetric variant of the EDHOC protocol.Draft-selander-ace-cose-ecdhe-08 [20]ProVerif [24](ii) An attacker can associate numerous sessions and perform attacks for the symmetric variant of the EDHOC protocol by using the same preshared key identifier.(iii) Only AD3 (for both symmetric and asymmetric variants) satisfies secrecy, perfect forward secrecy, and integrity at both the time of message arrival and the conclusion of the protocol.[23](i) Absence of nonrepudiation security property.Draft-selander-lake-edhoc-01 [21]Tamarin [25](ii) Lack of verification of ID_CREDR of Msg2 by the initiator.(iii) When the responder rejects recommended cipher suites, a security concern might arise because of a lengthy metasession spanning many EDHOC sessions.Ours(i) A resource exhaustion attack due to a significant amount of Msg1 sent to the responder. The responder does not authenticate Msg1 before computing expensive operations, hence depleting its resources.Draft-ietf-lake-edhoc-07 [19]BAN-Logic and AVISPA [26, 27](ii) The responder’s failure to ensure the integrity of Msg1 and the difficulty of the initiator in validating Msg2 threaten the security of the protocol.(iii) A partial privacy attack that exposes the responder’s identity. Beside the mere violation of the secrecy of the responder’s distinctiveness, it can enable the attacker to reduce the difficulty of stealing the public authentication keys by one step. Moreover, the privacy of ID_PSK, in symmetric-key option, is also violated as it is transmitted in plain text.It is critical to fix the highlighted security vulnerabilities before using EDHOC as a lightweight authenticated key exchange mechanism. Privacy-related threats are mainly initiated because the first message, from the initiator to the responder, is not authenticated. Hence, a preliminary authentication mechanism must be implemented. The responder and initiator can additionally guarantee the validity of Msg1 and Msg2 by using public-key certificates. In the case of a protracted metasession spanning several EDHOC sessions due to cipher suite rejection, the responder shall provide a mechanism that prevents the same initiator from resubmitting a new cipher suite proposal in the same session more than twice. Leveraging HMAC and timestamps can serve a good purpose in thwarting resource exhaustion attacks, as they let the responder first check the validity of the received message before performing computationally demanding instructions.


## 5. Conclusions

Although the rapid growth of the Internet of Things (IoT) technology is bringing a significant impact on society, efficient security protocols that are aware of the unique characteristics of IoT devices are still in their infant stage. With this regard, IETF is in progress to standardize one application layer protocol (known as EDHOC) that can assist secure communication across IoT devices while remaining lightweight. Consequently, in this paper, we formally analysed the security of this protocol using BAN-Logic and AVISPA to investigate its resilience to withstand attacks. The results show that both variants of the protocol have some serious security and privacy flaws. Primarily, a resource exhaustion attack that violates the availability of a responder’s service by depleting its resources over expensive cryptographic operations such as encryption and signature can result. Next, an attacker can easily break the privacy ofID_CREDR as it can establish the session key K2 with the responder, which results in partial privacy disclosure of the responder’s identity. A similar attack can happen when an attacker captures ID_PSK in the symmetric-key option of the protocol. Furthermore, an attacker can use the responder’s failure to verify the integrity of Msg1 and the difficulties of the initiator in validating Msg2. Finally, we recommend that the protocol should consider authenticating the first message and provide a way to validate the second message while offering a solution to protect against resource exhaustion attacks. In future works, the authors would like to develop efficient solutions to mitigate these attacks while maintaining the lightweight nature of the EDHOC protocol.



---

*Source: 7314508-2021-09-13.xml*