Keywords

1 Introduction

A consistent threat to the various generations of cellular communications technologies is the deployment of malicious radio nodes called international mobile subscriber identity (IMSI) catchers to undermine the identities and locational privacy of user equipment. As the technology has developed over several generations, the cellular communications trust model has matured by moving as much of the information passed between user equipment and legitimate radio nodes to after they have mutually authenticated their identities [9]. However, an adversary always has an advantage because the standards require user equipment to connect to the strongest signal in a network. Specifically, the adversary can jam legitimate signals to force user equipment in the vicinity to connect to it.

In fact, adversaries have several ways of circumventing 5G network security controls because implementations are required to serve previous generations of cellular technologies that have weaker security controls, and security vulnerabilities have been discovered during the development of the 5G standard. Relying on encryption to protect transmitted information creates a security bottleneck – if encryption fails, the 5G security guarantees are undermined. Building additional security protections in the 5G standard to prevent or respond to the deployment of IMSI catchers in an administrative area would increase the privacy protection offered to user equipment.

Research has been undertaken to detect IMSI catcher deployments. Several signatures have been proposed to identify their malicious activity and the 5G standard mandates the use of information from user equipment to detect if an IMSI catcher is operating in an administrative area. However, these are weak responses to attacks because IMSI catchers are detected only after they have successfully connected to user equipment. Responding to adversaries before they connect to user equipment decreases the likelihood that the privacy guarantees of the 5G standard would be violated.

This chapter presents a distributed consensus algorithm that builds an additional layer of defense in the 5G standard that would restrict the deployment of IMSI catchers in an administrative area. The solution requires that specific network semantics be maintained to create a contextual integrity property. Although this property is weaker than cryptographic integrity, it enables intrusion detection to be focused by reducing the semantic space that must be surveyed. The property depends on the fact that a 5G control network has access to a greater number of legitimate radio nodes in a particular administrative area than an adversary, and will be able to form a consensus on whether or not a new radio node is malicious. This enables a 5G system operator to control the mobility of radio nodes in an administrative area.

The consensus processes leverage the 5G broadcast network semantics so that radio nodes can interrogate a new radio node in an administrative area. The goal is to warn user equipment in the administrative area not to connect to an IMSI catcher in advance of it exploiting vulnerabilities. The algorithm can detect adversaries that present themselves as new radio nodes or masquerade as legitimate radio nodes, as well as adversaries that have conducted passive reconnaissance to detect legitimate radio nodes. The algorithm uses existing infrastructure and communications models in the 5G standard to perform its interrogation.

The algorithm is presented as a \(\pi \)-calculus process algebra that expresses how mobile multiagent distributed systems concurrently pass messages and communications channels between themselves. The \(\pi \)-calculus also models modifications to radio node and control network agents to enable them to interrogate and form a consensus on adversary presence, as well as the ability of user equipment to form a consensus on whether or not to act on alerts. The algorithm is verified using \(\pi \)-calculus equivalence relations to demonstrate that the added consensus messages are distinguishable from those sent by an adversary simulating a radio node and that deadlocks are not created during the user equipment registration procedure.

The algorithm reduces the likelihood of privacy violations [13] should the 5G encryption model be compromised because it enables the network to automatically instruct user equipment not to establish connections with suspicious radio nodes. Incorporating the automatic response in the 5G standard would enable IMSI catchers to be ejected from a network before they connect with legitimate user equipment, independent of the organizational policies of 5G implementations. Implementing the consensus algorithm also benefits 5G security controls because they can leverage the anomalies detected by sensor-based and network-based IMSI catcher detection solutions directly in the standard. The consensus algorithm also increases the amount and the uncertainty of reconnaissance conducted by adversaries because they are more likely to be detected as they attempt to identify legitimate radio nodes.

2 Related Work

This section reviews the different kinds of IMSI catchers and their countermeasures. The goal is to extract adversary capabilities that can be used to formulate the adversary model in this research. The primary security concern of the cellular communications infrastructure is to prevent breaches of identity and locational privacy of user equipment.

Park et al. [14] analyzed the capabilities of IMSI catchers that were being sold to governments in 2019. Some of the devices they studied passively listened on unencrypted public channels to discern the temporary identifiers of user equipment during the registration procedure. Active IMSI catchers act as radio nodes. By exploiting various protocol vulnerabilities, they are able to intercept permanent identifiers and track user equipment, and potentially eavesdrop on communications if they can compromise the control network. An IMSI catcher can force a connection in various ways. Some devices jam the frequency bands of legitimate radio nodes in an attempt to force connections with user equipment in an administrative area. Other devices can automatically forge the identities of nearby radio nodes before attempting to intercept user equipment. Another way to undermine privacy is to force a downgrade to a more insecure communications standard during the negotiation of the ciphertext suite. The option to downgrade is possible due to the backward compatibility requirements that include LTE and earlier standards. Shaik et al. [16] leveraged a 4G protocol vulnerability that enabled the modification of the stated capabilities of user equipment to cap the data transmission rate and drain battery power.

Several vulnerabilities have been discovered in the 5G-AKA key protocol during its development. Cremers and Dehnel-Wild [3] employed a Tamarin symbolic protocol tester to assess a protocol draft, discovering a replay attack that enables an attacker to receive user equipment keys by swapping uplink control information (UCI). Borgaonkar et al. [2] demonstrated that an adversary could steal the IMSI or subscription permanent identifier of user equipment in a replay attack because the user equipment portion of the encryption protocol does not employ randomness [2]. Basin et al. [1] also used Tamarin to demonstrate that the 5G standard had various under-defined notions of authentication that enable an adversary to replay keys and violate forward secrecy.

Several methods have been developed for assessing the risks posed by IMSI catchers. Yocam et al. [19] developed a risk assessment methodology for analyzing the trade-offs between IMSI catcher security and risk, enabling 5G implementers to select cost-effective security controls. They assessed the effects of incorrect security implementations as well as the ability of security controls to combat legacy downgrade, denial-of-service and message interception attacks. Khan et al. [10] proposed a pseudonym scheme for 4G networks, like the 5G subscription permanent identifier, to prevent identity leaks during user equipment registration. This would also increase the security of the 5G standard, because if a backward compatibility attack is discovered, the 4G standard would have additional cleartext security.

Sensor-based methods identify anomalies in publicly-broadcasted channels. The methods cannot survey dedicated channels between user equipment and radio nodes [14]; instead, they look for misconfigured or new radio nodes. Examples of sensor solutions are sICC [5] and SITCH [20].

