A Secure Group-Based AKA Protocol for Machine-Type Communications

Abstract

The fifth generation wireless system (5G) is expected to handle with an unpredictable number of heterogeneous connected devices while guaranteeing a high level of security. This paper advances a group-based Authentication and Key Agreement (AKA) protocol that contributes to reduce latency and bandwidth consumption, and scales up to a very large number of devices. A central feature of the proposed protocol is that it provides a way to dynamically customize the trade-off between security and efficiency. The protocol is lightweight as it resorts on symmetric key encryption only, hence it supports low-end devices and can be already adopted in current standards with little effort. Using ProVerif, we prove that the protocol meets mutual authentication, key confidentiality, and device privacy also in presence of corrupted devices, a threat model not being addressed in the state-of-the-art group-based AKA proposals. We evaluate the protocol performances in terms of latency and bandwidth consumption, and obtain promising results.

Appendices

A Formal Specification of Security Requirements

ProVerif allows for syntactical extension of the applied pi-calculus, such as events and choices, to ease the specification of security requirements. Confidentiality can be modelled as a reachability property. The secrecy of a term m is preserved if an attacker, defined as an arbitrary process, cannot construct m from any run of the protocol. More precisely, the definition of reachability-based secrecy says that an attacker cannot build a process A that can output the secret term m.

