A Systematic Approach to Formal Verification and Vulnerability Analysis of Access Control Mechanisms in 5G Core Network

open_access
Open Access
Author:
Akon, Mujtahid Al
Graduate Program:
Computer Science and Engineering
Degree:
Master of Science
Document Type:
Master Thesis
Date of Defense:
February 09, 2026
Committee Members:
Syed Rafiul Hussain, Thesis Advisor/Co-Advisor
G. Gary Tan, Committee Member
Mahmut Kandemir, Program Head/Chair
Keywords:
5G Core Network
Access Control
Formal Analysis
Vulnerabilities
Cellular Network Security
Abstract:
In this work, we present 5GCVerif, a model-based testing framework designed to formally analyze the access control framework of the 5G Core. With its modular design, 5GCVerif employs various abstraction techniques to craft an abstract model that captures the intricate details of the 5G Core’s access control mechanism. This approach offers customizability and extensibility in constructing the abstract model and addresses the state explosion problem in model checking. 5GCVerif also sidesteps the challenge of exhaustively generating models for all possible core network configurations by restricting the model checker to explore policy violations only within the valid network configurations. Using 5GCVerif, we evaluated 55 security properties, leading to the discovery of five new vulnerabilities in 5G Core’s access control mechanism. The uncovered vulnerabilities can result in multiple attacks including unauthorized entry to sensitive information, illegitimate access to services, and denial-of-services.