Network-based IMSI catcher detection schemes attempt to identify adversaries by the artifacts they leave in communications networks. However, they require the cooperation and information sharing from network operators, which is not always guaranteed [14]. Steig et al. [17] proposed a detection scheme for identifying active and passive IMSI catchers in 4G networks. The scheme measures the locations of known radio nodes in an area; since legitimate radio nodes rarely change their locations, alarms are raised if their positions have changed. Dabrowski et al. [4] developed a rubric for identifying signs of IMSI catchers. Their scheme detects anomalies in user equipment registration when an attacked device reconnects with a legitimate network. They also propose the use of radio nodes and sensors to listen to registration procedures in order to detect malicious cipher downgrades.

A number of IMSI catchers have been developed or theorized in the literature. Passive IMSI catchers are sensors that gather publicly-broadcasted information before targeted user equipment has been authenticated whereas active IMSI catchers exploit vulnerabilities to trick user equipment into believing they are legitimate radio nodes. Regardless of the type of IMSI catcher, the primary objective of the adversary is to extract the unique identities of user equipment to undermine their privacy. Secondary objectives include tracking user equipment and eavesdropping on communications. Various means for forcing connections with user equipment are possible, including jamming the signals of legitimate radio nodes. While the 5G standalone mode resolves the historical attack vectors, vulnerabilities exist that can be exploited by a dedicated adversary [9].

Inherent to all the countermeasures is the requirement that 5G network operators have procedures to eject IMSI catchers from their networks after they are detected. However, none of the methods automatically remove adversaries from networks; they only inform the operators of the presence of IMSI catchers.

3 5G Defense in Depth

This section describes the 5G registration procedure and specifies an adversary model that is employed as the foundation of the contextual integrity property. The section also describes the boundaries that must be maintained for the consensus algorithm to successfully mitigate IMSI catchers and provide tighter mobility control in 5G networks. The consensus algorithm, which is constructed from pre-existing communications models used during the user equipment registration procedure, is described along with certain modifications.

Fig. 1.
figure 1

Session diagram of the 5G registration procedure [6].

Full size image

3.1 5G Device Registration Procedure

Figure 1 shows the 5G registration procedure [6]. The procedure, which involves three participants across multiple communications models, has more than 100 steps. This research models Step 2 in the procedure up to the establishment of an encrypted communications channel between user equipment (UE) and a radio node (gNB). All the communications between the agents from the new access and mobility management function (AMF) onwards are treated as a single agent because they constitute various parts of the control network (CN). Steps 12 to 20 are beyond the scope of the model because neither the user equipment nor the radio node can see their transitions in the network.

The first stage is to establish radio communications between the user equipment and radio node. The radio resource control (RRC) procedure establishes the connection between the two devices. The user equipment messages the radio node and begins a timer to complete the handshake. The radio node then sends the frequency of a direct communications channel and requests a temporary identifier from the user equipment. After switching to the new channel, the radio node sets up the signal radio bearer (\(SRB_1\)) and sends it to the user equipment in a RRCSetup message. This message contains the MAC address of the radio node. Following this, the radio node informs the new access and mobility management function that the user equipment wishes to connect to its administrative area. This function negotiates the transfer of the security context of user equipment from the access and mobility management function of the old radio node to the access and mobility management function of the new radio node. This function is omitted from the model because it does not contribute to channel encryption.

The new access and mobility management function begins a series of security checks via the radio node to authenticate the user equipment. First, it requests a subscription permanent identifier (SUPI) from the user equipment, which is a concatenation of the mobile country code (MCC), mobile network code (MNC) and IMSI number of the user equipment. Next, the 5G-AKA protocol [8] is executed to enable the user equipment and radio node to authenticate each other’s keys. The two authentication checks are condensed to one step in the formal model presented in the next section.

At this point, the new access and mobility management function performs a series of checks to ensure that the user equipment is permitted to operate in the administrative area. These are beyond the scope of this work. After the access and mobility management function confirms that the user equipment is allowed to operate, it informs the radio node to proceed with the negotiation of the security mode (SM) function to create the encrypted channel. The radio node sends a session key and requests a ciphertext suite. The user equipment then responds and the encrypted channel is established.

3.2 Active Adversary Model

IMSI catchers are passive or active. Since passive devices do not participate in a network, this work focuses on an adversary with an active IMSI catcher. The goal of the algorithm is to prevent the adversary from completing a registration procedure with user equipment in an administrative area. Therefore, the modeled adversary does not have the ability to jam legitimate radio node signals. Since the proposed defense-in-depth mechanism is intended to provide additional security to 5G systems via the contextual integrity property, it is explicitly assumed that the adversary has cryptanalytic functions that have broken the 5G-AKA protocol. In order to intercept the identity of user equipment, it is assumed that the adversary can simulate messages sent by the radio node and control network during the registration procedure. The security model assumes that the adversary has not compromised any of the other radio nodes in the network and, therefore, cannot manipulate the internal state of other agents except via the messages they transmit. The model also assumes that the adversary has conducted passive network reconnaissance to identify legitimate radio nodes.

3.3 Contextual Integrity Property

The consensus algorithm described in the next section will not prevent all attempts to undermine the privacy promises of the 5G standard. Its purpose is to delay privacy violations by adding an additional defense-in-depth layer should the 5G-AKA protocol be broken. It also makes the reconnaissance phase of an attack more limited and precarious by forcing the adversary to only listen to traffic in a passive manner. The algorithm provides a mechanism for the control network and legitimate radio nodes to control radio node mobility in an administrative area. All this is achieved, through the monitoring and control of network semantics that remain immutable via intrusion detection systems, in order to construct the contextual integrity property.

Since the devices operate in a wireless network, they can only see messages sent and received by other devices in the coverage area provided by the radio node. There is no guarantee that user equipment will observe the state transition of any device with which it communicates. But this does mean that it can observe messages of agents with which it is not in direct communication. Additional model simplifications are that only the sending and receiving of messages cause state transitions in a device and all messages are assumed to be sent on a reliable channel.

As stated in Sect. 3.2, it is assumed that the adversary has broken the 5G-AKA protocol, but does not have access to the radio node/control network communications public key infrastructure (PKI). This will be proved in Sect. 6. The representation of the adversary’s cryptanalytic capabilities is expressed in Sect. 4 as \(K_m=K_{AC1}\). Since the adversary has compromised the 5G-AKA protocol, the consensus algorithm only works if the number of legitimate radio nodes \(N_{gNB}\) is greater than the number of malicious/imitated radio nodes set up by the adversary \(N_{A}\), i.e., \(N_{gNB} > N_{A}\). If the adversary employs more radio nodes than the legitimate network, it would be able to use the consensus algorithm to establish connections with user equipment. However, this requires more resources and coordination than merely deploying a jammer.

