From Control to Chaos: A Comprehensive Formal Analysis of 5G’s Access Control

Mujtahid Akon Md Toufikuzzaman Syed Rafiul Hussain

Pennsylvania State University Pennsylvania State University Pennsylvania State University
mba5773@psu.edu mpt5763@psu.edu hussain1@psu.edu

Abstract—We develop CoreScan, a comprehensive formal anal- the involvement of diverse vendors and third-party tenants,
ysis framework for analyzing the access control mechanism makes the security of the 5GC more critical than ever.
of 5G core networks. In doing so, we build the first com- A fundamental security challenge in the 5GC is the issue
prehensive formal model for the access control mechanism of of over-privilege, which typically occurs when a malicious
5G core network that considers the indirect communication or malfunctioning NFs controlled by either service providers
mode and 5G roaming. Given a global property, CoreScan or third-party tenants gains unintended or illegitimate access
employs the compositional verification technique that leverages to resources or services of other NFs. To address this, the 3rd
the assume-guarantee style reasoning approach to decompose Generation Partnership Project (3GPP)— the organization
the system model into multiple disjoint components and applies responsible for developing cellular network specifications—
the split assertion principle to identify local assumptions and has adopted OAuth (Open Authorization) 2.0, a state-of-
guarantees. The model’s global security property holds if and the-art access control framework, to authorize NF access.
only if all local guarantees derived from the global property However, OAuth design has been proven to be insecure
are verified in their respective components. CoreScan features and susceptible to various attacks [1]. This signifies that the
a configurable adversary model, enabling the evaluation of integration of OAuth in 5GC may also entail critical flaws.
access control properties under diverse adversary capabilities. Hence, malicious or compromised NFs controlled by third-
We tested 61 access control properties with CoreScan and
parties can exploit the flaws to obtain unauthorized access to
uncovered five new classes of exploitable privilege escalation
sensitive data, modify it, or cause denial-of-service (DoS).
Since the introduction of access control mechanisms in
vulnerabilities in the 5G standards. Additionally, we found
5GC, two prior efforts attempted to systematically analyze
that most previously known overprivilege vulnerabilities in
its security [2], [3]. These analyses, however, fall short
direct communication also extend to indirect communication
because of the following reasons: (i) static program analysis
and roaming settings.
performed on the open-source 5GC implementations to com-
pute least privilege permissions is imprecise, and the use of
1. Introduction incomplete open-source 5GC implementations as reference
is error-prone [2]; (ii) formal analysis is incomplete due
to not accounting for indirect communication modes and
The fifth-generation cellular network (5G) presents the 5G roaming, which are integral to 5GC operations and
latest advancement in wireless technology. It is now be- introduce unique access control challenges due to multi-hop
ing deployed by operators worldwide. To deliver on its interactions and cross-network trust boundaries. Specifically,
promises, such as enhanced Mobile Broadband (eMBB) and multi-hop interactions introduced by the indirect commu-
Ultra-Reliable Low Latency Communication (URLLC), 5G nication mode involve data passing through intermediary
has undergone significant transformations from its predeces- nodes such as a proxy, also known as SCP in 5GC. All
sors. A central component of this evolution is the 5G core these expand the attack surface and increase the risk of
network (5GC), which manages communication, connectiv- unauthorized access, while cross-network trust boundaries
ity, and data routing for 5G devices and services. Unlike in roaming scenarios require secure coordination between
previous generations that relied on dedicated, proprietary two different network operators, complicating access control
hardware for specific network services, the 5GC employs a enforcement; and (3) finally, the analysis cannot effectively
service-based architecture (SBA). This architecture breaks manage state explosion problems. Therefore, in this paper,
the core into multiple functional components, known as we pose the following research question: Is it possible to
Network Functions (NFs). The NFs are implemented as develop a formal analysis framework to comprehensively
software-based services capable of running in virtualized verify the access control mechanism of a 5GC, including
or cloud environments. Additionally, 5G supports software- indirect communication mode and 5G roaming service?
defined networking (SDN) and invites third-party businesses However, we run into the following challenges to address
and enterprises to leverage and contribute to the 5GC. How- the above research question. First, the standard body [4]
ever, the integration of these new technologies, along with does not provide any 5G reference implementations. Ex-
isting open-source implementations [5], [6], [7] are incom- expensive and often requires manual intervention [11], [12].
plete, error-prone, and do not strictly follow the specification We observe that the 5GC access control system consists
requirements, making them unsuitable for formal analysis. of multiple functionally disjoint features, each defined by a
Most importantly, the attribute-based access control mech- unique set of attributes, with only a small set of common
anism in the 5G core [8] involves over 50 types of NFs, attributes (§3). We leverage this structure by modeling a
hundreds of services, and thousands of APIs, resulting in a bare-bone component using only the common attributes,
vast space of attributes to consider in each access control requiring no assumptions. Additional components are built
decision. Formally verifying security properties in a system on top, each incorporating a disjoint feature-specific attribute
of this size is, therefore, challenging due to the state explo- set. Since these feature-specific components are disjoint
sion problem. Additionally, the 5G access control design is and their local guarantees target only component-specific
specified in natural language, which introduces ambiguity, attributes, they can be independently verified, rendering their
lacks formal rigor, and complicates precise interpretation assumptions trivial (i.e., true). CoreScan consists of five
and formalization. such components—nf-domain, slicing, roaming, indirect,
The most closely related work to our approach is and other—in addition to the bare-bone one. Following the
5GCVerif [3], which introduced the first formal model of split assertion principle [13], global security properties are
5GC’s access control mechanism and its formal analysis. decomposed into local guarantees, each verified in its cor-
This framework formulates the verification of 5G access responding component, while the local assumptions are re-
control mechanism as a model-checking problem. It lever- duced to triviality. Thus, to verify a global security property
ages the small model theorem [9] to reduce the model’s in CoreScan, we test the corresponding local guarantees
state space, effectively limiting it to a smaller, representative in their respective components. The global property holds
subset (e.g., reducing from 50 NFs to 5 NFs) without com- if and only if all local guarantees are satisfied. Because
promising accuracy. The model is then tested against various components and their guarantees are disjoint, any local
access control properties using a model-checker to uncover violation directly reflects a flaw in the overall system.
counterexamples indicative of over-privilege attacks. How- CoreScan adopts a modular design not only in terms of
ever, 5GCVerif has several limitations. (A) It only considers components but also across NF components, attributes, key
the direct communication mode, where an NF interacts API requests/responses, and communication subjects and
directly with another without a proxy. With the introduction objects. This modularity enhances model extensibility and
of 5G standards in Release 16, the indirect communication customization. The threat model is highly flexible, allowing
mode, which involves a proxy between two interacting NFs, any communicating entity to be treated as an adversary with
becomes highly critical. This mode significantly alters 5G varying degrees of capability. Specifically, adversaries can
access control and warrants additional security analysis. (B) inherit partial or full capabilities of consumer NFs, producer
The framework overlooks 5G roaming services, a critical NFs, SCPs, or even the serving network during roaming, en-
5GC feature where NFs from different networks interact. abling the analysis of diverse security properties from mul-
Since these networks reside in separate trust domains, they tiple perspectives. To further improve scalability, we apply
may introduce security risks that 5GCVerif fails to address. abstraction techniques across components, simplifying data
(C) There are flaws in 5GCVerif’s implementation of certain types, attribute values, and behaviors. These abstractions
authorization logic, potentially causing it to miss some at- significantly reduce complexity, allowing efficient modeling
tacks. For example, we identified a novel attack (§7.1.1) that of the intricate interactions involved in 5G access control.
5GCVerif failed to detect due to an oversight in verifying Findings. Using CoreScan, we tested 61 security properties
an attribute during a service grant. (D) Finally, 5GCVerif across six model components, revealing 10 distinct types
does not scale while capturing and analyzing both direct of access control attacks, including five newly discovered
and indirect communication modes and roaming scenarios. attacks. Additionally, we found that a 5G core utilizing
Our approach. To address the above limitations, we design indirect communication via SCP and/or roaming also suffers
CoreScan, which can be viewed as an alternative instantia- from most access control flaws identified in prior studies [3],
tion of the general 5GCVerif framework but employs differ- [14]. Our experimental results show that CoreScan signifi-
ent modeling and verification approaches to tackle additional cantly improves both scalability and runtime. Compared to
challenges. To address the scalability challenge, we adopt the baseline [3], CoreScan achieves a 9-27 times speedup
a compositional verification approach based on assume- for reachability property checks and uses 55% fewer states
guarantee reasoning [10]. In this approach, the 5GC’s access despite supporting more complex features such as indirect
control system’s model is logically divided into smaller com- communication and roaming.
ponents, each represented as a finite state machine (FSM). A Contributions. In summary, this paper has the following
component assumes a local property (assumption) and ver- main contributions:
ifies another (guarantee). These components are connected • We introduce the first comprehensive formal model for
such that each assumption corresponds to a guarantee of the access control mechanism of 5G core network that
another, like in a chain, and the global property holds if all considers indirect communication mode and 5G roaming.
local guarantees derived from it are satisfied. • We develop CoreScan, an assume-guarantee style com-
However, deriving meaningful local assumptions and positional verification framework for formally analyz-
guarantees from a global property can be computationally ing the access control design of the 5G core network.
 (denoted by NFType) in the 5GC, such as the Access
NRF (vNRF) UDM NRF UDM and Mobility Management Function (AMF), Session Man-
agement Function (SMF), and Unified Data Management
UE vSEPP hSEPP
(UDM). These NFs collectively manage mobility, session
AMF SMF AUSF SMF handling, and subscriber data. Depending on demand, multi-
ple NF instances of the same NFType may run concurrently,
UPF DN UPF DN each identified by a unique NFInstanceID. For simplicity,
RAN
5G Core 5G Core since we typically assume a single NF instance per NFType
VPLMN HPLMN in our analysis, we use the terms: NF, and NF instance
5G Non-roaming Architecture Control Plane interchangeably.
Data Plane 5G roaming connects networks from different operators,
5G Roaming Architecture enabling a seamless user experience across networks. Each
network is identified by a unique Home Public Land Mobile
Figure 1: Simplified 5G system architecture. In non- Network (PLMN) ID. A typical roaming scenario (Fig-
roaming (blue), the UE connects to the 5G Core (green) ure 1) involves the Home PLMN (HPLMN) (orange region),
via RAN. In roaming, the UE connects to the HPLMN to which the UE is subscribed, and the Visited PLMN
(orange) through the VPLMN (blue). Roaming-specific (VPLMN) (green region), which the UE connects to while
elements are shown in purple text. roaming. In this setup, the UE attaches to the RAN of the
VPLMN, which provides local services and interacts with
its own core network. To retrieve subscriber information and
CoreScan operates on a formal model to rigorously other required data, the VPLMN communicates with the
verify a wide range of security properties. Leverag- HPLMN through secure inter-PLMN interfaces—typically
ing the split assertion principle, it decomposes both via the Inter-PLMN Backbone (IPX)—using vSEPP (Visited
the system model and security properties into indepen- Security Edge Protection Proxy) and hSEPP (Home Security
dent components, enabling scalable and effective model- Edge Protection Proxy) to ensure secure and authenticated
checking. A configurable adversary component further inter-operator communication.
allows CoreScan to evaluate properties under diverse
adversarial conditions. 2.2. Network Isolation
• We tested 61 security properties with CoreScan and
discovered five new classes of exploitable privilege es- Network slicing is a core feature of 5G, enabling the
calation attacks in 5G standards. We also confirmed that creation of multiple virtual networks on shared physical in-
most previously known overprivilege vulnerabilities also frastructure. Each slice is an end-to-end network customized
apply to indirect communication and 5G roaming. The to specific service requirements, such as bandwidth, latency,
model, properties, and findings are open source at [15]. and security. Identified by a unique ID called sNssai, a
Responsible disclosure. We shared our findings and pro- network slice spans resources across the RAN, transport
posed patches with GSMA [16] which agreed to acknowl- network, and core network, ensuring logical separation be-
edge them under CVD-2025-0101. We are collaborating tween slices. This separation is key to prevent performance
with GSMA to draft and submit multiple Change Requests and security issues in one slice from impacting others.
(CRs) to 3GPP [4] for updating 5G security specifications.
2.3. 5G Access Control
2. Background To facilitate communication between NFs in the 5GC,
each NF exposes a set of standard API functions, called
This section briefly describes the 5G access control NFOperations, that other NFs can invoke. NFOperations
mechanism and the necessary concepts to understand our are grouped in NFServices, with each NFService consists of
model, methodology, and findings. several NFOperations managing a specific set of resources.
An NF can offer one or more NFServices. Each NFService
2.1. 5G & 5G Roaming Architecture and, optionally, NFOperation is assigned with a permission
scope called service-level scope and operation-level scope,
A basic 5G non-roaming architecture comprises three respectively. Scope refers to the specific set of permissions
key components (blue region of Figure 1): User Equipment granted to an NF to access an NFOperation during NF
(UE), i.e., are end-user devices; Radio Access Network communications. For example, AMF provides an NFSer-
(RAN); and the 5G Core or 5GC (green region). RAN vice namf comm, which contains NFOperations, providing
connects UEs to the core via radio links. To support diverse communication services with a UE. Among these NFOper-
services, the 5GC adopts a Service-Based Architecture com- ations, CreateUEContext allows the creation of UE context
prising a set of modular functional blocks, called network for signaling and communication. The AMF defines both
functions (NFs), each responsible for performing a specific the service-level namf-comm scope and the operation-level
set of tasks. 3GPP defines over 50 types of standard NFs namf-comm:ue-contexts:mobility scope for this interaction.
 the network down, e.g., due to inactivity, an NF can also
