# LAKEE: A Lightweight Authenticated Key Exchange Protocol for Power
Constrained Devices

Seyedsina Nabavirazavi
Florida International University
<EMAIL_ADDRESS>
&S. Sitharama Iyengar
Florida International University
<EMAIL_ADDRESS>

###### Abstract

The rapid development of IoT networks has led to a research trend in designing
effective security features for them. Due to the power-constrained nature of
IoT devices, the security features should remain as lightweight as possible.
Currently, most of the IoT network traffic is unencrypted. The leakage of
smart devices’ unencrypted data can come with the significant cost of a
privacy breach. To have a secure channel with encrypted traffic, two endpoints
in a network have to authenticate each other and calculate a short-term key.
They can then communicate through an authenticated and secure channel. This
process is referred to as authenticated key exchange (AKE). Although Datagram
Transport Layer Security (DTLS) offers an AKE protocol for IoT networks,
research has proposed more efficient and case-specific alternatives. This
paper presents LAKEE, a straightforward, lightweight AKE protocol for IoT
networks. Our protocol employs elliptic curve cryptography for generating a
short-term session key. It reduces the communication and computational
overhead of its alternatives while maintaining or improving their security
strength. The simplicity and low overhead of our protocol make it a fit for a
network of constrained devices.

_K_ eywords Authenticated Key Exchange $\cdot$ Authentication $\cdot$ Session
Establishment $\cdot$ Elliptic Curve Cryptography $\cdot$ Internet of Things
$\cdot$ Constrained Application Protocol $\cdot$ IoT $\cdot$ Protocol Design
$\cdot$ Smart City

##  1 Introduction

###  1.1 The Rise of IoT

Security issues of IoT networks have been a focal point for researchers since
the rise of IoT. Research has offered various mechanisms for achieving
security goals, i.e., confidentiality, integrity, and availability in this
field. However, providing security would not be straightforward in this
domain. IoT devices are power-constrained and have specific functionality.
Using general-purpose protocols for every IoT device would result in more
battery consumption and less quality of service. Therefore, numerous protocols
have been proposed for each layer of the IoT protocol stack. IoT designers
have to choose between WiFi, Bluetooth, ZigBee, LoRaWan, and Z-Wave as their
network protocol. Moreover, there is no standard solution for handling
security issues in IoT, such as IPSec or SSL for the Internet. In the
application layer, Constrained Application Protocol (CoAP) and MQTT are mainly
used between the constrained IoT devices and servers. MQTT protocol [1] has
some limitations. For example, it can be used only for very low processor
devices and can communicate mainly with Amazon cloud applications for servers.
CoAP uses RESTful architecture to access the resources from a server through
URI (Universal Resource Identifier) and message communication. [2], [3] These
two application layer protocols provide security features which are far from
being perfectly efficient.

###  1.2 The Problem of AKE

One of the classic security problems is the design of authenticated key
exchange protocols in which two parties authenticate each other and agree on a
session key. The parties involved have to prove their claimed identity. The
AKE protocol should be secure against an active adversary who can inject,
modify, and delete packets. Most common AKE protocols rely on a trusted third
party to certify the claimed identity of parties. In Transport Layer Security
(TLS) handshake, for example, the server’s identity is verified using the
server’s public key and the digital signature of the SSL certificate
authority. In Kerberos, the Authentication Server and the Ticket Granting
Server are trusted third parties. [4] Some AKE protocols, such as Google’s
QUIC protocol, are multi-stage. In these protocols, different runs of the
protocol are not independent, and the former keys are used to derive the next
key [5]. In some cases, AKE is based on a pre-shared secret between parties.
The high entropy pre-shared secret ensures forward secrecy. In this paper, we
present LAKEE, an AKE protocol which is certificateless and based on a pre-
shared secret. Our protocol avoids the public key infrastructure by using
symmetric keys to be as lightweight as possible for employment in IoT
networks. [6]

We implement our protocol as an application on top of CoAP. Research has an
interest in building application layer protocols, such as HTTP [7] and SOAP
[8], on top of CoAP. Our practice is the same.

The contributions of the present work can be summarized below.

  * •

We propose a lightweight and effective protocol which guarantees secure
communication by establishing a secure session. We have implemented our
protocol in Python using the aiocoap [9] library.

  * •

The protocol can easily integrate with the existing system deploying DTLS-PSK
without requiring additional code.

  * •

After session establishment, the transport layer can use the generated key to
encrypt application layer messages securely. More precisely, the session
parameters are mapped to the DTLS session parameters without requiring any
modification in the existing session format for DTLS-PSK mode. Thus the
transport layer can protect the application layer message using the encryption
mechanism of DTLS-PSK.

  * •

We estimate our protocol’s communication and computation overhead and compare
it with the alternative protocols. We prove that the overhead of the protocol
is significantly less than its competitors.

  * •

We verify the security strength of the proposed protocol both by formal logic
and simulation tools.

##  2 Related Work

Many researchers have focused on balancing the tradeoff between security and
overhead of session establishment protocols in the context of IoT devices. Pan
et al. [10] offer a lightweight certificateless protocol based on elliptic
curves and bilinear pairing. However, a third component, as a key generation
center (KGC), is required. The total number of messages for key exchange is
also 4, which is more than our proposed protocol. It is not clear which
participant is responsible for initiating the protocol.

Kalra et al. [11] and Kumari et al. [12] proposed authentication methods, but
they depend on HTTP cookies. Moreover, when the cookie of a user-server
connection resets, the number of steps is increased to 5. It is also shown
that the Kalra and Kumari protocols are not desirably secure. [12], [13]

Shin et al. [14] have proposed a security framework for MQTT, enabling the
client and server to come up with a symmetric session key based on the AugPAKE
protocol. [15] The protocol proposed by Yeh et al. [16] is a lightweight
authentication method which employs elliptic curve cryptography and hashing to
provide two endpoints with a session key. Hashing is known to be more
efficient than encryption and can therefore benefit IoT networks. However, the
method is dependent on a third element called Registration GW-node. Moreover,
the login phase has 4 messages. Albalas et al. apply both
Rivest–Shamir–Adleman (RSA) and Elliptic Curve Cryptography (ECC) for key
generation in CoAP and discuss the advantages of ECC. The session key
establishment scheme proposed by Dey and Hossain [17] has 7 steps involving 3
participants; the smart device, the service provider, and the home gateway.

Bhattacharyya et al. [18] have proposed LESS, a simple and lightweight
authenticated key exchange protocol for IoT devices. The proposed protocol is
implemented on top of the CoAP layer. The main difference between LESS and our
protocol is the session key generation. In LESS, the server is responsible for
choosing the session keys, which are transferred to the client in the second
and fourth messages of the protocol. Majumder et al. [19] have also proposed
an authenticated key exchange protocol based on ECC. They verify the security
strength of their protocol both formally (using the BAN logic) and practically
(using the AVISPA simulation tool). However, their protocol, ECC-CoAP, is not
implemented, and its compatibility with CoAP is not verified. For example,
CoAP may unexpectedly fragment the messages if they are larger than a limit.