An implicit race condition exists in the consensus algorithm. This is borne from the real-time requirements of some 5G communications models involved in the user equipment registration procedure [7]. Computing the overhead and timing of a successful consensus is beyond the scope of the proposed model.

Fig. 2.
figure 2

Network topology facilitating the consensus algorithm.

Full size image

3.4 Defense-in-Depth Consensus Algorithm

The consensus algorithm depends on multiple radio nodes to control radio node mobility in an administrative area via an interrogation process. The interrogation process begins when a new radio node cannot be reached via the public key infrastructure of the radio node. Figure 2 shows the relationships between the agents in the interrogation process. Upon detecting an unreachable radio node, the legitimate radio nodes interrogate it by pretending to be user equipment. They begin their own radio resource control procedures to gain the adversary’s MAC address from its \(SRB_1\) messages. If the unreachable radio node is an IMSI catcher, two things can occur. If all the legitimate radio nodes do not recognize the adversary’s MAC address, they form a consensus between themselves and page warnings to user equipment in their administrative area. However, if only one legitimate radio node recognizes the adversary, then the radio nodes that do not recognize it query the control network to resolve the deadlock. If the control network does not recognize the adversary, it informs the querying radio node, which proceeds to page its warning and instruct other legitimate radio nodes to do this as well.

Another possibility described in the adversary model is to impersonate the MAC address of a legitimate radio node. If the radio node recognizes this during an interrogation, it immediately pages its warning and messages the control network to coordinate with another radio node in the area to do this as well.

A final possibility is when the adversary has deduced which user equipment are actually radio nodes. In this case, when the adversary refuses to connect, the radio node waits for the adversary to use its 5G-AKA key during an observed radio resource control procedure and intercept the key. The radio node then pages its warning containing this key instead of the MAC address and tells the control network to coordinate another warning page.

User equipment has its own consensus algorithm to decide how to respond to paged warnings. As long as the conditions in the previous section are met, user equipment receives two paged warnings from different radio nodes containing either the adversary’s MAC address or 5G-AKA key. After the consensus is reached, the user equipment disconnects and restarts its registration procedure. The user equipment portion of the radio resource control and non-access stratum (NAS) procedures are modified to check that they do not reconnect to the adversary.

4 \(\pi \)-Calculus Model of 5G Registration

This section lays the foundation for the defense-in-depth consensus algorithm. The qualitative description of the 5G registration procedure in Sect. 3.1 is formally specified as a \(\pi \)-calculus. The adversary model and contextual integrity property are also formalized.

Note that only the relevant \(\pi \)-calculus results are presented. These include the \(\pi \)-calculus operations used to describe the communications models of processes that represent agents in the 5G registration procedure and defense-in-depth mechanism. Interested readers are referred to Milner et al. [11, 12] and Sangiorgi and Walker [15] for details about the \(\pi \)-calculus.

4.1 \(\pi \)-Calculus Semantics

The \(\pi \)-calculus expresses the evolution of concurrent processes in a distributed system as they pass names among themselves. The names represent variables or communications channels. The \(\pi \)-calculus operations used to model the consensus algorithm are:

$$\begin{aligned} P::=\bar{x}y.P\; |\; x(z).P\; |\; \nu z\; z.P\; | \;\tau .P\; |\; P|P'\; |\; P+P'\; |\; [x=y].xP\; |\; \bar{0} \end{aligned}$$

where P represents a subsequent process or the underlying state machine of a device.