Network Network deactivate itself by requesting NRF to remove its NFProfile
Consumer NRF Producer
via DeregReq API ( 7 ). (ii) AT Request (accessTokenReq or
1 RegReq (NFProfile)
ATR): A consumer NF (NC ) invokes accessTokenReq ( 4 )
RegResp (Success) to ask for an AT from NRF. Based on the request parame-
2 UpdateReq (NFProfile) ter values and the NFProfiles of the prospective producer
UpdateResp (Update Success) NFs (NP s), NRF verifies the request and, if authorized,
3 NFDiscReq (NFService, NFtypes,...) grants an AT to the NC . AT contains important information
NFDiscResp (NFProfile) regarding permissions, e.g., NFInstanceIDs of the allowed
NC s & NP s, allowed scopes, etc., for the NP to verify NF-
4 accessTokenReq
(Expected NFService, NFType, ...)
Service Request ( 6 ). Note that AT is considered a resource
for accessTokenReq. (iii) NF Discovery Request (NFDiscReq
Check authorization
Generate access token or DR): Any time the NC wants some resource access
accessTokenResp or services from another NF, it first needs to identify the
(access token, expires_in, ...) endpoints, (e.g., IP address) of the potential producer NFs
in the 5GC that may serve its need. As NFs are dynamic,
5 NFDiscReq (NFService, NFtypes,...)
the consumer needs to query NRF to get this information.
NFDiscResp (NFProfile) NRF exposes NF Discovery Request (NFDiscReq) API ( 3 ,
6 ServiceReq (access token) 5 ) for this purpose. NFDiscReq can be invoked before or
Verify access token after the accessTokenReq as required. Both accessTokenReq
Execute NFService and NFDiscReq require authorization checks via NRF and
ServiceResp (Success) thus are called authorization request. Note that discovered
7 DeregReq (NFProfile)
NFProfiles are considered a resource for NFDiscReq. (iv)
Service Request (ServiceReq): Once the consumer NF has
DeregResp (Success) both AT and the potential producer’s endpoint, it finally
invokes resource access or service request via this API ( 6 .
Figure 2: Access control interactions between NFs. Refer Upon receiving the request, NP verifies the AT information
to Figure 5 for corresponding API usage in the 5GC against its NFProfile to determine if NC is authorized for
access control model. resource access and, if allowed, grants resource access.
Authorization verification process. Each NFProfile con-
To limit unwanted resource access during NF interac- tains a special set of attributes that NRF uses to authorize
tions, 3GPP adopts the Client Credentials mode [17] of the consumer’s authorization requests. These attributes are
OAuth 2.0 protocol. In this mode, to access any resources by called authorization attributes and can be defined at multiple
invoking an API call, the client must present a valid access levels and thus provide some flexibility in describing a
token (AT) to the resources owner that the owner will verify fine-grained access control. For instance, allowedNfTypes is
before granting resource access to the client. The client can an authorization attribute in the NFProfile of the producer
obtain the AT from the authorization server, a trusted entity NF and refers to a list of NFs of certain NFTypes that
to both the client and the resource owner. In the 5GC, a are allowed to access the producer NF’s resources. It may
special NF acts as the authorization server called Network be defined globally for all NFServices in the producer’s
Repository Function (NRF). The client NF invoking the API NFProfile, or separately for each NFService, or even for
(i.e., NFOperation) is called consumer NF or NC in short, each NFOperation. If defined, NFOperation level parameter
whereas the resource owner is the NF that receives, verifies, dominates over NFService level and so on. For example, if
and grants/rejects the NFOperation, also known as producer in its NFProfile, an AMF instance defines allowedNfTypes
NF or simply NP . as {AMF, SMF} (NF-level), but one of its NFServices,
Authorization APIs. A simplified diagram of how NFs amf-comm, defines it as {AMF} only (NFService level),
interact each other before NFService access is shown in Fig- then no NF instance of NFType except AMF, even SMF,
ure 2. (i) NF Register, Update and Deregister Request: Each can access any NFOperations under amf-comm. Some other
NF maintains a multi-level key-value pair data structure, notable authorization attributes are allowedNFInstances, al-
called an NFProfile, which contains its attributes, e.g., NFIn- lowedNssais, allowedNFDomains, and allowedPlmns. From
stanceID, NFType; states, e.g., NFStatus (nf registered or a producer NF’s point of view, they respectively define lists
not); and authorization rules: allowedNfTypes, allowedNs- of NFTypes, sNssais, fqdns1 and plmns of NF instances that
sais. Each NF instance is identified by its NFInstanceID may be considered for resource access. Resource access is
attribute. To register a new NF instance to the 5GC, its NF- granted only if all authorization attribute checks are pass.
Profile is sent to the configured NRF via RegReq API ( 1 ).
Since NFProfile is dynamic, any changes to it are reported
to NRF via UpdateReq API ( 2 ). This is crucial for 5G
access control since NRF may use NFProfiles to authorize 1. a Fully Qualified Domain Name (FQDN) is a DNS-resolvable name
an accessTokenReq ( 4 ) and grant AT for the NC . To scale used for service discovery and routing between NFs.
2.4. Communication Types attributes to the NRF via UpdateReq. Besides, a rogue
consumer NF may alter message parameter values arbitrar-
The 5GC supports three primary modes of communica- ily while sending an authorization request. During indirect
tion [18]. In direct communication (Figure 2), NFs interact communication, a compromised SCP may impersonate le-
directly with each other, without a proxy, making it ideal for gitimate NFs and alter, replay, or spoof requests/responses,
scenarios where low latency is crucial. However, this method tricking other components into trusting unauthorized access
may expose NFs to security risks and scalability issues. To requests, leading to data leaks, unauthorized service access,
address these concerns, the Service Communication Proxy or even manipulation of user data. Finally, while roaming,
(SCP) facilitates indirect communication, which intermedi- a visiting NRF, being part of a foreign network from the
ates between NFs, handling all requests and responses, i.e., perspective of the home network and UE, may exhibit
accessTokenReq, NFDiscReq, and ServiceReq ( 1 - 5 in Fig- malicious intent, thereby altering authorization request pa-
ure 3 in § 3.2). This approach is expected to enhance secu- rameters before forwarding them to arbitrary destination
rity through policy enforcement, load balancing, and traffic NRFs, i.e., home NRFs. The above adversary assumptions
monitoring while also improving scalability by decoupling are inferred from prior security weaknesses observed in the
NF interactions. Lastly, hybrid communication also involves cloud microservices [21], [22], [23], [24], [25], [26], [27]
SCP but combines both direct and indirect modes, allowing and are consistent with 3GPP TR 33.875 [28].
operators to balance performance and security based on Other Assumptions. (1) We assume all single-hop network
specific network needs. In this mode, NFDiscReq always packets are mutually authenticated. Thus, our threat model
bypasses SCP for performance, while ServiceReq always does not question the mutual authenticity of the network
routes through SCP for enhanced security. Depending on the packets as opposed to the Dolev-Yao [29] adversary model.
mutual authentication between the consumer NF and NRF, (2) We assume the malicious NF does not drop, mod-
accessTokenReq may or may not route through SCP in this ify, intercept, or eavesdrop a request/response sent from
mode ( 6 - 8 in Figure 3, accessTokenReq is routed through a legitimate authenticated NF, as these capabilities do not
SCP assuming lack of mutual authentication between NC affect authorization. (3) All tokens and certificates, e.g., AT,
and NRF), depending on the mutual authentication between CCA, etc., are integrity-protected and cannot be modified
NF and NRF at the transport layer [8]. Details about com- by any party except the originator. (4) For 5G roaming,
munication modes are available in Appendix A. all intermediate nodes, such as SEPP and IPXs between
the vPLMN and the hPLMN, are benign since the com-
3. Motivating Example municating nodes are mutually authenticated to each other,
providing an end-to-end implicit authentication and dealing
In this section, we present our threat model and provide with encrypted and integrity-protected payloads only. (5)
a motivating example that highlights the need for formal NRF (resp., hNRF for roaming) acting as an authorization
analysis of 5G access control. We then discuss the high- server is not considered malicious because of the elevated
level workflow and insights underpinning the design of trust of the operator in it.
CoreScan.

3.1. Threat Model 3.2. An Example of Privilege Escalation Attack

Since the 5GC system facilitates third-party services and Let us walk through an example to highlight the neces-
the NFs are deployed as cloud-based microservices, the sity of our enhanced model-checking approach. Consider
5GC access control system is vulnerable to a wide range a scenario in Figure 3 where an AMF instance in the
of threats. For instance, external NFs operated by third- 5GC wants to create a session management context with
party tenants such as Mobile Virtual Network Operators an SMF instance via indirect communication. The AMF
or MVNOs [19], [20], or compromised NFs due to cloud instance sends a ServiceReq (PostSmContexts) with relevant
misconfigurations [21], [22] may act as malicious NFs and parameters, which is routed through an SCP ( 1 ). Upon
illegitimately access unauthorized resources. While the ul- receiving the request, the SCP, acting on behalf of the AMF,
timate goal of a malicious NF is often privilege escalation, obtains an access token (ATSMF ) using accessTokenReq and
our analysis considers distinct threat models based on com- response ( 2 ), discovers the appropriate SMF instance using
munication types, as well as the capabilities and intentions NFDiscReq from the NRF ( 3 ), and then makes the PostSm-
of different NFs. Contexts API call to the SMF ( 4 ). Since the SCP is a proxy,
Adversary Capabilities Our threat model assumes that an the AMF includes a signed token called Client Credentials
attacker compromises an NF/SCP of the 5GC in some way Assertion (CCAAMF ) token in the service request to SCP.
discussed above and thus has full control over the NF/SCP. NRF and/or a producer NF use the CCA token in indirect or
Consequently, it can forge and issue arbitrary messages to hybrid communication mode to identify a legitimate request.
other legitimate NFs in the network. Also, a compromised The CCAAMF contains AMF’s NFInstanceID, an expiration
NF, i.e., a consumer or producer NF, with the supervi- time, and aud:‘NRF’ and ‘PRODUCER NF’, since the CCA
sion of the Operations, Administration, and Management is for both the NRF and the expected producer. The NRF
(OAM) System, may modify and/or misreport its NFProfile or SMF verifies the CCA token’s authenticity each time it
 indefinitely. Besides, when SMF sends the malicious Ser-
AMF PCF SCP NRF S
SMF viceReq ( 9 ), it signs this message with its signature that
SR: PostSmContexts contains SMF’s NFInstanceID as the consumer. However,
(CCAAMF) while verifying this request, PCF does not verify that SMF’s
1 ATR (CCAAMF)
2 NFInstanceID in the request signature does not match the
ATSMF
consumer field in the ATPCF (i.e, AMF’s NFInstanceID). As
DR (CCAAMF) evident from the above example, this sophisticated attack
3
NFProfileSMF
is difficult to detect manually, underscoring the need for
SR: PostSmContexts (CCAAMF, ATAMF) systematic formal analysis. Previous work [3] failed to
4
5 201 Created detect this type of vulnerability because it could not model
201 Created ATR (CCAAMF, target=PCF)
6
and analyze indirect communications due to state explosion.
ATR (CCAAMF, target=PCF)
7
ATPCF
ATPCF
4. Design Overview
8
SR: AMPolicyCreate (ATPCF)
9
201 Created 4.1. Design Philosophy of CoreScan
Figure 3: Message flow demonstrating the motivating
attack example. Here, AMF is the consumer, and SMF To tackle such scaling limitations, we design CoreScan
in red acts as a malicious actor exploiting CCAAMF based on compositional verification by leveraging the
via hybrid communication to obtain ATPCF . NRF is the assume-guarantee style reasoning paradigm. As the 5G
authorization server and SCP is the proxy used for core can include numerous producer and consumer NFs,
hybrid communication, assuming mutual authentication each with various services and operations, similar to
between SMF and PCF is not established in transport 5GCVerif [3], at first, we employ the small model theorem to
layer [8]. Here, CCAAMF = id: AMF ID, aud: ‘NRF’, reduce the verification of an unbounded parametrized system
‘PRODUCER NF’ and ATPCF = consumer: AMF ID, to a verification of a small constant parameter value system.
producer: PCF, DR: NFDiscReq, ATR: accessTokenReq, The small model theorem suggests that if all interactions in
SR: ServiceReq. the large system are represented in the smaller system, any
receives a request, ensuring that SCP can only act on behalf property valid for the smaller system will also be valid for
of AMF. the larger one. Based on that, we can project the set of
At first glance, this process seems secure. However, reachable states in a large 5GC onto a reduced set of key
we discovered a critical vulnerability after modeling and producers and consumers while preserving critical system
verifying the indirect communication mode of 5GC’s access behaviors within this simplified model.
control specified by the 3GPP Release 17 [30]. Suppose the While the small model theorem effectively reduces the
SMF acts maliciously. Upon receiving the PostSmContexts number of consumer and producer NFs in the model, it
request with the CCAAMF ( 4 ), it could exploit CCAAMF alone cannot address the additional complexities introduced
by immediately sending a fabricated accessTokenReq to in CoreScan. For instance, the small model theorem re-
SCP using hybrid communication mode to obtain an access quires CoreScan to model two entities of NRFs: visiting
token ATPCF :consumer: AMF ID, producer: PCF from the (vNRF) and home (hNRF) NRFs of serving and home
NRF ( 6 – 8 ). The goal of the malicious SMF is to illegit- networks, respectively, for inter-network communications
imately obtain some services from a PCF (Policy Control (e.g., Vodafone in the UK with T-Mobile in the USA),
Function) instance such as forge/modify/delete the Access whereas 5GCVerif required none. Additionally, 2 out of 4
and Mobility Policy data (defining rules for network access, NF communication modes [18] require the modeling of an
mobility management, and service prioritization), which the SCP component. CoreScan also aims for a comprehensive
AMF has legitimate access to originally (Figure 3). SCP, model by incorporating additional security-sensitive param-
being the proxy for SMF, forwards the request to the NRF eters (e.g., fqdn, plmn), further increasing its complexity.
along with CCAAMF obtained from SMF ( 7 ). The NRF We address this problem via compositional verification
verifies the replayed CCAAMF and, seeing it as valid, grants technique [31]. Here, we disintegrate the model into several
access token ATPCF :consumer: AMF ID, producer: PCF small components and verify local properties of individual
to the SMF assuming that the request has come from the components to imply that these properties hold in the entire
AMF (similar to 2 ). With ATPCF , the SMF can then il- system. This technique leverages the assume-guarantee rea-
legitimately forge AMF-related resources, e.g., Access and soning proposed by Pnueli [10]. Let a system consists of two
Mobility Policy data, and send them to PCF by invoking the components M1 and M2 . Similar to Hoare triple, Pnueli’s
AMPolicyCreate operation via direct communication ( 9 ). system uses AM G form, meaning that if a component
The vulnerability arises because the CCA and SCP M is part of a system that satisfies property A (assumption),
combined allow the SMF to misuse the granted AT, which then the system must satisfy property G (guarantee). The
has a sufficient lifetime, allowing the SMF to exploit it simplest form of compositional reasoning based on the
transitivity principle can be expressed as follows: composed into several unique functionalities called fea-
trueM0 A tures, each defined by a distinct set of NF attributes. A
AM1 G feature functionally represents a high-level operational ca-
pability or service offered by the network, while its at-
trueM0 ||M1 G tributes define feature identity, configure authorization poli-
The above rule states that if trueM0 A and AM1 G cies, and manage related resources. For instance, the (net-
hold, then trueM0 ||M1 G must hold. Here M0 ||M1 de- work) slicing feature corresponds to a logical network in
notes the composite state space of M0 and M1 . 5GC and includes feature-specific attributes:{sNssais, al-
Let, the set of model components be M = lowedNssais,...} to configure and authorize slice-specific ac-
{M0 , M1 , . . . , Mn }, the set of all assumptions, A = cess. Similarly, the roaming feature includes feature-specific
{A0 , A1 , . . . , An }, and the set of all guarantees G = attributes:{plmns, allowedPlmns,...}. Note that the feature-
{G0 , G1 , ..., Gn }. To verify if a model M of the system sat- specific attributes are disjoint from one another.
isfies a desired property G, i.e., trueM G, compositional Some attributes, e.g., NFType and allowedNfTypes are,
verification asks to satisfy a series of proof: Ai Mi Gi  however, fundamental and required by default for all valid
for all i = 0, 1, . . . , n. However, a critical challenge is NF instances, regardless of features. These shared attributes
to devise compositional rules to find the appropriate set form the base feature. Consequently, roaming and slicing,
of triplets {(Ai , Mi , Gi ) | i = 0, 1, . . . , n} such that the both features, must include base feature attributes: {NFType,
local assumption Ai satisfy the local guarantee Gi where allowedNfTypes, ...}, apart from their corresponding feature-
Gi = Ai+1 for all i. Here, G = Gn denotes the global specific attributes.
property to be satisfied in the system. Formally, let the base feature be F0 = {c1 , c2 , ..., }
To identify the appropriate set of triplets and the local where each ci is a core attribute of F0 . Let, F1 (e.g., slicing)
assumptions, we leverage the following observation. The and F2 (e.g., roaming) be two additional features with at-
authorization verification for a service request in the 5GC tribute sets: F1 = {a1 , a2 , ...}, and F2 = {b1 , b2 , ...}. Since
system depends on multiple authorization attributes, and the F1 and F2 are distinct (i.e, F1 = F2 ) and both include the
checks on different authorization attributes are independent. base feature F0 , the following holds: (F1 −F0 )∩(F2 −F0 ) =
This observation enables us to employ the principle of split ∅, or equivalently, F1 ∩ F2 = F0 . For any feature Fi where
assertion [13] to identify appropriate triplets and the local i = 0, we call attributes in Fi −F0 feature-specific attributes
assumptions. A split invariant is a conjunctively separable and those in F0 base or common attributes. For simplicity,
assertion, which is a global inductive invariant and is a we refer to feature-specific attributes as feature attributes or
Boolean combination of local invariants. It has the form attributes in short, unless stated otherwise.
G1 (V1 ) ∧ G2 (V2 ) ∧ . . . Gn (Vn ), one for each component The key insight is that if a 5GC system is decomposed
M1 , M2 , . . . Mn . On the other hand, a local invariant to a into features, and each feature’s authorization logic is ver-
component Mk is defined only over the variables Vk that ified independently, then the overall access control logic
belong to Mk . of the system is also correctly verified. This is supported
Employing split invariant rules to compositional reason- by two observations: (1) except for the base feature, other
ing enables us to decompose a global property of the 5GC features are optional (e.g., private 5G networks may lack
access control system into several smaller local properties in slicing or roaming); and (2) feature-specific attributes are
such a way that each local property targets only a small part disjoint, so cross-feature authorization logic does not arise.
of the whole system that is independent of the rest. With For example, a consumer NF’s sNssais is checked against
this approach, we can divide the large model of the 5GC allowedNssais (both under slicing), while plmns is checked
access control system and each security requirement (i.e., against allowedPlmns (both under roaming).
a global property) into n smaller and disjoint components Leveraging this insight, we model the 5GC system by
and n local properties so that each local property depends decomposing it into features, each represented as a sepa-
on only one smaller model component. Each decomposed rate model component instantiated as FSMs. This modu-
model corresponds to distinct authorization attributes and lar approach transforms the large, complex state space of
is significantly smaller than the combined model of the the monolithic access control system into several smaller,
system consisting of other disjoint features (see §4.2.2). feature-specific components, each with significantly reduced
This significantly reduces the state space and makes it state space— an essential step toward mitigating state ex-
manageable for the state-of-the-art model checkers to verify plosion. Further details about modeling components are
the local properties of the smaller model components in a provided in §5.
reasonable time. Indeed, this approach enables us to detect
the attack example in Section 3.2 by modeling only the small 4.2.2. 5GC Property Decomposition. Given the decom-
component associated with the indirect communication. posed components of the monolithic 5G access control
system, if a global security property can be partitioned into
4.2. High-level Overview of CoreScan local properties aligned with individual components, then,
by the split-assertion principle (§4.1), verifying each local
4.2.1. 5GC Model Decomposition. We observe that the property within its respective component suffices to establish
5GC access control behaviors can be systematically de- the global property for the system.
 M2 , being an extension of M0 and satisfying A2 M2 G2 
1 Technical 4 Component Specific 7 CE Verification implies that M2 satisfies both G0 and G2 . Moreover, since
Specification Local Property against Specification M1 ∩ M2 = M0 , i.e., all attributes between M1 − M0 and
Refine M2 − M0 are disjoint, by construction, M2 also satisfies
2 Abstract 5 8
G1 provided M1 satisfies G1 . Thus, we get M2 satisfies
Component satisfying Model Checker Violation G0 ∧ G1 ∧ G2 . In this manner, we can show that if we can
construct a component Mi ∈ M − M0 as an extension of
Unsatisfied Verified
M0 and verify Gi ∈ G against Mi ∈ M, then the composite
3
Threat-instrumented
6 state space M = M0 ||M1 || . . . ||Mn will satisfy the target
Counterexample (CE)
property G = G0 ∧ G1 ∧ G2 ∧ · · · ∧ Gn .
Refine
Since Gi targets only the component-specific authoriza-
tion attributes in Mi , and G0 is tested against M0 , we can
Figure 4: CoreScan workflow for an iteration i ignore all assumptions Ai since assumptions only flow from
M0 to Mi . Global property G will be satisfied if only if
for all i, Gi satisfies Mi individually. The above insight
A global property applies to the entire 5GC system hints at the following approach for systematically analyzing
and spans multiple components, whereas a local property 5G access control as presented in CoreScan: for each
is restricted to a single component. For example, consider feature Fi , CoreScan constructs a model component Mi .
the high-level global property: A consumer NF can access Incorporating the threat model gives a threat-instrumented
services/resources only if it is authorized to do so [3], where model Mi . For ease of exposition, in the rest of the paper,
services/resources refer to response packets such as the we use Mi and Mi interchangeably to denote the threat-
NFProfile (in response to NFDiscReq), an AT (in response instrumented model. Based on the model, we construct a
to accessTokenReq), or a service response (in response to local security property Gi targeting only the component-
ServiceReq). A more concrete global property ϕ states: If specific attributes and verify it against Mi . If Mi satisfies
an AT for a producer NF is granted to a consumer NF in a Gi , the analysis terminates. Figure 4 presents the system
accessTokenReq, then the consumer’s NFProfile attributes architecture for an iteration of CoreScan.
must match the authorization attributes in the producer Model Checking Process. We use nuXmv [32], a state-of-
NF’s NFProfile. This property is global because it leaves the-art model checker, against individual components for the
unspecified which specific attributes should be checked, property verification. The model checking process leverages
implying that the monolithic system must verify all relevant the Counter-Example Guided Abstraction Verification (CE-
attributes (e.g., sNssais, plmns) from all available features GAR) principle [33] to verify the properties systematically.
(e.g., slicing, roaming). Here, a component Mi is tested against a local property
Deriving a local property from a global one is a special- Gi to find if it satisfies Mi , i.e., Mi |= Gi . If it is true, it
ization problem: the global property is refined by adding means that the property is verified in the concrete system
component-specific elements. For example, in the slicing under verification. Consequently, we proceed to verify the
component, the local property ϕslicing specifies that the next component Mi+1 with the corresponding local property
consumer’s sNssais must be authorized by the producer’s Gi+1 . However, if Mi |= Gi , then the model checker
allowedNssais. Specifically, local property ϕslicing is: if an gives a counterexample. Now, we have two considerations.
AT for a producer NF is granted to a consumer NF in If the counterexample also exists in the concrete system,
a accessTokenReq, then the consumer’s sNssais attribute then we find a security violation and report it. Otherwise,
must match the allowedNssais attribute in the producer NF’s it is a spurious counterexample (false positive) because of
NFProfile. Similarly, for roaming, the local property ϕroaming the over-approximation due to abstraction applied during
requires that the consumer’s plmns appear in the producer’s model construction. So, we refine Mi to eliminate the spu-
allowedPlmns. rious counterexample. This process continues until the local
property is satisfied in the component. Additionally, in case
4.2.3. CoreScan Workflow. Leveraging the model and we encounter a counterexample that is indeed a violation,
property decomposition techniques, at first, we construct to explore further violations, we refine Gi to suppress the
the bare-bone component M0 , instantiating the base feature counterexample by adding/modifying constraints on model
(§4.2.1) and verify local guarantee property G0 against it attributes. The above approach is repeated until all model
(§4.1). M0 is independent of any particular assumption; thus components are tested.
A0 = true. The rest of the components are constructed Workflow Summary. (i) Following the 5G standard, we
on top of this assuming trueM0 G0  valid, i.e., for all construct six components of the system, equivalent to six
i, j = 0, 1, 2..., n − 1 and i = j , Mi ∩ Mj = M0 . FSMs, instead of modeling the 5GC access control system
If trueM0 G0  is valid, we can construct M1 by as a whole ( 2 in Figure 4). (ii) Then we instrument our
extending M0 with a new feature and verify G1 against threat model in each component ( 3 ). (iii) After that, we take
M1 targeting only the component-specific authorization at- a high-level global access control property and disintegrate
tributes. Thus, A1 M1 G1  being valid implies M1 satisfies it to obtain the local property for each disjoint model com-
both local properties G0 and G1 , i.e., G0 ∧ G1 . Similarly, ponent ( 4 ). (iv) Now, we pass to verify the local property
 Consumer vNRF SCP
registerNRF / ReqReq(NFProfile) & nrfRegistered = T 13 !prodDeregistered /
- /SR (CCA, AT) prodSelected = F
16 SRtoSCPsuccess/- Access SRsuccess/ - SR 8 atrVerified/ ATR(CCA,...) 15 ServiceReq Ready for
SRtoSCP Consumer- 10 hRNF_ATResp(AT)/ vRNF_ATResp(AT) Initialized SR
Initialized Granted m=d Initialized vNRF NRF NRF accessGranted / 12
irect 3 drVerified / DR(CCA,...)
/ SR(A Deregistered Registered SRtoSCP_Resp(...) prodSelected /- AT Granted
m=hybrid / T) 3 5 hRNF_DRResp(..)/ vRNF_DRResp(...)
prodSelected & atExpired /
Ready for

vNRF-(h)NRF
1 m=indirect / SRtoSCP(CCA, AT) !prodDeregistered / DeregReq(NfId) / nrfRegistered = F
SR
atValid / - atValid / - atValid = F
SR
SRtoSCP(CCA) prodSelected = F NRF (hNRF) Complete atExpired /
m = (direct | hybrid) & prodSelected & atValid = F
prodSelected & atValid / - tokFor = - / - NF 11
atExpired / prodSelected /- registerNRF / ReqReq(NFProfile) & nrfRegistered = T !prodSelected /
Discovered atrSuccess /
atValid / - atValid=F SCP-vNRF DR(CCA, tgtPlmn)
atExpired / SCP !prodDeregistered / atValid = T
Consumer AT 9 atrVerified [& CCAverified]/ 2
m = (direct | hybrid) & atValid=F Consumer- atResp(AT) (h)NRF Start prodSelected = F
Granted (h)NRF 7 !atValid &
Registered 6 drSuccess /
prodSelected NRF Deregistered 4 drVerified [ & CCAverified] / Registered tokFor = nfInstance /
NF !prodSelected / drResp(NFProfile) 2 !prodSelected & prodSelected = T ATR(CCA, tgtNfId, tgtPlmn)

Producer-(h)NRF
!prodDeregistered / DR(tgtPlmn) atrSuccess / DeregReq(NfId) / nrfRegistered = F SCP-NRF tokFor = nfInstance /
Discovered !atValid &
prodSelected = F atValid = T DR(CCA,tgtPlmn)
Producer (hProducer) DR atFor = nfType /
m = (direct | hybrid) & !atValid & Initialized ATR(CCA, tgtNfType, tgtPlmn)
drSuccess / tokFor = nfInstance / registerProd / ReqReq(NFProfile) & prodRegistered = T
!prodSelected & 4 tokFor = nfType / ATR
prodSelected=T ATR(tgtNfId, tgtPlmn) Initialized
tokFor = nfInstance/ ATR(CCA, tgtNfType, tgtPlmn)
DR(tgtPlmn) producer 14 srValid & ATauthorized/ producer SCP-
DR !atValid & Deregistered accessGranted = T Registered (h)Producer
Initialized atFor = nfType / ATR Consumer-
m = (direct | hybrid) Initialized DeregReq(NfId) / prodRegistered = F
ATR(tgtNfType, tgtPlmn) (h)Producer 1 Consumer- SCP
& tokFor = nfType /
ATR(tgtNfType, tgtPlmn)

Figure 5: Simplified Abstract model M of the comprehensive 5GC access control mechanism combining all features.
The visiting and the home network producer instances are co-located for simplicity. Similarly, hNRF and NRF
(non-roaming) are co-located. Blue-colored transitions and interfaces depict an authorization flow involving both
indirect communication and roaming.).