##  3 Background

###  3.1 Constrained Application Protocol (CoAP)

CoAP is an application layer protocol for resource-constrained internet
devices. For web integration, CoAP can be converted to HTTP. It also meets the
fundamental requirements of IoT communication, which are multicast support,
low overhead, and simplicity. CoAP is built on top of the User Datagram
Protocol (UDP). As UDP is unreliable, unlike Transmission Control Protocol
(TCP), an optional request/response layer is included in the messaging. The
CoAP message structure is shown in figure 1 CoAP supports four types of
messages: Confirmable (CON), Non-Confirmable (NON), Acknowledgement (ACK), and
Reset (RST). A confirmable message guarantees reliability. Each confirmable
message is replied to with an ACK by the server with the same message ID.
Otherwise, it will be retransmitted using a default timeout and exponential
back-off between retransmissions. However, non-confirmable messages are
unreliable and are not replied to with an ACK. If the recipient cannot process
a Non-confirmable message, it may reply with an RST message.

Figure 1: CoAP message structure [20]

###  3.2 Elliptic Curve Cryptography (ECC)

ECC, proposed by Victor Miller and Neal Koblitz [21], [22], is a key-based
cryptography technique based on the algebraic structure of elliptic curves
over finite fields. It usually is an alternative to the RSA cryptographic
algorithm. ECC features smaller ciphertext, keys, signatures and a faster
generation of keys and signatures. The fundamental downside of ECC is that,
due to the complexity of its mathematical foundation, it is difficult to
implement securely.

An elliptic curve $E$ is defined over a prime finite field $F_{p}$. This
smooth projective curve of genus 1 is denoted as $E/F_{P}$ and holds the
following elliptic curve equation:

$y^{2}mod\,p=(x^{3}+ax+b)mod\,p$

We employ the mathematical operation of scalar point multiplication to perform
an Elliptic Curve Diffie–Hellman Key Exchange (ECDH). The security strength of
ECC lies in the difficulty of solving the Elliptic Curve Discrete Logarithm
Problem (ECDLP). Similar to the Diffie-Helman Problem (DHP), ECDLP is based on
the discrete logarithm problem and does not pursue any polynomial-time
algorithm.

###  3.3 Datagram Transport Layer Security (DTLS)

IoT applications frequently encounter a variety of communication patterns that
the Transmission Control Protocol (TCP) is unable to support effectively. Due
to energy constraints, devices may often go into sleep mode; thus, it is
infeasible to maintain a long-lived connection in IoT applications. In
consequence, IoT networks use UDP as the transport protocol. Therefore, the
SSL/TLS protocol, which makes TCP secure, is not applicable to the IoT
environment. IoT networks can benefit from DTLS, which is a derivation of TLS
protocol and provides the same security services on top of UDP.

CoAP can optionally use DTLS. CoAP defines four security modes.

  * •

NoSec.

  * •

PreSharedKey,

  * •

RawPublicKey,

  * •

Certificate

DTLS provides CoAP with a nonoptimal handshake protocol with a long-lived key
in the PresharedKey mode. It takes 6 messages (7 steps) to establish a session
with this handshake. [23], [24] DTLS handshake protocol which can be used in
CoAP for session establishment, is illustrated in figure 2.

Figure 2: DTLS session-establishment in the PreSharedKey mode

##  4 Proposed Protocol

In this section, we present the LAKEE protocol completely. $X\rightarrow S:M$
denotes X sends message M to S. Figure 3 illustrates the protocol, which has 4
steps including 3 messages, while Table i@ explains the notations used.

Figure 3: Proposed protocol for authenticated key exchange Table 1: Symbols & Notation table Notation | Description
---|---
C | client/IoT device
S | server
$F_{p}$ | large prime finite field over p
P | a generator point on $E/F_{p}(a,b)$ with order n
$E_{p}(a,p)$ | an elliptic curve over the finite field $F_{p}$ and cyclic group generator $P$
Y | long-term symmetric key between client and server
$r_{c}$ | random number selected by the client
$r_{s}$ | random number selected by the server
$client\\_rand$ | client’s shared data for producing the session key where $client\\_rand=r_{c}.P$
$server\\_rand$ | server’s shared data for producing the session key where $server\\_rand=r_{s}.P$
$[E(.)_{k}]$ | authenticated encryption of a plaintext using a symmetric key k
$h(m)$ | unkeyed one-way hash value of message m
$\|$ | concatenation
$\\#C_{i}$ | client identifier
$a.P$ | scalar point multiplication; Point P is multiplied by scalar a.

###  4.1 Pre-negotiation

Before starting the handshake, the client and server must have agreed upon a
prime finite field, an elliptic curve, a generator point, a key derivation
function, and the symmetric high-entropy key Y.

###  4.2 Step 1. Client Challange

$C\rightarrow S:\\#C_{i},E_{y}(h(\\#C_{i}),client\\_rand,T1)$

At first, the client generates a random number ($r_{c}$). It then computes
client’s challenge as $client\\_rand=r_{c}.P$. The client concatenates the
hash of its ID, client_rand, and current timestamp and encrypts the outcome
with the pre-shared key Y. The client then sends its ID with the encrypted
message to the server. The server recognizes the raw identifier, associating
this message with a session initiation request. The client reveals his
identity in this message. The novelty of our protocol is that the client
challenges and authenticates the server first, reducing the required number of
messages.

###  4.3 Step 2. Server Response and Challenge

$S\rightarrow C:E_{y}(client\\_rand+P,server\\_rand,T2)$

or

$S\rightarrow C:E_{y}(client\\_rand+2P,server\\_rand,T2)$

After receiving the session initiation message from the client, the server
checks the number of failed session initiation requests within a time frame
originating from the message’s source IP address. If it’s greater than 3, the
message is not processed. Otherwise, the server tries to decrypt the message
using the pre-shared key. The server records the current time and checks
$|T_{2}-T_{1}|\leq\Delta T$. If it holds, the shared secret is retrieved, and
a random number is generated ($r_{s}$). The server then computes the server’s
challenge as $server\\_rand=r_{s}.P$. It decides whether it is time to change
the long-term secret (Y). The strategy with which the server chooses the time
is out of the scope of the paper and is dependent on the information it stores
about the clients. If the server decides to maintain Y, it sums the client’s
challenge with generator P ($client\\_rand$ is a point on the curve). It then
sends the result alongside its own challenge to the client. If it decides to
change Y during the handshake, it sums the client’s challenge with twice the
generator (2P) and sends the result alongside its own challenge to the client.
When the information in the incoming is irrelevant, the handshake is
terminated, and the number of failed attempts from the client’s IP range is
increased.

