Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model

Abstract

The 5th generation mobile communication technology (5G) authentication and key management (AKA) protocol specified by the 3rd generation partnership project (3GPP) includes three cases because it introduces synchronization failure and message authentication code (MAC) failure procedures. Thus, there may be interactions between these cases, forming vulnerabilities that do not exist in any single case. However, this is not fully considered in the existing formal analysis and improvement of the 5G AKA protocol. To solve this problem, this paper formally analyzes the security of the latest version of the 5G AKA protocol based on the mixed strand space model for mixed protocols and finds many new attacks, including cross attacks for mixed cases. Then, a secure and efficient primary authentication and key agreement protocol for 5G networks is proposed, which is named the 5G-AKA’. In the 5G-AKA’ protocol, the pre-shared key between the user equipment (UE) and the home network (HN) is replaced with a derivation key of the pre-shared key, the challenge–response mechanism between the serving network (SN) and the HN is added, the subscription permanent identifier (SUPI) of the UE is added to the second message between the SN and the HN, and the MAC failure is replaced with a timeout mechanism on the HN. Finally, the 5G-AKA’ protocol is proved secure in the mixed strand space model and can overcome these attacks of the latest version of the 5G AKA protocol. Additionally, the comparative analysis shows that the 5G-AKA’ protocol is better than the recently improved 5G AKA protocols in security, and the 5G-AKA’ protocol is efficient and is backward compatible with the 5G AKA protocol.

1. Introduction

With the continuous popularization of the 5th generation mobile communication technology (5G), in the near future, the 5G network, as an important communication infrastructure, will penetrate into diversified vertical industries and fields such as transportation, medical treatment and industry, and support various information interactions between people, people and things, and things and things [1]. In the 5G network, three different primary authentication and key agreement protocols are defined in the related 3rd generation partnership project (3GPP) specifications [2,3,4], including the 5G authentication and key agreement (AKA) protocol, the improved extensible authentication protocol method for 3rd generation authentication and key agreement (EAP-AKA’) protocol and the 5G extensible authentication protocol method for transport layer security (EAP-TLS) protocol. The first two protocols are based on the shared key cryptography, while the last one is based on the public key cryptography. These protocols all aim to provide mutual authentication of subscribers and networks. Currently, they are in the process of standardization.

The 5G AKA protocol [2,3,4] is developed directly from the evolution packet system (EPS)-AKA protocol of the long-term evolution (LTE)/4th generation mobile communication technology (4G) network [3], so it inherits certain security vulnerabilities from the EPS-AKA protocol such as impersonation attacks, man-in-the-middle attacks (MitM) and denial of service (DoS) attacks [5,6,7,8,9,10,11]. Dehnel-Wild et al. [12] analyzed the 5G AKA protocol of technical specification (TS) 33.501 v0.7.0. They discovered a protocol vulnerability that would enable the attacker to impersonate another user to a serving network (SN). Based on the Tamarin model checker [13], Basin et al. [14] investigated the security properties of the 5G AKA protocol of TS 33.501 v15.1.0, and several major issues were revealed, which are related to user localization, leakage of activity, the impact of active attackers and the presence of malicious SN while roaming. In [15], Liu et al. pointed out that the 5G AKA protocol suffers from link-ability attacks, and then proposed a new authentication scheme by making use of the Diffie–Hellman key exchange algorithm for generating the session key. This scheme was successful in preventing link-ability attacks along with a MitM attack.

For the more recent 5G AKA protocol, Borgaonkar et al. [16] found a new attack. They claimed that the protection mechanism of the sequence number (SQN) can be defeated under specific replay attacks due to its use of exclusive-or (XOR) and a lack of randomness. In [17], Cremers et al. modeled all the key components of the 5G AKA protocol (i.e., the user equipment, the serving network and the home network) according to the definition in the 3GPP specification document. They discovered an attack that exploits a potential race condition and additionally showed that solving the race condition for the honest case does not necessarily prevent the attack. In [18], Koutsos et al. investigated the privacy properties of the 5G AKA protocol using the Bana–Comon logic [19,20]. They discovered a novel de-synchronization attack and proved that their proposed protocol guarantees the privacy properties. In [21], Braeken et al. proposed a novel version of the 5G AKA protocol to prevent active attacks and gain resistance against malignant serving networks. Unfortunately, there is a possibility of having SN impersonation, so this scheme does not eliminate the vulnerability towards the MitM attack. Further, Gharsallah et al. [22] also attempted to launch a revised version of the 5G AKA protocol. However, their proposed protocol suffers from privacy preservation as the device identities are clearly transmitted in the air which leads to numerous security attacks.

As time goes on, more and more attacks of the 5G AKA protocol were found due to the insecure channel between different network domains in the legacy mobile network. In [23], Hu et al. discovered an attack exploiting the subscription concealed identifier (SUCI) to track a subscriber in the 5G network, which is directly caused by the insecure air channel. To cover this issue, they proposed a secure authentication scheme by utilizing the existing public key infrastructure (PKI) mechanism. Further, they found a location sniffing attack, which can be implemented by an attacker through inexpensive devices [24]. Similarly, they proposed a fix scheme based on the existing PKI mechanism. In [25], Edris et al. modeled the 5G AKA protocol with symbolic modeling using ProVerif based on three and four entities models, and then proposed their security consideration. Further, Mariya et al. [26] proposed an enhanced version of the authentication and key agreement protocol for the 5G system that surmounts the limitations existing in the 5G AKA protocol. Parne et al. [27] introduced a protocol that preserves the privacy of the user identity and overcomes the identified problems of the 5G AKA protocol. Similarly, 3GPP has also been enhancing the security of the 5G AKA protocol [2,3,4].

Because the 5G AKA protocol [2,3,4] introduces synchronization failure and message authentication code (MAC) failure procedures, it has three cases, so there may be interactions between these cases, forming vulnerabilities that do not exist in any single case. However, this is not fully considered in the above security analysis and improvement of the 5G AKA protocol. Therefore, we formally analyze the security of the latest version of the 5G AKA protocol considering three cases at the same time. Then, we propose a secure and efficient primary authentication and key agreement protocol for 5G networks, named the 5G-AKA’. Finally, we prove that the 5G-AKA’ protocol is secure, and it is efficient and backward compatible.

The main contributions of this paper are as follows:

• We formally analyze the security of the latest version of the 5G AKA protocol in the mixed strand space model for mixed protocols [28] and give twenty-one attack scenarios of the 5G AKA protocol. Based on these attack scenarios, we find many new attacks of the 5G AKA protocol, including cross attacks for mixed cases.
• We propose the 5G-AKA’ protocol, and then formally analyze its security in the mixed strand space model for mixed protocols [28]. As a result, no attack scenario is obtained. By discussion and analysis, the 5G-AKA’ protocol can overcome these attacks of the 5G AKA protocol, thus it is secure.
• Based on comparative analysis, the 5G-AKA’ protocol is better than the 5G AKA protocol and the recently improved 5G AKA protocols in security, and is efficient and backward compatible.

The rest of this paper is organized as follows. Section 2 provides an overview of the latest version of the 5G AKA protocol. In Section 3, we formally analyze the security of the latest version of the 5G AKA protocol in the mixed strand space model. Section 4 describes our proposed 5G-AKA’ protocol and gives the security analysis of the 5G-AKA’ protocol in the mixed strand space model. In Section 5, we present some discussions and we conclude the paper in Section 6.

2. Overview of the 5G AKA Protocol

According to [2,3,4], the steps of the latest version of the 5G AKA protocol in the 3GPP standard version v17.4.0 of TS 33.501 are illustrated in Figure 1.

In Figure 1, the detailed steps of the latest version of the 5G AKA protocol are as follows:

• When the security anchor function (SEAF) initiates authentication with the user equipment (UE), the UE sends $SUCI$ to the SEAF, where the UE includes mobile equipment (ME) and a universal subscriber identity module (USIM).

  $$SUCI=x\cdot G\left|\right|{\left\{SUPI\right\}}_{EK}\left|\right|MA{C}_{UE}$$

  (1)

  $$EK\left|\right|ICB\left|\right|MK=KDF(x\cdot y\cdot G)$$

  (2)

  $$MA{C}_{UE}=HMAC(MK,{\left\{SUPI\right\}}_{EK})$$

  (3)

  where $SUCI$ denotes a SUCI of the UE, $SUPI$ denotes the subscription permanent identifier (SUPI) of the UE, $x\cdot G$ and $x$ are an ephemeral public/private key pair of the UE for the Diffie–Hellman exchange, $y\cdot G$ and $y$ are an ephemeral public/private key pair of the home network (HN) for the Diffie–Hellman exchange, $EK$ is an encryption key, $ICB$ is an initial counter block (ICB), $MK$ is a MAC key, $MA{C}_{UE}$ is a MAC of the UE, $KDF()$ is a key derivation function and $HMAC()$ is a hash function for computing MAC, $\left|\right|$ denotes a cascade of fields.
• Upon receiving $SUCI$, the SEAF sends $SUCI$ and $SNN$ to the authentication server function (AUSF). $SNN$ denotes the serving network name (SNN) of the SN.
• If the SEAF is entitled to use $SNN$, then the AUSF stores the receiving $SNN$ and sends $SUCI$ and $SNN$ to the unified data management (UDM).
• The UDM invokes the subscriber identity de-concealing function (SIDF) whether $SUCI$ is received. Then, the SIDF de-conceals $SUCI$ to gain $SUPI$ before the UDM can process the request. Based on $SUPI$, the UDM/ARPF (authentication credential repository and processing function) chooses the authentication method.
• When 5G AKA is selected, the UDM/ARPF generates $RAND$, calculates $AUTN$ and $XRES*$, and derives $K_{AUSF}$, and then creates a 5G home environment authentication vector from $RAND$, $AUTN$, $XRES*$ and $K_{AUSF}$. $RAND$ is an unpredictable challenge of the HN.

  $$AUTN=SQN\oplus AK\left|\right|AMF\left|\right|MAC$$

  (4)

  $$MAC=f_1(K,SQN|\left|RAND\right||AMF)$$

  (5)

  $$XRES=f_2(K,RAND)$$

  (6)

  $$CK=f_3(K,RAND)$$

  (7)

  $$IK=f_4(K,RAND)$$

  (8)

  $$AK=f_5(K,RAND)$$

  (9)

  $$K_{AUSF}=KDF(CK||IK,SNN||SQN\oplus AK)$$

  (10)

  $$XRES*=KDF(CK||IK,SNN|\left|RAND\right||XRES)$$

  (11)

  where $AUTN$ is an authentication token of the HN, $SQN$ is a fresh sequence number generated by the HN, $AK$ is an anonymity key, $AMF$ is the authentication management field (AMF) and the separation bit of the AMF is set 1, $MAC$ is a MAC of the HN, $K$ is a long-term key between the UE and the HN, $f_1()$ and $f_2()$ are two message authentication functions, $f_3()$, $f_4()$ and $f_5()$ is three key generating functions, $CK$ is a cipher key, $IK$ is an integrity key, $K_{AUSF}$ is a key derived from $CK$ and $IK$, $XRES$ is an expected response and $XRES*$ is an expected response derived from $CK$ and $IK$.
• The UDM sends the 5G home environment authentication vector to the AUSF together with $SUPI$. When an authentication and key management for applications (AKMA) subscription is used, the UDM also sends $AKMA$ to the AUSF. $AKMA$ denotes the AKMA indication and routing indicator.
• The AUSF stores the $XRES*$ temporarily together with the received $SUPI$.
• The AUSF generates a 5G authentication vector from the 5G home environment authentication vector received from the UDM/ARPF by computing $HXRES*$ from $XRES*$, computing $K_{SEAF}$ from $K_{AUSF}$, replacing $XRES*$ with $HXRES*$, and replacing $K_{AUSF}$ with $K_{SEAF}$ in the 5G home environment authentication vector.

  $$HXRES*=SHA256(RAND||XRES*)$$

  (12)

  $$K_{SEAF}=KDF(K_{AUSF},SNN)$$

  (13)

  where $HXRES*$ is a hashing $XRES*$, $SHA256()$ is a hash function.
• The ASUF creates a 5G serving environment authentication vector by removing $K_{SEAF}$ from the 5G authentication vector, and then sends the 5G serving environment authentication vector (i.e., $RAND$, $AUTN$ and $HXRES*$) to the SEAF.
• The SEAF stores $HXRES*$, and then sends $RAND$, $AUTN$, $ngKSI$ and $ABBA$ to the UE. $ngKSI$ is used by the UE and the access and mobility management function to identify the $K_{AMF}$ and the partial native security context that is created if the authentication is successful. $ABBA$ denotes the anti-bidding down between architectures (ABBA) parameter.
• In the UE, the ME forwards $RAND$ and $AUTN$ to the USIM. Upon receipt of $RAND$ and $AUTN$, the USIM first computes the anonymity key $AK$ and retrieves the sequence number $SQN$. Next, the USIM computes $XMAC$ and compares this with $MAC$ which is included in $AUTN$. Then, the USIM verifies that the received $SQN$ is in the correct range. If $XMAC$ is the same as $MAC$ and $SQN$ is in the correct range (i.e., $SQ{N}_{UE}<SQN$, where $SQ{N}_{UE}$ denotes the highest sequence number the USIM has accepted), then the USIM computes a response $RES$, $CK$ and $IK$, and then returns $RES$, $CK$ and $IK$ to the ME. The ME then computes $RES*$, $K_{AUSF}$ and $K_{SEAF}$.

  $$XMAC=f_1(K,SQN|\left|RAND\right||AMF)$$

  (14)

  $$RES=f_2(K,RAND)$$

  (15)

  $$RES*=KDF(CK||IK,SNN|\left|RAND\right||RES)$$

  (16)

  where $RES$ is a response and $RES*$ is a response derived from $CK$ and $IK$.
• The UE sends $RES*$ to the SEAF.
• The SEAF computes $HRES*$ and compares this with $HXRES*$. If they coincide, then the SEAF considers the authentication as successful from the serving network’s point of view. If not, then the SEAF considers the authentication as unsuccessful.

  $$HRES*=SHA256(RAND||RES*)$$

  (17)

  where $HRES*$ is a hashing $RES*$.
• The SEAF sends the received $RES*$ to the AUSF.
• The AUSF compares the received $RES*$ with the stored $XRES*$. If $RES*$ and $XRES*$ are equal, then the AUSF considers the authentication as successful from the home network point of view. Then, the AUSF informs the UDM about the authentication result.
• The AUSF indicates to the SEAF whether the authentication was successful or not from the home network point of view (i.e., $Result$). If the authentication was successful, then the ASUF also sends $K_{SEAF}$ and $SUPI$ to the SEAF.

In step 11, if $XMAC$ and $MAC$ are different, then the USIM indicates to the ME a MAC failure of $AUTN$. Then, the UE sends the “MAC failure” indication to the SEAF. Further, the SEAF sends the “MAC failure” indication to the AUSF. Finally, the ASUF sends the “MAC failure” indication to the UDM/ARPF.