in the local component via a model checker ( 5 ). If the path: 7 - 2 - 8 - 3 - 9 - 3 - 10 - 2 - 11 . Now SCP reaches state
property is satisfied, we relax the property to explore other Ready for SR ( 12 ) and initiates ServiceReq to hProducer
paths in the model. Otherwise, we follow the steps from and, if hProducer approves, is granted service access to
§4.2.3 to find each attack( 6 - 8 ). reach state ST Complete via path: 13 - 4 - 14 - 4 - 15 . Then,
SCP forwards the obtained resource to the consumer via
5. Decomposed Model Construction interface 1 . The consumer finally reaches access granted
state upon receiving the resource ( 16 ).
5.1. Abstract model Although the 5GC abstract model presented in Figure 5
is highly simplified, it is evident that all aspects of 5GC
The abstract model of the 5GC can be represented as access control design are difficult to model and formally
a set of FSMs interacting with each other. An FSM is verify due to their complexities and large state space.
represented as a 5-tuple {S, I, O, S0 , F }, where S denotes a
finite set of states, I is a finite set of inputs, O is a finite set 5.2. Features to Components
of outputs, S0 is the set of initial states, and F represents
the finite set of state transitions that define the system’s To manage the state space efficiently, the concept of
transition relation. features is introduced in §4.2.1. Instantiation of a feature
Figure 5 illustrates the comprehensive abstract model M involves constructing an abstract model component (com-
combining all features of the 5GC access control design as ponent in short) consisting of only the respective feature
several interacting FSMs representing different 5GC entities attributes from the 5GC access control design. Thus, a
communicating via respective common interfaces. The in- component is a subset of the comprehensive model M. Each
teracting FSMs include: consumer (MC ), producer (MP ), component is constructed by carefully going through the
NRF/hNRF (MN ), SCP (MS ) and vNRF (MV ). Blue- technical documents [8], [18], [34], [35], [36] specified in
colored transitions and interfaces depict an authorization 3GPP Release 18 [30]. By following the model decompo-
flow example involving both indirect communication and sition principle (§4.2.1), we first start by constructing the
roaming, and involve all five FSMs. In this example, a bare-bone component M0 , instantiating the base feature:
consumer starts from Consumer Registered state by sending {NFType, allowedNfTypes,...}. It does not include network
a ServiceReq to SCP with CCA token attached ( 1 ) through entities such as SCP or vNRF or any attributes related to
interface 1 . SCP starts from SCP Start state, constructs network slices (e.g., sNssais, allowedNssais) or inter-PLMN
and sends NFDiscReq to vNRF ( 2 ) via interface 2 . and communications (e.g., plmns, allowedPlmns). Specifically,
reaches DR Initialized state. vNRF at NRF Registered state, M0 contains a pair of NC and NP instances, an NRF
verifies the packet and forwards it to the correct hNRF ( 3 ) instance, all important access control packets (Figure 2)
via interface 3 . hNRF verifies the request along with the such as UpdateReq, accessTokenReq, and ServiceReq, and
CCA token, and if successful, responds with discovered finally, the corresponding response packets, i.e., discovered
NFProfiles to SCP via path: 4 - 3 - 5 - 2 . SCP selects a NFProfile and constructed AT. Component M0 is entitled to
producer from the discovered ones and reaches NF Dis- verify a local property G0 (§4.1).
covered state. From here, SCP issues accessTokenReq to The following components are constructed on top of M0 .
vNRF and receives an AT to reach AT Granted state via the For instance, M1 is constructed by adding attributes related
 Consumer NRF