###  4.4 Step 3. Server Authentication and Client Response

$C\rightarrow S:E_{y}(server\\_rand+P,T3)$

or

$C\rightarrow S:E_{y}(server\\_rand+2P,T3)$

In this stage, the client decrypts the server’s message with the shared
secret. It records the current time and checks $|T_{3}-T_{2}|\leq\Delta T$. If
it holds, the client verifies the server’s response provided that the message
contains $client\\_rand+P$ or $client\\_rand+2P$. In the second case, it
realizes that it should update Y during this handshake. The client then
calculates $server\\_rand+P$ or $server\\_rand+2P$ accordingly. It
concatenates it with the current timestamp, encrypts the outcome, and sends
the message to the server. The client locally calculates a shared secret which
is a point on the elliptic curve.

$secret=rc.server\\_rand$

Using the horizontal position of the secret on the curve and the agreed key
derivation function (KDF), the client calculates the session key.

$session\\_key=KDF(secret_{x})$

If it also had to update Y, it calculates a new long-term key using the
vertical position of the secret on the curve and the KDF.

$Y^{\prime}=KDF(secret_{y})$

###  4.5 Step 4. Client Authentication

In this stage, the server decrypts the client’s message with the shared
secret. It records the current time and checks $|T_{4}-T_{3}|\leq\Delta T$. If
it holds, the server verifies the client’s response the same as the previous
step and calculates the session key.

$secret=rs.client\\_rand$

Using the horizontal position of the secret on the curve and the KDF, the
server calculates the session key.

$session\\_key=KDF(secret_{x})$

If it also had to update Y, it calculates the following.

$Y^{\prime}=KDF(secret_{y})$

In contrast with typical Internet users, each IoT device reaches out to a
limited number of servers. We assume, as a consequence, that providing each
client-server pair with a shared secret is feasible. Our certificateless
protocol is independent of any authorities and third parties. Therefore, the
proof of the parties’ identity relies on the possession of the pre-shared and
symmetric secret. As it is certificateless, our protocol with minor changes is
employable in mesh IoT networks where any node can act as a client or a server
dynamically.

##  5 Implementation

We have implemented our protocol on top of CoAP using the aiocoap python
library. [9] We aimed to have a reproducible implementation, and it serves
only as self-documenting code. We acknowledge that it could be more efficient
by employing C++, for example. It is publicly available on Github111Please
refer to https://github.com/sina-nabavi/LAKEE-over-aiocoap.. The client
performs all of the steps sequentially and in a single function. In contrast,
the server would not block for an individual client. Therefore, it must store
the handshake progress information, such as the challenge it sent to that
particular client, and process the corresponding client’s response upon
reception. The first message (client challenge) is a Confirmable (CON)
message. The second message (server response and challenge) is the
Acknowledgement (ACK) of the first, and the third message’s (client response)
type is Non-Confirmable (NON). After sending the third message, the client
would not wait for a reply from the server.

We have used the PyCryptodome package for encryption and elliptic curve
operations. The AES block cipher is used because it has been standardized and
resistant to side-channel attacks. Moreover, there are hardware acceleration
mechanisms available for AES. The cipher in the CCM mode calculates a message
authentication code (MAC) for each message to verify whether the received data
is authentic. We employ the curve edwards448, also known as Ed448-Goldilocks,
with the following equation. [25]

$-x^{2}+y^{2}=1-39081x^{2}y^{2}$

The curve aims for a 224-bit security level, meaning that it is designed to
increase the cost of breaking a discrete logarithm computation to $2^{224}$
bit operations. [26] Daniel J. Bernstein and Tanja Lange have shown that this
curve meets the ECDLP and ECC requirements. [27] However, Edwards448 points
and scalars are bigger than those of other curves. We use a fixed 128-bit
shared secret and the base point of the curve as the generator. PBKDF2 is used
with SHA512 for deriving the session keys and new long-term secrets. [28] The
ECDH secret has enough entropy for us to derive the keys without a salt and a
large iteration number. The iteration number is 16 in the implementation.

The code reports the execution time at the end of the handshake. It varies by
the running hardware. Once the key exchange has finished, the responsibility
can shift from CoAP to DTLS for providing channel security. With the correct
parameters, a DTLS session can be instantiated without having to perform the
DTLS_PSK 7-step handshake.

  * •

cipher suite = TLS_PSK_WITH_AES 128 CCM 8

  * •

read state = S_k.x with encryption nonce

  * •

write state = S_k.y with encryption nonce

Along with the above parameters, one has to instantiate the client and
server’s initialization vectors, generate a sequence number, and fill other
parameters for the desired DTLS session, such as Peer certificate with NULL.

##  6 Security Evaluation

In this section, we evaluate the security strength of our protocol.

###  6.1 Properties of the Protocol

The security goals are achieved as stated below.

  * •

Confidentiality: All the secrets, including the timestamps and challenges, are
encrypted.

  * •

Integrity: We use the AES-CCM ciphersuite, which performs MAC(message
authentication code)-then-Encrypt for every message. The MACs and the hash of
the client ID guarantee the integrity of messages.

  * •

Entity Authentication: Instead of digital signatures and certificates, the
approach of this protocol for entity authentication is challenge-response. The
random numbers used for building the session keys are used as challenges, and
the other party needs the pre-shared secret and the negotiated curve to be
able to process them.

  * •

Message Authentication: As stated, MACs computed for transmitted messages
provide message authentication.

  * •

Non-repudation: As the client is expected to be an IoT device for which there
are pre-defined tasks, we do not count non-repudiation as a necessary property
for our protocol. Hence, we base our protocol on the pre-shared symmetric key.
Also, instead of digital signatures, which provide non-repudiation, we use
MACs which provide authentication.

  * •

Perfect Forward Secrecy: In the proposed scheme, if the key Y is compromised
and the adversary is able to read $client\\_rand$ and $server\\_rand$, he
cannot calculate the session key as he should obtain at least one of the
secret randoms. The adversary cannot obtain the secret randoms from
$client\\_rand$ and $server\\_rand$ due to the hardness of the elliptic curve
discrete logarithm problem.

###  6.2 Quantitative Security Analysis

In this part, we discuss the security of our protocol against famous attacks.
Table 2 compares the security strength of LAKEE with alternative protocols.

####  6.2.1 Man-in-the-Middle Attack

The assumption of our scheme is that the pre-shared key (i.e., $Y$) remains a
secret. Consequently, an adversary would not be able to modify plain messages,
including the session initiation message. Besides, the MACs computed for each
message make them unforgeable.

####  6.2.2 Denial-of-Service (DoS) Attack

The number of times an IoT device can attempt to be authenticated is limited
within a timeframe. In the session initiation phase of our scheme, if the IoT
device fails to be authenticated by the server within 3 attempts, the IoT
device will be blocked for a specific period. Hence, an adversary will not be
able to send multiple requests (more than 3) to overload the system resource
to make the services unavailable to the legitimate client. Thus, our protocol
restricts the DoS attack.