In step 11, if $SQN$ is not in the correct range (i.e., $SQ{N}_{UE}\ge SQN$), then the USIM computes $AUTS$, and then sends $AUTS$ with a “Synchronization failure” indication to the ME. Then, the UE sends $AUTS$ with the “Synchronization failure” indication to the SEAF. Further, the SEAF sends $RAND$ and $AUTS$ with the “Synchronization failure” indication to the AUSF. Finally, the ASUF sends $RAND$ and $AUTS$ with the “Synchronization failure” indication to the UDM/ARPF.

$$AUTS=SQ{N}_{UE}\oplus A{K}^{\ast }\left|\right|MAC-S$$

(18)

$$MAC-S=f_1^{\ast }(K,SQ{N}_{UE}|\left|RAND\right||AM{F}_0)$$

(19)

$$A{K}^{\ast }=f_5^{\ast }(K,RAND)$$

(20)

where $A{K}^{\ast }$ is an anonymity key, $MAC-S$ is a MAC of the UE, $AM{F}_0$ is a dummy value of all zeros, $f_1^{\ast }()$ is a message authentication function and $f_5^{\ast }()$ is a key generating function.

Upon receiving the “MAC failure” indication or the “Synchronization failure” indication, the UDM/ARPF creates a new 5G home environment authentication vector and runs a new authentication procedure with the UE, i.e., go to step 5 to continue the 5G AKA protocol. Under normal communication conditions, these failures do not often occur [2,3,4]. However, they can often be used by the penetrator to perform many attacks on the 5G AKA protocol (see Section 3). In [14,15,18,24], the authors also exploited the usage of the different types of failures, MAC-based or synchronization-based, to track a specific subscriber, and then given the corresponding revised schemes.

3. Formal Verification and Analysis of the 5G AKA Protocol

To simplify the formal verification and analysis, we assume that:

• The parties of the 5G AKA protocol shown in Figure 1 are simplified as the UE, the SN and the HN. The USIM and the ME are located in the UE, and the SEAF is located in the SN. The AUSF, the UDM, the ARPE and the SIDF are located in the HN.
• There is a session key between the SN and the HN, and it is secure.
• $ngKSI$ and $ABBA$ do not affect the security of the 5G AKA protocol, so they are ignored here.

According to these assumptions, the 5G AKA protocol shown in Figure 1 can be summarized into three cases as follows:

Case (I): the verification of $AUTN$ succeeds and the authentication is successful. The steps of this case are as follows:

• $UE\to SN$: $SUCI$;
• $SN\to HN$: ${\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$;
• $HN\to SN$: ${\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$;
• $SN\to UE$: $RAND\left|\right|AUTN$;
• $UE\to SN$: $RES*$;
• $SN\to HN$: ${\{RES*\}}_{K_{SN,HN}}$;
• $HN\to SN$: ${\left\{Result\right|\left|K_{SEAF}\right|\left|SUPI\right\}}_{K_{SN,HN}}$.

where $SUCI$, $RAND\left|\right|AUTN$ and $RES*$ are three messages exchanged between the UE and SN, ${\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, ${\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$, ${\{RES*\}}_{K_{SN,HN}}$ and ${\left\{Result\right|\left|K_{SEAF}\right|\left|SUPI\right\}}_{K_{SN,HN}}$ are four messages exchanged between the SN and the HN.

Case (II): the verification of $AUTN$ fails and it is a synchronization failure. The steps of this case are as follows:

• $UE\to SN$: $SUCI$;
• $SN\to HN$: ${\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$;
• $HN\to SN$: ${\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$;
• $SN\to UE$: $RAND\left|\right|AUTN$;
• $UE\to SN$: $Syncf\left|\right|AUTS$;
• $SN\to HN$: ${\left\{Syncf\right|\left|RAND\right|\left|AUTS\right\}}_{K_{SN,HN}}$.

where $SUCI$, $RAND\left|\right|AUTN$ and $Syncf\left|\right|AUTS$ are three messages exchanged between the UE and SN, ${\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, ${\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$ and ${\left\{Syncf\right|\left|RAND\right|\left|AUTS\right\}}_{K_{SN,HN}}$ are three messages exchanged between the SN and the HN.

Case (III): the verification of $AUTN$ fails and it is a MAC failure. The steps of this case are as follows:

• $UE\to SN$: $SUCI$;
• $SN\to HN$: ${\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$;
• $HN\to SN$: ${\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$;
• $SN\to UE$: $RAND\left|\right|AUTN$;
• $UE\to SN$: $MACf$;
• $SN\to HN$: ${\left\{MACf\right\}}_{K_{SN,HN}}$.

where $SUCI$, $RAND\left|\right|AUTN$ and $MACf$ are three messages exchanged between the UE and SN, ${\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, ${\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$ and ${\left\{MACf\right\}}_{K_{SN,HN}}$ are three messages exchanged between the SN and the HN.

In the above cases, $K_{SN,HN}$ denotes the session key between the SN and the HN, $Syncf$ denotes the “Synchronization failure” indication and $MACf$ denotes the “MAC failure” indication.

The strand space model [28,29,30] is a well-studied formal analysis method for security protocols. In [28], Fábrega et al. studied the case of mixed protocols, where principals use secret material in more than one protocol. In such cases, the two protocols can potentially interact, forming vulnerabilities not present in either protocol alone. To find these vulnerabilities, they proposed a mixed strand space model for such cases.

As mentioned above, there are three cases in the 5G AKA protocol, so there may be interactions between these cases, forming vulnerabilities that do not exist in any single case. In order to find these vulnerabilities, we use the mixed strand space model [28] to analyze the security of the 5G AKA protocol as follows.

3.1. Mixed Strand Space for the 5G AKA Protocol

Definition 1.

A regular strand space${\sum }_{\mathrm{I}}$is a space for case I of the 5G AKA protocol if${\sum }_{\mathrm{I}}$is the union of three kinds of strands: (1) Initiator strands$s\in {\mathrm{Init}}_{\mathrm{I}}[UE$,$SN$,$HN$,$SUCI$,$RAND$,$AUTN$,$RES*]$with trace:$<+SUCI$,$-RAND\left|\right|AUTN$,$+RES*>$. The principal associated with this strand is$UE$.$XMAC$computed locally is equal to$MAC\subset AUTN$and$SQN\subset AUTN$is in the correct range (i.e.,$SQ{N}_{UE}<SQN$); (2) Responder strands$r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$,$SN$,$HN$,$SUCI$,$SNN$,$RAND$,$H_1$,$H_2$,$H_3$,$Result$,$K_{SEAF}$,$SUPI]$with trace:$<-SUCI$,$+{\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$,$-{\left\{RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}$,$+RAND\left|\right|H_1$,$-H_3$,$+{\left\{H_3\right\}}_{K_{SN,HN}}$,$-\left\{Result\right||K_{SEAF}$$\left|\right|SUPI{\}}_{K_{SN,HN}}>$. The principal associated with this strand is$SN$. $H_1$,$H_2$and$H_3$are three messages that are not inspected by$SN$, where$H_2=SHA256(RAND||H_3)$; (3) Server strands$t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$,$SN$,$HN$,$SUCI$,$SNN$,$RAND$,$AUTN$,$HXRES*$,$RES*$,$Result$,$K_{SEAF}$,$SUPI]$with trace:$<-{\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$,$+{\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$,$-{\{RES*\}}_{K_{SN,HN}}$,$+{\left\{Result\right|\left|K_{SEAF}\right|\left|SUPI\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is$HN$.

Definition 2.

A regular strand space${\sum }_{\mathrm{II}}$is a space for case II of the 5G AKA protocol if${\sum }_{\mathrm{II}}$is the union of three kinds of strands: (1) Initiator strands$s\in {\mathrm{Init}}_{\mathrm{II}}[UE$,$SN$,$HN$,$SUCI$,$RAND$,$AUTN$,$Syncf$,$AUTS]$with trace:$<+SUCI$,$-RAND\left|\right|AUTN$,$+Syncf\left|\right|AUTS>$. The principal associated with this strand is$UE$.$XMAC$computed locally is equal to$MAC\subset AUTN$, but$SQN\subset AUTN$is not in the correct range (i.e.,$SQ{N}_{UE}\ge SQN$); (2) Responder strands$r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$,$SN$,$HN$,$SUCI$,$SNN$,$RAND$,$H_1$,$H_2$,$Syncf$,$H_4]$with trace:$<-SUCI$,$+{\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$,$-{\left\{RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}$,$+RAND\left|\right|H_1$,$-Syncf\left|\right|H_4$,$+{\left\{Syncf\right|\left|RAND\right|\left|H_4\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is$SN$.$H_1$,$H_2$and$H_4$are three messages that are not inspected by$SN$; (3) Server strands$t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$,$SN$,$HN$,$SUCI$,$SNN$,$RAND$,$AUTN$,$HXRES*$,$Syncf$,$AUTS]$with trace:$<-{\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$,$+{\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$,$-{\left\{Syncf\right|\left|RAND\right|\left|AUTS\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is$HN$.

Definition 3.

A regular strand space${\sum }_{\mathrm{III}}$is a space for case III of the 5G AKA protocol if${\sum }_{\mathrm{III}}$is the union of three kinds of strands: (1) Initiator strands$s\in {\mathrm{Init}}_{\mathrm{III}}[UE$,$SN$,$HN$,$SUCI$,$RAND$,$AUTN$,$MACf]$with trace:$<+SUCI$,$-RAND\left|\right|AUTN$,$+MACf>$. The principal associated with this strand is$UE$.$XMAC$computed locally is not equal to$MAC\subset AUTN$. (2) Responder strands$r\in {\mathrm{Resp}}_{\mathrm{III}}[UE$,$SN$,$HN$,$SUCI$,$SNN$,$RAND$,$H_1$,$H_2$,$MACf]$with trace:$<-SUCI$,$+{\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$,$-{\left\{RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}$,$+RAND\left|\right|H_1$,$-MACf$,$+{\left\{MACf\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is$SN$.$H_1$and$H_2$are two messages that are not inspected by$SN$. (3) Server strands$t\in {\mathrm{Serv}}_{\mathrm{III}}[UE$,$SN$,$HN$,$SUCI$,$SNN$,$RAND$,$AUTN$,$HXRES*$,$MACf]$with trace:$<-{\left\{SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$,$+{\left\{RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$,$-{\left\{MACf\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is$HN$.

Definition 4.

An infiltrated mixed strand space$\sum ,\mathcal{P}$is a space for the 5G AKA protocol if$\sum ={\sum }_{\mathrm{I}}\cup {\sum }_{\mathrm{II}}\cup {\sum }_{\mathrm{III}}\cup \mathcal{P}$, where penetrator strands$p\in \mathcal{P}$[28,29,30].

Definition 1 gives a regular strand space for case I of the 5G AKA protocol (i.e., ${\sum }_{\mathrm{I}}$), including initiator strands, responder strands and server strands for case I of the 5G AKA protocol. Definition 2 gives a regular strand space for case II of the 5G AKA protocol (i.e., ${\sum }_{\mathrm{II}}$), including initiator strands, responder strands and server strands for case II of the 5G AKA protocol. Definition 3 gives a regular strand space for case III of the 5G AKA protocol (i.e., ${\sum }_{\mathrm{III}}$), including initiator strands, responder strands and server strands for case III of the 5G AKA protocol. Definition 4 gives an infiltrated mixed strand space for the 5G AKA protocol, including ${\sum }_{\mathrm{I}}$, ${\sum }_{\mathrm{II}}$, ${\sum }_{\mathrm{III}}$ and penetrator strands (i.e., $\mathcal{P}$).

3.2. The Initiator’s Guarantee of the 5G AKA Protocol

Theorem 1.

Suppose: (1)$\sum$is a space for the 5G AKA protocol, and$\mathcal{C}$is a bundle containing an initiator strand$s\in {\mathrm{Init}}_{\mathrm{I}}[UE$,$SN$,$HN$,$SUCI$,$RAND$,$AUTN$,$RES*]$; (2)$K\notin {\mathcal{K}}_P$and$K_{SN*,HN}\notin {\mathcal{K}}_P$, where$SN*$denotes any authorized SN; (3)$RAND$is uniquely originating in$\sum$. Then,$\mathcal{C}$contains a unique server strand$t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$,$S{N}^{\prime }$,$HN$,$SUC{I}^{\prime }$,$SN{N}^{\prime }$,$RAND$,$AUTN$,$(HXRES*{)}^{\prime }$,$(RES*{)}^{\prime }$,$Result$,${K^{\prime }}_{SEAF}$,$SUPI]$and a responder strand$r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$,$S{N}^{\prime }$,$HN$,$SUC{I}^{″}$,$SN{N}^{\prime }$,$RAND$,$AUTN$,$(HXRES*{)}^{\prime }$,$(RES*{)}^{\prime }$,$Result$,${K^{″}}_{SEAF}$,$SUP{I}^{″}]$, where$x^{\prime }\subset SUC{I}^{\prime }$,$SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$,$SN{N}^{\prime }\subset (RES*{)}^{\prime }$,$SN{N}^{\prime }\subset {K^{\prime }}_{SEAF}$,$SUP{I}^{″}\subset SUC{I}^{″}$and${K^{″}}_{SEAF}$is generated for$SUP{I}^{″}$. Alternatively,$\mathcal{C}$contains a unique server strand$t\in {\mathrm{Serv}}_{\mathrm{III}}[UE$,$S{N}^{\prime }$,$HN$,$SUC{I}^{\prime }$,$SN{N}^{\prime }$,$RAND$,$AUTN$,$(HXRES*{)}^{\prime }$,$MACf]$and a responder strand$r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$,$S{N}^{\prime }$,$HN$,$SUC{I}^{″}$,$SN{N}^{\prime }$,$RAND$,$AUTN$,$(HXRES*{)}^{\prime }$,$(RES*{)}^{\prime }$,$Result$,${K^{″}}_{SEAF}$,$SUP{I}^{″}]$,$r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$,$S{N}^{\prime }$,$HN$,$SUC{I}^{″}$,$SN{N}^{\prime }$,$RAND$,$AUTN$,$(HXRES*{)}^{\prime }$,$Syncf$,${H^{″}}_4]$or$r\in {\mathrm{Resp}}_{\mathrm{III}}[U{E}^{″}$,$S{N}^{\prime }$,$HN$,$SUC{I}^{″}$,$SN{N}^{\prime }$,$RAND$,$AUTN$,$(HXRES*{)}^{\prime }$,$MACf]$, where$x^{\prime }\subset SUC{I}^{\prime }$,$SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$,$SN{N}^{\prime }\subset (RES*{)}^{\prime }$,$SUP{I}^{″}\subset SUC{I}^{″}$and${K^{″}}_{SEAF}$is generated for$SUP{I}^{″}$.

Proof of Theorem 1.

By assumptions (2) and (3), $K\notin {\mathcal{K}}_P$ and $RAND$ are uniquely originating in $\sum$, so $MAC=f_1(K,SQN|\left|RAND\right||AMF)\subset AUTN\subset term(<s,2>)$ must uniquely originate on a server strand $t$ according to Definitions 1 to 4.

(1)

If $t$ is a server strand of Definition 1, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUPI]$, where $x^{\prime }\subset SUC{I}^{\prime }$, $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$, $SN{N}^{\prime }\subset (RES*{)}^{\prime }$ and $SN{N}^{\prime }\subset {K^{\prime }}_{SEAF}$. By assumption (2), $K_{S{N}^{\prime },HN}\notin {\mathcal{K}}_P$, so ${\{(RES*{)}^{\prime }\}}_{K_{S{N}^{\prime },HN}}=term(<t,3>)$ must originate on a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, ${H^{″}}_1$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, where $SUP{I}^{″}\subset SUC{I}^{″}$ and ${K^{″}}_{SEAF}$ is generated for $SUP{I}^{″}$. Since $K_{S{N}^{\prime },HN}\notin {\mathcal{K}}_P$, ${\left\{RAND\right|\left|{H^{″}}_1\right||(HXRES*{)}^{\prime }\}}_{K_{S{N}^{\prime },HN}}$ $=term(<r,3>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so ${H^{″}}_1=AUTN$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$.

(2)

If $t$ is a server strand of Definition 2, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $x^{\prime }\subset SUC{I}^{\prime }$, $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$ and $SQ{N^{\prime }}_{UE}\subset AUT{S}^{\prime }$. By assumption (2), $K\notin {\mathcal{K}}_P$, so $(MAC-S{)}^{\prime }=f_1(K,SQ{N^{\prime }}_{UE}\left|\right|RAND\left|\right|AM{F}_0)\subset AUT{S}^{\prime }\subset term(<t,3>)$ must originate on an initiator strand $s^{\prime }\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $S{N}^{″}$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{″}$, $Syncf$, $AUT{S}^{\prime }]$, where $AUT{N}^{″}=SQ{N}^{″}\oplus AK\left|\right|AMF\left|\right|MA{C}^{″}$ and $MA{C}^{″}=f_1(K,SQ{N}^{″}$$\left|\right|RAND\left|\right|AMF)$. Since $K\notin {\mathcal{K}}_P$, $MA{C}^{″}\subset AUT{N}^{″}\subset term(<s^{\prime },2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUTN$. By assumption (1) and Definition 1, $SQ{N}_{UE}<SQN$ on $s$. However, $SQ{N}_{UE}\ge SQN$ on $s^{\prime }$ according to Definition 2. Therefore, $s$ and $s^{\prime }$ cannot be in the same run of the protocol, so $s^{\prime }$ must exist in the past run of the protocol. However, it is impossible from $SQ{N}_{UE}\ge SQN$ to $SQ{N}_{UE}<SQN$ because $SQ{N}_{UE}$ increases. That is to say, it is impossible that $s^{\prime }$ exists in the past run of the protocol and $s$ exists in the current run of the protocol. Hence, $t$ is not a server strand of Definition 2.

(3)

If $t$ is a server strand of Definition 3, then $t\in {\mathrm{Serv}}_{\mathrm{III}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $MACf]$, where $x^{\prime }\subset SUC{I}^{\prime }$ and $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $RAND$ originates at $n_0=<t,2>$, where $v_0=term(<t,2>)={\left\{RAND\right|\left|AUTN\right||(HXRES*{)}^{\prime }\}}_{K_{S{N}^{\prime },HN}}$. Let $S=\{n\in \mathcal{C}:RAND\subset term(n)\wedge v_0\not\subset term(n\left)\right\}$. Since $term(<s,2>)=RAND\left|\right|AUTN\in \mathcal{C}$, $S$ is non-empty. Hence, $S$ has at least one ≤-minimal element $n_2$ and the sign of $n_2$ is positive. $n_2$ does not lie on a penetrator strand but must lie on a regular strand instead (Lemma 5.4 in [29]). By inspection, $n_1$ precedes $n_2$ on the regular strand and $term(n_1)=v_0$, and the regular strand containing $n_1$ and $n_2$ is a responder strand $r$. If $r$ is a responder strand of Definition 1, then $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, where $SN{N}^{\prime }\subset (RES*{)}^{\prime }$, $SUP{I}^{″}\subset SUC{I}^{″}$ and ${K^{″}}_{SEAF}$ is generated for $SUP{I}^{″}$. If $r$ is a responder strand of Definition 2, then $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, ${H^{″}}_4]$. If $r$ is a responder strand of Definition 3, then $r\in {\mathrm{Resp}}_{\mathrm{III}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $MACf]$. □

According to Theorem 1, the corresponding attack scenarios can be obtained as shown in Figure 2, Figure 3, Figure 4 and Figure 5, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 2, Figure 3, Figure 4 and Figure 5, the green dashed box represents the initiator strand of Theorem 1, while the blue dashed boxes represent the server strands and the responder strands of Theorem 1. The fields marked in red on the server strand and the responder strand are some fields that cannot be agreed with the UE, which are caused by MitM attacks.

According to Figure 2, Figure 3, Figure 4 and Figure 5, some specific attacks can be found as follows.

(1)

$UE$ cannot find that $SUC{I}^{\prime }$ and $SUC{I}^{″}$ are replayed because $AUTN$ does not contain the challenge of the UE (i.e., $x$), which is included in $SUCI$. That is to say, the replay attacks on the SN and the HN can be formed, resulting in the energy consumption ion of the SN and the HN.

(2)

$UE$ successfully authenticates $HN$, but does not authenticate $SN$ because $AUTN$ does not contain $SNN$, which makes that $SN{N}^{\prime }$ is included in $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$ and ${K^{\prime }}_{SEAF}$, and the principal associated with the responder strand is $S{N}^{\prime }$. In [14], the authors also pointed out this security issue. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(3)

Both ${K^{\prime }}_{SEAF}$ and ${K^{″}}_{SEAF}$ cannot be agreed with the UE because $SN{N}^{\prime }$ is included in them. That is to say, the key agreement fails, resulting in a new authentication and key agreement process.

(4)

In Figure 3, Figure 4 and Figure 5, there are interactions between different cases of the 5G AKA protocol, named cross attacks. They are caused by the penetrator taking advantage of $Syncf$ and $MACf$. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(5)

In Figure 3 and Figure 4, the penetrator replays an encrypted $MACf$ between the SN and the HN to make authentication failure. In Figure 5, the penetrator directly sends $MACf$ to the SN to make authentication failure. They are called MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(6)

The server strand and the responder strand of Theorem 1 may exist in the past run of the protocol because they do not contain the challenge of the UE (i.e., $x$), which is included in $SUCI$. That is to say, $RAND\left|\right|AUTN$ on the UE may be a replayed message and $SQN\subset AUTN$ is still in the correct range. As a result, the location privacy of the UE can be compromised by reidentifying $RES*$. That is to say, the location privacy of the UE can be compromised.

Theorem 2.

Suppose: (1) $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing an initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $Syncf$, $AUTS]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN*,HN}\notin {\mathcal{K}}_P$, where $SN*$ denotes any authorized SN; (3) $RAND$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUPI]$ and a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{‴}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{‴}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{‴}}_{SEAF}$, $SUP{I}^{‴}]$, and both $t$ and $r$ must exist in the past run of the protocol, where $x^{\prime }\subset SUC{I}^{\prime }$, $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$, $SN{N}^{\prime }\subset (RES*{)}^{\prime }$, $SN{N}^{\prime }\subset {K^{\prime }}_{SEAF}$, $SUP{I}^{‴}\subset SUC{I}^{‴}$ and ${K^{‴}}_{SEAF}$ is generated for $SUP{I}^{‴}$. Alternatively, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$ and a responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $x^{\prime }\subset SUC{I}^{\prime }$, $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$, $SQ{N^{\prime }}_{UE}\subset AUT{S}^{\prime }$ and $SUP{I}^{″}\subset SUC{I}^{″}$. Alternatively, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{III}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $MACf]$ and a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, ${H^{″}}_4]$ or $r\in {\mathrm{Resp}}_{\mathrm{III}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $MACf]$, where $x^{\prime }\subset SUC{I}^{\prime }$, $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$, $SN{N}^{\prime }\subset (RES*{)}^{\prime }$, $SUP{I}^{″}\subset SUC{I}^{″}$ and ${K^{″}}_{SEAF}$ is generated for $SUP{I}^{″}$, and both $t$ and $r$ must exist in the past run of the protocol when $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$.

Proof of Theorem 2.

By assumptions (2) and (3), $K\notin {\mathcal{K}}_P$ and $RAND$ are uniquely originating in $\sum$, so $MAC=f_1(K,SQN|\left|RAND\right||AMF)\subset AUTN\subset term(<s,2>)$ must uniquely originate on a server strand $t$ according to Definitions 1 to 4.

(1)

If $t$ is a server strand of Definition 1, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUPI]$, where $x^{\prime }\subset SUC{I}^{\prime }$, $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$, $SN{N}^{\prime }\subset (RES*{)}^{\prime }$ and $SN{N}^{\prime }\subset {K^{\prime }}_{SEAF}$. By assumption (2), $K\notin {\mathcal{K}}_P$. Since $CK=f_3(K,RAND)$ and $IK=f_4(K,RAND)$, $CK\notin {\mathcal{K}}_P$ and $IK\notin {\mathcal{K}}_P$, so $CK\left|\right|IK\notin {\mathcal{K}}_P$. Hence, $(RES*{)}^{\prime }=KDF(CK\left|\right|IK,SN{N}^{\prime }\left|\right|RAND\left|\right|RES)$ $\subset term(<t,3>)$ must originate on an initiator strand $s^{\prime }\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{″}$, $(RES*{)}^{\prime }]$, where $AUT{N}^{″}=SQ{N}^{″}\oplus AK\left|\right|AMF\left|\right|MA{C}^{″}$ and $MA{C}^{″}=f_1(K,SQ{N}^{″}|\left|RAND\right||AMF)$. Since $K\notin {\mathcal{K}}_P$, $MA{C}^{″}\subset AUT{N}^{″}$ $\subset term(<s^{\prime },2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUTN$. By assumption (1) and Definition 2, $SQ{N}_{UE}\ge SQN$ on $s$. However, $SQ{N}_{UE}<SQN$ on $s^{\prime }$ according to Definition 1. Therefore, $s$ and $s^{\prime }$ cannot be in the same run of the protocol, so $s^{\prime }$ must exist in the past run of the protocol. Because $SQ{N}_{UE}$ increases, it is possible from $SQ{N}_{UE}<SQN$ to $SQ{N}_{UE}\ge SQN$. That is to say, it is possible that $s^{\prime }$ exists in the past run of the protocol and $s$ exists in the current run of the protocol. Hence, it is possible that $t$ is a server strand of Definition 1. By assumption (2), $K_{S{N}^{\prime },HN}\notin {\mathcal{K}}_P$, so ${\{(RES*{)}^{\prime }\}}_{K_{S{N}^{\prime },HN}}=term(<t,3>)$ must originate on a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{‴}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{‴}$, $SN{N}^{\prime }$, $RAND$, ${H^{‴}}_1$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{‴}}_{SEAF}$, $SUP{I}^{‴}]$, where $SUP{I}^{‴}\subset SUC{I}^{‴}$ and ${K^{‴}}_{SEAF}$ is generated for $SUP{I}^{‴}$. Since $K_{S{N}^{\prime },HN}\notin {\mathcal{K}}_P$, ${\left\{RAND\right|\left|{H^{‴}}_1\right||(HXRES*{)}^{\prime }\}}_{K_{S{N}^{\prime },HN}}$ $=term(<r,3>)$ must originate on a server strand $t^{″}$. Since $RAND$ is uniquely originating in $\sum$, $t^{″}=t$, so ${H^{‴}}_1=AUTN$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{‴}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{‴}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{‴}}_{SEAF}$, $SUP{I}^{‴}]$. From the above, $s^{\prime }$ exists in the past run of the protocol and $MAC\subset AUTN\subset term(<s^{\prime },2>)$ originates on $t$, so $t$ must exist in past run of the protocol. From the above, ${\{(RES*{)}^{\prime }\}}_{K_{S{N}^{\prime },HN}}=term(<t,3>)$ originates on $r$, so $r$ also must exist in the past run of the protocol.

(2)

If $t$ is a server strand of Definition 2, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $x^{\prime }\subset SUC{I}^{\prime }$, $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$ and $SQ{N^{\prime }}_{UE}\subset AUT{S}^{\prime }$. By assumption (2), $K_{S{N}^{\prime },HN}\notin {\mathcal{K}}_P$, so ${\left\{Syncf\right|\left|RAND\right|\left|AUT{S}^{\prime }\right\}}_{K_{S{N}^{\prime },HN}}=term(<t,3>)$ must originate on a responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, ${H^{″}}_1$, ${H^{″}}_2$, $Syncf$, $AUT{S}^{\prime }]$, where $SUP{I}^{″}\subset SUC{I}^{″}$. Since $K_{S{N}^{\prime },HN}\notin {\mathcal{K}}_P$, ${\left\{RAND\right|\left|{H^{″}}_1\right|\left|{H^{″}}_2\right\}}_{K_{S{N}^{\prime },HN}}=term(<r,3>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so ${H^{″}}_1=AUTN$ and ${H^{″}}_2=(HXRES*{)}^{\prime }$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$.

(3)

If $t$ is a server strand of Definition 3, then $t\in {\mathrm{Serv}}_{\mathrm{III}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $MACf]$, where $x^{\prime }\subset SUC{I}^{\prime }$ and $SN{N}^{\prime }\subset (HXRES*{)}^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $RAND$ originates at $n_0=<t,2>$, where $v_0=term(<t,2>)={\left\{RAND\right|\left|AUTN\right||(HXRES*{)}^{\prime }\}}_{K_{S{N}^{\prime },HN}}$. Let $S=\{n\in \mathcal{C}:RAND\subset term(n)\wedge v_0\not\subset term(n\left)\right\}$. Since $term(<s,2>)=RAND\left|\right|AUTN\in \mathcal{C}$, $S$ is non-empty. Hence, $S$ has at least one ≤-minimal element $n_2$ and the sign of $n_2$ is positive. $n_2$ does not lie on a penetrator strand but must lie on a regular strand instead (Lemma 5.4 in [29]). By inspection, $n_1$ precedes $n_2$ on the regular strand and $term(n_1)=v_0$, and the regular strand containing $n_1$ and $n_2$ is a responder strand $r$. If $r$ is a responder strand of Definition 1, then $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, where $SN{N}^{\prime }\subset (RES*{)}^{\prime }$, $SUP{I}^{″}\subset SUC{I}^{″}$ and ${K^{″}}_{SEAF}$ is generated for $SUP{I}^{″}$. From the above, it is possible that $r$ is a responder strand of Definition 1 because it is possible from $SQ{N}_{UE}<SQN$ to $SQ{N}_{UE}\ge SQN$, and both $r$ and $t$ must exist in the past run of the protocol. If $r$ is a responder strand of Definition 2, then $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $Syncf$, ${H^{″}}_4]$. If $r$ is a responder strand of Definition 3, then $r\in {\mathrm{Resp}}_{\mathrm{III}}[U{E}^{″}$, $S{N}^{\prime }$, $HN$, $SUC{I}^{″}$, $SN{N}^{\prime }$, $RAND$, $AUTN$, $(HXRES*{)}^{\prime }$, $MACf]$. □

According to Theorem 2, the corresponding attack scenarios can be obtained as shown in Figure 6, Figure 7, Figure 8, Figure 9 and Figure 10, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 6, Figure 7, Figure 8, Figure 9 and Figure 10, the green dashed box represents the initiator strand of Theorem 2, while the blue dashed boxes represent the server strand and the responder strand of Theorem 2. The fields marked in red on the server strand and the responder strand are some fields that cannot be agreed with the UE, which are caused by MitM attacks.

According to Figure 6, Figure 7, Figure 8, Figure 9 and Figure 10, some specific attacks can be found as follows:

(1)

$UE$ cannot find that $SUC{I}^{\prime }$ and $SUC{I}^{″}$ are replayed because $AUTN$ does not contain the challenge of the UE (i.e., $x$), which is included in $SUCI$. That is to say, the replay attacks on the SN and the HN can be formed, resulting in the energy consumption ion of the SN and the HN.

(2)

$UE$ successfully authenticates $HN$, but does not authenticate $SN$ because $AUTN$ does not contain $SNN$, which means that $SN{N}^{\prime }$ is included in $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$ and ${K^{\prime }}_{SEAF}$, and the principal associated with the responder strand is $S{N}^{\prime }$. In [14], the authors also pointed out this security issue. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(3)

In Figure 6, Figure 8, Figure 9 and Figure 10, there are interactions between different cases of the 5G AKA protocol, i.e., cross attacks. They are caused by the penetrators taking advantage of $Syncf$ and $MACf$. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(4)

In Figure 8 and Figure 9, the penetrator replays an encrypted $MACf$ between the SN and the HN to make authentication failure. In Figure 10, the penetrator directly sends $MACf$ to the SN to make authentication failure. They are called MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(5)

The server strand and the responder strand of Theorem 2 in Figure 6 and Figure 8 only exist in the past run of the protocol according to Theorem 2, i.e., $RAND\left|\right|AUTN$ on the initiator strand of Theorem 2 in Figure 6 and Figure 8 is a replayed message and $SQN\subset AUTN$ is not in the correct range. As a result, the location privacy of the UE can be compromised by identifying $Syncf$. Further, the server strand and the responder strand of Theorem 2 in Figure 7, Figure 9 and Figure 10 may exist in the past run of the protocol because they do not contain the challenge of the UE (i.e., $x$), which is included in $SUCI$. That is to say, $RAND\left|\right|AUTN$ on the UE in Figure 7, Figure 9 and Figure 10 can be a replayed message and $SQN\subset AUTN$ is not in the correct range. As a result, the location privacy of the UE can be compromised by identifying $Syncf$. In [14,15,18,24], the authors also exploited this attack. That is to say, the location privacy of the UE can be compromised.

Theorem 3.

Suppose: $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing an initiator strand $s\in {\mathrm{Init}}_{\mathrm{III}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $MACf]$. Then, the penetrator can complete the entire message exchange without any responder strand or server strand.

Proof of Theorem 3.

By the above assumption and Definition 3, $XMAC$ computed locally is not equal to $MAC\subset AUTN\subset term(<s,2>)$, so $MAC$ does not originate on any responder strand and server strand. □

According to Theorem 3, the corresponding attack scenario can be obtained as shown in Figure 11.

In Figure 11, the green dashed box represents the initiator strand of Theorem 3. According to Figure 11, $UE$ does not authenticate $SN$ and $HN$. The penetrator $P$ can perform a masquerading attack, where $RAND\left|\right|AUTN$ is forged or tampered by $P$. In the other words, the penetrator can forge or tamper with $RAND\left|\right|AUTN$ to make the UE respond to a “MAC failure” indication, resulting in authentication failure. This is also called MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

3.3. The Server’s Guarantee of the 5G AKA Protocol

Theorem 4.

Suppose: (1) $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing a server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN*,HN}\notin {\mathcal{K}}_P$, where $SN*$ denotes any authorized SN; (3) $RAND$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUC{I}^{\prime }$, $RAND$, $AUTN$, $RES*]$ and a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, where $x^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{″}\subset SUC{I}^{″}$ and ${K^{″}}_{SEAF}$ is generated for $SUP{I}^{″}$.

Proof of Theorem 4.

By assumption (2), $K\notin {\mathcal{K}}_P$. Since $CK=f_3(K,RAND)$ and $IK=f_4(K,RAND)$, $CK\notin {\mathcal{K}}_P$ and $IK\notin {\mathcal{K}}_P$, so $CK\left|\right|IK\notin {\mathcal{K}}_P$. Hence, $RES*=KDF(CK||IK,SNN|\left|RAND\right||RES)\subset term(<t,3>)$ must originate on an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUC{I}^{\prime }$, $RAND$, $AUT{N}^{\prime }$, $RES*]$, where $x^{\prime }\subset SUC{I}^{\prime }$ and $SQ{N}^{\prime }\subset AUT{N}^{\prime }$. Since $K\notin {\mathcal{K}}_P$, $MA{C}^{\prime }=f_1(K,SQ{N}^{\prime }|\left|RAND\right||AMF)$ $\subset AUT{N}^{\prime }\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{\prime }=SQN$ and $AUT{N}^{\prime }=AUTN$. Hence, $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUC{I}^{\prime }$, $RAND$, $AUTN$, $RES*]$. By assumption (2), $K_{SN,HN}\notin {\mathcal{K}}_P$, so ${\{RES*\}}_{K_{SN,HN}}=term(<t,3>)$ must originate on a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAND$, ${H^{″}}_1$, $HXRES*$, $RES*$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, where $SUP{I}^{″}\subset SUC{I}^{″}$ and ${K^{″}}_{SEAF}$ is generated for $SUP{I}^{″}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAND\right|\left|{H^{″}}_1\right||HXRES*\}}_{K_{SN,HN}}=term(<r,3>)$ must originate on a server strand $t^{″}$. Since $RAND$ is uniquely originating in $\sum$, $t^{″}=t$, so ${H^{″}}_1=AUTN$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$. □

According to Theorem 4, the corresponding attack scenario can be obtained as shown in Figure 12, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 12, the green dashed box represents the server strand of Theorem 4, while the blue dashed boxes represent the initiator strand and the responder strand of Theorem 4. The fields marked in red on the initiator strand and the responder strand are some fields that cannot be agreed with the HN, which are caused by MitM attacks.

According to Figure 12, $HN$ successfully authenticates $UE$ and $SN$, but some specific attacks can be found as follows:

(1)

$HN$ cannot find that $SUCI$ is replayed, which is not equal to $SUC{I}^{\prime }$ and $SUC{I}^{″}$. This is because $SUCI$ does not contain the challenge of the HN (i.e., $RAND$). That is to say, the replay attacks on the HN can be formed, resulting in the energy consumption ion of the HN.

(2)

${K^{″}}_{SEAF}$ and $SUP{I}^{″}$ cannot be agreed with the HN because the HN does not send ${K^{″}}_{SEAF}$ and $SUP{I}^{″}$ together with $RAND$, which makes that ${K^{″}}_{SEAF}$ and $SUP{I}^{″}$ can be a replayed key and a replayed SUPI, respectively. That is to say, the key agreement fails, resulting in a new authentication and key agreement process.

Theorem 5.

Suppose: (1) $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing a server strand $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN*,HN}\notin {\mathcal{K}}_P$, where $SN*$ denotes any authorized SN; (3) $RAND$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains an initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $RAND$, $AUTN$, $Syncf$, $AUTS]$ and a responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$, where $x^{\prime }\subset SUC{I}^{\prime }$ and $SUP{I}^{″}\subset SUC{I}^{″}$.

Proof of Theorem 5.

By assumption (2), $K\notin {\mathcal{K}}_P$, so $MAC-S=f_1^{\ast }(K,SQ{N}_{UE}||RAND$$\left|\right|AM{F}_0)\subset AUTS\subset term(<t,3>)$ must originate on an initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $RAND$, $AUT{N}^{\prime }$, $Syncf$, $AUTS]$, where $x^{\prime }\subset SUC{I}^{\prime }$ and $SQ{N}^{\prime }\subset AUT{N}^{\prime }$. Since $K\notin {\mathcal{K}}_P$, $MA{C}^{\prime }=f_1(K,SQ{N}^{\prime }|\left|RAND\right||AMF)\subset AUT{N}^{\prime }$ $\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{\prime }=SQN$ and $AUT{N}^{\prime }=AUTN$. Hence, $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $S{N}^{\prime }$, $HN$, $SUC{I}^{\prime }$, $RAND$, $AUTN$, $Syncf$, $AUTS]$. By assumption (2), $K_{SN,HN}\notin {\mathcal{K}}_P$, so $\left\{Syncf\right||RAND$$\left|\right|AUTS{\}}_{K_{SN,HN}}=term(<t,3>)$ must originate on a responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAND$, ${H^{″}}_1$, ${H^{″}}_2$, $Syncf$, $AUTS]$, where $SUP{I}^{″}\subset SUC{I}^{″}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAND\right|\left|{H^{″}}_1\right|\left|{H^{″}}_2\right\}}_{K_{SN,HN}}$ $=term(<r,3>)$ must originate on a server strand $t^{″}$. Since $RAND$ is uniquely originating in $\sum$, $t^{″}=t$, so ${H^{″}}_1=AUTN$ and ${H^{″}}_2=HXRES*$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$. □

According to Theorem 5, the corresponding attack scenario can be obtained as shown in Figure 13, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 13, the green dashed box represents the server strand of Theorem 5, while the blue dashed boxes represent the initiator strand and the responder strand of Theorem 5. The fields marked in red on the initiator strand and the responder strand are some fields that cannot be agreed with the HN, which are caused by MitM attacks.

According to Figure 13, $HN$ successfully authenticates $UE$ and $SN$. However, $HN$ cannot find that $SUCI$ is replayed, which is not equal to $SUC{I}^{\prime }$ and $SUC{I}^{″}$. This is because $SUCI$ does not contain the challenge of the HN (i.e., $RAND$). That is to say, the replay attacks on the HN can be formed, resulting in the energy consumption ion of the HN.

Theorem 6.

Suppose: (1) $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing a server strand $t\in {\mathrm{Serv}}_{\mathrm{III}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAND$, $AUTN$, $HXRES*$, $MACf]$; (2) $K_{SN*,HN}\notin {\mathcal{K}}_P$, where $SN*$ denotes any authorized SN. Then, $\mathcal{C}$ contains a responder strand $r\in {\mathrm{Resp}}_{\mathrm{III}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAN{D}^{\prime }$, ${H^{\prime }}_1$, ${H^{\prime }}_2$, $MACf]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$.

Proof of Theorem 6.

By assumption (2), $K_{SN,HN}\notin {\mathcal{K}}_P$, so ${\left\{MACf\right\}}_{K_{SN,HN}}=term(<s,3>)$ must originate on a responder strand $r\in {\mathrm{Resp}}_{\mathrm{III}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAN{D}^{\prime }$, ${H^{\prime }}_1$, ${H^{\prime }}_2$, $MACf]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$. □

According to Theorem 6, the corresponding attack scenario can be obtained as shown in Figure 14, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 14, the green dashed box represents the server strand of Theorem 6, while the blue dashed box represents the responder strand of Theorem 6. The fields marked in red on the responder strand are some fields that cannot be agreed with the HN, which are caused by MitM attacks.

According to Figure 14, $HN$ successfully authenticates $SN$, but only authenticates $UE$ based on $SUCI$, and some specific attacks can be found as follows.

(1)

$HN$ cannot find that $SUCI$ is replayed, which is not equal to $SUC{I}^{\prime }$. This is because $SUCI$ does not contain the challenge of the HN (i.e., $RAND$). That is to say, the replay attacks on the HN can be formed, resulting in the energy consumption ion of the HN.

(2)

The penetrator directly sends $MACf$ to the SN to make authentication failure. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(3)

The responder strand of Theorem 6 may exist in the past run of the protocol because it does not contain the challenge of the HN, i.e., ${\left\{MACf\right\}}_{K_{SN,HN}}$ on the HN of Theorem 6 can be a replayed message, resulting in a replay attack. In the other words, the penetrator replays an encrypted $MACf$ between the SN and the HN to make an authentication failure. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

3.4. The Responder’s Guarantee of the 5G AKA Protocol

Theorem 7.

Suppose: (1) $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAND$, $H_1$, $H_2$, $H_3$, $Result$, $K_{SEAF}$, $SUPI]$; (2) $K*\notin {\mathcal{K}}_P$ and $K_{SN*,HN}\notin {\mathcal{K}}_P$, where $SN*$ denotes any authorized SN and $K*$ denotes a pre-shared key between $HN$ and any authorized $UE$; (3) $RAND$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUP{I}^{\prime }]$ and an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{\prime }\subset SUC{I}^{″}$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset (RES*{)}^{\prime }$, $K^{\prime }\subset {K^{\prime }}_{SEAF}$ and ${K^{\prime }}_{SEAF}$ is generated for $SUP{I}^{\prime }$. Alternatively, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{III}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $MACf]$ and an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{\prime }\subset SUC{I}^{″}$, $K^{\prime }\subset AUT{N}^{\prime }$ and $K^{\prime }\subset (HXRES*{)}^{\prime }$.

