Array 16 (2022) 100254

Contents lists available at ScienceDirect

Array
journal homepage: www.elsevier.com/locate/array

Formalization and evaluation of EAP-AKA’ protocol for 5G network access

security
Ed Kamya Kiyemba Edris a ,∗, Mahdi Aiash a , Jonathan Loo b
a School of Science and Technology, Middlesex University, The Burroughs, Hendon, London, NW4 4BT, United Kingdom
b
School of Computing and Engineering, University of West London, St Mary’s Rd, Ealing, London, W5 5RF, United Kingdom

ARTICLE INFO ABSTRACT

Keywords: The end user’s Quality of Experience (QoE) will be improved while accessing services in Fifth Generation
5G Mobile Network (5G), supported by enhanced security and privacy. The security guarantees offered by the
EAP-AKA’ Authentication and Key Agreement (AKA) protocols will be depended upon by end users and network operators.
Security protocol
The AKA protocols have been standardized for 5G networks, and the Extensible Authentication Protocol (EAP)-
Formal methods
AKA’ protocol is one of the main authentication mechanisms that has been specified for User Equipment (UE)
Verification
Authentication
and network mutual authentication. This article models the EAP-AKA’ protocol and conducts an extensive
ProVerif formal verification of the EAP-AKA’ protocol as defined in the 5G security standard to determine whether the
Applied pi calculus protocol is verifiably secure for 5G. It provides a security evaluation of the EAP-AKA’ protocol based on the
Performance evaluation current 5G specifications using ProVerif, a security protocol proof verifier. It also presents security properties
that support the security verification, as well as quantitative properties that are used to assess the protocol’s
performance. Finally, it compares the EAP-AKA’ and 5G-AKA protocols’ security and performance results.

1. Introduction significant research conducted on primary authentication but mostly

covers 5G-AKA protocol, hence why this paper is focussing on verifying
The Fifth Generation Mobile Networks (5G) will support applica- EAP-AKA’ protocol with ProVerif [2] proof verifier and evaluating its
tions like the Internet of Things (IoT) and Vehicle to Everything (V2X),
performance using analytical and simulation methods.
as well as user mobility, dense connectivity, and massive Machine Type
The main contribution of this paper is summarized as follows:
Communication (mMTC). The immense growth of mobile device and
multimedia applications usage has led to the need for seamless connec- • It interprets security properties and models the EAP-AKA’ proto-
tivity and rapid growth of mobile data traffic. 5G will be supported col as described in the 3GPP standard.
by technologies such as visualization, edge computing and Device
• It conducts a formal analysis and verification of the protocol to
to Device (D2D) communications. Mobile subscribers with their User
automatically identify the security properties.
Equipment (UE) will be able to access 5G network services via the
• It presents our security consideration on EAP-AKA’, to provide the
new generation Radio Access Network (ngRAN), therefore secure access
drive 5G security standard requirements as specified by Third Gener- basis for future formal analysis and verification of next-generation
ation Partnership Project (3GPP) in [1]. Users and Mobile Network AKA protocols.
Operators (MNOs) should be able to rely on stated security properties • It evaluates EAP-AKA’ protocol’s performance using two models
such as authentication, secrecy, and integrity provided by 5G security. and compares with 5G-AKA.
To access the network, the UE must be authenticated, and additional
authentication and authorization are essential to access services pro- The rest of the paper is structured as follows. In Section 2, related
vided by the MNO or other Data Networks (DN). The UE, Serving work on the EAP framework, 5G security, and formal methods are
Network (SN), and Home Networks (HN) use the Authentication and presented. In Section 3, EAP–AKA’ protocol based on 3GPP standard is
Key Agreement (AKA) protocols for security assurance. presented. Section 4 presents the protocol modelling and discusses the
The 5G standard [1] covers the most significant security needs in security requirements. The formalization of the protocol is discussed
5G and specifies Extensible Authentication protocol (EAP)-AKA’ as one in 5. In Section 6 a formal security analysis of EAP-AKA’ and security
of the methods used in the primary authentication. There has been

∗ Corresponding author.
E-mail addresses: [email protected] (E.K.K. Edris), [email protected] (M. Aiash), [email protected] (J. Loo).

https://doi.org/10.1016/j.array.2022.100254
Received 1 September 2022; Received in revised form 10 October 2022; Accepted 25 October 2022
Available online 28 October 2022
2590-0056/© 2022 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).
E.K.K. Edris et al. Array 16 (2022) 100254

considerations are discussed. Section 7 presents the performance eval- The authors in [5] modelled the entire architecture of the 5G EAP-
uation of the protocol. The concluding remarks and future work are AK’A protocol through symbolic model verification with analysis. They
summarized in Section 8. also formally verified the security of the protocol. With a thorough
formal investigation of the security-related characteristics of the 5G
2. Related work EAP-TLS authentication protocol, the authors in [3] reviewed EAP
using ProVerif. The authors discussed the EAP framework and anal-
The authors in [3–5] reviewed the EAP concept that was spec- ysed the security features based on 5G-AKA in [12,15]. With security
ified under Request for Comment (RFC) 3748 as an authentication analysis based on Lowe’s taxonomy, the authors in [16] formally mod-
framework. [6]. It can be used on dedicated links, wired and wireless elled and examined the EAP-AKA’ using Tamarin. The related work
networks, and runs directly on data link layers without requiring an in officially analysed the EAP-AKA’ protocol using formal methods
IP address. 3GPP designed the EAP-AKA protocol, which was then with various automated tools, but they did not evaluate the protocol’s
confirmed by the EAP WG in RFC 4187 [7]. It was later specified effectiveness. In contrast, this research formally analysed and evaluated
as an EAP method for authentication and session key distribution for the protocol’s performance using the two techniques that are covered
Universal Mobile Telecommunications System (UMTS). Identity privacy in the next sections.
support, result indications, and a fast re-authentication procedure were
all added to the EAP-AKA. This made the use of AKA method for 3. EAP-AKA’ protocol
primary authentication possible within the EAP framework, later im-
proved in RFC 9048 [8] with a new EAP method, EAP-AKA’. A new 3GPP defined the EAP-AKA’ protocol as one of the main methods
key derivation function was added, which binds the derived keys with of AKA between a mobile device and its HN in the 5G security stan-
the name of the access network, preventing binding attacks [4]. dard [1]. The authentication protocol includes a home control feature
In addition, the EAP-AKA’ can be used to authenticate the UE to that enables the HN operator to determine whether the device is au-
network access in a 5G, non-3GPP networks and integrated in security thenticated in each network and make the final authentication decision.
frameworks [9]. The protocol was specified in TS 33.501 [1] as a 5G After a successful run of the protocol, all parties should be able to derive
primary authentication method. The EAP-AKA’ uses cipher key (CK’) and agree on an anchor key, which is used to generate session keys for
and integrity key (IK’) as specified in TS33.402 [10] with an updated communication between UEs and Next Generation Node B (gNodeB) in
hash function Secure Hashing Algorithm (SHA)-256 and Hash based the local network. Additionally, for secondary authentication between
Message Authentication Code (HMAC)-SHA-256 [4]. the UE and external DN, EAP method is preferred.

2.1. Authentication procedure 3.1. EAP architecture overview

The AKA is an authentication process where parties involved ex- The 5G system consists of the following:
change messages to verify one another through mutual authentication
and session key agreement. The 5G system supports AKA between the • UE: A Mobile Equipment (ME) which stores the Universal Sub-
UE and SN, authorized by the HN. It provides ciphering, integrity scriber’s Identity Module (USIM) with cryptographic capabili-
and replay protection and privacy within the 5G, enabling the UE to ties like symmetric encryption algorithms, HMAC, and session
access the HN via SN securely. 5G support primary authentication and counter, Subscriber’s Permanent Identifier (SUPI), public key of
secondary authentication methods for accessing the network in 5G and its HN, key K.
services from external DN, respectively. The EAP framework can be • HN: Comprises security functions and the database that support
used for both methods, as specified in 5G standard [1]. authentication, generates vectors and stores user subscription
data.
2.2. Protocol verification using formal methods and automated proof veri- • SN: The radio access network to which the UE connects to access
fier the HN.

As illustrated in Fig. 1, the security architecture of 5G comprises