sp SR - / SR(AT)
q/Re/Resp /- registerNRF / ReqReq(NFProfile) & nrfRegistered = T
yRe
over nReq
NRF
ess Initialized Ready
cc
Disc ssToke su for SR atrVerified / atResp(AT)
Acc
e SR !prodDeregistered / NRF NRF
NFService
Access prodSelected = F Deregistered drVerified/drResp(NFProfile) Registered
ServReq/Resp NFService prodSelected & atExpired /
operation Granted atValid=F prodSelected /- DeregReq(NfId) / nrfRegistered = F
operation atValid / - atValid / -
atExpired / AT
prodSelected NF atValid=F Granted Consumer-NRF Producer-NRF
Consumer
Discovered !prodSelected /
Control variables Registered !prodDeregistered / Producer
DR(tgtNfType) atrSuccess /
(updateLevel, adversaryPresent, adversaryDiscoveryReq, ...) prodSelected = F registerProd / ReqReq(NFProfile) & prodRegistered=T
!atValid & atValid = T
!prodSelected & drSuccess / tokFor = nfInstance / srValid & ATauthorized /
Figure 6: Schematic of the bare- tokFor = nfInstance/ prodSelected=T ATR(tgtNfId) producer accessGranted=T
producer
Registered
DR(tgtNfType)
bone component M0 . The gray region DR !atValid &
Deregistered
DeregReq(NfId) / prodRegistered=F
atFor = nfType /
encapsulates the protocol module, tokFor = nfType / Initialized
ATR(tgtNfType) ATR
ATR(tgtNfType,) Initialized Consumer-Producer
while the dotted rectangle denotes the
abstracted NRF instance with its NF-
Profile not modeled. Figure 7: Simplified abstract model of the bare-bone component M0 .