####  6.2.3 Replay Attack

A timestamp is associated with each message. If a participant receives an old
message, it is not processed, and the connection is terminated. Hence, an
adversary may not be able to use the captured messages to perform a replay
attack. The adversary is also not able to change the timestamps as they are
encrypted and protected with MAC.

####  6.2.4 Insider Attack

In this type of attack, an insider of the remote server acts as an adversary
after getting some user credentials stored on the remote server. As the
session key cannot be computed by acquiring $client\\_rand$ and $\\_rand$ and
the adversary needs to know at least one of the random secrets, the protocol
is safe against insider attack.

####  6.2.5 User and Server Impersonation Attack

As the attacker is not in possession of key Y, it cannot impersonate either
client or server as all the messages include MACs and cannot be forged.

####  6.2.6 Offline Password Guessing Attack

This attack mainly occurs in password-based authentication schemes, which is
also a challenge-response scheme. However, in our proposed scheme, the
challenge will differ at each epoch. Hence, the attacker cannot randomly guess
the response to authenticate himself.

####  6.2.7 Known Session Specific Temporary Attack

The session key is calculated at the ends, not transmitted with the messages.
Hence, LAKEE is secure against known session specific temporary attack.

####  6.2.8 Invalid Curve Attack

When the attacker forces the server to compute a common secret using a point
outside the defined curve, an invalid curve attack has occurred. As the client
and server verify random points they receive, i.e., $client\\_rand$ and
$server\\_rand$, they would terminate the connection if each point is in
infinity or outside the chosen curve.

####  6.2.9 The MOV attack

As all the points are transferred encrypted, we would not expect an adversary
to obtain the random points (i.e., $server\\_rand,client\\_rand$). If any of
the random points are guessed or acquired in polynomial time, there are two
ways to prevent the adversary from obtaining the generator point (i.e., P). 1)
Keep the embedding degree k greater than 100. 2) If the curve’s subgroup
divides the curve order, then the embedding degree should be the smallest
$k\geq 2$ such that $n|q^{k}-1$ for all values k from 2 to 100.

Table 2: Security Strength Secure Against | LESS [18] | Dey et al. [17] | ECC-CoAP [19] | LAKEE
---|---|---|---|---
Man-in-the-middle attack | Yes | Yes | Yes | Yes
Denial-of-service (DoS) attack | No | No | Yes | Yes
Replay attack | Yes | Yes | Yes | Yes
Insider attack | Yes | Yes | Yes | Yes
User impersonation attack | Yes | Yes | Yes | Yes
Server impersonation attack | Yes | No | Yes | Yes
Offline password guessing attack | No | No | Yes | Yes
Known session specific temporary attack | Yes | Yes | Yes | Yes
Session key computation attack | Yes | Yes | Yes | Yes
Invalid curve attack | N/A | N/A | No | Yes
The MOV attack | N/A | N/A | No | Yes

###  6.3 AVISPA Tool

In this section, we demonstrate that LAKEE is secure against relevant threats
using the Automated Verification Internet Security Protocol and Applications
(AVISPA) simulator program.

####  6.3.1 Introduction to the AVISPA Simulation Tool

AVISPA is a role-based simulator that assigns a specific role to each protocol
participant. A specification provided in a supported language is used to
verify a protocol. The primary language supported by AVISPA is High-Level
Protocol Specification Language (HLPSL). The working structure of AVISPA is
depicted in figure 4. HLPSL2IF translates HLPSL specification into an
Intermediate Format (IF), where IF is a low-level language. The backends of
the AVISPA tool use IF to analyze whether the security and authentication
goals written in the specification are satisfied or violated. The AVISPA then
produces the output SAFE and UNSAFE, respectively. The current version of the
AVISPA tool supports 4 different types of backends.

  * •

On-the-fly Model Checker (OFMC)

  * •

Constraint logic-based attack searcher (CL-At Se)

  * •

State of the Art based Model Checker (SATMC)

  * •

Tree Automata based protocol for the security protocol analysis (TA4SP)

Figure 4: The architecture of the AVISPA tool

####  6.3.2 OFMC

The AVISPA tool includes several backends for analyzing protocols. We use
OFMC, a tool for falsification or verification for a bounded number of
sessions. OFMC employs the Dolev-Yao intruder model [29] to check several
parallel sessions executed by honest agents. The input to this backend is a
description of a transition system, and the output is either SAFE, showing
that limited sessions are secure, or UNSAFE with an attack trace.

####  6.3.3 HLPSL

We now discuss the basics of the AVISPA tool’s protocol specification
language. HLPSL is a role-based language with which we can specify the actions
of each participant in a protocol. For specifying a protocol in the HLPSL
language, we have to define the following.

  * •

Basic Roles: For both the client and the server, we have to define a role,
including their actions, such as receiving and sending messages in certain
formats.

  * •

Transitions: Each transition is the representation of the receipt of a message
and the sending of a reply message. Transitions are defined for a certain
role.

  * •

Composed Roles: For grouping our basic roles and representing a whole protocol
session, we have to define a session role. For storing the global constants
and composition of multiple sessions, we have to define an environment role.
The intruder can actively take action in this environment. These composed
roles do not have a transition section, but they have a composition section in
which the basic roles are instantiated.

  * •

Security Goals: In the environment role, we have to declare which parameters
are shared secrets and which parameters are used for the authentication of
participants.

For more information about the syntax of HLPSL and examples, please refer to
the AVISPA manual. [30]

####  6.3.4 Simulation Results

We have defined our protocol in HLPSL with the following simplifications. We
have not included timestamps and have defined elliptic curve mathematical
functions simply as hash functions.

Figure 5: AVISPA verification result

⬇

role client(C: agent, S:agent, K:symmetric_key,Mul: hash_func,

X:text,

Succ: hash_func,

SND, RCV: channel(dy))

played_by C def=

local State:nat,

Ci: text,

Rc, Client_rand, Server_rand, SK: message

const

sec_1, sec_2, sec_3, sec_4,

auth_1,auth_2:protocol_id

init State:= 0

transition

1. State=0 /\ RCV(start) =|>

State’:=2 /\ Rc’ := new()

/\ secret(Rc’, sec_1,{C})

/\ Client_rand’ := Mul(Rc’.X)

/\ Ci’ := new()

/\ SND({Succ(Ci’).Client_rand’}_K)

/\ secret(Client_rand’, sec_2,{C,S})

2. State=2 /\ RCV({Succ(Client_rand).Server_rand’}_K)=|>

State’:=4 /\ SK’:=Mul(Rc.Server_rand’)

/\ SND({Succ(Server_rand’)}_K)

/\ witness(C,S,auth_2, Server_rand’)

/\ request(C,S, auth_1, Client_rand)

end role

%%%