Due to the use of strong abstractions, simplifications, and con- the following entities as described in [1,11]. The UE, Security Anchor
straints in the properties analysis, formal methods and automated Function (SEAF), Authentication Server Function (AUSF), Authenti-
verification have been applied to authentication protocols like AKA cation Credentials Repository and Processing Function (ARPF) and
in the past with weak guarantees. To give solid guarantees, formal Unified Data Management (UDM). The SEAF is deployed in the SN,
approaches have already been used to examine security protocols in [3, while the AUSF and ARPF are located in the HN. Additionally, the
4,11]. Most verification approaches and tools struggle with AKA pro- UE shares the secret key and other information with ARPF which are
tocol properties like in EAP-AKA’, because of cryptographic primitives used during the AKA procedure. The subscriber unique identity SUPI is
applications such as Sequence Number (SQN) and Exclusive-OR (XOR), encrypted as Subscription Concealed Identifier (SUCI) when UE sends
whose algebraic features make symbolic reasoning difficult [12]. As a it to HN and only decrypted by the HN. The UE and SEAF must achieve
result, manual proof evaluations are not suitable for certain tools. mutual authentication and must be in the possession of session key
Many automated verification tools, such as Tamarin [13] Auto- before communicating as this occurs on an unsecure wireless channel
mated Validation of Internet Security Protocols and Applications while the communication between SEAF, AUSF and ARPF occurs on a
(AVISPA) [14] and ProVerif [2], can be used for this analysis. ProVerif presumed secure wired channel.
assesses the security of cryptographic protocols, and it uses Dolev–Yao The EAP framework defines the roles of peer, pass-through authen-
models to facilitate user-defined equational theories and the verifi- ticator, and back-end authentication server under RFC 3748. The EAP
cation of a wide range of security features. ProVerif also recognizes server, which is the back-end authentication server, terminates the EAP
cryptographic primitives specified by rewrite rules and equations that authentication mechanism with the peer, the entities are shown in
satisfy the finite variant property. To support protocol reasoning, the Fig. 2. When EAP-AKA’ is utilized in a 5G system, the EAP framework
syntax is combined with a formal semantics. As a result, we consider is supported in the following way [1]:
ProVerif to be an appropriate tool for our analysis. In [3,5], it was
applied to formally check security characteristics assurances of AKA • The peer is represented by the UE.
protocols. • The pass-through authenticator is represented by the SEAF.

2
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 1. 5G system architecture.

Fig. 2. 5G EAP entities.

• The backend authentication server is represented by the AUSF key derivation using the at_kdf_input parameters. The keys related to
with the support of ARPF and UDM. authentication include keys: K, CK, IK, CK’, and IK’ which are used
to generate the EMSK (𝐾𝐴𝑈 𝑆𝐹 ) then 𝐾𝑆𝐸𝐴𝐹 and later used to derive
The main EAP-AKA’ Attributes in the EAP-request/response are
other keys to secure communication between the UE and other network
AT_RAND, AT_AUTN, AT_RES, AT_MAC, AT_KDF, AT_KDF_INPUT,
AT_MAC, AT_AUTS. There are some significant changes that have been entities. In addition, the KDF input parameters for CK’ and IK’ are the
made in EAP-AKA’, as per 5G security specifications [8] as follows: same only separated by the return of a 256-bit output, with CK’s 128
most significant bits and IK’s 128 least significant bits [10].
• Network name field: Both the UE and the SEAF must generate the
SNN, setting the service code to ‘‘5G’’ and the network identifier
to ‘‘SNID’’ for the network to which the UE is authenticating and 4. Modelling of EAP-AKA’ protocol
for the SEAF to SN to which the AUSF is delivering authentication
data.
• The identifiers: SUPI, SUCI, SNID. In this modelling, the values used for Authentication Vectors (AV)
• Inputs in key derivation: It is critical for identity privacy, privacy- are defined in Table 1: They include a random nonce RAND as a
friendly and non trackable identifiers in 5G. challenge, AUTN as an authentication token to validate the challenge’s
• Session identifiers: = EAP Type code ∥ RAND ∥ AUTN. It carries freshness and authenticity, and an expected reply as XRES to the
the AT_KDF_INPUT attribute, which ensures that the UE and AUSF challenge. The EAP-AKA’ protocol is modelled with four entities (UE,
are both aware of the access network’s name. To enable future SEAF, AUSF, and ARPF/UDM). The focus is on authentication and
extensions, it offers key derivation function negotiation via the authentication failure, not re-authentication. XOR and HN public keys
AT_KDF parameter. with Elliptic Curve Integrated Encryption Scheme (ECIES) profiles are
used to conceal the SQN and SUPI, respectively. By including ‘‘SNN’’ in
3.2. Keys derivation the chain of key derivations parameters, the anchor key 𝐾𝑆𝐸𝐴𝐹 binding
with SN is enforced, guaranteeing that the anchor key is specific for an
During the derivation of 𝐾𝑆𝐸𝐴𝐹 from the 𝐾𝐴𝑈 𝑆𝐹 following a suc- authentication process between a network and a UE. 5G authentication
cessful authentication procedure between the UE and the HN, the that utilizes the ARPF and USIM directly provides a stronger guarantee,
UE’s identity and the access network ID are used as inputs in the similar to fast re-authentication in EAP-AKA’.

3
E.K.K. Edris et al. Array 16 (2022) 100254