to feature nf-domain:{fqdns, allowedNFDomains,...}. M1 state variables, transitions, and authorization logic, repre-
is entitled to test the local property G1 . Similarly, M2 , sents the access control-related stateful functionalities of the
M3 , M4 , and M5 are built upon M0 by adding features protocol participants. We separately model each API request
and authorization attributes corresponding to network slic- and response in the protocol module by capturing only
ing: {sNssais, allowedNssais,...}, roaming: {plmns, allowed- the relevant authorization-related HTTP header and body at-
Plmns,...}, indirect (communications): {CCA,...} and finally tributes as state variables. For instance, out of 119 attributes
other consisting of miscellaneous attributes of the NFProfile: in the NFDiscReq packet, we model only five authorization-
{load, priority,...}, respectively. M2 − M5 are entitled to relevant ones in M0 : {requesterNFType, serviceName, ...}.
verify target local properties G2 − G5 , respectively. The corresponding NFDiscResp is modeled as an NFProfile
representing the discovered producer. Other requests, like
5.3. Construction of Bare-bone Component (M0 ) accessTokenReq and ServiceReq, are modeled similarly. Fig-
ure 7 depicts the abstract model of the protocol module.
We present the bare-bone model component M0 to il- This modular and parameterized design choice also sig-
lustrate the construction of each component. M0 simulates a nificantly reduces model complexity while providing the
simplified 5GC as a set of communicating FSMs (Figure 6) flexibility to instantiate multiple protocol runs with dif-
and includes five entities: two consumer instances: NC1 and ferent consumer–producer pairs, each capable of running
NC2 , two producer instances: NP1 and NP2 , and a single different authorization requests. For instance, at runtime, any
NRF instance. Each consumer and producer FSM main- consumer instance (e.g., NC1 or NC2 ) in M0 can act as NC
tains an NFProfile via state variables (e.g., NFInstanceID, by populating its NFProfile attribute-values. Similarly, one
NFType) and needs to register it to NRF to enable NF inter- of the two producer instances (NP1 , NP2 ) can be selected as
communication in the network via RegReq or UpdateReq NP . In one protocol run, one can instantiate the protocol
(not shown in Figure 6). A registered consumer NF initiates module with NC =NC1 and NP =NP2 and can model NC1
network interaction through a pair of authorization requests, issuing an ServiceReq to access resources/services from
i.e., NFDiscReq and accessTokenReq, before requesting ser- NP2 . In another run, the module can be instantiated with NC
vices or resources via ServiceReq. The NRF, modeled as a =NC2 and NP =NP1 , modeling NC2 issuing an NFDiscReq
trusted singleton, verifies authorization requests based on the to access resources/services from NP1 .
NFProfiles of consumers and expected producers. Since its Finally, M0 includes a construct called modelParam
own NFProfile does not directly participate in authorization to capture configurable features and corresponding control
checks, its NFProfile is abstracted away and, thus, not logic. For example, the 3GPP specification [8] allows oper-
modeled. Instead, we capture its essential behaviors using ators to reject authorization requests missing optional API
dedicated model variables, e.g., isNFDiscovered which en- attributes with the requester- prefix. We model this behavior
codes the authorization logic for NF Discovery and stores using a non-deterministic, optionally configurable boolean
NRF’s authorization decision upon receiving an NFDiscReq. variable, requesterInfoReq, defined under modelParam.
We design a parameterized module called protocol
(gray region in Figure 6) to model access control-related 5.4. Construction of M1 -M5
protocol interactions between a consumer-producer pair.
This module includes a generic consumer (NC ) and a Components M1 and M2 are structurally similar to M0
producer (NP ), one instance of each request/response type and do not require modeling additional FSMs, however,
between them, and models variables capturing NRF’s autho- require modeling component-specific attributes as discussed
rization logic. We represent the protocol module with syn- in §5.2. M3 includes an additional FSM, vNRF, to model the
chronous communicating FSMs. Each FSM, defined using behaviors of visiting network’s NRF. Finally, to incorporate
indirect and hybrid communication modes, another FSM
called SCP is added in M4 . To simplify the modeling and
slice:
l NRF slice:
overcome state explosion, M4 includes a special ServiceReq
message specific to SCP to supply important attributes so accessTokenReq slice: slice:
1
that SCP can use those to form valid authorization requests (service: )
on behalf of the consumer NF. Some important parameters allowed to access of
include CCA token, important NFProfile attributes for au- All slices of added
thorization requests, etc. access token
2
For components M0 , M1 , M2 , M3 , and M5 , we consider service: ,
a threat model where a single registered consumer NF or producerSlice:
a producer NF, compromised by a malicious actor, sends NFDiscReq
fabricated network packets (NFDiscReq, accessTokenReq, 3
(NFType: , service: )
etc.) to seek unauthorized access to the services or resources NFProfile
provided by the benign entities in 5GC (benign NFs, NRFs). ServiceReq
Additionally, M3 considers that the vNRFs, being an entity 4
(operation:
, access token) confirms slice access
in a foreign network, can also be malicious and thus can operation specific for slice
exhibit malicious intent. Finally, for component M4 , our granted
threat model considers SCP to be malicious and can create Success
5
and alter network packets before forwarding to arbitrary des-
tinations in search of unauthorized access. We incorporate Figure 8: Message flow for Coarse Scope Attack
the above adversary capabilities into the respective Mi to 7.1. New Attacks
obtain the threat-instrumented component Mi .
CoreScan uncovered five new access control attacks.
6. Implementation The implications of these attacks range from privilege es-
calation and sensitive information exposure to denial-of-
We use nuXmv [32] model checker to model and ver- service. In what follows, we discuss the uncovered vulner-
ify access control properties for CoreScan. nuXmv is an abilities, attack details, and their impacts.
infinite-state symbolic model checker used for the formal
7.1.1. Coarse Scope Attack (A1). This attack exploits
verification of finite- and infinite-state systems. It facilitates
producerSlice, an optional attribute of the access token,
modeling through an intuitive and high-level language SMV
and affects all communication modes and 5G roaming.
(Symbolic Model Verifier). In this language, the system
Assumption. In this attack, a consumer NF (NC ) acts as an
under consideration can be described using modules that de-
adversary and thus can forge/modify and send any network
fine states, transitions, and variables. The modeling process
packets on behalf of the consumer. We also assume that the
involves specifying the system’s behavior and its various
adversary NF has authorized access to at least one network
components, including their interactions and constraints.
slice of the victim producer NF (NP ) but not others.
Property checking in nuXmv is performed by specifying
Vulnerability. The root cause of this attack lies in the
formal properties using temporal logic such as LTL (Linear
incorrect handling of the producerSlice attribute in
Temporal Logic). Once the system model and properties
the access token issued by the NRF after a successful ac-
are defined, nuXmv uses symbolic techniques to explore all
cessTokenReq authorization. Specifically, instead of includ-
possible states and transitions within the model. It checks
ing only the authorized slices for the requested NFService,
whether the specified properties hold true in all possible sce-
the NRF mistakenly adds all slices of the producer NF to
narios or if there are counterexamples where the properties
the producerSlice attribute. Consequently, a malicious
might be violated.
consumer NF can use this access token to access NFService
operations across all slices served by the producer NF,
7. Evaluation beyond those to which the malicious NF is authorized to.
Additionally, there are issues during ServiceReq validation
With CoreScan, we modeled the access control mecha- by the producer NF. First, the producerSlice attribute
nism specified by 3GPP Release 18 [30] and analyzed it with is optional and may not be present in the access token. Even
61 properties. We first present CoreScan’s effectiveness in if it is included, some producer NFs may not support this
detecting new and prior attacks. We also discuss the nuances attribute, making the attack trivial in such cases [8], [35]. In
and our observations while constructing models alongside other cases, during ServiceReq validation, the producer NF
the recommendations to make 5GC access control more cannot verify whether the NRF has incorrectly included all
robust and complete. We then demonstrate the efficiency slices, leading it to approve service requests for unauthorized
and performance of CoreScan with respect to the time slices from the consumer NF.
CoreScan takes to verify a property and compare that with Attack Description. Figure 8 illustrates Coarse Scope At-
that of the prior work 5GCVerif. We use a machine with tack using a simplified direct communication model. Con-
Intel i5-7200U CPU and 8GB DDR3 RAM for evaluation. sider a scenario where the adversarial consumer NF (NC )
 Assumptions. Beyond the assumptions of Coarse Scope At-
: SMF : AMF SCP NRF
tack, this attack additionally requires that the 5GC network
1 obtains CCA supports hybrid communication via SCP, and that a CCA
token is used for authentication and authorization.
DR (CCA , target = UDM) Vulnerability. This attack is enabled by two key issues:
2
DR (CCA , target = UDM) (1) During indirect or hybrid communication, a benign NF
3 leaks its CCA token to the adversarial serving NF without
From CCA , NRF authorizes ensuring replay protection. The malicious NF can then use
request based on 's credentials this token to impersonate the legitimate consumer NF and
and grants access to NFProfile send authorization requests to the NRF via SCP. Since SCP
signed and forwarded the request, the NRF cannot detect
NFProfile
4
that an adversary replayed the token. Although the 5G
NFProfile specification states that the CCA token should be short-lived,
5
it does not mention potential lifespans. Moreover, time-
Figure 9: Message flow for NFProfile Leakage Attack based replay protection is not reliable, and due to network
reliability issues, it is safe to assume that the malicious
consumer NF will have sufficient time to send at least one
authorization request using the CCA, which is sufficient to
is part of slice 1 and is authorized to access NFService exploit the attack. Other than a ‘short’ lifespan, 3GPP has
S of a producer NF (NP ). The NFService S is divided not provided any other mechanism for replay protection for
into two logical slices, S1 (serving slice 1) and S2 (serving CCA tokens. (2) SCP does not verify whether the CCA
slice 2). Thus, NC is only permitted to access S1 and token was originally signed by the sender NF, allowing the
not S2 . However, CoreScan identifies a counterexample malicious NF to exploit this lack of validation.
where the consumer NF gains unauthorized access to S2 Attack Description. Consider a scenario (Figure 9) where a
via ServiceReq. The attack proceeds as follows: The mali- benign NF instance N2 of NFType:AMF has authorized ac-
cious consumer NF invokes accessTokenReq to request an cess to services from two NF instances: N1 of NFType:SMF
access token for NFService S from the NRF ( 1 ). The NRF and N3 of NFType:UDM (not shown in Figure 9). When
authorizes this request because S1 serves slice 1, which NC N2 makes a service request to N1 via SCP (in either
is allowed to access. However, while generating the access hybrid or indirect communication mode), it reveals its CCA
token, the NRF incorrectly includes all slices of NP , i.e., token: id: N1 , aud: NRF, SMF  to N1 , which acts as
both slice 1 and slice 2, as per the 5G specification TS the adversary ( 1 ). The adversarial NF N1 then crafts a
33.501, which states that the producerSlice attribute malicious NFDiscReq impersonating N2 to search for the
should be the superset of all network slices served by the NFProfiles of UDM instances accessible to N2 (e.g., N3 ).
producer NF’s NFServices. With the access token in hand It forges NFDiscReq by setting the target NFType to UDM,
( 2 ), the adversarial consumer retrieves the endpoints (IP attaches N2 ’s CCA token, and sends it via SCP ( 2 ). SCP
addresses) of the producer NF by invoking NFDiscReq ( 3 ). repackages, signs, and forwards the request to NRF ( 3 ).
The consumer NF then uses the access token to invoke an Now, NRF, mistakenly identifying the request as originating
API operation (OpS2 ) under NFService S2 via ServiceReq, from N2 , authorizes it based on N2 ’s access rights and
requesting a service or resource from slice 2 ( 4 ). The retrieves the NFProfile of N3 . It then sends this sensitive
producer NF, upon validating the access token, finds that the NFProfile information to SCP, which forwards it to N1 ( 4 -
producerSlice attribute includes slice 2. Consequently, 5 ), thereby leaking sensitive information to the adversary
it mistakenly grants access, allowing the consumer NF to under the guise of legitimate access.
obtain the unauthorized service ( 5 ). Impact. The impact of this attack is that a malicious NF
Impact. With this attack a malicious consumer NF can gain can gain unauthorized access to sensitive NFProfiles, poten-
unauthorized access to NFService operations across multiple tially exposing critical configuration and service information
slices, bypassing slice-specific access controls. This exploit of other NF instances. This leakage compromises network
compromises the isolation between network slices, poten- security, potentially enabling further exploitation and unau-
tially leading to data leakage, service disruption, and unau- thorized service usage.
thorized resource usage. Although the attack is demonstrated
above for direct communication, CoreScan discovered the 7.1.3. CCA Replay Attack (A3). This attack shares sim-
same attack for indirect communication, hybrid, and 5G ilarities with the demo attack illustrated in Figure 3 and
roaming. discussed in § 3.2. We initially discovered the demo attack
in 2023 while analyzing Release-17 [37]. In 2024, we
7.1.2. NFProfile Leakage Attack (A2). In this attack, a ma- switched to Release-18 [30] and found that the vulnerability
licious NF exploits a vulnerability in the CCA token-based was patched in Release-18 [8] because- (1) The producer
hybrid communication mode (§3.2) to extract NFProfiles of NF now verifies, in the direct communication, that the
any NF instances that the legitimate NF, which signed the consumer’s NFInstanceID in the access token matches the
CCA token, has access to. NFInstanceID in the request signature, preventing unau-
 :AMF :SMF :SMF :SMF : UDM
slice: 1, 2 slice: 2 SCP NRF slice: 1 slice: vSCP vNRF hNRF slice

1 obtains CCA from 1 ATR(req=SMF, target=UDM, slice:2)

2 ATR (CCA , target = SMF, slice:2)

Verifies and allows access of
:UDM to ,
3 ATR (CCA , target = SMF, slice:2)
despite being from slice:1
ATSMF (slice: 2)
4 DR (CCA , target= SMF, slice: 2) 2 ATUDM (id= , slice:2, NFType:UDM)
NFProfile
5 SR (CCA , ATSMF (slice: 2)) 3 Discovery
6 Success

4 SR (slice:2, ATUDM)
Figure 10: Message flow for CCA Replay Attack

Figure 11: Message flow for CCA Evasion Attack