role server(S: agent,C:agent, K: symmetric_key, Mul: hash_func,

X: text,

Succ: hash_func,

SND,RCV:channel(dy))

played_by S def=

local State: nat,

Ci: text,

Rs, Server_rand, Client_rand, SK: message

init State:=1

transition

1. State=1 /\ RCV({Succ(Ci’).Client_rand’}_K)=|>

State’ :=3 /\ Rs’ := new()

/\ secret(Rs’, sec_3,{S})

/\ Server_rand’ := Mul(Rs’.X)

/\ secret(Server_rand’, sec_4,{S,C})

/\ SND({Succ(Client_rand’).Server_rand’}_K)

/\ witness(S,C, auth_1, Client_rand’)

2. State=3 /\ RCV({Succ(Server_rand)}_K)=|>

State’ := 5 /\ request(S,C, auth_2, Server_rand)

/\ SK’ := Mul(Client_rand.Rs)

end role

%%%

role session(C: agent, S: agent, K: symmetric_key, Mul: hash_func, X: text,
Succ: hash_func)

def= local SNDC, RCVC, SNDS, RCVS: channel(dy)

composition

client(C, S, K, Mul, X, Succ, SNDC, RCVC) /\

server(S, C, K, Mul, X, Succ, SNDS, RCVS)

end role

%%%

role environment()

def=

const

c,s, i: agent,

kcs, kci, kis: symmetric_key,

x: text,

succ: hash_func,

mul: hash_func

intruder_knowledge = {c,s, kci, kis, succ, mul}

composition

session(c,s,kcs,mul,x,succ) /\

session(c,s,kcs,mul,x,succ) /\

session(c,i,kci,mul,x,succ) /\

session(i,s,kis,mul,x,succ)

end role

goal

secrecy_of sec_1

secrecy_of sec_2

secrecy_of sec_3

secrecy_of sec_4

authentication_on auth_1

authentication_on auth_2

end goal

environment()

In our specification, the client authenticates the server on comprehension of
SRand (server_rand), and the server authenticates the client on comprehension
of CRand (client_rand). SRand, CRand, Srand (rs), and Crand (rc) are shared
secrets. We have not included the session key in shared secrets as it is not
transferred in the protocol. We have used the SPAN + AVISPA virtual machine
and SPAN graphical tool [31] to parse our specification and the OFMC backend
to verify our protocol. The result in figure 5 indicates that our protocol is
safe.

###  6.4 Formal Verification Using the SVO Logic

Although Majumder et al. [19] and Mahmood et al. [32] use the BAN logic [33]
in order to verify their protocol formally, we firmly believe that BAN logic
is not suitable for verifying key exchange protocols. Alternatively, we use
the SVO Logic [34]. Syverson and Oorschot [34] revealed that BAN analysis
might lead to inappropriate conclusions in some settings. Therefore, they
presented a logic capturing the desirable properties of the BAN family of
logics, including BAN [33], AT [35], GNY [36], and VO, [37] that is both sound
and relatively easy to use

####  6.4.1 Preliminaries of SVO Logic

In this section, we briefly review the SVO logic, the notations, rules, and
axioms. However, we omit some definitions unused in our analysis, such as the
concept of public key. [38]

##### Notation

The entities’ names who want to perform an authenticated key exchange are
Client and Server. We have assumed that the Client and Server have shared a
long-term key. We use the symbols for Client (C), Server (S), the pre-shared
key (Y), and the session key (k).

P believes X : The principal P may act as though X is true.

P received X : The principal P received a message containing X. P can read and
repeat X.

P said X : The principal P at some time sent a message including X.

P says X : The principal P must have said X since the beginning of the current
protocol run.

P has X : X is either,

  * •

Initially available to P,

  * •

Received by P,

  * •

Freshly generated by P,

  * •

Constructible by P from the above.

P controls X : The principal P has jurisdiction over X. P is an authority on X
and should be trusted on this matter.

fresh (X) : X has not been sent in any message prior to the current protocol
run.

$P\xleftrightarrow{\text{k}}Q$ : P and Q may use the shared key k to
communicate. k will never be discovered by any principal but P,Q, or a
principal trusted by P or Q.

$PK_{\delta}(P,k)$ : k is a public key-agreement key of P. A Diffie-Hellman
key formed with k is shared with P.

$\\{M\\}_{k}$ : Encryption of message M using key k. Encrypted messages are
uniquely readable and verifiable as such by holders of the right keys.

$P\xleftrightarrow{\text{k}{-}}Q\equiv(P\xleftrightarrow{\text{k}}Q\wedge
P\text{ has }k)$ : No one aside from P and Q and those they trust knows or
could deduce k. While P knows k, Q may or may not. k is said to be P’s
unconfirmed secret.

$P\xleftrightarrow{\text{k}{+}}Q$ : P knows k, and has received evidence
confirming that Q knows k. No parties other than P and Q and those they trust
knows k. k is P’s confirmed secret suitable for Q.

##### SVO Rules

The SVO logic has two inference rules:

Modus Ponens : From $\varphi\,$ and $\varphi\rightarrow\psi$ infer $\psi$

Necessiation : From $\vdash\varphi$ infer $\vdash\text{P believes}\,\varphi$

’$\vdash$’ is a metalinguistic symbol. ’$\Gamma\,\vdash\,\varphi$’ means that
$\varphi$ is derivable from the set of formulae $\Gamma$ and the stated axioms
using the inference rules. ’$\vdash\varphi$’ is a theorem, i.e., derivable
from axioms alone without any additional assumptions.

##### SVO axioms

In this part we introduce the SVO axioms.

Belief Axioms
1\. $(\textit{ P believes }\varphi\wedge\textit{ P believes
}(\varphi\rightarrow\psi))\rightarrow\textit{ P believes }\psi$
2\. $\textit{ P believes }\varphi\rightarrow\textit{ P believes (P believes
}\varphi)$

Source Association Axiom
3\. $(P\xleftrightarrow{\text{k}}Q\wedge\textit{R received }\\{\textit{X from
Q}\\}_{k})\rightarrow(\textit{Q said X}\wedge\textit{ Q has X})$

Key Agreement Axiom
4\. $(PK_{\delta}(P,k_{P})\wedge PK_{\delta}(Q,k_{Q}))\rightarrow
P\xleftrightarrow{F_{0(k_{P},k_{Q})}}Q$

$F_{0}(k,k^{\prime})$ implicitly names the (Diffie-Hellman) function that
combines $k$ with $k^{-}1$ (or, $k^{\prime}$ with $k^{-}1$) to form a shared
key. This is the axiom the BAN logic lacks.

Receiving Axioms
5\. $\textit{P received }(X_{1},...,X_{n})\rightarrow\textit{P received
}X_{i},\textit{for i = 1,...,n}$
6\. $(\textit{P received}\\{X\\}_{k+}\wedge\textit{P has
}k^{-})\rightarrow\textit{P received X}$