Table 1 long-term IPSec, (D)TLS, or DIAMETER sessions. SEAF and AUSF are
5G EAP-AKA’ notation and description.
Diameter-based systems that run over IPSec or TLS.
Notation Description 3GPP tries to address security issues of fake base station and non-
SNname/SNN Service code:SNID repudiation by increasing home control. This is achieved by AUSF
K Symmetric key (UE, HN)
sending authentication confirmation to ARPF, HN confirming the UE’s
𝑃 𝐾𝐻𝑁 Public key (HN)
𝑆𝐾𝐻𝑁 Private key (HN) identity and authorizing the SN sending the SNN to UE [1,11]. The
SIDF Decrypt SUCI function assumption is that EAP-AKA’ provides the same security as EAP-AKA
RAND Random nonce challenge or better. However, the EAP-AKA’ can be affected by same attacks
SUCI/SUPI User’s Network Access as 5G-AKA protocol like monitoring, location, desynchronization and
Identifier (NAI)
AUTN (SQNHN ⊕ AK,MAC,AMF)
linkability attacks, which affects the privacy properties [18].
MAC,MAC2 f1(K, (SQNHN, Rand,AMF) There have been no revealed attacks that compromise the AKA
RES, XRES f2(K, Rand) security properties defined under the originally assumed trust model
CK f3(K, Rand) and that of EAP-AKA’ [8]. Despite this, the diameter protocol is still
IK f4(K, Rand)
vulnerable to man-in-the-middle, malware, and DDoS attacks [11,19].
AK f5(K, Rand)
CK’ ik, ck, snn, (sqn⊕ak) Diameter dependent on the peer-to-peer principle rather than end-to-
IK’ ik, ck, snn, (sqn ⊕ak) end encryption. Furthermore, interception and information gathering
𝐾𝐴𝑈 𝑆𝐹 /EMSK KDF((CK’, IK’), is possible due to diameter’s use of same route for request/response
(SNN, SQN ⊕ AK)) message exchange.
𝐾𝑆𝐸𝐴𝐹 KDF(𝐾𝐴𝑈 𝑆𝐹 , SNN)
SQN Sequence Number
MACS f1* (AMF, RAND, K, SQNUE) 4.2. Protocol message exchange
AK* f5* (K, Rand)
AUTS (SQNUE ⊕ AK) ∥ MACS The EAP-AKA’ protocol process is divided into the following three
h(x) Hash value of message x
{x}{k} Encrypted message x
stages using authentication vectors (AV) and exchange messages (msg),
as shown in Table 1.
Stage 1: Initiation and Method Selection
It involves the initialization and authentication method selection. As
4.1. Security assumptions and requirements shown in Fig. 3, the SEAF initiates authentication process with the UE.
Msg1. SEAF→UE: (EAP-Request/Identity)
If the channel between the SN and HN is presumed to be secure, 1. The SEAF send Identity request to UE.
it should provide confidentiality, integrity, authenticity, and replay Msg2. UE→ SEAF: (SUCI)
protection using cryptographic primitives, keys and HMAC, according 2. The UE sends authentication request in msg2 which includes SUCI
to the standards in TS 33.501 [1]. In case where the SN-HN channel is and HNID.
not secure, it is exposed to the same attacks as the UE-SN channel [11]. Msg3. SEAF → AUSF: (SUCI, SNN)
The entities which execute the diameter protocol, as well as the 3. The SEAF receives msg2 sends SUCI and SN name to AUSF in msg3.
AKA itself, could be compromised if attacker capabilities grow. This as- Msg4. AUSF → ARPF: (SUCI, SNN)
sumption is supported by 5G characteristics that increase the attacker’s The AUSF sends msg4 to UDM/ARPF in HN. Before using the SNN,
vector [11]. It is also possible that the attacker might have the actual AUSF checks and verifies that the SEAF is authorized. When the ARPF
USIM under his or her control, in which case the attacker might have receives msg4, SUCI is de-concealed into SUPI using SIDF and chooses
access to all secret values contained in the USIM, including SUPI, K, and an authentication method.
SQN. Although EAP-AKA’ lacks cipher suite negotiation capabilities, Phase 2: The Protocol
it does have a mechanism for determining key derivation functions. The EAP-AKA’ protocol flows in a form of EAP Challenge-Response
Mutual authentication, secrecy, cryptographic binding, and session between entities as illustrated in Fig. 4.
independence are all security qualities provided by SHA-256, which are Msg5.ARPF → AUSF:EAP-AKA’ AV (RAND, AUTN,
comparable to those supplied by EAP-AKA [8]. It is also assumed that XRES, SNN, CK’ ∥ IK’, SUPI)
because SHA-256 is a pseudo-random function, an attacker will not be UDM/ARPF produces authentication vectors AV with AMF* after re-
able to deduce the pre-shared secret from any keys in any practically ceiving SUPI. RAND and SQN are generated first, followed by XRES and
feasible way. Different identifiers are used by EAP-AKA’ to identify the AUTN. Calculates CK and IK, as well as CK’ and IK’. In msg4, the ARPF
authenticating UE. Even though the protocol key strength precludes transmits EAP-Response/AKA’AV to the AUSF, signalling that EAP-AKA’
brute force assaults, it does not provide channel binding. would be utilized.
Secrecy, confidentiality, integrity, authenticity, and privacy are the Msg6. AUSF → SEAF: (RAND, AUTN, SNN)
desired security features for the EAP-AKA’ protocol [1]. The UE must When the AUSF receives msg5, it stores XRES and SUPI before sending
safely assume only SN authorized by their HN can be used for authenti- EAP-Request/AKA’-Challenge to the SEAF in msg6.
cation. The UE must use implicit key authentication and confirmation Msg7. SEAF → UE: (RAND, AUTN, ngKSI, ABBA)
to authenticate SN with the SNN. After key confirmation, a UE must In Auth-Request, msg7, the SEAF sends RAND and AUTN to the UE. The
get weak agreement on SNN with its HN. ABBA parameter must be included in this message to enable binding
In the process of AKA between UE and HN, the SN must be able down protection.
to verify the UE by authenticating SUPI. EAP-AKA’ is responsible for Msg8. UE → SEAF: (RES, MAC)
maintaining the secrecy of 𝐾𝑆𝐸𝐴𝐹 and since it is the anchor key. It When the UE receives msg7, it forwards RAND and AUTN to the USIM,
emphasizes that the same 𝐾𝑆𝐸𝐴𝐹 should never be generated twice. Pri- which checks if the AUTN may be accepted to verify the AV’s freshness.
vacy in 5G has been strongly defined, subscription privacy is concerned It generates AK and obtains SQN. Then it generates MAC2, checks to see
with subscribers’ personal data to ensure confidentiality, anonymity, (i) if MAC2 = MAC and (ii) if SQN is in the range, if SQNUE < SQNHN.
and untraceability and avoid attacks [17]. 5G has precise requirements USIM calculates RES if (i) and (ii) are the predicted responses. Finally,
on privacy, the SUPI and SQN must remain secret in presence of passive it calculates CK and IK. The UE receives RES, CK, and IK from the USIM,
attacks to avoid attack such as data leakage. Over communication then compute CK’, IK’ and returns RES with MAC2.
channels, these security features are utilized to construct and maintain Msg9. SEAF → AUSF: (RES, MAC)

4
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 3. EAP- AKA’ phase 1.

Fig. 4. EAP-AKA’ phase 2.

The SEAF transparently forwards msg8 as msg9 to AUSF. There is an SEAF sends Success message in msg11 with ngKSI and the ABBA pa-
optional exchange of further EAP messages after msg9. rameter. The UE drives EMSK (𝐾𝐴𝑈 𝑆𝐹 ) from CK’and IK’ and generates
𝐾𝑆𝐸𝐴𝐹 using the same methods as the AUSF.
Msg10. AUSF → SEAF:EAP-Success (KSEAF, SUPI)
Phase 3: Re-synchronization
When AUSF receives RES and MAC2, it verifies them by comparing If the SQN is out of sync, the re-synchronization technique is used to
RES with XRES; if the two are equal, AUSF consider the authentication update it on the HN side. This is initiated by an AUTN verification
successful and informs the UDM. If not, it sends error message to SEAF. fail, whereby the USIM lets the UE know whether it is a MAC or
Otherwise it derives EMSK (𝐾𝐴𝑈 𝑆𝐹 ) from CK’ and IK’, the calculates synchronization failure, and sends the AUTS parameter to the UE, as
𝐾𝑆𝐸𝐴𝐹 from 𝐾𝐴𝑈 𝑆𝐹 . Then sends 𝐾𝑆𝐸𝐴𝐹 to SEAF in msg10 as the anchor shown in Fig. 5.
Msg12. UE → SEAF: (Mac_failure, Synch_failure, AUTS)
key.
In msg 12 with AUTS, the UE sends mac_failure and synch_failure to
Msg11. SEAF → UE: EAP-Success (ngKSI,ABBA) SEAF.

5
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 5. EAP-AKA’ phase 3.

Msg 13. SEAF → AUSF: (Synch_failure,AUTS) Table 2

ProVerif process language.
SEAF may request the UE to re-identify its self in case of a mac_failure
Term Grammar
or launch a new authentication session if it is a sync_failure and sends
msg13 to AUSF. Msg 14. AUSF → ARPF: (Synch_failure,AUTS, a, b, c, k, s name
x, y, z variable
Rand) M,N ∶∶= terms
With RAND transmitted to the UE in msg6, and AUTS received in h(D1, . . . ,Dn) function application
msg 13, the AUSF sends msg14 to the UDM/ARPF. The ARPF ob- f(M1,. . . ,Mn) constructor application
D ∶∶= expressions
tains SQNUE from AUTS, verifies that SQNHN’s range, and determines
fail failure
whether the SQN created with SQNHN will be accepted by the USIM. P,Q ∶∶= processes
As a result, the UDM/ARPF computes fresh AV, checks AUTS, and out(N,M); P output
resets the value of the counter SQNHN to SQNUE after a successful in(N, x : T); P input
!𝑃 !P replication
verification. The UDM/ARPF transmits new AV to the AUSF for the UE
0 nil
to perform a new authentication protocol run [1,11]. P ∣ Q parallel composition
new a : T; P restriction
let x : T = D in P else Q expression evaluation
5. Verification of EAP-AKA’ protocol if M then P else Q conditional

This section formalizes the EAP-AKA’ protocol using formal methods

and ProVerif.
free supi:id [private].
query attacker (supi).
5.1. Formal verification using ProVerif free kseaf:key [private].
query attacker (kseaf).
In ProVerif, the declaration formalizes the behaviour of crypto-
graphic primitives, which include variables, constants, names, and query u: host, a: host, r: nonce,
channels, to show reachability, secrecy, correspondence assertions, and kseaf:key, k: key;
observational equivalence of the protocol. The main process establishes event(endAUSF(u, a, r, k)) ==>
the blueprint of the assessing scheme. Constants and variables, as well event(beginUE(u, a, r, k)).
as cryptographic functions specified as constructors and equations, can query u: host, a: host, r: nonce,
be defined as free (unsecure) or private (secure). The beginning and kseaf:key, k: key;
termination of participating entities are defined by processes, and the inj-event(endAUSF(u, a, r, k)) ==>
execution is kept parallel. Then queries are run to ensure that a proto- inj-event(beginUE(u, a, r, k)).
col’s correctness and secrecy are maintained. Cryptographic primitives
are represented by terms constructed from an unlimited number of The protocol was modelled and run in ProVerif using the secure
names like (a, b, c, . . . ) and an infinite number of variables like (x, pubsec channel, there was no effect on the protocol, and no attack
y, z, . . . ) and a finite number of function symbols such as 𝑓 1, … , 𝑓 𝑛. was found. However, when the protocol was run on the compro-
In addition, the application of function symbols to terms is influenced mised channel, the authentication did not hold as assumed by the 5G
by a set of reduction rules. The syntax and grammar of the ProVerif standard. This is a similar attack against 5G-AKA protocol [11].
process language are displayed in Table 2 [2]. The secrecy of UE’s identity, long-term key, anchor key and au-
thentication of UE to SN hold, according to ProVerif results in Fig. 6.
However, the authentication of SN to UE does not hold on both non-
5.2. Protocol formal analysis injective and inject agreements. The UE received msg4 and trans-
mitted msg5, as indicated by the e1 showing that the SEAF sent
These are some of queries used in the simulation. msg4. All protocol parameters are taken as arguments in these events.

6
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 6. EAP-AKA’ unsafe ProVerif results.

Fig. 7. Attack trace.

Except for e2, which checks if xsqn = xor(xored sqn, ak), by the attack derivation, but the genuine attack is represented by the
xmac = f1((xsqn, xrand), ki), xmac = mac and if attack trace, which is an executable trace of the considered process.
xsqn = sqnue. If the inputs are true, a 𝑅𝐸𝑆 message is conveyed; The derivation and trace are a set of steps, inputs, and outputs on the
otherwise, a MAC_failure or synch_failure message is sent for communication channel, as well as related events.
authentication failure or re-authentication initiation.
However, because msg4 can be replayed, resulting in many e2
5.3.1. Attack derivation and trace
for a single e1, this correspondence cannot be proved directly in
The attacker 𝐼 intercepts communication between entities, imper-
ProVerif. The study also discovers that event e2, which has res as an
sonates the UE, and continues the protocol with SEAF, which completes
argument that cannot be executed before autn and rand have been
the protocol with the attacker instead of the UE. The attacker’s actions
sent, i.e. before e1. Which fails as false in ProVerif.
are depicted in Fig. 7 and concisely explained in steps below; some
content has been excluded for simplicity:
5.3. The attack against EAP-AKA’ protocol
• The event(endSEAF(x1_80)) ==> event
As illustrated in Figs. 6 and 7, the ProVerif results indicate that there (beginSEAF(x1_80)) is queried, the attacker’s goal is achie-
was an attack on the protocol. The attacker’s behaviour is represented ved, when he gets suci_4228 using attacker(suci_4228)

7
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 8. EAP-AKA’ safe results.

and attacker (rand_4227) for rand_4227 together with 6.2. Security analysis 2
function SHA256 to obtain SHA256(rand_4227, x1_4230).
• The attacker’s goal is also achieved when event endSEAF(a) • Secrecy: Since SUPI’s secrecy is maintained, then this require-
is executed in session copy a_4234, SEAF completes a session ment is met. Key derivations parameters are protected in transit
with the attacker at event {57}. The injective agreement fails and storage by employing XOR and anonymity keys. F1 and
when event endSEAF(a_5801) is completed during session F* give 𝑆𝑄𝑁 privacy protection. The protocol’s confidentiality
a_5800. maintained and privacy are preserved.
• Aliveness: HN obtains the aliveness of UE from the SN, with
the UE agreeing to a non-injective agreement on 𝑆𝑁𝑁. Further-
6. Protocol security analysis more, the HN acquires fresh aliveness as a result of the injective
agreement on 𝐾𝑆𝐸𝐴𝐹 with the UE.
This section analyses the EAP-AKA’ protocol’s security properties • Weak Agreement: This is met when SN obtains non-injective
using taxonomies defined in [20,21] for security analysis 1 and 2, agreement with UE on 𝑆𝑈 𝑃 𝐼 and the key confirmation using
respectively, utilized to check formal methods outcome. 𝑆𝑁𝑁 as parameter. However, as the ProVerif results show, the
weak agreement does not hold.
• Non-injective Agreement: After 𝐾𝑆𝐸𝐴𝐹 confirmation and 𝐻𝑁𝐼𝐷
6.1. Security analysis 1
being part of SUPI, the UE gets non-injective agreement on 𝑆𝑁𝑁
with its HN. The UE receives injective agreements on 𝐾𝑆𝐸𝐴𝐹 from
• Mutual Entity Authentication: If RES = XRES, the UE is implicitly both the SN and the UE. This due to 𝐾𝑆𝐸𝐴𝐹 ’s derivation involving
authenticated to the HN and SN, as SNN is included in the suc- 𝐴𝑇 _𝑅𝐴𝑁𝐷 from HN and SNN from SN, any agreement on 𝐾𝑆𝐸𝐴𝐹
cessful authentication and 𝐾𝑆𝐸𝐴𝐹 confirmation. This is enforced between the HN and the UE ensures that the UE is attached to an
when SUPI and SNN are transmitted to the HN and are proven to authorized SN. But the SN-UE authentication fails due to a change
hold. in the channel security assumption.
• Mutual Key Authentication: The UE and HN authentication is • Injective Agreement: The injective agreement on 𝐾𝑆𝐸𝐴𝐹 between
predicated on the secrecy of 𝐾𝑆𝐸𝐴𝐹 , it is implicitly authenticated the UE and the SN is critical to the protocol’s goal, and estab-
by incorporating 𝐾𝐴𝑈 𝑆𝐹 and SNN in its derivation parameters. lishing this for various pairs of parties means 𝐾𝑆𝐸𝐴𝐹 cannot be
• Mutual Key Confirmation: This condition is enforced by a success- derived twice in the same session. As a result, using 𝐴𝑇 _𝑅𝐴𝑁𝐷
ful AKA roundtrip between the entities and with 𝐾𝑆𝐸𝐴𝐹 confirma- in the 𝐾𝑆𝐸𝐴𝐹 derivation ensures injective agreement on 𝐾𝑆𝐸𝐴𝐹
tion. between the HN and the UE. It is worth noting that any agreement
• Key Freshness: Although there is no function in ProVerif to check with HN on 𝐾𝑆𝐸𝐴𝐹 based on SNN informs the UE that SN is
key freshness, the UE validates the AUTN freshness during the trustworthy. To ensure that the session with SN was authorized by
authentication process by checking if SQNUE > SQNHN. Addi- the HN, the UE obtains an injective agreement on 𝐾𝑆𝐸𝐴𝐹 from the
tionally, every 𝐾𝑆𝐸𝐴𝐹 is linked to SN by SNN, which guarantees HN. The SN, on the other hand, is unable to gain the same level
the key freshness, 𝐾𝑆𝐸𝐴𝐹 from prior sessions cannot be reused in of trust from the UE since the SN-UE injective agreement does not
new sessions. occur.
• Unknown-Key Share: In ProVerif, the reachability property is
It must be considered that key K could be leaked through eavesdrop-
utilized to check for aliveness. This attack is prevented by the
ping on the communication channel, hacking the USIM card, an insider
entities’ identity and key binding. SUPI, HNID and SNN in the
attack via the USIM vendor, mobile provider or side channels [11]. This
derivation of 𝐾𝑆𝐸𝐴𝐹 , and the dependence on a preshared key K would allow an attacker to impersonate a user to the SN, compromising
between UE and HN also prove this condition. Moreover, 𝐾𝑆𝐸𝐴𝐹 the UE’s privacy. Misuse of keys, on the other hand, could cause the SN
is only provided to SEAF after AUSF has verified the RES and to send traffic on behalf of the UE. However, knowing the 𝐾𝑆𝐸𝐴𝐹 es-
MAC2. tablished in one session is not enough to derive 𝐾𝑆𝐸𝐴𝐹 from a previous
• Key Compromise Impersonation Resilience: 𝐾𝑆𝐸𝐴𝐹 is implicitly session or a future session in 5G. The network name binding in the EAP-
authenticated and stays a secret. However, even if the attacker AKA’ protocol can also help to mitigate some of the attacks that affect
discovers 𝐾𝑆𝐸𝐴𝐹 keys used in all previous sessions and the key the old EAP-AKA protocol, such as privacy attacks, but its configuration
K material is compromised, the current session remains confi- should not be based on the location of where a request originates
dential. It does not, however, hold for forward secrecy or post- unless the location information can be confirmed using cryptographic
compromise secrecy. EAP-AKA’ fails to meet these standards be- methods. In case, the SN requests a large number of authentication
cause knowing key K allows an attacker to deduce all previous runs for a UE from a HN to induce a DoS, resynchronization and
and future keys. tracking/monitoring mechanisms should prevent this type of attack by
limiting the number of authentication tries [8].

8
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 9. EAP-AKA state transition system.

Table 3 on both non-injective and injective agreements a shown in Fig. 8. The

Process extensions.
security mechanism that protects the diameter sessions should also be
Term Grammar enhanced.
𝐴, 𝐵.𝐶 ∶∶= extended processes
𝑃 plain process 7. Protocol performance evaluation
𝐴∣𝐵 parallel composition
𝜈𝑥.𝐴 variable restriction
𝜈𝑛.𝐴 name restriction This section evaluates the protocol’s performance using analytical
{ 𝑀 ∕𝑥 } active substitution and simulation approaches in [25]. EAP-AKA’ protocol is assessed and
compared with 5G-AKA protocol in [11].

7.1. Analytical performance evaluation

Furthermore, [12,18,22] ignored the sophistication of today’s at-
tackers. They assumed that security mechanisms in place would protect
The analytical modelling in [25,26] associates an enhanced label
the diameter protocol, the channel, and HN entities, but they did not
to each communication and each decryption based on the ProVerif
consider attacks in [19,23,24], that even a secure network can be
and Applied pi-calculus processes used in the protocol verification. It
compromised, resulting in a larger attack vector [11]. Because the non-
is supported with enhanced operational semantics based on labelled
injective and injective agreements between SN and UE fails, a replay bisimilarity [27], processes that build finite state spaces, and maintains
attack is possible. However, after the replayed message has made a communication output and input components with their grammatical
roundtrip to the HN, the SQN and unlink-ability problems [18] can contexts. Each prefix of a particular process is given a context label 𝜗
be solved. The resynchronization is accomplished by either checking and the processes’ parallel composition (|) defines the entire system. As
if the SQNUE sent in AUTS is greater than SQNHN, or setting SQNHN indicated in Table 3, the new names are formed using the restriction
to SQNUE. operator 𝜈𝑛𝑃 , which operates as a static binder in the procedure 𝑃 for
Therefore, if the standard is underspecified, the protocol vulner- the variable 𝑛. The transition of systems can be used to demonstrate
ability could allow the multiple attacks in 5G. Another additional communication, illustrated in Figs. 9 and 10 for EAP-AKA’ and 5G-AKA
measure is the use of Diffie–Hellman key exchange for perfect forward protocols, respectively.
secrecy, but the computation cost is too much in terms of mobile device To evaluate quantitative aspects of transitions like cryptographic
resources. Also, the authentication relying on the 𝐾𝐴𝑈 𝑆𝐹 in AUSF is not processes that conduct encryption and decryption, the cost is assigned
as strong as direct authentication between the ARPF and the USIM [11]. to individual transitions derived from their labels [26]. The protocol’s
When the protocol was simulated again with a secure communica- cost in terms of the time overhead of the primitives’ actions, transition
tion channel in HN environment and using more robust mechanisms costs, which are determined by examining enhanced labels are given.
such as cryptographic techniques, and randomness, it was found that It is assumed that each entity has its processing unit, assigned a
the authentication on UE and SN holds as assumed by the 5G standard cost of 1 to each tag ∥ 𝑖, output and input are given the same cost. In a

9
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 10. 5G-AKA state transition system.

Table 4 Table 5
Cost description. Cost labels for the protocols.
Term Description EAP-AKA’ 5G-AKA
𝑛 message size c1 = 2s + e c1 = 2s+e
𝑚𝑖 𝑖th encryption size c2 = 3s c2 = 3s
𝑒 unitary encryption cost c3 = 3s c3 = 3s
𝑑 unitary decryption cost c4 = d c4 = d
𝑠 unitary output cost c5 = 5s + 8e c5 = 5s+7e
𝑙𝑖 label of the state c6 = 5s c6 = 5s
𝑐𝑖 cost of the label c7 = 5s c7 = 5s
c8 = 5d c8 = 4d
c9 = 2s + e c9 = s+e
c10 = 2s c10 = s
∑
transition, the cost of transmission is equal to 𝑛 ∗ 𝑠+ 𝑙𝑖=1 𝑚𝑖 ∗ 𝑒 the cost c11 = d c11 = 2s
of decryption is equal to 𝑛 ∗ 𝑑, and the terms are specified in Table 4. C12 = 2s c12 = 2s
C13 = s c13 = d
The cost 𝑐𝑖 of the protocol in relation to its label 𝑙𝑖 are presented in
Section 7.1.2. Cryptography primitives, system architecture, protocols,
and encryption algorithms such as ECC, SQN, AKA challenge, and XOR
influence the cost. from binding with process 𝑃 𝑖 to 𝑃 𝑗. As a result, it is equivalent to the
sum of all viable transition costs from 𝑃 𝑖 to 𝑃 𝑗, and rates correlate
7.1.1. Quantitative measurement with individual costs inside a transition system, as stated in [26]. A
The enhanced operational semantics are used to obtain the quan- CTMC C is represented as a directed graph, where the nodes are the
tifiable data required to generate the Continuous-time Markov chain states of C and states reachable from one another are connected by
(CTMC) process [28]. CTMC is made up of a number of states, labelled
arcs, as shown in Figs. 9 and 10. Because of this, the rates at which the
transitions in those states, and a sequence of random values, the
process switches between states can be organized in a square/generator
probabilities of which depend on the values of previous states [29].
matrix represented as . The graph’s adjacency matrix contains a
In [26], the costs are regarded as exponential distributions’ parameters,
when the transitions’ exponential distributions are calculated, the arcs representation of the CTMC for the process (𝐶𝑇 𝑀𝐶(𝑃 )). Moreover,
that share a source and a target are collapsed, resulting in the numerical the elements of 𝑄 are used to illustrate the instantaneous transition
process 𝑃 . rates [26]. The transition rate between two states 𝑃 𝑖 and 𝑃 𝑗, denoted
Additionally, the parameter rate 𝑟 is connected to a transition to by the symbol 𝑞(𝑃𝑖 , 𝑃𝑗 ), is the rate at which transitions between these
estimate the rate, or transition probabilities at which a system switches states take place using Eq. (1).

10
E.K.K. Edris et al. Array 16 (2022) 100254

𝑙1 𝑙2 𝑙3 𝑙4 𝑙5 𝑙6 𝑙7 𝑙8 𝑙9 𝑙10 𝑙11 𝑙12 𝑙13

𝑙1 ⎛ −𝑥 𝑥 0 0 0 0 0 0 0 0 0 0 0 ⎞
⎜ ⎟
𝑙2
⎜ 0 −3𝑠 3𝑠 0 0 0 0 0 0 0 0 0 0 ⎟
𝑙3 ⎜ 0 0 −3𝑠 3𝑠 0 0 0 0 0 0 0 0 0 ⎟
𝑙4
⎜ 0 0 0 −𝑑 𝑑 0 0 0 0 0 0 0 0 ⎟
⎜ ⎟
𝑙5 ⎜ 0 0 0 0 −𝑧 𝑧 0 0 0 0 0 0 0 ⎟
𝑙6 ⎜ 0 0 0 0 0 −5𝑠 5𝑠 0 0 0 0 0 0 ⎟
⎜ ⎟
𝐐𝟏 = 𝑙7 ⎜ 0 0 0 0 0 0 −5𝑠 5𝑠 0 0 0 0 0 ⎟
𝑙8 ⎜ 0 0 0 0 0 0 0 −5𝑑 5𝑑 0 0 0 0 ⎟
⎜ ⎟
𝑙9 ⎜ 0 0 0 0 0 0 0 0 −𝑥 𝑥 0 0 0 ⎟
𝑙10 ⎜ 0 0 0 0 0 0 0 0 0 −2𝑠 2𝑠 0 0 ⎟
⎜ ⎟
𝑙11
⎜ 0 0 0 0 0 0 0 0 0 0 −𝑑 𝑑 0 ⎟
𝑙12 ⎜ 0 0 0 0 0 0 0 0 0 0 0 −2𝑠 2𝑠 ⎟
⎜ 0 0 0 0 0 0 0 0 0 0 0 0 −𝑠 ⎟
𝑙13 ⎝ ⎠

Box I.

𝑙1 𝑙2 𝑙3 𝑙4 𝑙5 𝑙6 𝑙7 𝑙8 𝑙9 𝑙10 𝑙11 𝑙12 𝑙13

𝑙1 ⎛ −𝑥 𝑥 0 0 0 0 0 0 0 0 0 0 0 ⎞
⎜ ⎟
𝑙2
⎜ 0 −3𝑠 3𝑠 0 0 0 0 0 0 0 0 0 0 ⎟
𝑙3 ⎜ 0 0 −3𝑠 3𝑠 0 0 0 0 0 0 0 0 0 ⎟
𝑙4
⎜ 0 0 0 −𝑑 𝑑 0 0 0 0 0 0 0 0 ⎟
⎜ ⎟
𝑙5 ⎜ 0 0 0 0 −𝑦 𝑦 0 0 0 0 0 0 0 ⎟
𝑙6 ⎜ 0 0 0 0 0 −5𝑠 5𝑠 0 0 0 0 0 0 ⎟
⎜ ⎟
𝐐𝟐 = 𝑙7 ⎜ 0 0 0 0 0 0 −5𝑠 5𝑠 0 0 0 0 0 ⎟
𝑙8 ⎜ 0 0 0 0 0 0 0 −4𝑑 4𝑑 0 0 0 0 ⎟
⎜ ⎟
𝑙9 ⎜ 0 0 0 0 0 0 0 0 −𝑤 𝑤 0 0 0 ⎟
𝑙10 ⎜ 0 0 0 0 0 0 0 0 0 −𝑠 𝑠 0 0 ⎟
⎜ ⎟
𝑙11
⎜ 0 0 0 0 0 0 0 0 0 0 −2𝑠 −2𝑠 0 ⎟
𝑙12 ⎜ 0 0 0 0 0 0 0 0 0 0 0 −2𝑠 2𝑠 ⎟
⎜ 0 0 0 0 0 0 0 0 0 0 0 0 −𝑑 ⎟
𝑙13 ⎝ ⎠

Box II.

Table 6 one to evaluate the performance of a procedure 𝑃 [29]. The reward

Metrics variables. structure of a process 𝑃 is a vector of rewards with the same number
Variable Description of components as the number of derivatives of 𝑃 . Performance mea-
w s + e surements for a process 𝑃 were computed from information and the
x 2s+e stationary distribution 𝛱 of the 𝐶𝑇 𝑀𝐶. Eq. (3) is used to calculate
y 5s+7e
z 5s+8e
the total reward of a process 𝑃 [26].
∑
𝑅(𝑃 ) = 𝜌𝑃𝑖 𝑋 𝛱(𝑃𝑖 ). (3)
𝑃𝑖 ∈𝑑(𝑃 )

Therefore, add the values of 𝑃 𝑖, multiply by the matching reward

∑ structure with the encryption algorithm used and the time spent for
⎧
⎪𝑞(𝑃𝑖 , 𝑃𝑗 ) = $(𝜃𝑘 ) if 𝑖 ≠ 𝑗 summation. Whereas comparing the non-zero reward value against
⎪ 𝜃𝑘 the rate of the relevant transition [30], one can determine the sys-
⎪ 𝑃 𝑃
𝑖⃖⃖⃗ 𝑗
𝑞𝑖𝑗 = ⎨ ∑ 𝑛 (1) tem’s throughput in terms of the quantity of work completed per unit
⎪− 𝑞 if 𝑖 = 𝑗 time [25].
⎪ 𝑗=1 𝑖𝑗
⎪ 𝑗≠𝑖
⎩ 7.1.2. Parameters and metrics
System performance metrics become understandable since they are To assess the performance of 5G protocols, Markov chains and
finite and cyclic in Eq. (2), these measurements of process 𝑃 are other mathematical techniques are used after specifying the proto-
obtained by utilizing the stationary probability distribution 𝛱 for the cols, describing the cost function and the semantics of the labelled
CTMC and bounding it with 𝑃 . enhanced operation. The stationary Markov chain distributions 𝛱𝑖 =
(𝑋0 , … , 𝑋𝑛−1 )(𝑖 = 1, 2, and 𝑛 = 6, 8) for the protocols, using the
∑
𝑛
following linear equation to serve as the solution for each protocol as
𝛱𝑄 = 0 𝑎𝑛𝑑 𝛱(𝑥𝑖 ) = 1. (2)
𝑖=0
Eq. (4) [26].

The answers to the systems’ linear equations are the stationary ∑

𝑛−1
𝛱𝑄 = 0 𝑎𝑛𝑑 𝑋𝑖 = 1. (4)
distributions for each system. Associating a reward structure, allows
𝑖=0

11
E.K.K. Edris et al. Array 16 (2022) 100254

[ ]
𝑀 𝑀 𝑀 𝑀 𝑀 𝑀 𝑀 𝑀 𝑀 𝑀 𝑀 𝑀 𝑀
𝛱1 = , , , , , , , , , , , , (5)
𝑥 3𝑠 3𝑠 𝑑 𝑧 5𝑠 5𝑠 5𝑑 𝑥 2𝑠 𝑑 2𝑠 𝑠

[ ]
𝑁 𝑁 𝑁 𝑁 𝑁 𝑁 𝑁 𝑁 𝑁 𝑁 𝑁 𝑁 𝑁
𝛱2 = , , , , , , , , , , , , (6)
𝑥 3𝑠 3𝑠 𝑑 𝑦 5𝑠 5𝑠 4𝑑 𝑤 2𝑠 2𝑠 2𝑠 𝑑
EAP-AKA’ Protocol: Tables 5 and 6 illustrate the cost and transition
association, while Fig. 9 displays the transition state and labels. To
ensure that the transition system has stationary distributions and has
both finite and cyclic beginning states, the following generator matrix
𝑄1 = CTMC (EAP-AKA’) is generated, and the stationary distribution is
𝛱1 (see Box I) and Eq. (5), where 𝑀 = 30𝑠 + 10𝑒 + 7𝑑.
Where:
13𝑀
𝑀= (7)
30𝑠 + 10𝑒 + 7𝑑
5G-AKA Protocol: Tables 5 and 6 illustrate the cost and transition
association while Fig. 10 displays the status of the transition and
the labels. The following generator matrix 𝑄2 = CTMC (5G-AKA) is
generated, and the stationary distribution is 𝛱2 (see Box II) and Eq. (6),
where 𝑁 = 29𝑠 + 9𝑒 + 6𝑑.
Where:
13𝑁
𝑁= (8)
29𝑠 + 9𝑒 + 6𝑑

7.1.3. Analytical results

The cost of each protocol is analysed using efficiency and through-
put metrics.
Efficiency: To measure the effect of cryptographic primitives on the
performance of the protocol, value 0 is assigned to any other transition
and value 1 to any transition in which the decryption is enabled,
therefore the following is given value 1:

1. the 4th, 8th, 11th transitions in EAP-AKA’

2. the 4th, 8th, 13th transitions in 5G-AKA
Fig. 11. Protocols’ efficiency and throughput based on analytical approach.
The protocols’ performance as measured by the metric 𝑅 is as
follows: Table 7
𝑀 Performance evaluation of the protocols.
′
𝑅(𝐸𝐴𝑃 − 𝐴𝐾𝐴 ) = (9) Protocols Efficiency Throughput
7𝑑
𝐸𝐴𝑃 −𝐴𝐾𝐴′ 𝑑
EAP-AKA’ 7𝑑 30𝑠+10𝑒+7𝑑
𝑁 5G-AKA 5𝐺−𝐴𝐾𝐴 𝑑
𝑅(5𝐺 − 𝐴𝐾𝐴) = (10) 6𝑑 29𝑠+9𝑒+6𝑑
6𝑑
If the encryption algorithm is the same for both protocols and the
same quantitative performance evaluation metric is employed, it is easy
7.1.4. Performance analysis 1
to demonstrate how one protocol is expensive than the other for every
The results in Table 7 and Fig. 11 show that 5G-AKA protocol is
positive using 𝑠, 𝑑, and 𝑒.
more effective and has greater throughput than EAP-AKA’ protocol, it
Throughput : This is the outcome of linking a transition reward to
uses more messages between the UE and AUSF. Using the continuous
an activity’s rate and transition, the CTMC is cyclic, and each label
time method allows the assessment of the protocol’s performance based
represents a different transaction. A transition reward is assigned to the
on its stationary distribution, if any. Additionally, ProVerif and applied
rate of the last protocol communication but nothing to all other commu- 𝑝𝑖 calculus are applied for security characteristics and bisimilarity
nications, then throughput of the protocol is calculated. Additionally, labelling, respectively [25,26].
the results show a correlation between a cryptographic algorithm’s
energy usage and its time complexity [25].
7.2. Simulation performance evaluation approach
The following are calculations for the reward structure and total
rewards: For comparability of the protocol effectiveness, a simulation ap-
𝜌1 = (0......𝐶12 ),
(𝐶11 ) = 𝑑, proach is used for further evaluation, whereby the results and compared
′ 3𝑑 (11) and analysed. This is achieved by simulating the protocol in NS-3,
𝑅(𝐸𝐴𝑃 − 𝐴𝐾𝐴 ) =
30𝑠 + 10𝑒 + 7𝑑 which is installed and configured on an Ubuntu Linux virtual machine
𝜌2 = (0......𝐶12 ),
(𝐶13 ) = 𝑑, in a VirtualBox environment running on a Windows computer [25].
2𝑑 (12) The setup emulates the 5G non-standalone implementation with
𝑅(5𝐺 − 𝐴𝐾𝐴) = 5G radio technology and LTE core network based on the NS-3 5G
29𝑠 + 9𝑒 + 6𝑑
mmWave module [31,32]. To model 5G communication, the nodes, net

12
E.K.K. Edris et al. Array 16 (2022) 100254

Fig. 12. Protocols computational cost based on simulation approach.

Table 8
Cryptographic operations compute time.
Notation Description Computational
time (ms)
𝑇𝐸 execution 21.5
𝑇𝐴𝑣 authentication vector 33.5
𝑇𝐾𝐷𝐹 key generation 12.0
𝑇ℎ hash digest function 5
𝑇𝑆𝑒 symmetric encoding 4
𝑇𝑆𝑑 symmetric decoding 5.5
𝑇𝐴𝑒 asymmetric encoding 8
𝑇𝐴𝑑 asymmetric decoding 9.5
𝑇𝑉 verification 12.5

Table 9
Cryptographic primitive length/size.
Cryptographic primitive Value
Strings 32 bits
SQN 48 bits
Identity 64 bits Fig. 13. EAP-AKA’ protocol communication cost based on simulation approach.
MAC 64 bits
Nonce 128 bits
Symmetric key 128 bits
Asymmetric key 256 bits estimated times in milliseconds (ms) as illustrated in Table 8. The
RES 256 bits
variations in computational times of the protocols are shown in Fig. 12.
SHA256 256 bits

7.2.3. Communication cost

Table 10
The protocol’s cryptographic primitives and messages are utilized as
Performance evaluation metrics.
parameters to assess the communication cost, defined in Tables 9 and
Parameters Values
10. AMF, 𝑠𝑦𝑛𝑐ℎ_𝑓 𝑎𝑖𝑙 and 𝑚𝑎𝑐_𝑓 𝑎𝑖𝑙 messages are represented as strings.
Throughput bits/milliseconds
Latency milliseconds
The term 𝑚 refers to those cryptographic primitive numerical values
𝑚 messages primitive cost part of messages between entities and used as input in NS-3 simulation,
𝑛 total sum of 𝑚 while 𝑛 is the sum of all 𝑚 in the protocol and 𝑛 = (𝑚1, 𝑚2, 𝑚3, 𝑚4....)
in bits. Therefore, EAP-AKA’ = (384, 448, 448, 1082, 1082, 1082, 592, 592,
224, 32) and 5G-AKA = (384, 448, 448, 1738, 928, 672, 256, 256, 192, 576).
device, applications, and topology helpers were adjusted to represent Throughput (𝑏𝑖𝑡𝑠∕𝑚𝑠) and latency (𝑚𝑠) are performance metrics of 𝑛
5G-AKA and EAP-AKA’ protocols entities. In addition, the security at- during the protocol simulation to determine the communication cost.
tributes, cryptographic operatives were defined using applications with
a sendMessage () function for protocol exchange messages [25,33]. 7.2.4. Simulation results
The quantified security protocol findings were extracted from the
7.2.1. Parameter and metrics trace pcap and XML files produced by NS-3 simulation for both proto-
The protocols’ computational and communication inputs are based cols, measuring throughput and latency based on metrics in Table 10.
on 3GPP recommended 5G cryptographic primitives and algorithms [1,
11]. 7.2.5. Performance analysis 2
It is assumed that a successful authentication run was completed,
7.2.2. Computational cost hence, the resynchronization phase is not evaluated. Table 11 provides
To approximately measure the computational cost of the proto- an overview of the computational cost of each security protocol, and
cols, time cost of message attributes processing is defined and given Fig. 12 illustrates the comparison. It shows that EAP-AKA’ compute

13
E.K.K. Edris et al. Array 16 (2022) 100254

Table 11
Protocols computational cost.
Protocols Time values Time (ms)
EAP-AKA’ 𝑇𝐸 + 7𝑇𝑆𝑒 + 𝑇𝐴𝑒 + 7𝑇𝑆𝑑 + 𝑇𝐴𝑑 + 1𝑇𝐴𝑣 + 8𝑇𝐾𝐷𝐹 + 12𝑇𝑉 557.2
5G-AKA 𝑇𝐸 + 6𝑇𝑆𝑒 + 𝑇𝐴𝑒 + 6𝑇𝑆𝑑 + 𝑇𝐴𝑑 + 1𝑇𝐴𝑣 + 8𝑇𝐾𝐷𝐹 + 2𝑇ℎ + 11𝑇𝑉 542.5

8. Conclusion

The EAP framework and EAP-AKA’ protocol specifications were

presented in this article based on the 3GPP standard. All the security
presumptions and requirements have been identified through inter-
pretation and analysis of the 5G standard and the EAP-AKA’ RFC. It
formally analysed and verified the protocol using ProVerif utilizing
automated reasoning about the security properties. It analysed the
protocol for security guarantees, identified some vulnerabilities and
provided recommendations. The performance of the EAP-AKA’ protocol
performance was evaluated and compared with the 5G-AKA proto-
col for effectiveness using analytical and simulation methods. These
strategies considered the cost variables that may affect the protocol’s
design and efficiency in security implementation. Using these methods,
future work will concentrate on verifying and evaluating future security
protocol guarantees and effectiveness.

CRediT authorship contribution statement

Ed Kamya Kiyemba Edris: Conceptualization, Methodology, In-

vestigation, Software, Formal Analysis, Validation, Resources, Writ-
ing – original draft, Editing, Visualization. Mahdi Aiash: Conceptual-
ization, Methodology, Writing – review, Supervision. Jonathan Loo:
Conceptualization, Writing – review, Supervision.

Declaration of competing interest

The authors declare that they have no known competing finan-

cial interests or personal relationships that could have appeared to
influence the work reported in this paper.

Data availability

No data was used for the research described in the article.

References

Fig. 14. 5G-AKA protocol communication cost based on simulation approach. [1] 3GPP. Security architecture; procedures for 5G system. Technical specifica-
tion (TS), (3GPP TS 33.501 V17.4.1 (2022-01)). Third Generation Partner-
Table 12 ship Project; 2022, URL https://portal.3gpp.org/desktopmodules/Specifications/
Protocols communication cost. SpecificationDetails.aspx?specificationId=3169.
[2] Blanchet B, Smyth B, Cheval V, Sylvestre M. ProVerif 2.01: automatic crypto-
Protocol Number of Communication
graphic protocol verifier, user manual and tutorial. In: Version from. 2020, URL
messages cost (bits)
https://prosecco.gforge.inria.fr/personal/bblanche/proverif.
(𝑚) (𝑛)
[3] Zhang J, Yang L, Cao W, Wang Q. Formal analysis of 5G EAP-tls authentication
EAP-AKA’ 10 5966 protocol using ProVerif. IEEE Access 2020.
5G-AKA 10 5898 [4] Edris EKK, Aiash M, Loo J, Alhakeem MS. Formal verification of secondary
authentication protocol for 5G secondary authentication. Int J Secur Netw
2021;16(4):223–34. http://dx.doi.org/10.1504/IJSN.2021.119379.
[5] Ajit M, Sankaran S, Jain K. Formal verification of 5G EAP-aka protocol. In: 2021
takes 557.2 ms compared to 545.6 ms for 5G-AKA. However, there is 31st international telecommunication networks and applications conference.
ITNAC, 2021, p. 140–6. http://dx.doi.org/10.1109/ITNAC53136.2021.9652163.
a slight difference in messages 4, 6, 8 and 9 of the protocols.
[6] Vollbrecht JR, Aboba B, Blunk LJ, Levkowetz H, Carlson J. Extensible authenti-
Additionally, the overall communication costs are listed in Table 12. cation protocol (EAP). RFC Editor, IETF; 2004, URL https://tools.ietf.org/html/
Figs. 13 and 14 illustrate throughput and latency plot graphs that were rfc3748.
created from NS-3 simulation with almost identical graphs. Both proto- [7] Arkko J, Lehtovirta V, Eronen P. Improved extensible authentication protocol
method for 3rd generation authentication and key agreement (EAP-AKA’). RFC
cols have the same amount of messages 𝑚 = 10, EAP-AKA’ has a higher
Editor,IETF; 2009, URL https://tools.ietf.org/html/rfc5448.
communication cost than 5G-AKA i.e., 5996 𝑏𝑖𝑡𝑠 𝑛 compared to 5898 [8] Arkko J, Lehtovirta V, Torvinen V, Eronen P. Improved extensible authen-
𝑏𝑖𝑡𝑠 𝑛. 5G-AKA’ has a better performance in terms of throughput and tication protocol method for 3GPP mobile network authentication and key
latency but simulation produces comparable results due the similarity agreementsw (EAP-AKA’). Tech. rep, (9048). IETF; 2021, http://dx.doi.org/10.
17487/RFC9048, URL https://www.rfc-editor.org/info/rfc9048.
in number messages, primitives and entities used. The usage of MAC2
[9] Edris EKK, Aiash M, Loo J. An introduction of a modular framework for
and a success message in EAP-AKA’ increases the cost slightly, even securing 5G networks and beyond. Network 2022;2(3):419–39. http://dx.doi.org/
though the hash of RES is only used in 5G-AKA. 10.3390/network2030026.

14
E.K.K. Edris et al. Array 16 (2022) 100254

[10] 3GPP. 3GPP system architecture evolution (SAE) system aspects, secu- [20] Menezes AJ, Oorschot PCV, Vanstone SA. Handbook of applied cryptography.
rity aspects of non-3GPP accesses. Technical specification (TS), (3GPP Boca Raton, Florida, USA: CRC Press; 2018, Includes bibliographical references
TS 33.402 V16.0.0(2020-07)). Third Generation Partnership Project; 2020, and index. ID: alma991001301199704781.
URL https://portal.3gpp.org/desktopmodules/Specifications/SpecificationDetails. [21] Lowe G. A hierarchy of authentication specifications. In: Proceedings 10th
aspx?specificationId=2297. computer security foundations workshop. IEEE; 1997, p. 31–43. http://dx.doi.
[11] Edris EKK, Aiash M, Loo J. Formal verification and analysis of primary authen- org/10.1109/CSFW.1997.596782, ID: ieee_s596782.
tication based on 5G-AKA protocol. In: The third international symposium on 5g [22] Dehnel-Wild M, Cremers C. Security vulnerability in 5G-AKA draft. Tech. rep,
emerging technologies. 5GET 2020, Paris, France: IEEE; 2020, p. 256–61. Department of Computer Science, University of Oxford; 2018.
[12] Basin D, Dreier J, Hirschi L, Radomirović S, Sasse R, Stettler V. A formal analysis [23] Engel T. Ss7: Locate. Track. Manipulate. In: Talk at 31st chaos communication
of 5G authentication. In: Proceedings of the 2018 ACM SIGSAC conference on congress. 2014.
computer and communications security. 2018, p. 1383–96. http://dx.doi.org/10. [24] RIFS G. Diameter roaming security - proposed permanent reference document.
1145/3243734.3243846. Tech. rep., GSMA; 2016.
[13] Meier S, Schmidt B, Cremers C, Basin D. The TAMARIN prover for the symbolic [25] Edris EKK, Aiash M, Loo J. Security protocol performance evaluation using
analysis of security protocols. In: Sharygina N, Veith H, editors. Computer applied Pi calculus and Markov chain based on 5G security. Comput Secur 2022,
aided verification, Vol. 8044. Berlin, Heidelberg: Springer Berlin Heidelberg; Submitted for Publication.
2013, p. 696–701. http://dx.doi.org/10.1007/978-3-642-39799-8_48, URL https: [26] Bodei C, Curti M, Degano P, Buchholtz M, Nielson F, Nielson HR, et al.
//www.research-collection.ethz.ch/handle/20.500.11850/68108. Performance evaluation of security protocols specified in Lysa. Electron Notes
[14] Armando A, Basin DA, Boichut Y, Chevalier Y, Compagna L, Cuellar JR, Theor Comput Sci 2005;112:167–89.
et al. The AVISPA tool for the automated validation of internet security [27] Abadi M, Blanchet B, Fournet C. The applied Pi calculus: Mobile val-
protocols and applications. Comput Aided Verif Proc 2005;3576:281–5, ID: ues, new names, and secure communication. J ACM 2017;65(1):1–41, ID:
wos000230755800027. hal_soai_HAL_hal_01423924v1.
[15] Cremers C, Dehnel-Wild M. Component-based formal analysis of 5G-AKA: Chan- [28] Stewart WJ. Introduction to the numerical solution of markov chains. Princeton
nel assumptions and session confusion. In: Network and distributed system University Press; 1994.
security symposium. NDSS, Internet Society; 2019. [29] Hillston J. A compositional approach to performance modelling, Vol. 12.
[16] Caixia LIU, Xinxin HU, Shuxin LIU, Wei YOU, Yu ZHAO. Security analysis of 5G Cambridge University Press; 2005.
network EAP-AKAṕrotocol based on Lowe’s taxonomy. J Electron Inf Technol [30] Bodei C, Curti M, Degano P, Buchholtz M, Nielson F, Nielson HR, et al. On
2019;41(8):1800–7. evaluating the performance of security protocols. In: International conference on
[17] van DB, Verdult R, de Ruiter J. Defeating IMSI catchers. In: Proceedings of parallel computing technologies. Springer; 2005, p. 1–15.
the 22Nd ACM SIGSAC conference on computer and communications security, [31] Nsnam. Ns-3 a discrete-event network simulator for internet systems. (NS-3.33).
Vol. 2015. 2015, p. 340–51. http://dx.doi.org/10.1145/2810103.2813615, ID: 2021.
acm2813615. [32] Mezzavilla M, Zhang M, Polese M, Ford R, Dutta S, Rangan S, et al.
[18] Koutsos A. The 5G-AKA authentication protocol privacy. In: 2019 IEEE eu- End-to-end simulation of 5G mmwave networks. IEEE Commun Surv Tutor
ropean symposium on security and privacy. IEEE; 2019, p. 464–79, ID: 2018;20(3):2237–63. http://dx.doi.org/10.1109/COMST.2018.2828880.
proquest2135414227. [33] Banerjee S, Odelu V, Das AK, Chattopadhyay S, Park Y. An efficient, anony-
[19] Enisa. Signalling security in telecom SS7/Diameter/5G. Tech. rep, Enisa; 2018, mous and robust authentication scheme for smart home environments. Sensors
URL https://www.enisa.europa.eu/publications/signalling-security-in-telecom- 2020;20(4):1215.
ss7-diameter-5g.

15