The operations are described as follows:

  • \(\mathbf {\bar{x}y.P:}\) Process P sends name y on channel x.

  • \(\mathbf {x(z).P:}\) Process P receives name z on channel x. Any subsequent z actions in process P are replaced by input z.

  • \(\mathbf {\nu z\; z.P:}\) A restriction of name z where sending or receiving on channel z can only occur if the involved process P already knows name z exists.

  • \(\mathbf {\tau .P:}\) Silent action \(\tau \) representing an action internal to process P that results in no name being sent or received.

  • \(\mathbf {P|P':}\) Composition of processes P and \(P'\) that can occur concurrently.

  • \(\mathbf {P+P':}\) Summation of processes P and \(P'\) representing the selection of one of the two processes.

  • \(\mathbf {[x=y].xP:}\) Matching of names x and y representing an if-then statement in the distributed system.

  • \(\mathbf {\bar{0}:}\) Null process \(\bar{0}\) takes no further action.

The processes evolve via communications with other intra-agent processes or with the environment (i.e., processes external to the process being analyzed).

4.2 Formalized 5G Registration Procedure

The 5G registration procedure must be completed for user equipment to communicate with a radio node gNB.

The user equipment process UE during the registration procedure is defined as:

$$\begin{aligned} UE = RRC_u.AMFS_u.NAS_u.SM_u \end{aligned}$$

which performs the explicit operations:

$$\begin{aligned} \begin{aligned} UE=\bar{p}_{int}.p(c).\bar{c}\;TID.c(s).\bar{c}\;fin.\\ c(er).\bar{c}\;eid.\\ c(K).[K=K_{AC1}]\bar{c}\;K_{AC2}.\\ c(k).\bar{c}\;fin.SESSION_u \end{aligned} \end{aligned}$$
(1)

The radio node process gNB during the registration procedure is defined as:

$$\begin{aligned} gNB=RRC_g.AMFS_g.AMF_g.SM_g \end{aligned}$$

which performs the explicit operations:

$$\begin{aligned} \begin{aligned} gNB=p(i).\bar{p}\;dc.dc(t).\bar{dc}\;SRB_1.dc(f).\\ \bar{sec}\;dc.\\ sec(a).\\ \bar{dc}\;K_{sesh}.dc(f).SESSION_g \end{aligned} \end{aligned}$$

The control network process CN during the registration procedure is defined as:

$$\begin{aligned} CN=AMFS_c.NAS_c.AMF_c \end{aligned}$$
(2)

which performs the explicit operations:

$$\begin{aligned} \begin{aligned} CN=sec(ci).\bar{ci}\;eidr.ci(i).\\ \bar{ci}K_{AC1}.ci(K).[K=K_{AC2}].\\ \bar{sec}\;ack \end{aligned} \end{aligned}$$

The radio node process gNB and control network process CN are composed into a singular process to represent their wired communications during the registration procedure. This is represented as:

$$\begin{aligned} HS=\nu \;sec\;gNB|CN \end{aligned}$$
(3)

where sec represents the encryption of gNB and CN communications using a public key infrastructure.

4.3 Active Adversary Model

The adversary model must simulate the outbound messages of the radio node’s \(RRC_g\) and \(SM_g\) processes, along with the control network’s \(AMFS_c\) and \(NAS_c\) processes. The communications models are represented as the process:

$$\begin{aligned} A_o=RRC_g.AMFS_c.NAS_c.SM_g \end{aligned}$$

which performs the explicit operations:

$$\begin{aligned} \begin{aligned} A_o=p(i).\bar{p}\;dc.dc(t).\bar{dc}\;SRB_M.dc(f).\\ \bar{dc}\;eidr.dc(i).\bar{dc}\;K_M.dc(K).\bar{dc}\;K_{sesh}.dc(f).INTERCEPT \end{aligned} \end{aligned}$$

The cryptanalytic capability of the adversary is expressed by making the names \(K_m = K_{AC1}\) when parsed by the user equipment process UE.

4.4 Formalized Contextual Integrity Property

The following theorem formally states the property that enables the defense-in-depth process to control the mobility of radio nodes in an administrative area.

Theorem 1:

If the assumptions in Sect. 3.4 hold, then the contextual integrity property is maintained if and only if the adversary never learns the name sec and cannot distinguish between a user equipment registration process and a radio node interrogation process.

Theorem 1 is proved using the results in Sects. 6.6 and 6.8.

5 Formalized Consensus Algorithm

This section presents the modified 5G processes that create the consensus algorithm before presenting the semantic artifacts that a 5G intrusion detection system can leverage to detect violations of mobility control in an administrative area.

The modifications to the user equipment process UE enables it to form a consensus from the paged warnings broadcast by multiple radio node processes when they have detected an adversary in the administrative area.

The modifications to the radio node process gNB enable it to pretend to be user equipment that attempts to connect with the adversary if it cannot be reached via the public key infrastructure. The radio node process interrogates the adversary via a modified user equipment registration process or it passively intercepts the adversary’s credentials that are transmitted publicly.

The modifications to the control network process CN enable it to respond to queries from deadlocked radio nodes and coordinate the immediate warning pages if the adversary is imitating a radio node or refuses to be interrogated.

The formalization of this defense-in-depth mechanism assumes that a process transitions through its state machine by maintaining strictly ordered traces. Also, messages are transmitted on a reliable channel.

The formalization treats the user equipment, adversary and radio node/con- trol network combination as three distinct entities. The communications between radio nodes and the control network are treated as intra-process communications.

5.1 UE Process Modifications

The modified form of the UE process is:

$$\begin{aligned} UE_m = RRC_{um}.AMFS_u.NAS_{um}.SM_u \end{aligned}$$

where processes \(RRC_{um}\) and \(NAS_{um}\) are modified in the event the registration process is re-attempted.

The UE process is modified to receive and act on warning pages from legitimate radio node processes. The consensus process can be inserted between any part of Eq. 1 up to the \(\bar{c}\;fin\) operation to maintain the contextual integrity property. This is achieved using the \(\pi \)-calculus abstraction of a context hole [.] placed anywhere in a process before its conclusion. A context hole enables another process to be inserted into a process being studied [15]. The UE consensus process is given by:

$$\begin{aligned} b_i(s_i,n_i).b_j(s_j,n_j).[s_i=s_j]RRC_{um} \end{aligned}$$
(4)

where \(s_{i,j} = SRB_m \vee K_m\) and \(n_i\) is a nonce from the radio node process \(gNB_i\).

The UE process portion of the registration must also be modified to act on any warning that passes the consensus. This requires its \(RRC_u\) and \(NAS_{u}\) processes to be modified.

The modified form of the \(RRC_u\) process is:

$$\begin{aligned} RRC_{um}=\bar{p}_{int}.p(c).\bar{c}\;TID.c(s).([s=s_i]RRC_{um}+\bar{c}\;fin) \end{aligned}$$

If the UE process ends up reconnecting with the adversary, it begins the process again until it connects with a legitimate radio node.

The modification to the \(NAS_u\) process is required if the adversary refuses to participate in the interrogation process. The adversary still has to broadcast its 5G-AKA key as cleartext [6], enabling a radio node process to intercept it. The UE process can, therefore, perform a consensus on the malicious keys. Hence, the reconnection algorithm also needs to begin when the key verification takes place.

The modified form of the \(NAS_u\) process is:

$$\begin{aligned} NAS_{um}=c(K).([K=K_M]RRC_{um}+\bar{c}\;K_{AC2}) \end{aligned}$$

5.2 gNB Process Modifications

This section describes the additional processes incorporated in a radio node process gNB that enable it to interrogate a new radio node that it cannot connect to using the name sec. The interrogation processes enable the radio node to control mobility in its administrative area. The modified form of the gNB process is:

$$\begin{aligned} \begin{aligned} gNB_i=RRC_g.AMFS_g.AMF_g.SM_g|\\ RRC_{ugs}.(([s=\emptyset ]R_g+D_g)|I_g|B_g) \end{aligned} \end{aligned}$$
(5)

The interrogation begins with the radio node process gNB simulating the \(RRC_u\) process of user equipment UE. Next, gNB attempts to form a local consensus using the MAC address obtained from the \(SRB_m\) message. However, if the adversary refuses the interrogation, gNB enacts the \(R_g\) process to intercept the adversary’s 5G-AKA key.

The simulated form of process UE is modified with a composite process to pass \(SRB_m\) securely to the gNB/CN process from the environment. This is given by:

$$\begin{aligned} RRC_{ugs}=\bar{p}_{int}.p(c).\bar{c}\;TID.c(s).(\bar{c}\;fin|\bar{bo}\;s) \end{aligned}$$

If the adversary refuses to engage in the interrogation, the radio node process gNB listens for the adversary to use the communications channel dc in any of its handshakes with user equipment. This is the channel in the \(NAS_c\) process where the control network passes its 5G-AKA key to user equipment. After the key has been intercepted, the gNB process simultaneously pages its warning to all user equipment and messages the control network to coordinate with another radio node to page another warning:

$$\begin{aligned} R_g=dc(K_s).(\bar{sec}\;K_s,reject|bo_i\;K_s)+sec(K,r).\bar{bo_i}\;K \end{aligned}$$

If the adversary engages with the interrogation process, the radio nodes attempt to resolve the consensus locally. The four possible algorithm terminations of the interrogation are ordered as expressed in Eq. 6 below:

  • Both radio nodes recognize the interrogated radio node and leave it to its operations.

  • One radio node recognizes the interrogated radio node, but the other radio node does not. In this case, the recognizing radio node waits for the other radio node interrogator to resolve the deadlock by sending a query to the control network. If the control network recognizes it, the deadlocked radio node informs the other radio node to terminate. Otherwise, both radio nodes page warning messages.

Equation 6a expresses the two ways a radio node can recognize an interrogated device whereas Eq. 6b expresses the two ways a radio node can ban an interrogated device:

$$\begin{aligned} \begin{aligned} D_g=[s=known][(sec(s',c).[s'=s].\bar{sec}\;s',conf|\bar{sec}\;s,conf.sec(s',c))+\\ (sec(s',a).[s'=s].\bar{sec}\;s',conf|\bar{sec}\;s,conf.sec(s',a)).\\ (sec(s,c)+sec(s,a).\bar{bo_i}\;s)] \end{aligned}\end{aligned}$$
(6a)
$$\begin{aligned} \begin{aligned} +[(sec(s',a).[s'=s].\bar{sec}\;s',alerta|\bar{sec}\;s,alerta.sec(s',a)).\bar{bo_i}s+\\ (sec(s',c).[s'=s].\bar{sec}\;s',alerta|\bar{sec}\;s,alerta.sec(s',c)).\bar{sec}\;s,query.\\ (sec(s,c).\bar{sec}\;s,conf+sec(s,a).(\bar{sec}\;s,alerta|\bar{bo_i}s))] \end{aligned} \end{aligned}$$
(6b)

  • Both radio nodes do not recognize the interrogated radio node and page warnings to user equipment in the area.

  • One radio node recognizes the interrogated radio node, but the other radio node does not. In this case, the recognizing radio node waits for the other radio node interrogator to resolve its deadlock by sending a query to the control network. If the control network does not recognize it, the deadlocked radio node pages a warning and instructs the other radio node interrogator to do this as well.