Proof of Theorem 7.

By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAND$ are uniquely originating in $\sum$, so ${\left\{RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}=term(<r,3>)$ must uniquely originate on a server strand $t$ according to Definitions 1 to 4.

(1)

If $t$ is a server strand of Definition 1, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUP{I}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset (RES*{)}^{\prime }$, $K^{\prime }\subset {K^{\prime }}_{SEAF}$ and ${K^{\prime }}_{SEAF}$ is generated for $SUP{I}^{\prime }$. By assumption (2), $K^{\prime }\notin {\mathcal{K}}_P$. Since $C{K}^{\prime }=f_3(K^{\prime },RAND)$ and $I{K}^{\prime }=f_4(K^{\prime },RAND)$, $C{K}^{\prime }\notin {\mathcal{K}}_P$ and $I{K}^{\prime }\notin {\mathcal{K}}_P$, so $C{K}^{\prime }\left|\right|I{K}^{\prime }\notin {\mathcal{K}}_P$. Hence, $(RES*{)}^{\prime }=KDF(C{K}^{\prime }\left|\right|I{K}^{\prime },$ $SNN\left|\right|RAND\left|\right|RE{S}^{\prime })\subset term(<t,3>)$ must originate on an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{″}$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{″}$ and $SQ{N}^{″}\subset AUT{N}^{″}$. Since $K^{\prime }\notin {\mathcal{K}}_P$, $MA{C}^{″}=f_1(K^{\prime },SQ{N}^{″}$$\left|\right|RAND\left|\right|AMF)\subset AUT{N}^{″}\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUT{N}^{\prime }$. Hence, $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$.

(2)

If $t$ is a server strand of Definition 2, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset AUT{S}^{\prime }$ and $SQ{N}_{U{E}^{\prime }}\subset AUT{S}^{\prime }$. By Definition 1, $(RES*{)}^{\prime }=KDF(C{K}^{\prime }\left|\right|I{K}^{\prime },SNN\left|\right|RAND\left|\right|RE{S}^{\prime })=term(<r,5>)$. By assumption (2), $K^{\prime }\notin {\mathcal{K}}_P$. Since $C{K}^{\prime }=f_3(K^{\prime },RAND)$ and $I{K}^{\prime }=f_4(K^{\prime },RAND)$, $C{K}^{\prime }\notin {\mathcal{K}}_P$ and $I{K}^{\prime }\notin {\mathcal{K}}_P$, so $C{K}^{\prime }\left|\right|I{K}^{\prime }\notin {\mathcal{K}}_P$. Hence, $(RES*{)}^{\prime }=term(<r,5>)$ must originate on an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{″}$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{″}$ and $SQ{N}^{″}\subset AUT{N}^{″}$. Since $K^{\prime }\notin {\mathcal{K}}_P$, $MA{C}^{″}=f_1(K^{\prime },SQ{N}^{″}$$\left|\right|RAND\left|\right|AMF)\subset AUT{N}^{″}\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUT{N}^{\prime }$. Hence, $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$. By assumption (2), $K^{\prime }\notin {\mathcal{K}}_P$, so $(MAC-S{)}^{\prime }=f_1^{\ast }(K^{\prime },SQ{N}_{U{E}^{\prime }}\left|\right|RAND$$\left|\right|AM{F}_0)\subset AUTS\subset term(<t,3>)$ must originate on an initiator strand $s^{\prime }\in {\mathrm{Init}}_{\mathrm{II}}[U{E}^{\prime }$, $S{N}^{‴}$, $HN$, $SUC{I}^{‴}$, $RAND$, $AUT{N}^{‴}$, $Syncf$, $AUT{S}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{‴}$ and $SQ{N}^{‴}\subset AUT{N}^{‴}$. Since $K^{\prime }\notin {\mathcal{K}}_P$, $MA{C}^{‴}=f_1(K^{\prime },SQ{N}^{‴}|\left|RAND\right||AMF)\subset AUT{N}^{‴}$ $\subset term(<s^{\prime },2>)$ must originate on a server strand $t^{″}$. Since $RAND$ is uniquely originating in $\sum$, $t^{″}=t$, so $SQ{N}^{‴}=SQN$ and $AUT{N}^{‴}=AUT{N}^{\prime }$. Hence, $s^{\prime }\in {\mathrm{Init}}_{\mathrm{II}}[U{E}^{\prime }$, $S{N}^{‴}$, $HN$, $SUC{I}^{‴}$, $RAND$, $AUT{N}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$. By Definition 1, $SQ{N}_{U{E}^{\prime }}<SQN$ on $s$. However, $SQ{N}_{U{E}^{\prime }}\ge SQN$ on $s^{\prime }$ according to Definition 2. Therefore, $s$ and $s^{\prime }$ cannot be in the same run of the protocol, so $s$ or $s^{\prime }$ must exist in the past run of the protocol. Since $s$ or $s^{\prime }$ exists in the past run of the protocol, $t$ must exist in the past run of the protocol. Because $(MAC-S{)}^{\prime }\subset AUT{S}^{\prime }\subset term(<t,3>)$ originates on $s^{\prime }$, $s^{\prime }$ must exist in the past run of the protocol, so $s$ must exist in the current run of the protocol. However, it is impossible from $SQ{N}_{U{E}^{\prime }}\ge SQN$ to $SQ{N}_{U{E}^{\prime }}<SQN$ because $SQ{N}_{U{E}^{\prime }}$ increases. That is to say, it is impossible that $s^{\prime }$ exists in the past run of the protocol and $s$ exists in the current run of the protocol. Hence, $t$ is not a server strand of Definition 2.

(3)

If $t$ is a server strand of Definition 3, then $t\in {\mathrm{Serv}}_{\mathrm{III}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $MACf]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $K^{\prime }\subset AUT{N}^{\prime }$ and $K^{\prime }\subset (HXRES*{)}^{\prime }$. By Definition 1, $(RES*{)}^{\prime }=KDF(C{K}^{\prime }\left|\right|I{K}^{\prime },SNN\left|\right|RAND$$\left|\right|RE{S}^{\prime })=term(<r,5>)$. By assumption (2), $K^{\prime }\notin {\mathcal{K}}_P$. Since $C{K}^{\prime }=f_3(K^{\prime },RAND)$ and $I{K}^{\prime }=f_4(K^{\prime },RAND)$, $C{K}^{\prime }\notin {\mathcal{K}}_P$ and $I{K}^{\prime }\notin {\mathcal{K}}_P$, so $C{K}^{\prime }\left|\right|I{K}^{\prime }\notin {\mathcal{K}}_P$. Hence, $(RES*{)}^{\prime }=term(<r,5>)$ must originate on an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{″}$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{″}$ and $SQ{N}^{″}\subset AUT{N}^{″}$. Since $K^{\prime }\notin {\mathcal{K}}_P$, $MA{C}^{″}=f_1(K^{\prime },SQ{N}^{″}$$\left|\right|RAND\left|\right|AMF)\subset AUT{N}^{″}\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUT{N}^{\prime }$. Hence, $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$. □

According to Theorem 7, the corresponding attack scenarios can be obtained as shown in Figure 15 and Figure 16, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 15 and Figure 16, the green dashed box represents the responder strand of Theorem 7, while the blue dashed boxes represent the initiator strand and the server strand of Theorem 7. The fields marked in red on the initiator strand and the server strand are some fields that cannot be agreed with the SN, which are caused by MitM attacks.

According to Figure 15 and Figure 16, some specific attacks can be found as follows:

(1)

$SN$ successfully authenticates $HN$, but does not authenticate $UE$. This is because $SN$ cannot inspect $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$ and $(RES*{)}^{\prime }$, and $SUPI$ is not sent with $RAND$, which means that $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$ and $(RES*{)}^{\prime }$ can be related to $SUP{I}^{\prime }$ rather than $SUPI$. Accordingly, $SUP{I}^{\prime }$ is included in $SUC{I}^{\prime }$ and $SUC{I}^{″}$, and is related to ${K^{\prime }}_{SEAF}$. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(2)

In Figure 16, there are interactions between different cases of the 5G AKA protocol, i.e., cross attacks. They are caused by the penetrators taking advantage of $MACf$. The penetrator replays an encrypted $MACf$ between the SN and the HN to make authentication failure, i.e., MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(3)

The initiator strand and the server strand of Theorem 7 may exist in the past run of the protocol because they do not contain the challenge of the SN, i.e., the messages received by the SN can be replayed messages. As a result, the penetrator can impersonate the UE and the HN to complete the entire 5G AKA protocol with the SN, forming DoS attacks on the SN. This results in the energy consumption ion of the SN.

Theorem 8.

Suppose: (1) $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing a responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAND$, $H_1$, $H_2$, $Syncf$, $H_4]$; (2) $K*\notin {\mathcal{K}}_P$ and $K_{SN*,HN}\notin {\mathcal{K}}_P$, where $SN*$ denotes any authorized SN and $K*$ denotes a pre-shared key between $HN$ and any authorized $UE$; (3) $RAND$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUP{I}^{\prime }]$ and an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{\prime }\subset SUC{I}^{″}$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset (RES*{)}^{\prime }$, $K^{\prime }\subset {K^{\prime }}_{SEAF}$ and ${K^{\prime }}_{SEAF}$ is generated for $SUP{I}^{\prime }$. Alternatively, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{II}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$ and an initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[U{E}^{\prime }$, $S{N}^{″}$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{\prime }\subset SUC{I}^{″}$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset AUT{S}^{\prime }$ and $SQ{N}_{U{E}^{\prime }}\subset AUT{S}^{\prime }$. Alternatively, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{III}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $MACf]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $K^{\prime }\subset AUT{N}^{\prime }$ and $K^{\prime }\subset (HXRES*{)}^{\prime }$.

Proof of Theorem 8.

By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAND$ are uniquely originating in $\sum$, so ${\left\{RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}=term(<r,3>)$ must uniquely originate on a server strand $t$ according to Definitions 1 to 4.

(1)

If $t$ is a server strand of Definition 1, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUP{I}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset (RES*{)}^{\prime }$, $K^{\prime }\subset {K^{\prime }}_{SEAF}$ and ${K^{\prime }}_{SEAF}$ is generated for $SUP{I}^{\prime }$. By assumption (2), $K^{\prime }\notin {\mathcal{K}}_P$. Since $C{K}^{\prime }=f_3(K^{\prime },RAND)$ and $I{K}^{\prime }=f_4(K^{\prime },RAND)$, $C{K}^{\prime }\notin {\mathcal{K}}_P$ and $I{K}^{\prime }\notin {\mathcal{K}}_P$, so $C{K}^{\prime }\left|\right|I{K}^{\prime }\notin {\mathcal{K}}_P$. Hence, $(RES*{)}^{\prime }=KDF(C{K}^{\prime }\left|\right|I{K}^{\prime },$ $SNN\left|\right|RAND\left|\right|RE{S}^{\prime })\subset term(<t,3>)$ must originate on an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{″}$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{″}$ and $SQ{N}^{″}\subset AUT{N}^{″}$. Since $K^{\prime }\notin {\mathcal{K}}_P$, $MA{C}^{″}=f_1(K^{\prime },SQ{N}^{″}$$\left|\right|RAND\left|\right|AMF)\subset AUT{N}^{″}\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUT{N}^{\prime }$. Hence, $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$.

(2)

If $t$ is a server strand of Definition 2, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset AUT{S}^{\prime }$ and $SQ{N}_{U{E}^{\prime }}\subset AUT{S}^{\prime }$. By assumption (2), $K^{\prime }\notin {\mathcal{K}}_P$, so $(MAC-S{)}^{\prime }=f_1^{\ast }(K^{\prime },SQ{N}_{U{E}^{\prime }}\left|\right|RAND$$\left|\right|AM{F}_0)\subset AUTS\subset term(<t,3>)$ must originate on an initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[U{E}^{\prime }$, $S{N}^{″}$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{″}$, $Syncf$, $AUT{S}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{″}$ and $SQ{N}^{″}\subset AUT{N}^{″}$. Since $K^{\prime }\notin {\mathcal{K}}_P$, $MA{C}^{″}=f_1(K^{\prime },SQ{N}^{″}|\left|RAND\right||AMF)\subset AUT{N}^{″}$ $\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUT{N}^{\prime }$. Hence, $s\in {\mathrm{Init}}_{\mathrm{II}}[U{E}^{\prime }$, $S{N}^{″}$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$.

(3)

If $t$ is a server strand of Definition 3, then $t\in {\mathrm{Serv}}_{\mathrm{III}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $MACf]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $K^{\prime }\subset AUT{N}^{\prime }$ and $K^{\prime }\subset (HXRES*{)}^{\prime }$. □

According to Theorem 8, the corresponding attack scenarios can be obtained, as shown in Figure 17, Figure 18 and Figure 19, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 17, Figure 18 and Figure 19, the green dashed box represents the responder strand of Theorem 8, while the blue dashed boxes represent the initiator strand and the server strand of Theorem 8. The fields marked in red on the initiator strand and the server strand are some fields that cannot be agreed with the SN, which are caused by MitM attacks.

According to Figure 17, Figure 18 and Figure 19, some specific attacks can be found as follows.

(1)

$SN$ successfully authenticates $HN$, but does not authenticate $UE$. This is because $SN$ cannot inspect $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$ and $(RES*{)}^{\prime }$, which means that $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$ and $(RES*{)}^{\prime }$ can be related to $SUP{I}^{\prime }$ rather than $SUPI$. Accordingly, $SUP{I}^{\prime }$ is included in $SUC{I}^{\prime }$ and $SUC{I}^{″}$, and is related to ${K^{\prime }}_{SEAF}$. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(2)

In Figure 17 and Figure 19, there are interactions between different cases of the 5G AKA protocol, i.e., cross attacks. They are caused by the penetrators taking advantage of $Syncf$ and $MACf$. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(3)

In Figure 19, the penetrator replays an encrypted $MACf$ between the SN and the HN to make authentication failure, i.e., MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(4)

The initiator strand and the server strand of Theorem 8 may exist in the past run of the protocol, i.e., the messages received by the SN can be replayed messages. As a result, the penetrator can impersonate the UE and the HN to complete the entire 5G AKA protocol with the SN, forming DoS attacks on the SN. This results in the energy consumption ion of the SN.

Theorem 9.

Suppose: (1) $\sum$ is a space for the 5G AKA protocol, and $\mathcal{C}$ is a bundle containing a responder strand $r\in {\mathrm{Resp}}_{\mathrm{III}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAND$, $H_1$, $H_2$, $MACf]$; (2) $K*\notin {\mathcal{K}}_P$ and $K_{SN*,HN}\notin {\mathcal{K}}_P$, where $SN*$ denotes any authorized SN and $K*$ denotes a pre-shared key between $HN$ and any authorized $UE$; (3) $RAND$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUP{I}^{\prime }]$ and an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $(RES*{)}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{\prime }\subset SUC{I}^{″}$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset (RES*{)}^{\prime }$, $K^{\prime }\subset {K^{\prime }}_{SEAF}$ and ${K^{\prime }}_{SEAF}$ is generated for $SUP{I}^{\prime }$. Alternatively, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{II}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$ and an initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[U{E}^{\prime }$, $S{N}^{″}$, $HN$, $SUC{I}^{″}$, $RAND$, $AUT{N}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{\prime }\subset SUC{I}^{″}$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset AUT{S}^{\prime }$ and $SQ{N}_{U{E}^{\prime }}\subset AUT{S}^{\prime }$. Alternatively, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{III}}[U{E}^{\prime }$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $MACf]$, where $SUP{I}^{\prime }\subset SUC{I}^{\prime }$, $SUP{I}^{\prime }\subset SUC{I}^{″}$, $K^{\prime }\subset AUT{N}^{\prime }$, $K^{\prime }\subset (HXRES*{)}^{\prime }$, $K^{\prime }\subset AUT{S}^{\prime }$ and $SQ{N}_{U{E}^{\prime }}\subset AUT{S}^{\prime }$.

Proof of Theorem 9.

It is the same as Theorem 8. □

According to Theorem 9, the corresponding attack scenarios can be obtained as shown in Figure 20, Figure 21 and Figure 22, where the messages between the HN and the authorized SN are protected by their session key.

In Figure 20, Figure 21 and Figure 22, the green dashed box represents the responder strand of Theorem 9, while the blue dashed boxes represent the initiator strand and the server strand of Theorem 9. The fields marked in red on the initiator strand and the server strand are some fields that cannot be agreed with the SN, which are caused by MitM attacks.

According to Figure 20, Figure 21 and Figure 22, some specific attacks can be found as follows.

(1)

$SN$ successfully authenticates $HN$, but does not authenticate $UE$. This is because $SN$ cannot inspect $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$ and $(RES*{)}^{\prime }$, which makes that $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$ and $(RES*{)}^{\prime }$ can be related to $SUP{I}^{\prime }$ rather than $SUPI$. Accordingly, $SUP{I}^{\prime }$ is included in $SUC{I}^{\prime }$ and $SUC{I}^{″}$, and is related to ${K^{\prime }}_{SEAF}$. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(2)

In Figure 20 and Figure 21, there are interactions between different cases of the 5G AKA protocol, i.e., cross attacks. They are caused by the penetrators taking advantage of $Syncf$ and $MACf$. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(3)

In Figure 20, Figure 21 and Figure 22, the penetrator directly sends $MACf$ to the SN to make an authentication failure, i.e., MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process.

(4)

The initiator strand and the server strand of Theorem 9 may exist in the past run of the protocol, i.e., the messages received by the SN can be replayed messages. As a result, the penetrator can impersonate the UE and the HN to complete the entire 5G AKA protocol with the SN, thus forming DoS attacks on the SN. This results in the energy consumption ion of the SN.

4. Our Proposed 5G-AKA’ Protocol and Its Security Analysis

4.1. The 5G-AKA’ Protocol

In order to overcome the above security problems of the latest version of the 5G AKA protocol, we propose a 5G-AKA’ protocol, which is illustrated in Figure 23.

Compared with the latest version of the 5G AKA protocol, the main improvements of our proposed 5G-AKA’ protocol are as follows:

• To cryptographically bind $x\cdot y\cdot G$ and $SNN$ to $K$, and protect $K$, we replace $K$ with $BK$ on the UE and the HN.

  $$BK=KDF(K,x\cdot y\cdot G||SNN)$$

  (21)

  where $BK$ is a base key derived from $K$.
• To prevent DoS attacks on the SN, we add the challenge–response mechanism between the SN and the HN. In detail, we add $RAN{D}_{SN}$ to the first three messages between the SEAF (located in the SN) and the AUSF (located in the HN) and add $RAND$ to the fourth message between the SEAF and the AUSF, where $RAN{D}_{SN}$ is an unpredictable challenge of the SEAF;
• Add $SUPI$ to the second message between the SEAF and the AUSF, matching with $SUCI$ in the first message between them;
• In the latest version of the 5G AKA protocol, $MACf$ is used to initiate a new authentication procedure for the UE. However, it causes a large number of attacks according to the above security analysis. Hence, we use a timeout mechanism on the HN instead of $MACf$ to initiate a new authentication procedure towards the UE. That is to say, if $XMAC$ and $MAC$ are different, then the UE directly discards the receives $RAND\left|\right|AUTN$, and the HN will initiate a new authentication procedure towards the UE when the HN does not receive an authentication response message or a synchronization failure message within a certain period of time.

According to the above descriptions, our proposed 5G-AKA’ protocol can be summarized into two cases as follows:

Case (I): the verification of $AUTN$ succeeds and the authentication is successful. The steps of this case are as follows:

• $UE\to SN$: $SUCI$;
• $SN\to HN$: ${\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$;
• $HN\to SN$: ${\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$;
• $SN\to UE$: $RAND\left|\right|AUTN$;
• $UE\to SN$: $RES*$;
• $SN\to HN$: ${\left\{RAN{D}_{SN}\right||RES*\}}_{K_{SN,HN}}$;
• $HN\to SN$: ${\left\{RAND\right|\left|Result\right|\left|K_{SEAF}\right|\left|SUPI\right\}}_{K_{SN,HN}}$.

where $SUCI$, $RAND\left|\right|AUTN$ and $RES*$ are three messages exchanged between the UE and SN, ${\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, $\left\{RAN{D}_{SN}\right|\left|SUPI\right||RAND$$\left|\right|AUTN\left|\right|HXRES*{\}}_{K_{SN,HN}}$, ${\left\{RAN{D}_{SN}\right||RES*\}}_{K_{SN,HN}}$ and $\left\{RAND\right|\left|Result\right||K_{SEAF}$$\left|\right|SUPI{\}}_{K_{SN,HN}}$ are four messages exchanged between the SN and the HN.

Case (II): the verification of $AUTN$ fails and it is a synchronization failure. The steps of this case are as follows:

• $UE\to SN$: $SUCI$;
• $SN\to HN$: ${\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$;
• $HN\to SN$: ${\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$;
• $SN\to UE$: $RAND\left|\right|AUTN$;
• $UE\to SN$: $Syncf\left|\right|AUTS$;
• $SN\to HN$: ${\left\{RAN{D}_{SN}\right|\left|Syncf\right|\left|RAND\right|\left|AUTS\right\}}_{K_{SN,HN}}$.

where $SUCI$, $RAND\left|\right|AUTN$ and $Syncf\left|\right|AUTS$ are three messages exchanged between the UE and SN, ${\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, $\left\{RAN{D}_{SN}\right|\left|SUPI\right||RAND$$\left|\right|AUTN\left|\right|HXRES*{\}}_{K_{SN,HN}}$ and ${\left\{RAN{D}_{SN}\right|\left|Syncf\right|\left|RAND\right|\left|AUTS\right\}}_{K_{SN,HN}}$ are three messages exchanged between the SN and the HN.

In the above cases, $K$ is replaced with $BK$. Similarly, we use the mixed strand space model [28] to analyze the security of our proposed 5G-AKA’ protocol as follows.

4.2. Mixed Strand Space for the 5G-AKA’ Protocol

Definition 5.

A regular strand space ${\sum }_{\mathrm{I}}$ is a space for case I of the 5G-AKA’ protocol if ${\sum }_{\mathrm{I}}$ is the union of three kinds of strands: (1) Initiator strands $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $RES*]$ with trace: $<+SUCI$, $-RAND\left|\right|AUTN$, $+RES*>$. The principal associated with this strand is $UE$. $XMAC$ computed locally is equal to $MAC\subset AUTN$ and $SQN\subset AUTN$ is in the correct range (i.e., $SQ{N}_{UE}<SQN$); (2) Responder strands $r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $H_1$, $H_2$, $H_3$, $Result$, $K_{SEAF}$, $SUPI]$ with trace: $<-SUCI$, $+{\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, $-{\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}$, $+RAND\left|\right|H_1$, $-H_3$, $+{\left\{RAN{D}_{SN}\right|\left|H_3\right\}}_{K_{SN,HN}}$, $-{\left\{RAND\right|\left|Result\right|\left|K_{SEAF}\right|\left|SUPI\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is $SN$. $H_1$, $H_2$ and $H_3$ are three messages that are not inspected by $SN$, where $H_2=SHA256(RAND||H_3)$; (3) Server strands $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$ with trace: $<-{\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, $+{\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$, $-{\left\{RAN{D}_{SN}\right||RES*\}}_{K_{SN,HN}}$, $+{\left\{RAND\right|\left|Result\right|\left|K_{SEAF}\right|\left|SUPI\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is $HN$.

Definition 6.

A regular strand space ${\sum }_{\mathrm{II}}$ is a space for case II of the 5G-AKA’ protocol if ${\sum }_{\mathrm{II}}$ is the union of three kinds of strands: (1) Initiator strands $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $Syncf$, $AUTS]$ with trace: $<+SUCI$, $-RAND\left|\right|AUTN$, $+Syncf\left|\right|AUTS>$. The principal associated with this strand is $UE$. $XMAC$ computed locally is equal to $MAC\subset AUTN$, but $SQN\subset AUTN$ is not in the correct range (i.e., $SQ{N}_{UE}\ge SQN$); (2) Responder strands $r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $H_1$, $H_2$, $Syncf$, $H_4]$ with trace: $<-SUCI$, $+{\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, $-{\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}$, $+RAND\left|\right|H_1$, $-Syncf\left|\right|H_4$, $+{\left\{RAN{D}_{SN}\right|\left|Syncf\right|\left|RAND\right|\left|H_4\right\}}_{K_{SN,HN}}>$. The principal associated with this strand is $SN$. $H_1$, $H_2$ and $H_4$ are three messages that are not inspected by $SN$; (3) Server strands $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$ with trace: $<-{\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}$, $+{\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|AUTN\right||HXRES*\}}_{K_{SN,HN}}$, $-\left\{RAN{D}_{SN}\right|\left|Syncf\right||RAND$$\left|\right|AUTS{\}}_{K_{SN,HN}}>$. The principal associated with this strand is $HN$.

Definition 7.

An infiltrated strand space $\sum ,\mathcal{P}$ is a space for the 5G-AKA’ protocol if $\sum ={\sum }_{\mathrm{I}}\cup {\sum }_{\mathrm{II}}\cup \mathcal{P}$, where penetrator strands $p\in \mathcal{P}$ [28,29,30].

Definition 5 gives a regular strand space for case I of the 5G-AKA’ protocol (i.e., ${\sum }_{\mathrm{I}}$), including initiator strands, responder strands and server strands for case I of the 5G-AKA’ protocol. Definition 6 gives a regular strand space for case II of the 5G-AKA’ protocol (i.e., ${\sum }_{\mathrm{II}}$), including initiator strands, responder strands and server strands for case II of the 5G AKA protocol. Definition 7 gives an infiltrated mixed strand space for the 5G-AKA’ protocol, including ${\sum }_{\mathrm{I}}$, ${\sum }_{\mathrm{II}}$ and penetrator strands (i.e., $\mathcal{P}$).

4.3. The Initiator’s Guarantee of the 5G-AKA’ Protocol

Theorem 10.

Suppose: (1) $\sum$ is a space for the 5G-AKA’ protocol, and $\mathcal{C}$ is a bundle containing an initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $RES*]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN,HN}\notin {\mathcal{K}}_P$; (3) $x$, $RAND$, $RAN{D^{\prime }}_{SN}$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$ and a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$.

Proof of Theorem 10.

Since $BK=KDF(K,x\cdot y\cdot G||SNN)$, $BK\notin {\mathcal{K}}_P$ according to assumption (2). Because $MAC=f_1(BK,SQN|\left|RAND\right||AMF)$ and $RAND$ is uniquely originating in $\sum$, $MAC\subset AUTN\subset term(<s,2>)$ must uniquely originate on a server strand $t$ according to Definitions 5 to 7.

(1)

If $t$ is a server strand of Definition 5, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$. By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAN{D^{\prime }}_{SN}$ are uniquely originating in $\sum$, so ${\left\{RAN{D^{\prime }}_{SN}\right||RES*\}}_{K_{SN,HN}}=term(<t,3>)$ must originate on a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, ${H^{″}}_1$, $HXRES*$, $RES*$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, where $SUP{I}^{″}\subset SUC{I}^{″}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D^{\prime }}_{SN}\right|\left|SUP{I}^{″}\right|\left|RAND\right|\left|{H^{″}}_1\right||HXRES*\}}_{K_{SN,HN}}$ $=term(<r,3>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so ${H^{″}}_1=AUTN$, $SUP{I}^{″}=SUPI$ and $U{E}^{″}=UE$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, $\left\{RAND\right|\left|Result\right||{K^{″}}_{SEAF}$$\left|\right|SUPI{\}}_{K_{SN,HN}}=term(<r,7>)$ must originate on a server strand $t^{″}$. Since $RAND$ is uniquely originating in $\sum$, $t^{″}=t$, so ${K^{″}}_{SEAF}=K_{SEAF}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D^{\prime }}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}=term(<t,1>)$ must originate on a responder strand $r^{\prime }$. Since $RAN{D^{\prime }}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$, so $SUC{I}^{″}=SUCI$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$.

(2)

If $t$ is a server strand of Definition 6, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUT{S}^{\prime }]$, where $SQ{N^{\prime }}_{UE}\subset AUT{S}^{\prime }$. Since $BK\notin {\mathcal{K}}_P$, $MAC-S^{\prime }=f_1^{\ast }(BK,SQ{N^{\prime }}_{UE}|\left|RAND\right||AM{F}_0)$ $\subset AUT{S}^{\prime }\subset term(<t,3>)$ must originate on an initiator strand $s^{\prime }\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $RAND$, $AUT{N}^{″}$, $Syncf$, $AUT{S}^{\prime }]$, so $x$ originates on $term(<s^{\prime },1>)$. By assumptions (1) and (2), $x$ originates on $term(<s,1>)$. Since $x$ is uniquely originating in $\sum$, $s^{\prime }=s$. However, $s^{\prime }\in {\mathrm{Init}}_{\mathrm{II}}$ and $s\in {\mathrm{Init}}_{\mathrm{I}}$, $s^{\prime }\ne s$. Hence, $t$ is not a server strand of Definition 6. □

Theorem 11.

Suppose: (1) $\sum$ is a space for the 5G-AKA’ protocol, and $\mathcal{C}$ is a bundle containing an initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $Syncf$, $AUTS]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN,HN}\notin {\mathcal{K}}_P$; (3) $x$, $RAND$, $RAN{D^{\prime }}_{SN}$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$ and a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$.

Proof of Theorem 11.

Since $BK=KDF(K,x\cdot y\cdot G||SNN)$, $BK\notin {\mathcal{K}}_P$ according to assumption (2). Because $MAC=f_1(BK,SQN|\left|RAND\right||AMF)$ and $RAND$ are uniquely originating in $\sum$, $MAC\subset AUTN\subset term(<s,2>)$ must uniquely originate on a server strand $t$ according to Definitions 5 to 7.

(1)

If $t$ is a server strand of Definition 5, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$. Since $BK\notin {\mathcal{K}}_P$, $CK=f_3(BK,RAND)\notin {\mathcal{K}}_P$ and $IK=f_4(BK,RAND)\notin {\mathcal{K}}_P$, so $CK\left|\right|IK\notin {\mathcal{K}}_P$. Hence, $RES*=KDF(CK||IK,SNN|\left|RAND\right||RES)\subset term(<t,3>)$ must originate on an initiator strand $s^{\prime }\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUT{N}^{″}$, $RES*]$, so $x$ originates on $term(<s^{\prime },1>)$. By assumptions (1) and (2), $x$ originates on $term(<s,1>)$. Since $x$ is uniquely originating in $\sum$, $s^{\prime }=s$. However, $s^{\prime }\in {\mathrm{Init}}_{\mathrm{I}}$ and $s\in {\mathrm{Init}}_{\mathrm{II}}$, $s^{\prime }\ne s$. Hence, $t$ is not a server strand of Definition 5.

(2)

If $t$ is a server strand of Definition 6, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUT{S}^{\prime }]$, where $SQ{N^{\prime }}_{UE}\subset AUT{S}^{\prime }$. Since $BK\notin {\mathcal{K}}_P$, $MAC-S^{\prime }=f_1^{\ast }(BK,SQ{N^{\prime }}_{UE}|\left|RAND\right||AM{F}_0)$ $\subset AUT{S}^{\prime }\subset term(<t,3>)$ must originate on an initiator strand $s^{\prime }$. Since $x$ is uniquely originating in $\sum$, $s^{\prime }=s$, so $SQ{N^{\prime }}_{UE}=SQ{N}_{UE}$ and $AUT{S}^{\prime }=AUTS$. Hence, $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$. By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAN{D^{\prime }}_{SN}$ are uniquely originating in $\sum$, so ${\left\{RAN{D^{\prime }}_{SN}\left|\right|Syncf\right|\left|RAND\right|\left|AUTS\right\}}_{K_{SN,HN}}=term(<t,3>)$ must originate on a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $SN$, $HN$, $SUP{I}^{″}$, $SUC{I}^{″}$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, ${H^{″}}_1$, ${H^{″}}_2$, $Syncf$, $AUTS]$, where $SUP{I}^{″}\subset SUC{I}^{″}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D^{\prime }}_{SN}\right|\left|SUP{I}^{″}\right|\left|RAND\right|\left|{H^{″}}_1\right|\left|{H^{″}}_2\right\}}_{K_{SN,HN}}=term(<r,3>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SUP{I}^{″}=SUPI$, $U{E}^{″}=UE$, ${H^{″}}_1=AUTN$ and ${H^{″}}_2=HXRES*$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D^{\prime }}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}=term(<t,1>)$ must originate on a responder strand $r^{\prime }$. Since $RAN{D^{\prime }}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$, so $SUC{I}^{″}=SUCI$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D^{\prime }}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$. □