thorized service requests from malicious NFs ( 9 in Fig-
ure 3). (2) CCA token now includes the expected producer’s
NFType instead of the generic ‘PRODUCER NF’ string. The malicious instance N2 validates both tokens and com-
This ensures that the demo attack fails in indirect or hybrid pletes the unauthorized service request ( 5 - 6 ). In this way,
communication due to the NFType mismatch between the a malicious SMF instance N2 of slice 1 achieves illegitimate
access token (e.g., PCF) and the CCA token (e.g., SMF). access to resources of SMF instance N3 of slice 2.
However, our 2024 analysis reveals that the demo attack Impact. NF interactions between NFs of the same type
persists due to a new flaw, leading to the discovery of are critical, especially, for 5G handover procedure in the
CCA Replay Attack, which remains exploitable despite the network side during mobility. The attack enables a malicious
Release-18 updates. NF to gain unauthorized access to services across different
network slices, disrupting the isolation between slices in 5G
Assumption. Beyond the assumptions in Coarse Scope At- networks.
tack, this attack assumes that a malicious NF, using hybrid
or indirect communication, can receive a CCA token from 7.1.4. CCA Evasion Attack (A4). In this attack, a malicious
a benign NF that it provides services to. consumer NF exploits vulnerabilities in certain NFs to gain
Vulnerability. This attack exploits the similar vulnerabilities unauthorized resource or service access through forged ser-
discussed in NFProfile Leakage Attack that uses NFDiscReq vice requests in hybrid or indirect communication scenarios,
API for hybrid or indirect communication to illegitimately particularly during roaming.
obtain NFProfiles. However, this attack exploits accessTo- Assumption. In addition to the assumptions in §7.1.1, this
kenReq in indirect communication to obtain illegitimate attack assumes the use of SCP in inter-PLMN, i.e., inter-
service access potentially from an unauthorized network network communication, where a consumer NF in the visit-
slice. Despite the security enhancements in Release-18 for ing network acts as an adversary. The attack is even possible
CCA and access tokens to mitigate the demo attack in direct in some non-roaming cases as well.
communication, a vulnerability persists when a malicious Vulnerability. The attack leverages the absence of CCA
NF makes an indirect or hybrid service request to another token validation during 5G roaming. In roaming scenarios,
NF instance of the same NFType but serves a different the producer NF in the home network (HPLMN) cannot
network slice. verify the CCA token received from the visiting network,
Attack Description. Consider a simplified scenario in Fig- as 5G standards rely on implicit hop-by-hop authentication,
ure 10, where the 5GC has an AMF instance N1 operating e.g., consumer NF to vSCP (SCP of the visiting network,
in both slice 1 and slice 2, along with two SMF instances: VPLMN), vSCP to vNRF (NRF of the VPLMN), vNRF
N2 (slice 1) and N3 (slice 2). Suppose that the malicious to hNRF (NRF of the HPLMN) [8]. However, this method
instance N2 intends to exploit this vulnerability. It waits for fails to prevent NF impersonation. The attack can also occur
a service request from N1 via indirect communication. Upon within the same PLMN if the producer NF or NRF opts not
receiving the CCA token CCAN1 : id: N1 , aud: NRF, SMF to use CCA tokens for indirect or hybrid communication, as
from N1 ( 1 ), N2 requests an access token from SCP for CCA token-based security is optional and may be replaced
accessing a service in slice 2 ( 2 ). The SCP forwards this by implicit methods based on the operator’s policy.
request to NRF, which, due to the CCA token’s presence, Attack Description. Consider a scenario where a malicious
assumes the request is from N1 with legitimate access consumer NF N1 of NFType:SMF and serves slice 1 only,
to slice 2 and issues the access token ATSMF sub: N1 , in the visiting network, aims to gain unauthorized access
aud: SMF ( 3 ).Next, if necessary, the SCP may perform to a UDM instance NP serving slice 2, which does not
a NFProfile search via NFDiscReq ( 4 ). Finally, the SCP authorize N1 (Figure 11). To exploit this, N1 sends a
initiates the service request using ServiceReq via indirect forged accessTokenReq by misreporting its slice information
communication, attaching CCAN1 and access token ATSMF . (slice 2 instead of slice 1) via the requesterSlice
 : UDM : UDM priority than N3 . However, the malicious N2 misreport this
: AMF SCP NRF Priority: 2 Priority: 1 seemingly security-insensitive attribute of the NFProfile to
1
NFRegReq/ NRF via UpdateReq/RegReq ( 1 ). Now, A consumer NF in-
NFUpdateReq stance N1 looking for some services from UDM searches for
DR (target=UDM, service: ) (priority = 0) available UDM instances via NFDiscReq ( 2 ) and discovers
2
NFProfiles both N2 and N3 . However, based on the priority and balance
selects (not shown in this example), it naively selects N2 . In the
due to lowest priority following communications, it obtains an access token from
ATR (service: ) NRF via accessTokenReq ( 3 ) and makes service requests
3
AT via ServiceReq to N2 ( 4 - 5 ), thus N2 ’s goal is achieved
SR(CCAAMF) SR(CCAAMF)
4 as it has successfully forced N1 to send request to it and
API, Access Token API, Access Token
deprives N3 which with lack of request will get removed
Received CCAAMF
Run other attacks
automatically by the network to reduce unnecessary load in
5 SRResponse
the cloud.
Impact. DoS attack is a direct consequence of the vulner-
ability. However, This vulnerability can exploited by the
Figure 12: Message flow for Forced NF Selection Attack malicious NF in several ways. For example, If the consumer
NF uses a hybrid or indirect communication mode to invoke
the service request to the malicious producer NF ( 4 - 5 ),
parameter. The request is forwarded from the vSCP to then it may leak its CCA token to the producer in a similar
the vNRF, which cannot validate the authenticity of the way to CCA Replay Attack. However, it solves a problem
request ( 1 ). The vNRF then forwards it to the hNRF, which of NFProfile Leakage Attackor CCA Replay Attackthat these
mistakenly assumes that N1 is part of slice 2, and issues an attacks are short-lived because of the short life span of the
access token: id:N1 , producerSlice:slice 2, target: UDM, CCA token. Exploiting this vulnerability, those attacks can
granting access to any UDM instances in slice 2 (e.g., NP ) be performed repeatedly by a malicious NF.
( 2 ). Using this token, N1 can then retrieve the endpoint
information of NP ( 3 ). Finally, with the access token and 7.2. Attack Validation
endpoint address, the malicious NF makes a ServiceReq
through SCP, gaining unauthorized access to services and Since commercial 5GC networks are closed-source,
resources in NP ’s slice 2 in the same way as 1 . we validated our findings using open-source implementa-
Impact. A malicious NF can impersonate any consumer NF tions [5], [6], [7]. Among these, only free5GC partially
to gain unauthorized access to services and resources across implements 5G access control but lacks support for indirect
the network, bypassing proper authentication checks. This communication and 5G roaming. Thus, only Coarse Scope
breach undermines network security, enabling unauthorized Attack could be effectively validated in free5GC. We found
service usage and data exposure. that the root cause of the attack in free5GC is the omission
of the optional producerSlice attribute in the access token,
7.1.5. Forced NF Selection Attack (A5). This attack ex- making exploitation trivial.
ploits a vulnerability in the 5G access control that opens For further validation, we submitted CoreScan findings
the door for other overprivileged attacks. Through this, a to GSMA along with feasible patches (appendix B). As of
malicious NF can misreport seemingly security-insensitive April 2025, GSMA has agreed to submit change requests
metadata of the NFProfile to force a benign consumer NF (CRs) for attacks A1–A3. For A5, GSMA considers the
to select the malicious NF as a producer NF. attack relevant but an implementation issue. So, no CR is
Assumption. Besides the assumptions of Coarse Scope required other than notifying GSMA members. A4 remains
Attack, this attack assumes that a malicious NF is capable under discussion. Further updates will be on Github [15].
of updating its metadata in the NFProfile, such as priority,
load, etc. 7.3. Existing Attacks
Vulnerability. The vulnerability lies in how an NF/SCP
selects a producer NFs from the list of NFProfiles ob- Apart from the above new attacks, CoreScan also con-
tained from NRF via NFDiscReq. According to the 5G firms some existing attacks found in previous works [3]. (1)
standard [35], a consumer NF/SCP uses attributes such as Confused Producer Attack: Here, a malicious consumer NF
load, and priority (with 0 meaning the highest priority) to exploits an attribute describing allowed producer’s NFType
select a suitable NF. Thus, a malicious NF can misreport in a legitimate access token to gain unauthorized access to
these NFProfile attributes to force other NFs to NRF so a different instance of the same NFType in another network
that other NFs select the malicious NF as a producer more slice, leading to potential overprivileged access and sensitive
frequently. data leakage. However, we found that this attack is no longer
Attack Description. Consider a simplified scenario (Fig- possible in Release-18 since 3GPP patched the attack by
ure 12) where the 5GC contains two UDM instances: N2 modifying the authorization checks. (2) Token Reuse Attack:
and N3 with priority 2 and 1 respectively, i.e., N2 has lower Here, a malicious consumer NF uses an unexpired access
token to access a producer NF’s services even after its compared to the original 5GCVerif. These results highlight
permissions are revoked, exploiting the lack of real-time the superior scalability and efficiency of CoreScan com-
validation of the token’s revocation status. All communica- pared to both standard and extended versions of 5GCVerif.
tion modes and 5G roaming suffer from this attack. (3) De-
fault Overprivilege Attack: Here, a malicious NFC exploits
the ‘allow by default’ rule in 3GPP’s specification, gain-
ing unauthorized access to network slices by removing its
serving slice attribute temporarily from its NFProfile. This
attack is also applicable in all communication modes and
roaming. (4) Authorization Bypass Attack: Here, a malicious
NFC exploits the lack of cross-NFProfile check between the
consumer and the producer NF, allowing it to gain sensitive
information from an unauthorized NF. We found that this
attack’s possibility depends on the operator’s policy since
some operator may implement it while others may not. This Figure 14: Performance analysis of CoreScan component
attack can be carried out across all communication modes,
including roaming scenarios. TABLE 1: Modeling and analysis efforts in terms of
number of states, transitions, and lines of code
Model/Components #State variables #states LoC
bare-bone 179 367 2320
nf-domain 225 548 2518
slicing 243 494 2771
roaming 282 634 2821
indirect 206 424 2517
other 212 437 2670
CoreScan 282 634 15617
5GCVerif [3] 471 1397 5150
(a) (b)
Avg 224.5 484 2602.83
Figure 13: Performance comparison of (a) CoreScan
and 5GCVerif-Extended, (b) CoreScan-Minimal and
5GCVerif. 7.5. Modeling and Analysis Effort

7.4. Performance Analysis Table 1 presents the number of state variables and states
for each CoreScan component, as well as for the full
Our model consists of six independent components that CoreScan model and the baseline 5GCVerif [3]. We im-
can verify properties concurrently and thus enhance scala- plemented CoreScan in the SMV language [32], with a total
bility. We benchmarked our approach against 5GCVerif [3], of 15,617 lines of code. Since all CoreScan components
which supports a limited subset of these components. To operate in parallel, the overall number of state variables and
ensure a fair comparison, we extended CoreScan to cover states correspond to that of the largest individual component.
all components analyzed in our study. Experiments were Among the six components, roaming is the most complex,
conducted seven times, varying the trace depth from 10 to with 282 state variables and 634 states, primarily due to the
70 in increments of 10. inclusion of an additional NRF instance (vNRF) and asso-
As shown in Figure 14, the runtime of the six compo- ciated forwarding network packets and authorization logic.
nents of CoreScan increases with trace depth; however, at On average, each CoreScan component is modeled with
each trace depth, the runtime across different components approximately 225 state variables, 484 states, and ∼2603
remains similar, with minimal variance observed across lines of code. Despite being more feature-rich and hav-
repetitions. Since the components execute in parallel, the ing a codebase nearly three times larger than 5GCVerif,
overall runtime of CoreScan is determined by the maximum CoreScan requires 40% fewer state variables and 55% fewer
runtime among them. states, highlighting its scalability and efficiency.
Figure 13(a) compares between CoreScan and the ex- The entire modeling process took approximately 13
tended version of CoreScan, demonstrating that CoreScan months, including understanding 5G specifications, de-
achieves significantly lower runtimes, with an average per- signing abstraction techniques, and encoding the mod-
formance improvement of over sevenfold. For the original els and properties. While 3GPP releases minor updates
5GCVerif, which supports only two components (AC-nftype (e.g., Release-17.3.0 to 17.4.0) roughly every three months,
and AC-snssai), we compare it with the maximum runtime these incremental changes can typically be integrated into
of these specific components in CoreScan, referred to as CoreScan within two weeks. In contrast, major releases
CoreScan-Minimal. Figure 13(b) confirms that CoreScan (e.g., Release-17 to Release-18) may require 2–3 months
delivers an average performance gain of more than ninefold to accommodate new features and structural changes.
 Verification of the 61 security properties took a total of positives (FP), i.e., spurious counterexamples. After refine-