Each of the use cases that a radio node consensus can follow is distinguished by the \(+\) summation operation.

The \(I_g\) process exists in the event that a radio node realizes that the \(SRB_m\) it received during the interrogation is imitating its identity. In this case, the imitated radio node simultaneously pages its warning and informs the control network to immediately coordinate a second paged warning. The \(I_g\) process is defined as:

$$\begin{aligned} I_g=sec(su,i).\bar{bo_i}\;su+[s=me].(\bar{sec}\;s,imitation|\bar{bo_i}\;s) \end{aligned}$$

Process \(B_g\) expresses a radio node paging all user equipment not to connect to a device with a given \(SRB_m\) or \(K_m\):

$$\begin{aligned} B_g=bo_i(s).\bar{b_i}\;s,n_i \end{aligned}$$

As stated in Sect. 3.4, the contextual integrity property is maintained if one of the \(D_g\), \(I_g\) or \(R_g\) processes is terminated by two radio nodes before the adversary completes its registration process simulation with a targeted user equipment.

5.3 CN Process Modifications

The control network participates in the defense-in-depth mechanism as a consensus deadlock breaker and coordinator of paged warnings for urgent violations of mobility control in an administrative area, such as the detection of radio node imitation or an adversary refusing interrogation. The modified form of the CN process defined in Eq. 2 is:

$$\begin{aligned} CN_{m}=AMFS_c.NAS_c.AMF_c|I_c|Q_c|R_c \end{aligned}$$

The \(Q_c\) process resolves the deadlock if one radio node recognizes an interrogated device, but another radio node does not. The radio node that does not recognize the name \(SRB_m\) queries the control network. The control network responds to the querying radio node to resolve the deadlock and allow for consensus termination. The \(Q_c\) process is specified as:

$$\begin{aligned} Q_c=sec(s,q).([s=known]\bar{sec}\;s,confirm+\bar{sec}\;s,alerta) \end{aligned}$$

The processes \(I_c\) and \(R_c\) ensure that user equipment receives multiple paged warnings:

$$\begin{aligned} I_c=sec(s,i).\bar{sec}\;s,imitation \end{aligned}$$
$$\begin{aligned} R_c=sec(k,r).[k=\bar{known}]\bar{sec}\;K,reject \end{aligned}$$

Specfically, processes \(I_c\) and \(R_c\) coordinate a second radio node page to user equipment so that the consensus process in Eq. 4 can terminate. In the case of the \(R_c\) process, the control network only sends the message if it does not recognize the adversary’s key \(\bar{known}\).

5.4 gNB-CN Process Coordination Modification

The process that models the intra-process communications between a radio node and control network is modified to include the extra radio node necessary for the consensus algorithm. The DiD process is specified as:

$$\begin{aligned} DiD = \nu \;sec,bo_i,bo_j\;CN_{m}|gNB_i|gNB_j \end{aligned}$$
(7)

5.5 Intrusion Detection Artifacts

Provided that the defense-in-depth consensus can terminate before an adversary can connect to targeted user equipment and the assumptions in Sect. 3.3 hold, the algorithm is able to maintain the contextual integrity property by identifying either the adversary’s MAC address in the \(SRB_1\) message or the key \(K_m\) it uses in the simulated 5G-AKA protocol. These artifacts can be used by intrusion detection systems to identify unauthorized agents that attempt to broadcast in an administrative area instead of waiting for signs of compromise to be discerned from artifacts due to user equipment reconnecting to the legitimate network after the IMSI catcher has released them.

6 Consensus Algorithm Equivalence Proofs

This section presents several proofs that collectively construct the contextual integrity property. The proofs demonstrate that, as long as the assumptions in Sect. 6.2 hold, the adversary can only intercept traffic or imitate a radio node if it wins a race condition. This occurs regardless of whether or not it has broken the 5G-AKA protocol.

The first section introduces the \(\pi \)-calculus process transitions and behavioral equivalences that are used to prove the contextual integrity property. Also, it presents the assumptions underlying the proofs.

The first proof demonstrates the indistinguishability between the cryptanalytic adversary and 5G registration process. The next proof shows that the adversary process cannot tell the difference between user equipment and a radio node that interrogates user equipment. The subsequent proofs demonstrate the termination of the user equipment consensus process (and registration renegotiation after it has been warned), and that user equipment can distinguish between the defense-in-depth process DiD and adversary process \(A_o\). The final proof shows that, given the assumptions, the adversary will not learn the name sec from the consensus algorithm and, thus, gain access to the gNB-CN intra-process communications.

These proofs collectively demonstrate that the consensus algorithm maintains the contextual integrity property described in Sect. 4.4.

6.1 Weak Transitions and Bisimulation