Here $K^{+}$ and $k^{-}$ are used to abstractly represent cognate keys, wheter
symmetric or assymetric. In the symmetric case, $k^{+}=k^{-}=k$. In the
assymetric case, $k^{+}$ is a public key and $k^{-}$ is the private key.

Posession Axioms
7\. $\textit{P received X }\rightarrow\textit{P has X}$
8\. $\textit{P has }(X_{1},...,X_{n})\rightarrow\textit{P has
}X_{i},\textit{for i = 1,...,n}$
9\. $(\textit{P has }X_{1}\wedge\textit{...}\wedge\textit{P has
}X_{n})\rightarrow\textit{P has }F(X_{1},...,X_{n})$

F is a meta-notation for any function computable in practice by P, e.g.,
encryption.

Comprehension Axiom
10\. $\textit{P believes}(\textit{P has }F(X))\rightarrow\textit{P
believes}(\textit{P has X})$

F is meta-notation for any function that is effectively one-one and such that
$F^{+}$ or $F^{-}$ is computable in practice by $P$.

Saying Axioms
11\. $\textit{P said }(X_{1},...,X_{n})\rightarrow\textit{P said
}X_{i}\wedge\textit{P has }X_{i},\\\ \textit{ for i = 1,...,n}$
12\. $\textit{P says }(X_{1},...,X_{n})\rightarrow(\textit{P
said}(X_{1},...,X_{n})\wedge\\\ \textit{ P says}X_{i}),\textit{ for i =
1,...,n}$

Freshness Axioms
13\. $fresh(X_{i})\rightarrow fresh(X_{1},...,X_{n}),\textit{for i =
1,...,n}.$
14\. $fresh(X_{1},...,X_{n})\rightarrow fresh\,F(X_{1},...,X_{n})$

F must genuinely depend on all component arguments. This means that it is
infeasible to compute the value of F without value of all the $X_{i}$.

Jurisdiction and Nonce-verification Axioms
15\. $(\textit{P controls }\varphi\wedge\textit{P says
}\varphi)\rightarrow\varphi$
16\. $(\textit{fresh(X) }\wedge\textit{P said X})\rightarrow\textit{P says X}$

Symmetric Goodness Axiom
17\. $P\xleftrightarrow{\text{k}}Q\equiv Q\xleftrightarrow{\text{k}}P$

Seeing Axioms
18\. $\textit{P received X }\rightarrow\textit{ P sees X}$
19\. $\textit{P sees }(X_{1},X_{2},...,X_{n})\rightarrow\textit{ P sees
}X_{i}$
20\. $(\textit{P sees }X_{1}\wedge...\wedge\textit{ P sees
}X_{n})\rightarrow\\\ \textit{ (P sees }F(X_{1},...,X_{n}))$

####  6.4.2 Verification of the Protocol using the SVO Logic

We should meet the goals below to have a secure and authenticated key
exchange.
G1. Entity authentication: C believes S says $F(X,N_{A})$. This goal
necessitates that, given $N_{A}$ known to be fresh to C, S recently sent a
message $F(X,N_{A})$, indicating that S has seen $N_{A}$ and has processed it.
G2. Secure key establishment: Participants believe they are in possession of a
good key to communicate with each other. The goal can be formulated as:
$\textit{C believes C }\xleftrightarrow{\textit{k}{-}}\textit{ S}$

It is important to note that in our goals, the session key is an unconfirmed
secret. No one knows or could derive k except C and S and those they trust.
This notation is different from confirmed secret. If k is a confirmed secret,
C knows k and has received evidence that S also knows k. It is apparent that
our protocol does not establish a confirmed secret.

##### Assumptions

We need the following assumptions for deriving our goals. The assumptions hold
for a successful handshake and not for a terminated one.
P1. $\text{C believes S }\xleftrightarrow{\text{Y}}\text{ C, S believes S
}\xleftrightarrow{\text{Y}}\text{ C}$
P2. $\text{C believes C sees }(client\\_rand,server\\_rand)$
$\text{ S believes S sees }(client\\_rand,server\\_rand)$
P3. $\text{C believes }\textit{fresh }(client\\_rand,T_{1},T_{2},T_{3})$
$\text{ S believes }fresh(server\\_rand,T_{1},T_{2},T_{3})$
P4. $\text{S believes S received }C_{i},\\{h(C_{i}),*_{c},T_{1}\\}_{Y}$
P5. $\text{C believes C received }\\{client\\_rand+P,*_{s},T_{2}\\}_{Y}$
P6. $\text{S believes S received }\\{server\\_rand+P,T_{3}\\}_{Y}$
P7. $\text{C believes }PK_{\delta}(C,client\\_rand)$
$\text{ S believes}PK_{\delta}(S,server\\_rand)$
P8. $\text{S belives (C says }(*_{c})\rightarrow\text{C says
}PK_{\delta}(C,*_{c}))$
$\text{ C belives (S says }(*_{s})\rightarrow\text{S says
}PK_{\delta}(S,*_{s}))$
P9. $\text{S believes C controls }PK_{\delta}(C,*_{c})$
$\text{ C believes S controls }PK_{\delta}(S,*_{s})$

##### Derivations

Based on the axioms, rules, and the assumptions, we can derive the following
about the protocol.
1\. S believes C said (server_rand + P, T3)
by P6, P1, Axiom 3, Nec. rule
2\. S believes fresh (server_rand + P, T3)
by P3, Axiom 13, Nec. rule, Axiom 1, Modus Ponens (MP) rule
3\. S believes C says (server_rand + P, T3)
by 1, 2, Axiom 1, Axiom 16, MP rule, Nec. rule
$\textbf{4. }\text{S believes C says }F(N_{s})$
by 3, Axiom 12

Derivation 4 satisfies our goal G1 for authenticating C. By following the same
steps for $client\\_rand$, authentication of S is provable.
$\textbf{5. }\text{S believes C said }(C_{i},h(C_{i}),*_{c},T_{1})$ by P7, P1,
Axiom 3, Nec. rule
$\textbf{6. }\text{S believes fresh }(C_{i},h(C_{i}),*_{c},T_{1})$
by P3, Axiom 1, Axiom 13, Nec. rule, MP rule
$\textbf{7. }\text{S believes C says }(C_{i},h(C_{i}),*_{c},T_{1})$
by 5, 6, Axiom 1, Axiom 16, Nec. rule, MP rule $\textbf{8. }\text{S believes C
says }(*_{c})$
by 7, Axiom 12, Axiom 1, Nec. rule., MP rule
$\textbf{9. }\text{S believes C says }PK_{\delta}(C,*_{c}))$
by 8, P8, Axiom 1, MP rule
$\textbf{10. }\text{S believes }PK_{\delta}(C,*_{c}))$
by 9, P9, Axiom 1, Axiom 15, Nec rule, MP rule
$\textbf{11. }\text{S believes }S\xleftrightarrow{\text{k}}C$
by 10, P7, Axiom 1, Axiom 4, Nec rule, MP rule
where k = $(*_{c},server\\_rand)$
$\textbf{12. }\text{S believes S sees }(*_{c})$
by P4, Axiom 1, Axiom 18, Axiom 19, Axiom 20, Nec rule
,MP rule
13\. S believes S sees K
by 12, P2, Axiom 1, Axiom 19, Axiom 20, Nec rule, MP
rule where k = $(*_{c},server\\_rand)$
$\textbf{14. }\text{S believes }S\xleftrightarrow{\text{k}{-}}C$
by 11, 13, Axiom 1, MP rule