According to Theorems 10 and 11, $UE$ successfully authenticates $HN$ and $SN$, and all fields except $RAN{D^{\prime }}_{SN}$ on the sever strand and the responder are agreed with the UE. $RAN{D^{\prime }}_{SN}$ is unknowable to the UE because it is mainly used for the challenge–response mechanism between the SN and the HN, which does not affect the security of the 5G-AKA’ protocol. Hence, MitM attacks are prevented.

In addition, those attacks in Section 3.2 are overcome as follows:

(1)

Since $BK=KDF(K,x\cdot y\cdot G||SNN)$ is used to calculate $AUTN$, the challenge of the UE (i.e., $x$), the pre-shared key between the UE and the HN (i.e., $K$) and $SNN$ are included in $AUTN$. As a result, $UE$ can find whether $SUCI$ is replayed, $UE$ successfully authenticates $HN$ and $SN$, and $RAND\left|\right|AUTN$ on the UE cannot be replayed, making that the location privacy of the UE cannot be compromised.

(2)

Since $MACf$ is replaced with a timeout mechanism on the HN, MAC failure attacks are prevented. Further, $RAND\left|\right|AUTN$ on the UE cannot be replayed maliciously to generate $Syncf$. As a result, the penetrator cannot take advantage of $Syncf$ and $MACf$ to performed cross attacks.