In the \(\pi \)-calculus, processes are compared using behavioral equivalences that examine process semantics to see if they are indistinguishable to an external observer. The primary equivalence used in the \(\pi \)-calculus is bisimulation, which compares process inputs and its internal transitions [15]. An example of internal process transitions is the messages passed between the radio node process gNB and control network process CN in Eq. 3.

Whether or not two processes are bisimilar can be viewed as a game between two observers [18]. An observer randomly selects one of the two processes being compared and transitions its state via the receipt of an input or an internal state transition. The other observer attempts to make the same transition on the other process with the same input/internal transition. The two processes are bisimilar if the game can run forever or the processes reach a configuration of inputs/internal transitions that has been encountered before. Otherwise, the processes are not bisimilar because the second observer is unable to copy the transition of the first process.

The equivalence proofs in this section use weak bisimulation (\(\approx \)) that relaxes the rule on comparing internal transitions [15]. In this bisimilarity, the observer cannot discern the number of internal transitions performed by a process. Zero or a positive number of internal transitions could have occurred between a process receiving inputs.

Weak bisimulation is used due to Assumption 2 in the next section. It is not guaranteed that a process can physically observe the transitions of other processes due to geographical separation. Therefore, the security of the system must be derived from the messages that processes send and receive.

6.2 Assumptions

All the proofs in this section are predicated on the assumptions in Sect. 3.3 and the introduction to Sect. 5. The assumptions are:

  1. 1.

    The state machines underlying the processes described in Sect. 5 maintain strictly ordered traces with no errors and their messages are transmitted on reliable channels.

  2. 2.

    A process can only see messages sent and received by other processes, not their internal state transitions.

  3. 3.

    Only the sending or receiving of messages cause state transitions to a process.

  4. 4.

    The adversary process has broken the 5G-AKA protocol \(K_M=K_{AC1}\) for user equipment, but does not have access to the radio node/control network communications public key infrastructure.

  5. 5.

    There are more legitimate radio nodes than malicious/imitated adversary radio nodes, i.e., \(N_{gNB} > N_{A}\).

6.3 Adversary and Registration Process Indistinguishability

The need for the defense-in-depth consensus algorithm is predicated on user equipment being unable to distinguish between a cryptanalytic adversary (IMSI catcher) simulating the messages emitted by the gNB/CN process and the gNB/CN process itself. Given the formalized adversary in Sect. 4.3 and the assumptions in Sect. 6.2, this section proves that the UE process cannot distinguish between the two processes given only the messages it receives. The direct proof below is truncated to start after \(RRC_g\) because the two processes do not differ until this point. The truncated adversary simulation process presented in Sect. 4.3 is:

$$\begin{aligned} A_o = \bar{dc}\;eidr.dc(i).\bar{dc}\;K_M.dc(K).\bar{dc}\;K_{sesh}.dc(f) \end{aligned}$$

and the truncated form of Eq. 3 is:

$$\begin{aligned} HS = \nu \;sec\;\bar{sec}\;dc.sec(a).\bar{dc}\;K_{sesh}.dc(f)| \end{aligned}$$
(8a)
$$\begin{aligned} sec(ci).\bar{ci}\;eidr.ci(i).\bar{ci}K_{AC1}.ci(K).[K=K_{AC2}]\bar{sec}\;ack \end{aligned}$$
(8b)

where Eqs. 8a and 8b express represent the gNB and CN processes, respectively.

Proposition 1:

The processes HS and \(A_o\) are indistinguishable to an observing UE process.

Proof:

Table 1 shows the comparison of the process transitions of the two processes. In transitions 1 and 6, HS has multiple internal actions that are not observed by the UE process whereas \(A_o\) has none. Therefore, the two processes are weakly bisimilar, i.e., \(A_o \approx HS\).   \(\square \)

Table 1. Reduction procedure of the \(A_o\) and HS processes.
Full size table

6.4 UE Registration and gNB Interrogation Process Indistinguishability

For the defense-in-depth consensus algorithm to control the mobility of radio nodes in an administrative area and deny IMSI catchers, the adversary must not be able to distinguish between a UE process and a gNB interrogation process. The only way the adversary could distinguish the processes is through prior reconnaissance. A weak bisimulation must be proven between the UE’s \(RRG_u\) process and the gNB’s modified \(RRC_{ugs}\) process to demonstrate the indistinguishability. This proof uses the same method as the previous section and focuses on the last transition because the two processes are identical until then.

Proposition 2:

The \(RRG_u\) and \(RRC_{ugs}\) processes are indistinguishable to an observing \(A_o\) process.

Proof:

Table 2 shows the comparison of the last transition of the two processes. The adversary cannot observe the intra-process DiD transition that sends its \(SRB_m\) to the other radio nodes in Eq. 5 to validate. Therefore the two processes are weakly bisimilar, i.e., \(RRC_u \approx RRC_{ugs}\).   \(\square \)

Table 2. Last transition of the UE and gNB interrogation processes.
Full size table

6.5 UE Consensus Algorithm Termination

The user equipment consensus algorithm begins when user equipment receives the first paged warning from a radio node. To ensure that the user equipment can complete its registration procedure and prevent a denial-of-service attack by the adversary, the consensus algorithm that is inserted into a context hole must either return to a null process or restart the registration procedure. The first step is to rearrange Eq. 4 so that it has a summation process if the matching operation fails. This is done using \(\pi \)-calculus structural congruences [15], a set of axioms that state the equivalent process structures. Using the SC-Sum-Inact rule where \(P+\bar{0}\equiv P\), Eq. 4 becomes:

$$\begin{aligned} \begin{aligned} b_i(s_i,n_i).b_j(s_j,n_j).[s_i=s_j]RRC_{um}\equiv \\ b_i(s_i,n_i).b_j(s_j,n_j).([s_i=s_j]RRC_{um}+\bar{0}) \end{aligned} \end{aligned}$$

where \(\bar{0}\) models the consensus reducing to an inactive process in all other cases, enabling the continuation of any subsequent process.

Proposition 3:

UE consensus terminates if user equipment only receive mismatched names s.

Proof:

Proof by contradiction. Assume that \(s_i=s_j\) is the only case that leads to an inactive process and all mismatches transition to the \(RRC_{um}\) process. When the consensus process reaches the matching prefix operation, only \(s_i=s_j\) leads to the initiation of the \(RCC_{um}\) process. This is a contradiction.   \(\square \)

6.6 Adversary and DiD Registration Process Distinguishability