Derivation 14 satisfies our goal G2. By following the same steps, we can infer
the key goodness goal for C as well.

##  7 Performance Analysis

In this section, we estimate the overhead of our protocol with respect to the
arithmetic and cryptographic operations used in our scheme.

###  7.1 Computation Overhead

To calculate the total computational cost of our protocol, we have borrowed
the primitive arithmetic and cryptographic operation timings from Kilinc et
al. [39], demonstrated in Table 3. The table shows the arithmetic mean and the
standard deviation of the following primitive operations for 1000 executions
each.

Table 3: Execution time of different cryptographic operation Notation | Description and execution time (ms)
---|---
$T_{ECPM}$ | Time complexity for the execution of the elliptic curve (ECC) point multiplication, $2.226ms$
$T_{E/D(S)}$ | Time complexity for the execution of the symmetric encryption/decryption, $3.85ms$
$T_{h}$ | Time complexity for the execution of the hash function, $0.0046ms$
$T_{ECPA}$ | Time complexity for the execution of the elliptic curve (ECC) point addition, $0.0288ms$
$T_{EMod}$ | Time complexity for the execution of the modular exponential operation, $3.85ms$
Table 4: Comparison of computational overhead Protocol | Overhead | Estimated Time
---|---|---
LAKEE | $6T_{ECPM}+3T_{E/D(s)}+34T_{h}$ | 25.06ms
ECC-CoAP [19] | $6T_{ECPM}+4T_{E/D(s)}+5T_{h}$ | 28.779ms
Dey and Hossain scheme [17] | $4T_{EMod}+6T_{E/D(s)}+6T_{h}$ | 38.527ms

$\textit{overhead =
}6T_{ECPM}+3T_{E/D(s)}+2T_{h}+32T_{h}=13.356+11.55+0.0092+0.1472=25.06\,ms$

Table 4 shows the efficiency of LAKEE in comparison with other protocols
seeking the same goal.

###  7.2 Communication Overhead

Table 5: Comparison of communication overhead Protocol | Number of Messages
---|---
LAKEE | 3
ECC-CoAP [19] | 4
LESS [18] | 4
Dey and Hossain scheme [17] | 5
DTLS Handshake [24] | 6

For calculating the communication overhead in bits, we have to specify the
length of each element. Ideally, the client ID is 64-bit long, and timestamps
are 32 bits long. If we use the curve Ed448, $server\\_rand$ and
$client\\_rand$ are 224 bits long. If we use other curves with a 128-bit
secury level, $server\\_rand$ and $client\\_rand$ would normally be 128 bits
long. The MAC, which the ciphersuite appends to the plaintext, has a fixed
size of 128 bits. We use SHA-1 as a hash function for the client’s ID with a
160-bit long output. The ciphertext would be the same size as the plaintext.
The message sizes are calculated below.

  * •

first message: $64+160+224+32+128=608\,bits$

  * •

second message: $224+224+32+128=608\,bits$

  * •

third message: $224+32+128=384\,bits$

  * •

total: $1600\,bits$

In practice, each message should include a header not necessarily specified in
the protocol. Therefore, besides the size of the messages in bits, the number
of messages corresponds to the protocol’s efficiency as well. LAKEE requires 3
messages for session key generation and authentication, which is less than its
alternatives. Table 5 compares the total number of messages required by LAKEE
and its alternatives.

##  8 Conclusion

In this paper, we proposed an efficient and lightweight authenticated key
exchange protocol for the setting of IoT by employing elliptic curve
cryptography. We addressed the performance and security shortcomings of the
existing protocols. The results are promising. and our protocol, LAKEE, is
proven to be more efficient than alternative protocols. LAKEE is implemented
as an application protocol using CoAP. The security of it is analyzed formally
and using the AVISPA security tool.

##  9 Future Work

One contribution to this work would be implementing the protocol in the
transport layer and enabling DTLS to use it for session key generation instead
of DTLS handshake. Another contribution would be securing LAKEE against
distributed denial of service attacks (DDoS). In the case of a DDoS attack,
blocking a certain IP range would not restrict adversaries’ access to the
network.