4.4. The Server’s Guarantee of the 5G-AKA’ Protocol

Theorem 12.

Suppose: (1) $\sum$ is a space for the 5G-AKA’ protocol, and $\mathcal{C}$ is a bundle containing a server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN,HN}\notin {\mathcal{K}}_P$; (3) $x$, $RAND$, $RAN{D}_{SN}$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $RES*]$ and a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$.

Proof of Theorem 12.

Since $BK=KDF(K,x\cdot y\cdot G||SNN)$, $BK\notin {\mathcal{K}}_P$ according to assumption (2). Because $CK=f_3(BK,RAND)$ and $IK=f_4(BK,RAND)$, $CK\notin {\mathcal{K}}_P$ and $IK\notin {\mathcal{K}}_P$, so $CK\left|\right|IK\notin {\mathcal{K}}_P$. By assumption (3), $x$ is uniquely originating in $\sum$, so $RES*=KDF(CK||IK,SNN|\left|RAND\right||RES)$ $\subset term(<t,3>)$ must originate on a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUT{N}^{\prime }$, $RES*]$, where $SQ{N}^{\prime }\subset AUT{N}^{\prime }$. Since $BK\notin {\mathcal{K}}_P$, $MA{C}^{\prime }=f_1(BK,SQ{N}^{\prime }|\left|RAND\right||AMF)$ $\subset AUT{N}^{\prime }\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{\prime }=SQN$ and $AUT{N}^{\prime }=AUTN$. Hence, $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $RES*]$. By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAN{D}_{SN}$ are uniquely originating in $\sum$, so ${\left\{RAN{D}_{SN}\right||RES*\}}_{K_{SN,HN}}=term(<t,3>)$ must originate on a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAN{D}_{SN}$, $RAND$, ${H^{″}}_1$, $HXRES*$, $RES*$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, where $SUP{I}^{″}\subset SUC{I}^{″}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right|\left|SUP{I}^{″}\right|\left|RAND\right|\left|{H^{″}}_1\right||HXRES*\}}_{K_{SN,HN}}$ $=term(<r,3>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so ${H^{″}}_1=AUTN$, $SUP{I}^{″}=SUPI$ and $U{E}^{″}=UE$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, $\left\{RAND\right|\left|Result\right||{K^{″}}_{SEAF}$$\left|\right|SUPI{\}}_{K_{SN,HN}}=term(<r,7>)$ must originate on a server strand $t^{″}$. Since $RAND$ is uniquely originating in $\sum$, $t^{″}=t$, so ${K^{″}}_{SEAF}=K_{SEAF}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}=term(<t,1>)$ must originate on a responder strand $r^{\prime }$. Since $RAN{D}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$, so $SUC{I}^{″}=SUCI$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$. □