∼32 minutes (excluding time for counterexample analysis). ment, we did not observe any spurious counterexamples
On average, CoreScan took 47 seconds to verify each (FP = 0), yielding a 100% precision (TP / (TP + FP) =
property up to depth 40, but only ∼0.2 seconds when it 1 where TP denotes true positives). Recall measures how
identifies a counterexample . many actual violations have been successfully detected, i.e.,
TP/(TP+FN) where FN denotes false negatives. However,
8. Related Work since, being an unknown quantity, the total number of
actual violations is undecidable, recall is not measurable.
Access control analysis of 5GC. Ensuring robust 5G access We have carefully constructed our formal models based on a
control has become essential due to the rapid and extensive comprehensive examination of the 5G specifications. Similar
deployment of the 5G-based applications [38]. Prior works to previous model-checking works [3], [40], we follow the
have formalized existing access control approaches [39], conventional approach of aiming for soundness instead of
[40], and have introduced novel access control frameworks completeness, i.e, if our approach reports a violation, it is
and enhancements to address emerging security demands indeed a violation; we cannot, however, detect all violations.
[14], [41], [42]. In addition, some research has explored Analysis Scope. CoreScan’s primary focus is to analyze
quantum-resistant access control mechanisms [43], too. To the design of the 5G access control mechanism. However,
analyze existing access control mechanisms, Akon et al. [3] it may not detect issues stemming from NF misconfigura-
proposed a formal model-checking approach using the small tions, implementation bugs, or other runtime vulnerabilities
model theorem to identify flaws in the 5G core’s access con- beyond its analysis capabilities. Additionally, our analysis
trol mechanism. Thorn et al. [2] designed a program anal- is limited by the 3GPP 5G standards, i.e., if an operator
ysis framework, performing static analysis on open-source enforces stricter policies beyond 5G standards, our findings
implementations of the 5G access control, and conducted may not apply. However, CoreScan’s modeling discipline
submodular analyses using the least privileged principle to allows operators to mark certain NFs as benign per the
identify potential over-privileges. However, the open-source operator’s policy, making analysis possible for such cases.
implementation they considered does not represent reference CoreScan covers both intra- and inter-PLMN access
implementation utilizing OAuth 2.0. In addition, none of control, enabling our analysis to apply to both Local Break-
these approaches cover indirect and hybrid communication out (LBO) and Home Routing (HR) scenarios. In LBO, user
and roaming scenarios, which have been prevalent from traffic is routed locally within the Visited PLMN (vUPF to
release 16 of the 5G standard. vDN), while in HR, traffic is tunneled back to the Home
Generic access control analysis. Extensive research has PLMN (vUPF to hUPF to hDN). The key distinction lies
been conducted on analyzing access control, particularly in in Data Network (DN) access [18]: in LBO, vUPF–vDN is
operating systems [44], [45] and the ARBAC model [46]. intra-PLMN, whereas in HR, vUPF–hUPF is inter-PLMN
Static analysis has also been applied for access control and hUPF–hDN is intra-PLMN.
analysis [47], [48], [49]. Gouglidis et al. [50] modeled Attack Domain. The scope of attacks identified by
Google’s RBAC (Role-Based Access Control) Identity and CoreScan is constrained by the specific security properties
Access Management (IAM) based on publicly available tested within the model. Therefore, we do not claim that the
information by constructing a temporal logic-based transi- set of discovered attacks is exhaustive.
tion system, which was then used to verify specific user- Defenses. We deliberately exclude detailed countermeasures
defined properties. Shen et al. [51] proposed a framework from the main body since adding fixes without carefully
that automatically adjusts configurations to resolve access- accounting for other system factors (e.g., backward compat-
deny issues by exploring configuration changes that enable ibility) can result in fragile or ineffective solutions. More-
minimal necessary permissions. Machine learning (ML) ap- over, some defenses (§7.1.4) require major design overhauls
proaches are also being applied to enhance access control, and are beyond the scope of this work. Instead, we are
as discussed by Nakamura et al. [52]. In addition, Natural collaborating with the GSMA CVD panel to formulate long-
Language Processing (NLP) techniques have been used to term recommendations for specification updates. Appendix
extract as well as generate access control policies [53], [54], B outlines potential short-term mitigations.
[55], [56]. In the context of 5G, OAuth 2.0 [17] serves as the
reference for access control. Several studies have previously 10. Conclusion and Future Work
examined OAuth implementations and identified security
vulnerabilities for specific use cases like microservice and We have developed CoreScan, the first comprehensive
web applications [57], [58], [59], [60], [61], [62]. Following formal analysis framework for analyzing the access control
Akon et al. [3], our work focuses on analyzing OAuth 2.0 mechanism of 5GC. CoreScan employs compositional veri-
within the context of 5GC standards. fication technique that leverages the assume-guarantee style
reasoning approach to decompose the system model into
9. Discussion disjoint components and uses the split assertion principle
identify local assumptions and guarantees. With CoreScan,
Analysis Accuracy. We leverage CEGAR framework we tested 61 access control properties and uncovered five
(§4.2.3) to iteratively refine the model and eliminate false new classes of exploitable privilege escalation vulnerabilities
in the 5G standards. In the future, we will develop mitigation [17] D. Hardt, “The OAuth 2.0 Authorization Framework,” RFC 6749.
techniques for the uncovered issues. [Online]. Available: {https://doi.org/10.17487/rfc6749}
[18] 3GPP, “System architecture for the 5G System (5GS),” TS 23.501,
Acknowledgments Version 18.7.0. [Online]. Available: {https://www.3gpp.org/ftp/Specs/
archive/23 series/23.501/23501-i70.zip}

We appreciate the anonymous reviewers and the shep- [19] “Telecoms: How 5G will revolutionise the MVNO market,” https://
telecoms.com/opinion/how-5g-will-revolutionise-the-mvno-market/,
herd for valuable feedback and GSMA’s support during [Online; accessed July 25, 2023].
the vulnerability disclosure process. This work has been
[20] “5GRadar: Discover how MVNOs can make the
supported by the NSF under grants 2145631 and 2215017, most of 5G,” https://www.5gradar.com/features/
the Defense Advanced Research Projects Agency (DARPA) discover-how-mvnos-can-make-the-most-of-5g, [Online; accessed
under contract number D22AP00148, and the NSF and July 25, 2023].
Office of the Under Secretary of Defense—Research and [21] “Over 900,000 Kubernetes instances found exposed
Engineering, ITE 2326898 and 2515378, as part of the online,” https://www.bleepingcomputer.com/news/security/
NSF Convergence Accelerator Track G: Securely Operating over-900-000-kubernetes-instances-found-exposed-online/, [Online;
accessed July 25, 2023].
Through 5G Infrastructure Program.
[22] “Hildegard: New TeamTNT Cryptojacking Malware Tar-
geting Kubernetes,” https://unit42.paloaltonetworks.com/
References hildegard-malware-teamtnt/, [Online; accessed July 25, 2023].
[23] “5G Networks Are Worryingly Hackable,” https://spectrum.ieee.org/
[1] D. Fett, R. Küsters, and G. Schmitz, “A comprehensive formal secu- 5g-virtualization-increased-hackability, [Online; accessed July 25,
rity analysis of OAuth 2.0,” in Proceedings of the 2016 ACM SIGSAC 2023].
Conference on Computer and Communications Security, 2016, pp.
1204–1215. [24] “CVE-2016-1906,” https://www.cvedetails.com/cve/CVE-2016-1906,
[Online; accessed July 25, 2023].
[2] S. Thorn, K. V. English, K. R. Butler, and W. Enck, “5gac-analyzer:
Identifying over-privilege between 5g core network functions,” in [25] “Kubernetes RBAC Used By Attackers To Deploy
Proceedings of the 17th ACM Conference on Security and Privacy in Persistent Backdoor,” https://phishingtackle.com/articles/
Wireless and Mobile Networks, 2024, pp. 66–77. kubernetes-rbac-used-by-attackers-to-deploy-persistent-backdoor/,
[Online; accessed July 25, 2023].
[3] M. Akon, T. Yang, Y. Dong, and S. R. Hussain, “Formal Analysis of
Access Control Mechanism of 5G Core Network,” in Proceedings of [26] “Malicious Kubernetes Helm charts can be used to
the 2023 ACM SIGSAC Conference on Computer and Communica- steal sensitive information from Argo CD deployments,”
tions Security, 2023, pp. 666–680. https://apiiro.com/blog/malicious-kubernetes-helm-charts-can-be-
[4] 3GPP Standard, www.3gpp.org. used-to-steal-sensitive-information-from-argo-cd-deployments/,
[Online; accessed July 25, 2023].
[5] Free5GC, www.free5gc.org.
[27] “OpenRAN – 5G hacking just got a
[6] Open5GS, open5gs.org. lot more interesting,” https://media.ccc.de/v/
[7] OpenAirInterface, https://www.openairinterface.org/. mch2022-273-openran-5g-hacking-just-got-a-lot-more-interesting,
[Online; accessed July 25, 2023].
[8] 3GPP, “5G; Security architecture and procedures for 5G System,”
TS 33.501, 18.7.0. [Online]. Available: {https://www.3gpp.org/ftp/ [28] 3GPP, “Study on security aspects of the 5G Service Based Architec-
Specs/archive/33 series/33.501/33501-i70.zip} ture (SBA),” TR 33.855, Version 16.1.0. [Online]. Available: {https:
//www.3gpp.org/ftp//Specs/archive/33 series/33.855/33855-g10.zip}
[9] Arons, Tamarah and Pnueli, Amir and Ruah, Sitvanit and Xu, Ying
and Zuck, Lenore, “Parameterized verification with automatically [29] D. Dolev and A. Yao, “On the security of public key protocols,” IEEE
computed inductive assertions?” in Computer Aided Verification: 13th Transactions on information theory, vol. 29, no. 2, pp. 198–208, 1983.
International Conference, CAV 2001 Paris, France, July 18–22, 2001
[30] 3GPP, “Release 18 Description; Summary of Rel-18 Work
Proceedings 13. Springer, 2001, pp. 221–234.
Items,” TR 21.918, 2024, 1.0.0. [Online]. Available: {https:
[10] A. Pnueli, “In transition from global to modular temporal reasoning //www.3gpp.org/ftp/Specs/archive/21 series/21.918/21918-100.zip}
about programs,” in Logics and models of concurrent systems.
[31] D. E. Long, Model checking, abstraction, and compositional verifi-
[11] R. Alur, P. Madhusudan, and W. Nam, “Symbolic compositional cation. Carnegie Mellon University, 1993.
verification by learning assumptions,” in International Conference on
Computer Aided Verification. Springer, 2005, pp. 548–562. [32] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti,
A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuXmv
[12] J. M. Cobleigh, D. Giannakopoulou, and C. S. Păsăreanu, “Learning symbolic model checker,” in International Conference on Computer
assumptions for compositional verification,” in Tools and Algorithms Aided Verification.
for the Construction and Analysis of Systems: 9th International
Conference. Springer, 2003, pp. 331–346. [33] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith,
“Counterexample-guided abstraction refinement,” in International
[13] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem et al., Handbook Conference on Computer Aided Verification.
of model checking. Springer, 2018, vol. 10.
[34] 3GPP, “5G; 5G Security Assurance Specification (SCAS);Service
[14] A. Security, “White Paper: A slice in time: Slicing security in Communication Proxy (SCP),” TS 33.522, 18.0.0. [Online].
5G Core Networks,” Tech. Rep., [Online; accessed December Available: {https://www.3gpp.org/ftp/Specs/archive/33 series/33.522/
1, 2022]. [Online]. Available: {https://info.adaptivemobile.com/ 33522-i00.zip}
network-slicing-security}
[35] ——, “5G System; Network function repository services; Stage 3,”
[15] CoreScan, https://github.com/SyNSec-den/CoreScan.
TS 29.510, 18.8.0. [Online]. Available: {https://www.3gpp.org/ftp/
[16] GSMA Coordinated Vulnerability Disclosure Specs/archive/29 series/29.510/29510-i80.zip}
Programme), https://www.gsma.com/security/
gsma-coordinated-vulnerability-disclosure-programme/.
[36] ——, “Procedures for the 5G System (5GS),” TS 23.502, Version [56] L. Ma, Z. Yang, Z. Bu, Q. Lao, and W. Yang, “Statement recognition
18.7.0. [Online]. Available: {https://www.3gpp.org/ftp/Specs/archive/ of access control policies in iot networks,” Sensors, vol. 23, no. 18,
23 series/23.502/23502-i70.zip} p. 7935, 2023.
[37] ——, “Release 17 Description; Summary of Rel-17 Work Items,” [57] T. Al Rahat, Y. Feng, and Y. Tian, “Oauthlint: an empirical study
Tech. Rep. [Online]. Available: {https://www.etsi.org/deliver/etsi tr/ on oauth bugs in android applications,” in 2019 34th IEEE/ACM
121900 121999/121917/17.00.01 60/tr 121917v170001p.pdf} International Conference on Automated Software Engineering (ASE).
[38] J. Kumar, A. Gupta, S. Tanwar, and M. K. Khan, “A review on 5g IEEE, 2019, pp. 293–304.
and beyond wireless communication channel models: Applications [58] ——, “Cerberus: Query-driven Scalable Security Checking for OAuth
and challenges,” Physical Communication. Service Provider Implementations,” arXiv preprint arXiv:2110.01005,
[39] L. Suárez, D. Espes, F. Cuppens, P. Bertin, C.-T. Phan, and P. Le Parc, 2021.
“Formalization of a security access control model for the 5G system,”
[59] E. Y. Chen, Y. Pei, S. Chen, Y. Tian, R. Kotcher, and P. Tague, “Oauth
in 2020 11th International Conference on Network of the Future
demystified for mobile application developers,” in Proceedings of the
(NoF). IEEE, 2020, pp. 150–158.
2014 ACM SIGSAC conference on computer and communications
[40] D. Basin, J. Dreier, L. Hirschi, S. Radomirovic, R. Sasse, and security, 2014, pp. 892–903.
V. Stettler, “A formal analysis of 5g authentication,” in Proceedings of
the 2018 ACM SIGSAC conference on computer and communications [60] R. Yang, G. Li, W. C. Lau, K. Zhang, and P. Hu, “Model-based
security. security testing: An empirical study on oauth 2.0 implementations,”
in Proceedings of the 11th ACM on Asia Conference on Computer
[41] I. Ahmad, T. Kumar, M. Liyanage, J. Okwuibe, M. Ylianttila, and and Communications Security, 2016, pp. 651–662.
A. Gurtov, “Overview of 5G security challenges and solutions,” IEEE
Communications Standards Magazine, vol. 2, no. 1, pp. 36–43, 2018. [61] “Oauth2 Access Token Request API of 5G system,”
https://forge.3gpp.org/swagger/tools/loader.html?yaml=TS29510
[42] A. Sukumar, A. Singh, A. Gupta, and M. Singh, “Enhancing security Nnrf AccessToken.yaml, [Online; accessed December 1, 2022].
and privacy implications in 5g network slicing,” in 2024 Fourth
International Conference on Advances in Electrical, Computing, [62] S. Bhattacharya, M. Najana, A. Khanna, and P. Chintale, “Securing
Communication and Sustainable Technologies (ICAECT). the gatekeeper: Addressing vulnerabilities in oauth implementations
[43] S. Dorozhynskyi, I. Zakutynskyi, M. Ryabyy, and A. Skurativskyi, for enhanced web security,” International Journal of Global Innova-
“Maximizing security and efficiency in 5g networks by means of tions and Solutions (IJGIS), 2024.
quantum cryptography and network slicing concepts,” in 2023 IEEE [63] “Free5GC’s access token implementation’,” https://github.com/
12th International Conference on Intelligent Data Acquisition and Ad- free5gc/nrf/blob/main/internal/sbi/processor/access token.go#L23,
vanced Computing Systems: Technology and Applications (IDAACS). 2025, accessed: 2025-01-15.
[44] H. Chen, N. Li, C. S. Gates, and Z. Mao, “Towards analyzing complex
operating system access control configurations,” in Proceedings of the
15th ACM symposium on Access control models and technologies.
Appendix A.
[45] L. Cheng, Y. Zhang, and Z. Han, “Quantitatively measure access 5G Communication Types
control mechanisms across different operating systems,” in 2013 IEEE
7th International Conference on Software Security and Reliability. The 5G Core network (5GC) supports three primary
[46] K. Jayaraman, V. Ganesh, M. Tripunitara, M. Rinard, and S. Chapin, communication modes: direct, indirect, and hybrid. In di-
“Automatic error finding in access-control policies.” rect communication, Network Functions (NFs) interact with
[47] P. Centonze, R. J. Flynn, and M. Pistoia, “Combining static and each other without any intermediaries, enabling low-latency
dynamic analysis for automatic identification of precise access-control
policies,” in Twenty-Third Annual Computer Security Applications
exchanges that are ideal for performance-sensitive applica-
Conference (ACSAC 2007). tions. However, this approach exposes NFs directly to one
[48] X. Li, Y. Chen, Z. Lin, X. Wang, and J. H. Chen, “Automatic policy another, which can introduce security risks such as unautho-
generation for {Inter-Service} access control of microservices,” in rized access or data tampering. Besides, the tight coupling of
30th USENIX Security Symposium (USENIX Security 21), 2021, pp. NFs may create scalability challenges in dynamic network
3971–3988. environments.
[49] F. Sun, L. Xu, and Z. Su, “Static detection of access control vulner- Indirect communication, as illustrated in Figure 15(a),
abilities in web applications,” in 20th USENIX Security Symposium
(USENIX Security 11).
requires all interactions, including access token requests
[50] A. Gouglidis, A. Kagia, and V. C. Hu, “Model checking access
and service requests, to be routed through the SCP. This
control policies: A case study using google cloud iam,” arXiv preprint approach ensures centralized control and helps to enforce
arXiv:2303.16688. traffic monitoring, policy enforcement, and load balancing.
[51] B. Shen, T. Shan, and Y. Zhou, “Multiview: Finding blind spots in By isolating NFs from direct exposure, indirect communica-
{Access-Deny} issues diagnosis,” in 32nd USENIX Security Sympo- tion strengthens the network’s overall security and reduces
sium (USENIX Security 23). potential vulnerabilities.
[52] S. Nakamura and Y. Tanaka, “Opportunities and challenges in apply- Finally, hybrid communication strikes a balance between
ing machine learning for access control,” Authorea Preprints.
direct and indirect communication by providing more flex-
[53] X. Xiao, A. Paradkar, S. Thummalapenta, and T. Xie, “Automated ibility on how service access token requests are routed.
extraction of security policies from natural-language software doc-
uments,” in Proceedings of the ACM SIGSOFT 20th International Figure 15(b) and (c) show examples of a hybrid commu-
Symposium on the Foundations of Software Engineering, 2012, pp. nication mode where discovery is always done directly, and
1–11. service request is always done through the SCP. Access
[54] S. H. Jayasundara, N. A. G. Arachchilage, and G. Russello, “Ra- token requests can be made either directly (as shown in
gent: Retrieval-based access control policy generation,” arXiv preprint Figure 15(b)) or through the SCP (as shown in Figure 15(c)),
arXiv:2409.07489, 2024.
depending on the presence of mutual authentication between
[55] M. Abdelgawad, I. Ray, S. Alqurashi, V. Venkatesha, and H. Shirazi,
“Synthesizing and analyzing attribute-based access control model
the consumer NF and the NRF.
generated from natural language policy statements,” in Proceedings
of the 28th ACM Symposium on Access Control Models and Tech-
nologies, 2023, pp. 91–98.
 Consumer SCP NRF Producer Consumer SCP NRF Producer Consumer SCP NRF Producer

1 SR 0 Discovery 0 Discovery

1 ATR (CCA)
2 Discovery 1 ATR
2 ATR (CCA)
3 ATR(CCA) 2 AT
3 Validate CCA
4 Validate CCA 3 Discovery
4 AT
5 AT
5 AT 4 SR(AT, CCA)
6 SR(AT, CCA)
5 SR(AT, CCA)
6 SR(AT, CCA) 7 SR(AT, CCA)
6 Validate AT
7 Validate AT 8 Validate AT
8 ServiceResp 7 ServiceResp
9 ServiceResp
9 ServiceResp 8 ServiceResp 10 ServiceResp

(a) (b) (c)

Figure 15: Simplified message flow for different communication models. (a) Indirect communication, where the AT
must always be requested through SCP. (b) Hybrid communication, where the AT is directly requested. (c) Hybrid
communication, where the AT is requested through SCP. Here, SR:ServiceReq, AT:access token, ATR:accessTokenReq,
and CCA: Client Credentials Assertion token.

Appendix B. the consumer NF’s certificate to prevent impersonation.

Potential Fixes for Identified Vulnerabilities This validation is currently absent in the 5G specifica-
tion, making such checks necessary.
The potential fixes for the new CoreScan attacks (§7.1)
are provided below. B.3. CCA Replay Attack

B.1. Coarse Scope Attack Since the underlying vulnerabilities are similar, the mit-
igation strategies proposed for NFProfile Leakage Attack
1) Clarify producerSlice semantics. The 5G speci- are sufficient to address this attack as well, requiring no
fication should clearly define the producerSlice in additional measures.
access tokens. Specifically, it should include only the
slices requested and authorized during accessTokenReq B.4. CCA Evasion Attack
verification to avoid ambiguity.
2) Clarify handling of optional attributes. The spec- We believe this vulnerability cannot be effectively miti-
ification should (i) clearly define what qualifies as gated without a major redesign, which is beyond the scope
an optional attribute and (ii) state the security impli- of this work and left for future investigation. However, we
cations if such attributes are omitted. Currently, the anticipate that 3GPP will introduce a proper authentication
term ‘optional’ is inconsistently used, resulting in am- scheme for 5G roaming in upcoming specifications.
biguity. For instance, optional parameters in NFDis-
cReq (e.g., targetSnssais) help refine search re-
sults without affecting security. In contrast, omit-
B.5. Forced NF Selection Attack
ting producerSlice from access tokens, as seen
If no other over-privilege attacks exist in the system,
in Free5GC [63], results in a trivial exploit. We
this vulnerability would, at worst, result in a DoS attack.
recommend producerSlice be treated as condi-
However, to prevent such outcomes, it is essential to patch
tional—mandatory whenever the 5GC supports slicing.
all related vulnerabilities, particularly those involving CCA
and SCP. To further mitigate DoS risks, we propose an
B.2. NFProfile Leakage Attack approach called Verifiable Attribute Reporting:
1) Ensure CCA Token Replay Protection. Short-lived • Integrity Checks: Attributes such as load and priority
replay protection is insufficient for CCA tokens, as should be verified by trusted monitoring systems rather
it can lead to overprivilege or DoS. To prevent this, than relying solely on NF self-reporting.
a nonce should be added to the CCA token by the • Telemetry Integration: The 5G standard should define
consumer NF. The NRF then tracks these nonces to mechanisms for leveraging network telemetry data to
guarantee each token is processed only once. independently assess NF load and performance. The
2) Validate CCA by SCP. The SCP should verify that the NRF should use this data to update NFProfile attributes,
credentials in the CCA token (e.g., sub) correspond to replacing self-reported values.
Appendix C. C.3. Reasons for Acceptance
Meta-Review
1) This paper identifies multiple impactful vulnerabilities.
The following meta-review was prepared by the program The formal analysis revealed 10 vulnerabilities and five
committee for the 2025 IEEE Symposium on Security and attacks. Compared against 5GCVerif as a state-of-the-
Privacy (S&P) as part of the review process as detailed in art solution, it shows significantly improved scalability.
the call for papers. 2) The paper provides a valuable step forward in an es-
tablished field. The findings of this research are novel,
offering insights that can guide future enhancements to
C.1. Summary
access control protocols.
This paper introduces CoreScan, a compositional verifi-
cation technique that models the 5g Core network by break- C.4. Noteworthy Concerns
ing it into smaller components to perform a comprehensive
formal analysis. Formal analysis of the 5g specification is 1) Corescan evaluation is limited to open-source 5G im-
challenging because of missing reference implementations, plementations as there was no access to commercial
natural language specification, and state explosion. CoreS- 5G Core systems.
can was utilized to test 61 access control properties and
found five new classes of exploitable privilege escalation Appendix D.
vulnerabilities in the 5G standards. Response to the Meta-Review
C.2. Scientific Contributions We acknowledge that CoreScan’s evaluation is limited
to open-source 5G Core implementations due to a lack of
• Identifies an Impactful Vulnerability -Provides a Valu- access to commercial systems. Thus, to compensate for this,
able Step Forward in an Established Field we submitted them to GSMA, which has acknowledged all
findings (A1-A5) under CVD-2025-0101. We are actively
working with GSMA on potential defenses and drafting
change requests (CRs) for 3GPP updates.