## References

  * [1] Muneer O. Bani Yassein, Mohammed Q. Shatnawi, Shadi Aljwarneh, and Razan Al-Hatmi.  Internet of things: Survey and open issues of mqtt protocol.  2017 International Conference on Engineering & MIS (ICEMIS), pages 1–6, 2017.
  * [2] Hoai Viet Nguyen and Luigi Lo Iacono.  Rest-ful coap message authentication.  2015 International Workshop on Secure Internet of Things (SIoT), pages 35–43, 2015.
  * [3] Maria Rita Palattella, Nicola Accettura, Xavier Vilajosana, Thomas Watteyne, Luigi Alfredo Grieco, Gennaro Boggia, and Mischa Dohler.  Standardized protocol stack for the internet of (important) things.  IEEE Communications Surveys Tutorials, 15(3):1389–1406, 2013.
  * [4] Jennifer G Steiner, B Clifford Neuman, and Jeffrey I Schiller.  Kerberos: An authentication service for open network systems.  In Usenix Winter, pages 191–202. Citeseer, 1988.
  * [5] Marc Fischlin and Felix Günther.  Multi-stage key exchange and the case of google’s quic protocol.  In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pages 1193–1204, 2014.
  * [6] Gildas Avoine, Sébastien Canard, and Loïc Ferreira.  Symmetric-key authenticated key exchange (sake) with perfect forward secrecy.  In Stanislaw Jarecki, editor, Topics in Cryptology – CT-RSA 2020, pages 199–224, Cham, 2020. Springer International Publishing.
  * [7] M. Harish, R. Karthick, R. Mohan Rajan, and V. Vetriselvi.  Securing coap through payload encryption: Using elliptic curve cryptography.  In Amit Kumar and Stefan Mozar, editors, ICCCE 2018, pages 497–511, Singapore, 2019. Springer Singapore.
  * [8] Guido Moritz, Frank Golatowski, and Dirk Timmermann.  A lightweight soap over coap transport binding for resource constraint networks.  In 2011 IEEE Eighth International Conference on Mobile Ad-Hoc and Sensor Systems, pages 861–866, 2011.
  * [9] Christian Amsüss.  aiocoap, 2014.
  * [10] Menghan Pan, Daojing He, Xuru Li, Sammy Chan, Emmanouil Panaousis, and Yun Gao.  A lightweight certificateless non-interactive authentication and key exchange protocol for iot environments.  In 2021 IEEE Symposium on Computers and Communications (ISCC), pages 1–7, 2021.
  * [11] Sheetal Kalra and Sandeep K. Sood.  Secure authentication scheme for iot and cloud servers.  Pervasive and Mobile Computing, 24:210–223, 2015.  Special Issue on Secure Ubiquitous Computing.
  * [12] Saru Kumari, Marimuthu Karuppiah, Ashok Kumar Das, Xiong Li, Fan Wu, and Neeraj Kumar.  A secure authentication scheme based on elliptic curve cryptography for IoT and cloud servers.  The Journal of Supercomputing, 74(12):6428–6453, December 2018\.
  * [13] Adesh Kumari, Vinod Kumar, M. YahyaAbbasi, and Mansaf Alam.  The cryptanalysis of a secure authentication scheme based on elliptic curve cryptography for iot and cloud servers.  In 2018 International Conference on Advances in Computing, Communication Control and Networking (ICACCCN), pages 321–325, 2018.
  * [14] SeongHan Shin, Kazukuni Kobara, Chia-Chuan Chuang, and Weicheng Huang.  A security framework for mqtt.  In 2016 IEEE Conference on Communications and Network Security (CNS), pages 432–436. IEEE, 2016.
  * [15] S Shin and Kazukuni Kobara.  Efficient augmented password-only authentication and key exchange for ikev2.  Technical report, 2012.
  * [16] Hsiu-Lien Yeh, Tien-Ho Chen, Pin-Chuan Liu, Tai-Hoo Kim, and Hsin-Wen Wei.  A secured authentication protocol for wireless sensor networks using elliptic curves cryptography.  Sensors, 11(5):4767–4779, 2011.
  * [17] Shreya Dey and Ashraf Hossain.  Session-key establishment and authentication in a smart home network using public key cryptography.  IEEE Sensors Letters, 3(4):1–4, 2019.
  * [18] Abhijan Bhattacharyya, Tulika Bose, Soma Bandyopadhyay, Arijit Ukil, and Arpan Pal.  Less: Lightweight establishment of secure session: A cross-layer approach using coap and dtls-psk channel encryption.  In 2015 IEEE 29th International Conference on Advanced Information Networking and Applications Workshops, pages 682–687, 2015.
  * [19] Suman Majumder, Sangram Ray, Dipanwita Sadhukhan, Muhammad Khurram Khan, and Mou Dasgupta.  Ecc-coap: Elliptic curve cryptography based constraint application protocol for internet of things.  Wireless Personal Communications, 116(3):1867–1896, Feb 2021.
  * [20] A Alhaj.  Constrained application protocol (coap) for the iot.  In IOT SEMINAR, HIGH INTEGRITY SYSTEM, FRANKFURT UNIVERSITY OF APPLIED SCIENCE, Frankfurt, 2018.
  * [21] Victor S. Miller.  Use of elliptic curves in cryptography.  In Advances in Cryptology, CRYPTO ’85, page 417–426, Berlin, Heidelberg, 1985. Springer-Verlag.
  * [22] N. Koblitz.  Towards a Quarter-Century of Public Key Cryptography.  Designs, codes and cryptography. Springer US, 2000.
  * [23] P. Eronen and H. Tschofenig.  Pre-shared key ciphersuites for transport layer security (tls).  RFC 4279, RFC Editor, December 2005.  http://www.rfc-editor.org/rfc/rfc4279.txt.
  * [24] E. Rescorla and N. Modadugu.  Datagram transport layer security version 1.2.  RFC 6347, RFC Editor, January 2012.  http://www.rfc-editor.org/rfc/rfc6347.txt.
  * [25] Mike Hamburg.  Ed448-goldilocks, a new elliptic curve.  Cryptology ePrint Archive, 2015.
  * [26] A. Langley et al.  Elliptic curves for security.  RFC 7748, RFC Editor, January 2016.  http://www.rfc-editor.org/rfc/rfc7748.txt.
  * [27] Daniel J. Bernstein and Tanja Lange.  Safecurves: choosing safe curves for elliptic-curve cryptography.
  * [28] B. Kaliski.  Password-based cryptography specification version 2.0.  RFC 2898, RFC Editor, September 2000.  http://www.rfc-editor.org/rfc/rfc2898.txt.
  * [29] Danny Dolev and Andrew Yao.  On the security of public key protocols.  IEEE Transactions on information theory, 29(2):198–208, 1983.
  * [30] TA Team et al.  Avispa v1. 1 user manual.  Information society technologies programme (June 2006) http://avispa-project. org, 2006.
  * [31] Olivier Heen, Thomas Genet, Stéphane Geller, and Nicolas Prigent.  An industrial and academic joint experiment on automated verification of a security protocol.  In Mobile and Wireless Networks Security, pages 39–53. World Scientific, 2008.
  * [32] Khalid Mahmood, Shehzad Ashraf Chaudhry, Husnain Naqvi, Saru Kumari, Xiong Li, and Arun Kumar Sangaiah.  An elliptic curve cryptography based lightweight authentication scheme for smart grid communication.  Future Gener. Comput. Syst., 81(C):557–565, apr 2018.
  * [33] Michael Burrows, Martin Abadi, and Roger Needham.  A logic of authentication.  ACM Trans. Comput. Syst., 8(1):18–36, feb 1990.
  * [34] Paul F Syverson and Paul C Van Oorschot.  A unified cryptographic protocol logic.  Technical report, NAVAL RESEARCH LAB WASHINGTON DC, 1996.
  * [35] Martin Abadi and Mark R Tuttle.  A semantics for a logic of authentication.  In Proceedings of the tenth annual ACM symposium on Principles of distributed computing, pages 201–216, 1991.
  * [36] Li Gong, Roger M Needham, and Raphael Yahalom.  Reasoning about belief in cryptographic protocols.  In IEEE Symposium on Security and Privacy, volume 1990, pages 234–248. Citeseer, 1990.
  * [37] Paul van Oorschot.  Extending cryptographic logics of belief to key agreement protocols.  In Proceedings of the 1st ACM Conference on Computer and Communications Security, CCS ’93, page 232–243, New York, NY, USA, 1993. Association for Computing Machinery.
  * [38] Paul Syverson and Iliano Cervesato.  The logic of authentication protocols.  In Riccardo Focardi and Roberto Gorrieri, editors, Foundations of Security Analysis and Design, pages 63–137, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg.
  * [39] H. Hakan Kilinc and Tugrul Yanik.  A survey of sip authentication and key agreement schemes.  IEEE Communications Surveys Tutorials, 16(2):1005–1023, 2014.