This section demonstrates that user equipment will receive two paged warnings from the modified gNB/CN processes if an adversary is discovered in the administrative area. The two warning messages distinguish the \(A_o\) and DiD processes, meaning that they are not weakly bisimilar. The next three proofs demonstrate this lack of equivalence by going through the reduction of the relevant \(\pi \)-calculus expressions.

Proposition 4:

UE can distinguish between the \(A_o\) and DiD processes after the gNB process has interrogated \(A_o\).

Proof:

The modified gNB/CN processes reduced to the relevant interrogation processes is:

$$\begin{aligned} \nu \;sec,bo_i,bo_j\;RCC_{us,i}D_{g,i}|B_{g,i}|RCC_{us,j}D_{g,j}|B_{g,j}|Q_c \end{aligned}$$

DiD sends multiple warnings to a UE process in two cases – both radio nodes do not recognize \(SRB_m\) and one radio node recognizes \(SRB_m\), but the control network does not when it is queried.

Case 1: Both radio nodes do not recognize \(SRB_1\):

$$\begin{aligned} (sec(s',a).[s'=s].\bar{sec}\;s',alerta|\bar{sec}\;s,alerta.sec(s',a)).\bar{bo_i}\;s| \end{aligned}$$
(9a)
$$\begin{aligned} (sec(s',a).[s'=s].\bar{sec}\;s',alerta|\bar{sec}\;s,alerta.sec(s',a)).\bar{bo_j}\;s| \end{aligned}$$
(9b)
$$\begin{aligned} sec(s,q).([s=known]\bar{sec}\;s,confirm+\bar{sec}\;s,alerta) \end{aligned}$$
(9c)

Equations 9a and 9b represent two different radio nodes and Eq. 9c represents the control network. If both gNB processes do not recognize \(SRB_M\) from the \(A_o\) process, they perform a consensus by messaging each other with name alerta over channel sec. After the consensus is complete, they page the adversary’s SRB in a warning to user equipment. A UE process receives two \(\bar{b_i}\;s,n_i\) names from the DiD’s \(B_{g,i}\) process.

Case 2: One radio node recognizes \(SRB_m\), but the control network does not when it is queried:

$$\begin{aligned} \begin{aligned}{}[(sec(s',c).[s'=s].\bar{sec}\;s',alerta|\bar{sec}\;s,alerta.sec(s',c)).\bar{sec}\;s,query.\\ (sec(s,c).\bar{sec}\;s,conf+sec(s,a).(\bar{sec}\;s,alerta|\bar{bo_i}s))]| \end{aligned}\\ \begin{aligned}{}[s=known][(sec(s',a).[s'=s].\bar{sec}\;s',conf|\bar{sec}\;s,conf.sec(s',a)).\\ (sec(s,c)+sec(s,a).\bar{bo_j}\;s)]| \end{aligned}\\ \begin{aligned} sec(s,q).([s=known]\bar{sec}\;s,confirm+\bar{sec}\;s,alerta) \end{aligned} \end{aligned}$$

During the radio node consensus, one radio node announces it recognizes SRB and the other does not. The radio node that does not sends a query message to the control network and the other radio node waits for a resolution:

$$\begin{aligned}{}[(sec(s,c).\bar{sec}\;s,conf+sec(s,a).(\bar{sec}\;s,alerta|\bar{bo_i}s))]|\\ [(sec(s,c)+sec(s,a).\bar{bo_j}\;s)]|\\ sec(s,q).([s=known]\bar{sec}\;s,confirm+\bar{sec}\;s,alerta) \end{aligned}$$

The control node receives the query and, if it does not recognize \(SRB_m\), it replies to the original querier with name alerta:

$$\begin{aligned}{}[(sec(s,a).(\bar{sec}\;s,alerta|\bar{bo_i}s))]|\\ [(sec(s,c)+sec(s,a).\bar{bo_j}\;s)]| \end{aligned}$$

Upon receiving the control network reply, the querying radio node simultaneously pages its \(\bar{b_i}\;s,n_i\) message to user equipment and instructs the other radio node to do this as well.

In both cases, the user equipment receives two \(\bar{b_i}\;s,n_i\) messages. As stated in Sect. 5.1, the messages are inserted in the user equipment consensus algorithm in Eq. 4 using a context hole. The adversary cannot do this as a result of Assumption 5. This implies that the \(A_o\) and DiD processes are not weakly bisimilar when the adversary is interrogated, i.e., .   \(\square \)

Proposition 5:

UE can distinguish between the \(A_o\) and DiD processes if the adversary attempts to imitate a radio node.

Proof:

The modified gNB/CN processes reduced to the imitation detection process is:

$$\begin{aligned} DiD=\;\nu \;sec,bo_i,bo_j\;RCC_{us,i}I_{g,i}|B_{g,i}|RCC_{us,j}I_{g,j}|B_{g,j}|I_c \end{aligned}$$
$$\begin{aligned} sec(su,i).\bar{bo_i}\;su+[s=me].(\bar{sec}\;s,imitation|\bar{bo_i}\;s)|\\ sec(su,i).\bar{bo_j}\;su+[s=me].(\bar{sec}\;s,imitation|\bar{bo_j}\;s)|\\ sec(s,i).\bar{sec}\;s,imitation \end{aligned}$$

Each radio node can detect it is being imitated upon seeing its \(SRB_1\) used by another process. The imitated radio node simultaneously sends its \(\bar{b_i}\;s,n_i\) message via the \(B_{g,i}\) process and informs the control network it is being imitated:

$$\begin{aligned} |\\ sec(su,i).\bar{bo_j}\;su+[s=me].(\bar{sec}\;s,imitation|\bar{bo_j}\;s)|\\ sec(s,i).\bar{sec}\;s,imitation \end{aligned}$$

The control network accepts the imitation warning and informs another radio node to page a second warning:

$$\begin{aligned} |\\ sec(su,i).\bar{bo_j}\;su\\ | \end{aligned}$$

The second radio node then sends its \(\bar{b_j}\;s,n_j\) message.

As mentioned in Sect. 5.1, user equipment can receive two \(\bar{b_i}\;s,n_i\) messages by inserting the messages in the consensus algorithm in Eq. 4 using a context hole. The adversary cannot do this as a result of Assumption 5. This implies that the \(A_o\) and DiD processes are not weakly bisimilar when the adversary is attempting to imitate a radio node, i.e., .   \(\square \)

Proposition 6:

UE can distinguish between the \(A_o\) and DiD processes if the adversary rejects interrogation by a radio node.

Proof:

The modified gNB/CN processes reduced to the rejection of interrogation processes is:

$$\begin{aligned} DiD=\;\nu \;sec,bo_i,bo_j\;RCC_{us,i}[s=\emptyset ]R_{g,i}|B_{g,i}|RCC_{us,j}[s=\emptyset ]R_{g,j}|B_{g,j}|R_c \end{aligned}$$
$$\begin{aligned}{}[s=\emptyset ]dc(K_s).(\bar{sec}\;K_s,reject|bo_i\;K_s)+sec(K,r).\bar{bo_i}\;K|\\ [s=\emptyset ]dc(K_s).(\bar{sec}\;K_s,reject|bo_j\;K_s)+sec(K,r).\bar{bo_j}\;K|\\ sec(k,r).[k=\bar{known}]\bar{sec}\;K,reject \end{aligned}$$

The rejected radio node waits for the adversary to send its 5G-AKA key as cleartext when attempting to register with a targeted user equipment. After intercepting the key, the radio node simultaneously pages its \(\bar{b_i}\;s,n_i\) warning via the \(B_{g,i}\) process and sends the key to the control network to coordinate a second warning:

$$\begin{aligned} |\\ [s=\emptyset ]dc(K_s).(\bar{sec}\;K_s,reject|bo_j\;K_s)+sec(K,r).\bar{bo_j}\;K|\\ sec(k,r).[k=\bar{known}]\bar{sec}\;K,reject \end{aligned}$$

The control network confirms that it is an unknown key represented by the name \(\bar{known}\) and coordinates a second radio node to page a warning:

$$\begin{aligned} |\\ sec(K,r).\bar{bo_j}\;K\\ | \end{aligned}$$

The second radio node sends its \(\bar{b_j}\;s,n_j\) message.

As mentioned in Sect. 5.1, user equipment can receive two \(\bar{b_i}\;s,n_i\) messages by inserting the messages in the consensus algorithm in Eq. 4 using a context hole. The adversary cannot do this as a result of Assumption 5. This implies that the \(A_o\) and DiD processes are not weakly bisimilar when the adversary rejects interrogation by a radio node, i.e., .   \(\square \)

The three propositions demonstrate that a defense-in-depth algorithm built in the 5G standard can automatically inform user equipment in an administrative area that an IMSI catcher is operating. This denies the adversary the ability to violate the privacy promises in the 5G standard as long as the DiD process wins the race condition.

6.7 UE Termination After a Successful DiD Process

After user equipment concludes its consensus algorithm regarding the paged warnings, it must disconnect from the adversary. However, in accordance with the 5G standard, user equipment will attempt to connect with the strongest radio node signal. While it is in the process of connecting with a new radio node, user equipment must ensure that it is not reconnecting to the adversary. This is accomplished by checking the name received in the paged warnings in the modified processes \(RRC_{um}\) and \(NAS_{um}\) in Sect. 5.1. According to Assumption 5, there must be a legitimate radio node for the user equipment to connect, otherwise the contextual integrity property would not be possible. The following proof demonstrates that if a legitimate radio node exists for connection after a successful consensus has been achieved, user equipment can terminate its registration process.

Proposition 7:

The modified UE registration process terminates after a successful defense-in-depth consensus.

Proof:

Proof by contradiction. Assume that no name s or \(K_m\) exists that passes the matching operations in the \(RRC_{um}\) and \(NAS_{um}\) processes.

Case 1: The adversary is successfully interrogated by two radio nodes. Propositions 4 and 5 show that the radio node consensus terminates and that user equipment will receive two paged warnings with the name s. After the user equipment consensus concludes, \(RRC_{um}\) proceeds to subsequent processes as long as \(s \ne SRB_m\).

Case 2: The adversary avoids being interrogated by both radio nodes, but a radio node intercepts its key. This is shown in Proposition 6. The modified registration process reaches \(NAS_{um}\) that continues to termination as long as K \(\ne \) K\(_m\).

Thus, the condition for the modified user equipment registration process to terminate is:

$$\begin{aligned} s \ne SRB_m \wedge K=K_m \end{aligned}$$

are not in the paged warnings. This contradicts the premise.   \(\square \)

6.8 Impossibility of \(A_o\) Learning sec

This brief proof demonstrates that, given the contextual integrity property in Sect. 3.3, Asumption 1 and the reduced processes in Sect. 6.6, an adversary will never learn the name sec that would give it access to the encrypted communications of the gNB/CN process.

Proposition 8:

DiD’s \(B_{g,i}\) processes will never broadcast the name sec.

Proof:

Proof by contradiction. Assume that process \(B_g\) is able to page the name sec. This implies that a radio node received the name via a registration process with user equipment or by interrogating an adversary. Given Assumption 1, this is a contradiction.   \(\square \)

7 Conclusions

The consensus algorithm presented in this chapter enforces control over radio node mobility in a 5G administrative area. The algorithm builds an additional defense-in-depth layer in the 5G standard by creating a contextual integrity property that reduces the likelihood of privacy violations should vulnerabilities be found in 5G-AKA protocol implementations. In particular, the 5G infrastructure automatically warns all the user equipment in an administrative area not to connect to IMSI catchers.

The algorithm depends on multiple radio nodes deceiving and interrogating a suspected IMSI catcher to discern if its credentials are legitimate. After a consensus on the malicious nature of IMSI catcher is reached between the radio nodes and control network, multiple paged warnings are broadcast to all the user equipment in the administrative area. Following this, each user equipment must form a consensus on whether to disconnect. The \(\pi \)-calculus was employed to represent modifications to the 5G communications models needed for the consensus algorithms. The contextual integrity property was verified using \(\pi \)-calculus equivalence proofs by demonstrating that the consensus processes are distinguishable from a cryptanalytic adversary.

The research demonstrates that it is possible to use network semantics to construct context-dependent security properties such as enforcing control over which devices are permitted to broadcast in a wireless network.

One avenue for future research is to incorporate the tolerance of race conditions in the algorithm to enable computations of the efficacy of 5G network implementations should the encrypted channels fail. This would also allow for a stricter equivalence relation to be used in the proofs because processes would have to have a notion of the internal state of the other communicating processes.

The algorithm may also be extended to incorporate malicious signatures gathered by sensor-based and network-based IMSI catcher detection systems. This would turn the detection systems into a prophylaxis instead of a remedy.

In order to incorporate the proposed defense-in-depth layer in the 5G standard, it would be necessary to implement the consensus algorithm to ascertain its feasibility. Current research is focusing on an implementation that measures the latency advantage needed to succeed with regard to the race conditions. Following this, the \(\pi \)-calculus will have to be translated into state machines/communications models that could be formally verified, before being implemented in the 5G standard.