Theorem 13.

Suppose: (1) $\sum$ is a space for the 5G-AKA’ protocol, and $\mathcal{C}$ is a bundle containing a server strand $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN,HN}\notin {\mathcal{K}}_P$; (3) $x$, $RAND$, $RAN{D}_{SN}$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $Syncf$, $AUTS]$ and a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$.

Proof of Theorem 13.

Since $BK=KDF(K,x\cdot y\cdot G||SNN)$, $BK\notin {\mathcal{K}}_P$ according to assumption (2). By assumption (3), $x$ is uniquely originating in $\sum$, so $MAC-S=f_1^{\ast }(BK,SQ{N}_{UE}|\left|RAND\right||AM{F}_0)\subset AUTS\subset term(<t,3>)$ must originate on a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUT{N}^{\prime }$, $Syncf$, $AUTS]$, where $SQ{N}^{\prime }\subset AUT{N}^{\prime }$. Since $BK\notin {\mathcal{K}}_P$, $MA{C}^{\prime }=f_1(BK,SQ{N}^{\prime }||RAND$$\left|\right|AMF)\subset AUT{N}^{\prime }\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{\prime }=SQN$ and $AUT{N}^{\prime }=AUTN$. Hence, $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $Syncf$, $AUTS]$. By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAN{D}_{SN}$ are uniquely originating in $\sum$, so ${\left\{RAN{D}_{SN}\right|\left|Syncf\right|\left|RAND\right|\left|AUTS\right\}}_{K_{SN,HN}}=term(<t,3>)$ must originate on a unique responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $SN$, $HN$, $SUP{I}^{″}$, $SUC{I}^{″}$, $SNN$, $RAN{D}_{SN}$, $RAND$, ${H^{″}}_1$, ${H^{″}}_2$, $Syncf$, $AUTS]$, where $SUP{I}^{″}\subset SUC{I}^{″}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right|\left|SUP{I}^{″}\right|\left|RAND\right|\left|{H^{″}}_1\right|\left|{H^{″}}_2\right\}}_{K_{SN,HN}}=term(<r,3>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SUP{I}^{″}=SUPI$, $U{E}^{″}=UE$, ${H^{″}}_1=AUTN$ and ${H^{″}}_2=HXRES*$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right|\left|SUCI\right|\left|SNN\right\}}_{K_{SN,HN}}=term(<t,1>)$ must originate on a responder strand $r^{\prime }$. Since $RAN{D}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$, so $SUC{I}^{″}=SUCI$. Hence, $r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$. □

According to Theorems 12 and 13, $HN$ successfully authenticates $UE$ and $SN$, and all fields on the initiator strand and the responder are agreed with the HN, so MitM attacks are prevented.

In addition, those attacks in Section 3.3 are overcome as follows:

(1)

Although $HN$ cannot find that $SUCI$ is replayed because $SUCI$ does not contain the challenge of the HN (i.e., $RAND$), $UE$ can find whether $SUCI$ is replayed because $BK=KDF(K,x\cdot y\cdot G||SNN)$ is used to calculate $AUTN$. Hence, this does not affect the security of the 5G-AKA’ protocol.

(2)

Since $MACf$ is replaced with a timeout mechanism on the HN, MAC failure attacks are prevented.

(3)

Since the HN sends $K_{SEAF}$ and $SUPI$ together with $RAND$, they can be agreed with the HN.

4.5. The Responder’s Guarantee of the 5G-AKA’ Protocol

Theorem 14.

Suppose: (1) $\sum$ is a space for the 5G-AKA’ protocol, and $\mathcal{C}$ is a bundle containing a responder strand $r\in {\mathrm{Resp}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $H_1$, $H_2$, $H_3$, $Result$, $K_{SEAF}$, $SUPI]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN,HN}\notin {\mathcal{K}}_P$; (3) $x$, $RAND$, $RAN{D}_{SN}$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$ and a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $RES*]$.

Proof of Theorem 14.

By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAND$ are uniquely originating in $\sum$, so ${\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}=term(<r,3>)$ must uniquely originate on a server strand $t$ according to Definitions 5 to 7.

(1)

If $t$ is a server strand of Definition 5, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUPI]$, where $SUPI\subset SUC{I}^{\prime }$, $x^{\prime }\subset AUT{N}^{\prime }$, $x^{\prime }\subset (HXRES*{)}^{\prime }$, $x^{\prime }\subset (RES*{)}^{\prime }$, $x^{\prime }\subset {K^{\prime }}_{SEAF}$ and ${K^{\prime }}_{SEAF}$ is generated for $SUPI$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, $\left\{RAND\right|\left|Result\right||K_{SEAF}$$\left|\right|SUPI{\}}_{K_{SN,HN}}=term(<r,7>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so ${K^{\prime }}_{SEAF}=K_{SEAF}$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right|\left|SUC{I}^{\prime }\right|\left|SNN\right\}}_{K_{SN,HN}}$ $=term(<t,1>)$ must originate on a responder strand $r^{\prime }$. Since $RAN{D}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$, so $SUC{I}^{\prime }=SUCI$ and $x^{\prime }=x$ according to assumption (1). As a result, $AUT{N}^{\prime }=AUTN$, $(HXRES*{)}^{\prime }=HXRES*$ and $(RES*{)}^{\prime }=RES*$. Hence, $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $RES*$, $Result$, $K_{SEAF}$, $SUPI]$. Since $BK=KDF(K,x\cdot y\cdot G||SNN)$, $BK\notin {\mathcal{K}}_P$ according to assumption (2). Because $CK=f_3(BK,RAND)$ and $IK=f_4(BK,RAND)$, $CK\notin {\mathcal{K}}_P$ and $IK\notin {\mathcal{K}}_P$, so $CK\left|\right|IK\notin {\mathcal{K}}_P$. By assumption (3), $x$ is uniquely originating in $\sum$, so $RES*=KDF(CK||IK,SNN|\left|RAND\right||RES)$ $\subset term(<t,3>)$ must originate on a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUT{N}^{″}$, $RES*]$, where $SQ{N}^{″}\subset AUT{N}^{″}$. Since $BK\notin {\mathcal{K}}_P$, $MA{C}^{″}=f_1(BK,SQ{N}^{″}|\left|RAND\right||AMF)$ $\subset AUT{N}^{″}\subset term(<s,2>)$ must originate on a server strand $t^{″}$. Since $RAND$ is uniquely originating in $\sum$, $t^{″}=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUTN$. Hence, $s\in {\mathrm{Init}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $RES*]$.

(2)

If $t$ is a server strand of Definition 6, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUC{I}^{\prime }$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $SUPI\subset SUC{I}^{\prime }$, $x^{\prime }\subset AUT{N}^{\prime }$, $x^{\prime }\subset (HXRES*{)}^{\prime }$ and $x^{\prime }\subset AUT{S}^{\prime }$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right|\left|Syncf\right|\left|RAND\right|\left|AUT{S}^{\prime }\right\}}_{K_{SN,HN}}=term(<t,3>)$ must originate on a responder strand $r^{\prime }\in {\mathrm{Resp}}_{\mathrm{II}}[U{E}^{″}$, $SN$, $HN$, $SUP{I}^{″}$, $SUC{I}^{″}$, $SNN$, $RAN{D}_{SN}$, $RAND$, ${H^{″}}_1$, ${H^{″}}_2$, $Syncf$, $AUT{S}^{\prime }]$, so $RAN{D}_{SN}$ originates on $term(<r^{\prime },2>)$. By assumptions (1) and (2), $RAN{D}_{SN}$ originates on $term(<r,2>)$. Since $RAN{D}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$. However, $r^{\prime }\in {\mathrm{Resp}}_{\mathrm{II}}$ and $r\in {\mathrm{Resp}}_{\mathrm{I}}$, $r^{\prime }\ne r$. Hence, $t$ is not a server strand of Definition 6. □

Theorem 15.

Suppose: (1) $\sum$ is a space for the 5G-AKA’ protocol, and $\mathcal{C}$ is a bundle containing a responder strand $r\in {\mathrm{Resp}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $H_1$, $H_2$, $Syncf$, $H_4]$; (2) $K\notin {\mathcal{K}}_P$ and $K_{SN,HN}\notin {\mathcal{K}}_P$; (3) $x$, $RAND$, $RAN{D}_{SN}$ is uniquely originating in $\sum$. Then, $\mathcal{C}$ contains a unique server strand $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$ and a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $Syncf$, $AUTS]$.

Proof of Theorem 15.

By assumptions (2) and (3), $K_{SN,HN}\notin {\mathcal{K}}_P$ and $RAND$ and uniquely originating in $\sum$, so ${\left\{RAN{D}_{SN}\right|\left|SUPI\right|\left|RAND\right|\left|H_1\right|\left|H_2\right\}}_{K_{SN,HN}}=term(<r,3>)$ must uniquely originate on a server strand $t$ according to Definitions 5 to 7.

(1)

If $t$ is a server strand of Definition 5, then $t\in {\mathrm{Serv}}_{\mathrm{I}}[UE$, $SN$, $HN$, $SUC{I}^{\prime }$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{\prime }}_{SEAF}$, $SUPI]$, where $SUPI\subset SUC{I}^{\prime }$, $x^{\prime }\subset AUT{N}^{\prime }$, $x^{\prime }\subset (HXRES*{)}^{\prime }$, $x^{\prime }\subset (RES*{)}^{\prime }$, $x^{\prime }\subset {K^{\prime }}_{SEAF}$ and ${K^{\prime }}_{SEAF}$ is generated for $SUPI$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right||(RES*{)}^{\prime }\}}_{K_{SN,HN}}$ $=term(<t,3>)$ must originate on a unique responder strand $r^{\prime }\in {\mathrm{Resp}}_{\mathrm{I}}[U{E}^{″}$, $SN$, $HN$, $SUC{I}^{″}$, $SNN$, $RAN{D}_{SN}$, $RAND$, ${H^{″}}_1$, $(HXRES*{)}^{\prime }$, $(RES*{)}^{\prime }$, $Result$, ${K^{″}}_{SEAF}$, $SUP{I}^{″}]$, so $RAN{D}_{SN}$ originates on $term(<r^{\prime },2>)$. By assumptions (1) and (2), $RAN{D}_{SN}$ originates on $term(<r,2>)$. Since $RAN{D}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$. However, $r^{\prime }\in {\mathrm{Resp}}_{\mathrm{I}}$ and $r\in {\mathrm{Resp}}_{\mathrm{II}}$, $r^{\prime }\ne r$. Hence, $t$ is not a server strand of Definition 5.