Authentication can be defined using correspondence assertions. An event e is a message emitted into a special channel that is not under the control of the attacker. To model correspondence assertions, we annotate processes with events such as $\mathtt {e}\langle M_1,...M_n \rangle$ and reason about the relationships ($\leadsto$) between events and their arguments in the form “if an event $\mathtt {e}\langle M_1,...M_n \rangle$ has been executed, then an event $\mathtt {e'}\langle N_1,...N_n \rangle$ has been previously executed”.

The applied pi-calculus supports the notion of observation equivalence. Informally, two processes are observational equivalent if an observer cannot distinguish the processes even if they handle different data or perform different computations. The indistinguishability characterization of the definition of observation equivalence allows us to capture privacy requirements.

Confidentiality. We check confidentiality of the session master key by proving that a fresh secret, which is encrypted with the key and sent in form of ciphertext on the public channel, cannot be obtained by the attacker. As soon as MTC and MME derive the session master key, each of them generates a ciphertext that encrypts the secret. They send the ciphertexts at the very end of the protocol run, accordingly the case. We specify the session master key confidentiality in ProVerif with the following query:

$$ \mathbf{query }\, {\text {attacker}}\, {\textit{(secret)}.} $$

ProVerif is suitable to prove confidentiality as it attempts to prove that a state in which the attacker knows the secret is unreachable. It follows that the secret is known only to MTC and MME.

Authentication. We specify MTC and serving network authentication requirements as correspondence assertions. Each assertion consists of a number of events. Events normally need to agree with some arguments to capture authentication. Thus, we introduce the terms that serve as arguments in our events as follows.

• $\textsc {imsi}$ refers to the permanent subscribe identity of the MTC;

• $\textsc {gid}$ refers to the group identifiers of the MME;

• $\textsc {sn}$ denotes the identifiers of the MME;

• ${\textsc {k}_{\textsc {asme}}}$ denotes the session master key;

• $\textsc {path\_mtc}$ denotes the path assigned to the MTC;

• $\textsc {Hgk\_mtc}$ refers to the session individual key derived from the GK tree and associated to the MTC;

• $\textsc {rand}$ refers to the random value generated by the HSS;

• $\textsc {Hch\_mtc}$ refers to the session challenge key derived from the CH tree and associated to the MTC;

Having seen the arguments, we can define the list of events needed to specify mutual group authentication between MTC and MME. The events reflect the two cases defined in the group-based AKA protocol.

• ${ \texttt {begin\_mtc\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, {\textsc {k}_{\textsc {asme}}} \rangle }$ means that the MME with identity $\textsc {sn}$ begins the authentication of the MTC with identity $\textsc {imsi}$ and group $\textsc {gid}$, and associates it with the key ${\textsc {k}_{\textsc {asme}}}$. The event regards the case A and is emitted by the MME after the authentication data response message.

• ${ \texttt {begin\_mtc\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hgk\_mtc} \rangle }$ means that the MME with identity $\textsc {sn}$ begins the authentication of the MTC with path $\textsc {path\_mtc}$ and group $\textsc {gid}$, and associates it with the key $\textsc {Hgk\_mtc}$. The event regards the case B and is emitted by the MME after the attach request.

• ${ \texttt {begin\_mme\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, \textsc {rand}, {\textsc {k}_{\textsc {asme}}} \rangle }$ means that the MTC with identity $\textsc {imsi}$ and group $\textsc {gid}$ begins the authentication of the MME with identity $\textsc {sn}$, and associates it with the random value $\textsc {rand}$ and key ${\textsc {k}_{\textsc {asme}}}$. The event regards the case A and is emitted by the MTC after the authentication request.

• ${ \texttt {begin\_mme\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hch\_mtc}, {\textsc {k}_{\textsc {asme}}} \rangle }$ means that the MTC with path $\textsc {path\_mtc}$ and group $\textsc {gid}$ begins the authentication of the MME with identity $\textsc {sn}$, and associate it with the keys $\textsc {Hch\_mtc}$ and ${\textsc {k}_{\textsc {asme}}}$. The event regards the case B and is emitted by the MTC after the authentication request derivable message.

• ${ \texttt {end\_mtc\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, {\textsc {k}_{\textsc {asme}}} \rangle }$ means that the MTC with identity $\textsc {imsi}$ and group $\textsc {gid}$ concluded the authentication of the MME with identity $\textsc {sn}$, and computed the key ${\textsc {k}_{\textsc {asme}}}$. The event regards the case A and is emitted by the MTC after the authentication response.

• ${ \texttt {end\_mtc\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hgk\_mtc} \rangle }$ means that the MTC with path $\textsc {path\_mtc}$ and group $\textsc {gid}$ concluded the authentication of the MME with identity $\textsc {sn}$, and computed the key $\textsc {Hgk\_mtc}$. The event regards the case B and is emitted by the MTC after the authentication response derivable message.

• ${ \texttt {end\_mme\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, \textsc {rand}, {\textsc {k}_{\textsc {asme}}} \rangle }$ means that the MME with identity $\textsc {sn}$ concluded the authentication of the MTC with identity $\textsc {imsi}$ and group $\textsc {gid}$, and associates it with the random value $\textsc {rand}$ and key ${\textsc {k}_{\textsc {asme}}}$. The event regards the case A and is emitted by the MME after the successful verification of res.

• ${ \texttt {end\_mme\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hch\_mtc}, {\textsc {k}_{\textsc {asme}}} \rangle }$ means that the MME with identity $\textsc {sn}$ concluded the authentication of the MTC with path $\textsc {path\_mtc}$ and group $\textsc {gid}$, and associates it with keys $\textsc {Hch\_mtc}$ and ${\textsc {k}_{\textsc {asme}}}$. The event regards the case B and is emitted by the MME after the successfully verification of res $_{\textsc {d}}$.

To formalize mutual authentication we need to distinguish the authentication of the MME to MTC and the authentication of the MTC to the MME. Moreover, we need to distinguish the two cases. We formalize the authentication of the MME to MTC in Case A and Case B as follows.

Definition 1

(Serving network authentication (Case A)). The protocol ensures serving network authentication for Case A if the correspondence assertion

$$\begin{aligned}&\mathtt {end\_mtc\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, {\textsc {k}_{\textsc {asme}}} \rangle ~\leadsto \\ {}&\mathtt {begin\_mtc\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, {\textsc {k}_{\textsc {asme}}} \rangle \end{aligned}$$

is true on every execution trace.

Definition 2

(Serving network authentication (Case B)). The protocol ensures serving network authentication for Case B if the correspondence assertion

$$\begin{aligned}&\mathtt {end\_mtc\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hgk\_mtc} \rangle ~\leadsto ~\\ {}&\mathtt {begin\_mtc\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hgk\_mtc} \rangle \end{aligned}$$

is true on every execution trace.

In a similar way, we can formalize the authentication of the MTC to the MME in Case A and Case B.

Definition 3

(MTC authentication (Case A)). The protocol ensures the authentication of MTC for Case A if the correspondence assertion

$$\begin{aligned}&\mathtt {end\_mme\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, \textsc {rand}, {\textsc {k}_{\textsc {asme}}} \rangle ~\leadsto \\ {}&\mathtt {begin\_mme\_A} \langle \textsc {imsi}, \textsc {gid}, \textsc {sn}, \textsc {rand}, {\textsc {k}_{\textsc {asme}}} \rangle \end{aligned}$$

is true on every execution trace.

Definition 4

(MTC authentication (Case B)). The protocol ensures the authentication of MTC for Case B if the correspondence assertion

$$\begin{aligned}&\mathtt {end\_mme\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hch\_mtc}, {\textsc {k}_{\textsc {asme}}} \rangle ~\leadsto \\ {}&\mathtt {begin\_mme\_B} \langle \textsc {path\_mtc}, \textsc {gid}, \textsc {sn}, \textsc {Hch\_mtc}, {\textsc {k}_{\textsc {asme}}} \rangle \end{aligned}$$

is true on every execution trace.

Privacy. To model MTC identity privacy as equivalence property, we use the definition of labelled bisimilarity ($\approx _l$) as defined by Abadi and Fournet. We reason about the processes of MTC, MME, and HSS, which map to the corresponding roles. Each device playing the role of MTC execute the same process MTC but are instantiated with different variable values (e.g. imsi, k). The requirement of MTC identity privacy can be conveniently specified as follows:

Definition 5

(MTC identity privacy).

$$ MTC\{^{\textsc {imsi}_A}/_{id}\}|MME|HSS\approx _lMTC\{^{\textsc {imsi}_B}/_{id}\}|MME|HSS $$

The definition above states that two processes instantiated with two different IMSI values have to be observationally equivalent. Such equivalence means that an attacker cannot distinguish whether the MTC participating in the protocol run is the one associated with $\textsc {imsi}_A$ or $\textsc {imsi}_B$, hence the privacy of the MTC identity is guaranteed. Note that the formulation of MTC identity privacy based on observational equivalence is more stringent than any formulation based on reachability. The latter formulation would need to assume that the attacker does not know any imsivalue in advance, an assumption that can be lifted up using observational equivalence.

The ProVerif code that describes the processes for MTC, MME, and HSS are respectively in Figs. 6, 7, and 8.

Fig. 6.

The process of MTC in ProVerif

Fig. 7.

The process of MME in ProVerif

Fig. 8.

The process of HSS in ProVerif

B Implementation and Analysis in OAI

The configuration used by our patched version of OAI is depicted in Fig. 9. It includes three virtual machines running Linux inside a single host Intel Core i7 processor with 4GB RAM. In particular, one machine (VM1) runs the Openairinterface5G module that simulate an MTCdevice and the eNodeB base station. The other two machines (VM2 and VM3) run the OPENAIR-CN module. Note that OAI does not currently support multiple MTC device, namely the Openairinterface5G module include only a device. However, we can run multiple runs of Openairinterface5G module in different machines to instantiate several MTC devices at cost of instantiating the same number of base stations.

Fig. 9.

Minimal network configuration needed for our patched version of OAI.

The communication between MTC device, MME, and HSS are performed through Ethernet interfaces. The communication between MTC device and eNodeB is done within VM1 and represents the S1-U interface in the 3GPP standard. The channel between VM1 and VM2 represent the S1-MME interface according the standard. VM3 is dedicated to the HSS, which uses a MySQL server for the storage of subscriber data.

1.1 B.1 Parameters

Some terms have no similar counterpart in the existing standards so we design them from scratch. This is the case of the two auxiliary parameters tree height and node depth. The first gives the height $\mathcal {H}$ of the inverted hash trees. It is used as an indicator of how many bits of the path should be used. This parameter is needed because the path is communicated in full bytes even though the size of the actual path might not be divisible by eight. We thus specify that the size of tree height is one byte. The parameter node depth gives the level on which the sub-root nodes $\textsc {gk}_{\text {ij}}$ and $\textsc {ch}_{\text {ij}}$ are placed in the inverted hash trees. The knowledge of path, tree height, and node depth allows the MME to deduce the structure of the inverted hash tree and to assess whether next MTC devices can be served according Case A or Case B.

Table 4. Sizes of parameters of EPS-AKA and group-based AKA at NAS level.

To compute the bandwidth consumption at NAS level, we consider the parameters and the sizes described in Table 4. We recall Eqs. 1 and 2 concerning the bandwidth consumption for the group-based protocol for the NAS and the S6a interface.

The bandwidth consumption for EPS-AKA at NAS level is

(3)

Table 5. Sizes of parameters of EPS-AKA and group-based AKA in the S6A interface.

Regarding the bandwidth consumption for the S6A interface, Diameter adds to each parameter 12 bytes for header and flags. Hence, the size of parameters are bigger in S6A interface than in NAS. The values of the parameters are synthesized in Table 5. The bandwidth consumption for EPS-AKA can be computed as

(4)

Fig. 10.

Bandwidth consumption comparison between EPS AKA and the group-based AKA on the NAS.

Fig. 11.

Bandwidth consumption comparison between EPS AKA and group-based AKA on the S6a interface

Fig. 12.

Increase in NAS bandwidth consumption and decrease in S6a bandwidth consumption when the group-based AKA is used instead of EPS-AKA.

Figure 10 shows that the group-based AKA has more bandwidth consumption than the EPS-AKA at NAS level. This is because the attach request message in the group-based AKA includes the parameters path and noncein addition to the standard parameters. However, the bandwidth consumption rate is inverted in the S6a interface, as described in Fig. 11. The group-based AKA consumes less bandwidth already when more than two MTC devices are considered. Notably, when the number of MTC devices to be served are more then three, the overall bandwidth consumption of group-based AKA is less than the one of EPS-AKA. This is depicted in Fig. 12.