(2)

If $t$ is a server strand of Definition 6, then $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUC{I}^{\prime }$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUT{N}^{\prime }$, $(HXRES*{)}^{\prime }$, $Syncf$, $AUT{S}^{\prime }]$, where $SUPI\subset SUC{I}^{\prime }$, $x^{\prime }\subset AUT{N}^{\prime }$, $x^{\prime }\subset (HXRES*{)}^{\prime }$ and $x^{\prime }\subset AUT{S}^{\prime }$. Since $K_{SN,HN}\notin {\mathcal{K}}_P$, ${\left\{RAN{D}_{SN}\right|\left|SUC{I}^{\prime }\right|\left|SNN\right\}}_{K_{SN,HN}}$ $=term(<t,1>)$ must originate on a responder strand $r^{\prime }$. Since $RAN{D}_{SN}$ is uniquely originating in $\sum$, $r^{\prime }=r$, so $SUC{I}^{\prime }=SUCI$ and $x^{\prime }=x$ according to assumption (1). As a result, $AUT{N}^{\prime }=AUTN$, $(HXRES*{)}^{\prime }=HXRES*$ and $AUT{S}^{\prime }=AUTS$. Hence, $t\in {\mathrm{Serv}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUPI$, $SUCI$, $SNN$, $RAN{D}_{SN}$, $RAND$, $AUTN$, $HXRES*$, $Syncf$, $AUTS]$. Since $BK=KDF(K,x\cdot y\cdot G||SNN)$, $BK\notin {\mathcal{K}}_P$ according to assumption (2). By assumption (3), $x$ is uniquely originating in $\sum$, so $MAC-S=f_1^{\ast }(BK,SQ{N}_{UE}|\left|RAND\right||AM{F}_0)\subset AUTS\subset term(<t,3>)$ must originate on a unique initiator strand $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUT{N}^{″}$, $Syncf$, $AUTS]$, where $SQ{N}^{″}\subset AUT{N}^{″}$. Since $BK\notin {\mathcal{K}}_P$, $MA{C}^{″}=f_1(BK,SQ{N}^{″}$$\left|\right|RAND\left|\right|AMF)\subset AUT{N}^{″}\subset term(<s,2>)$ must originate on a server strand $t^{\prime }$. Since $RAND$ is uniquely originating in $\sum$, $t^{\prime }=t$, so $SQ{N}^{″}=SQN$ and $AUT{N}^{″}=AUTN$. Hence, $s\in {\mathrm{Init}}_{\mathrm{II}}[UE$, $SN$, $HN$, $SUCI$, $RAND$, $AUTN$, $Syncf$, $AUTS]$. □

According to Theorems 14 and 15, $SN$ successfully authenticates $UE$ and $HN$, and all fields on the initiator strand and the responder are agreed with the HN, so MitM attacks are prevented.

In addition, those attacks in Section 3.4 are overcome as follows:

(1)

Since $SUPI$ is added to the second message between the SN and the HN, and $RAND$ is added to the fourth message between the SN and the HN, both $K_{SEAF}$ and $SUPI$ on the HN can be agreed with the SN, which means that $SN$ successfully authenticates $UE$ and obtains the corresponding $K_{SEAF}$.

(2)

Since $MACf$ is replaced with a timeout mechanism on the HN, MAC failure attacks are prevented. Further, $RAND\left|\right|AUTN$ on the UE cannot be replayed maliciously to generate $Syncf$ because $BK=KDF(K,x\cdot y\cdot G||SNN)$. As a result, the penetrator cannot take advantage of $Syncf$ and $MACf$ to performed cross attacks.

(3)

Since the challenge–response mechanism between the SN and the HN is added, the messages received by the SN cannot be replayed, preventing Dos attacks on the SN.

5. Discussion

5.1. Security of the 5G-AKA’ Protocol

According to the above security analysis of the latest version of the 5G AKA protocol, twenty-one attack scenarios can be obtained, where thirteen attack scenarios are related to $MACf$. In our proposed 5G-AKA’ protocol, $MACf$ is replaced with a timeout mechanism on the HN, so the thirteen attack scenarios are eliminated. As a result, those attacks in the thirteen attack scenarios are eliminated, including MAC failure attacks.

Without considering $MACf$, the comparative analysis of authentication properties [28,29,30] between the latest version of the 5G AKA protocol and our proposed 5G-AKA’ protocol is shown in

Table 1. The comparative analysis of authentication properties between the two protocols.

Protocols	Authentication Properties	UE to SN	UE to HN	SN to UE	SN to HN	HN to UE	HN to SN
5G AKA	Injection agreement	No	No	No	No	No	No
	Non-injection agreement	No	No	No	No	No	No
	Weaker agreement	No	Yes	No	Yes	Yes	Yes
5G-AKA’	Injection agreement	Yes	Yes	Yes	Yes	Yes	Yes
	Non-injection agreement	No	No	No	No	No	No
	Weaker agreement	No	No	No	No	No	No

.

From Table 1, in the latest version of the 5G AKA protocol, only the weaker agreement can be established, and even weak agreement cannot be established in the cases of “UE to SN” and “SN to UE”, because the UE cannot authenticate the SN, and the SN cannot authenticate the UE. However, in our proposed 5G-AKA’ protocol, mutual authentication and injection agreement among the UE, the SN and the HN can be established in all cases according to the security analysis of the 5G-AKA’ protocol.

According to the above security analysis of the latest version of the 5G AKA protocol, based on those missing agreements, the penetrator can perform MitM attacks and cross attacks. Additionally, based on replayed messages, replay attacks and masquerading attacks can be performed, the location privacy of the UE can be compromised and DoS attacks on the SN can be formed. However, according to the above security analysis of the 5G-AKA’ protocol, our proposed 5G-AKA’ protocol has overcome these attacks.

In terms of secrecy properties, the keys established in the latest version of the 5G AKA protocol are secret. However, if $K$ is leaked, then the attacker can calculate $K_{AUSF}$ and $K_{SEAF}$ based on those messages transmitted in the past run of the protocol. As a result, the attacker can decrypt those encrypted messages transmitted in the past run of the protocol. Therefore, the latest version of the 5G AKA protocol does not provide perfect forward secrecy. However, in our proposed 5G-AKA’ protocol, $K$ is replaced with $BK=KDF(K,x\cdot y\cdot G||SNN)$, providing perfect forward secrecy based on Diffie–Hellman exchange.

Therefore, our proposed 5G-AKA’ protocol is secure and can overcome those security problems of the latest version of the 5G AKA protocol. The comparative analysis of security properties between the 5G-AKA’ protocol and some recently improved 5G AKA protocols [22,23,24] is shown in

Table 2. The comparative analysis of security properties between the 5G-AKA’ protocol and some recently improved 5G AKA protocols [22,23,24].

Security Properties	5G AKA	[22]	[23]	[24]	5G-AKA’
Implement mutual authentication	No	No	No	No	Yes
Prevent MitM attacks	No	No	No	No	Yes
Resistance against cross attacks	No	No	No	Yes	Yes
Compromise the location privacy of the UE	No	Yes	Yes	Yes	Yes
Prevent masquerading attacks	No	No	No	No	Yes
Resistance against replay attacks	No	No	No	No	Yes
Defend against DoS attacks on the SN	No	No	No	No	Yes
Prevent MAC failure attacks	No	No	No	Yes	Yes
Provide key secrecy	Yes	Yes	Yes	Yes	Yes
Provide perfect forward secrecy	No	No	No	No	Yes

.

From Table 2, only some security properties can be guaranteed in the 5G AKA protocol and these recently improved 5G AKA protocols, but all security properties can be guaranteed in our proposed 5G-AKA’ protocol.

In [22], $AUTN$ contains the challenge of the UE (i.e., $r_{UE}$), so the first received message of the UE cannot be a replayed message, preventing the location privacy of the UE from being compromised. However, $AUTN$ does not contains $SNN$, so the UE cannot authenticate the SN. Because the UE and the HN cannot reach an agreement in $SNN$, MitM attacks can be performed. Since the MAC failure is inherited from the 5G AKA protocol, cross attacks and MAC failure attacks still exist in the protocol of [22]. The received messages of the SN do not contain the challenge of the SN (i.e., $r_{SEAF}$), so these messages can be replayed messages, forming replay attacks, masquerading attacks and Dos attacks on the SN. In addition, $K_{AUSF}$ and $K_{SEAF}$ are encrypted, so key secrecy is provided, but perfect forward secrecy cannot be provided because $K_{AUSF}$ and $K_{SEAF}$ can be calculated when $K$ is leaked.

In [23], the Eph Private key and Eph Public key of the UE, the public/private key pair of the SN and the public/private key pair of the HN are used to ensure the security of the channel between the UE and the SN, the security of channel between the UE and the HN, and the security of channel between the SN and the HN. Since the first received message of the UE is encrypted by the Eph Public key of the UE, this means that the message can only be decrypted by the Eph Private key of the UE, so it cannot be a replayed message, preventing the location privacy of the UE being compromised. However, the other parts fully inherit the 5G AKA protocol, so the other attacks of the 5G AKA protocol still exist in the protocol of [23]. Similarly, perfect forward secrecy cannot be provided.

In [24], both the synchronization failure and the MAC failure are constructed as the format of $RES*$, making it impossible to distinguish them, so as to prevent the location privacy of the UE from being compromised and prevent cross attacks and MAC failure attacks. However, the other parts fully inherit the 5G AKA protocol, so the other attacks of the 5G AKA protocol still exist in the protocol of [24]. Similarly, perfect forward secrecy cannot be provided.

Therefore, our proposed 5G-AKA’ protocol is better than the 5G AKA protocol, and these recently improved 5G AKA protocols in security.

5.2. Performance of the 5G-AKA’ Protocol

The comparative analysis between the 5G-AKA’ protocol and some recently improved 5G AKA protocols [22,23,24] in the number of messages, the number of fields, the amount of calculation and backward compatibility is shown in

Table 3. The comparative analysis between the 5G-AKA’ protocol and some recently improved 5G AKA protocols [22,23,24] in the number of messages, the number of fields, the amount of calculation and backward compatibility.

Comparative Items	5G AKA	[22]	[23]	[24]	5G-AKA’
The number of messages	MN	MN	MN	MN	MN-2
The number of fields	FN	FN + 9	FN-1	FN + 2	FN + 4
The amount of calculation	CA	CA + 2F	CA + 4PED-1ECDH-2F	CA + 2PED + 1F	CA + 1F
Backward compatibility	--	Yes	No	No	Yes

.

In Table 3, MN denotes the number of messages of the 5G AKA protocol. FN denotes the number of fields of the 5G AKA protocol. CA denotes the amount of calculation of the 5G AKA protocol. Note that the number of messages and the number of fields in Table 3 are the number of messages and the number of fields among the UE, the SN and the HN. ECDH denotes the generation and verification of an elliptic curve Diffie–Hellman (ECDH) exchange. PED denotes the encryption and decryption based on a public and private key pair. F denotes the generation and verification of a key function, a key derivation function, a MAC function or a hash function, which are grouped into one category because they have a similar amount of calculation [27]. According to [26], the computation overhead of the generation or verification of an ECDH exchange is 1290 us, the computation overhead of the encryption based on a public key is 2580 us, the computation overhead of the decryption based on a private key is 1750 us, the computation overhead of the hash function based on SHA-256 is 3.8 us, and the computation overhead of the MAC function based on HMAC-SHA256 is 67 us.

In our proposed 5G-AKA’ protocol, two messages related to $MACf$ are cut down because $MACf$ is replaced with a timeout mechanism on the HN. Four $RAN{D}_{SN}$, one $RAND$, and one $SUPI$ are added to the messages between the SN and the HN, while two $MACf$ are cut down, so four fields are added. Since $K$ is replaced with $BK=KDF(K,x\cdot y\cdot G||SNN)$ on the UE and the HN, the calculation amount of one F is added. From Table 3, compared with other protocols, our proposed 5G-AKA’ protocol reduces two messages. The 5G-AKA’ protocol adds more fields than the protocols in [23] and [24], but less than the protocol in [22]. In the amount of calculation, our proposed 5G-AKA’ protocol increases the least, while the protocols in [23] and [24] increase the most because they introduce multiple public-key encryption and decryption. Hence, our proposed 5G-AKA’ protocol is efficient. Especially for the UE, only a key derivation function is added, but one field and one message are reduced.

In addition, the protocols in [23] and [24] destroys the structure of the messages instead of adding fields to the messages or extending fields in the messages, so they are not backward compatible. Our proposed 5G-AKA’ protocol only extends $K$ and adds some fields to the messages between the SN and the HN, so it is forward compatible.

6. Conclusions

In this paper, we summarize the 5G AKA protocol into three cases according to the overview of the latest version of the 5G AKA protocol and then use the mixed strand space model for mixed protocols to formally analyze the security of the 5G AKA protocol. As a result, twenty-one attack scenarios of the 5G AKA protocol are obtained, where thirteen attack scenarios are related to the MAC failure, including MAC failure attacks. Based on these attack scenarios, we find that the mutual authentication between the UE and the SN cannot be established, and only the weaker agreement can be established among the UE, the SN and the HN, resulting in MitM attacks and cross attacks. Further, by replaying some message to the UE and the SN, replay attacks and masquerading attacks can be performed, the location privacy of the UE can be compromised and DoS attacks on the SN can be formed. In addition, the 5G AKA protocol cannot provide perfect forward secrecy.

To overcome these attacks, we propose a 5G-AKA’ protocol, in which the pre-shared key between the UE and the HN is replaced with a derivation key of the pre-shared key, the challenge–response mechanism between the SN and the HN is added, the SUPI of the UE is added to the second message between the SN and the HN, and the MAC failure procedure is replaced with a timeout mechanism on the HN. According to the 5G-AKA’ protocol, we summarize the 5G-AKA’ protocol into two cases and then use the mixed strand space model for mixed protocols to formally analyze the security of the 5G-AKA’ protocol. As a result, no attack scenario is obtained.

By discussion and analysis, the 5G-AKA’ protocol can establish mutual authentication and injection agreement among the UE, the SN and the HN, and can overcome the above security problems of the latest version of the 5G AKA protocol. Therefore, the 5G-AKA’ protocol is secure. The comparative analysis of security properties between the 5G-AKA’ protocol and some recently improved 5G AKA protocols shows that the 5G-AKA’ protocol is better than these recently improved 5G AKA protocols in security. The comparative analysis between the 5G-AKA’ protocol and some recently improved 5G AKA protocols in the number of messages, the number of fields, the amount of calculation and backward compatibility shows that the 5G-AKA’ protocol is efficient, and is backward compatible with the 5G AKA protocol.

Recently, some authors also point out that the protection mechanism of SQN can be defeated due to its use of XOR in the 5G AKA protocol. This paper does not consider this security problem, and we will further study this security problem in the future.