Over the past decade, 5G technologies have been widely adopted worldwide, and the telecommunications industry is now moving toward the standardization of 6G. However, a significant gap remains in ensuring the safety and security of this vital infrastructure. Each new generation has introduced technical debt, but 5G marked a shift toward a modular architecture that supports cloud-native deployments. Current methods for testing and verifying designs and deployments are still largely manual and resource-intensive. Greater scrutiny of this infrastructure has revealed security weaknesses in both protocol designs and their software and hardware implementations. Specifically, the protocols within the 5G control plane suffer from unclear and incomplete specifications. Given the scale and importance of this infrastructure, it is essential for the community to revisit its assumptions regarding protocol design.

We address this challenge by proposing a framework to formally specify the protocols used in the control plane of the 5G system. We shall focus on the 3GPP Non-Access Stratum (NAS) protocol for demonstration purposes. In this paper, we introduce a novel transactional model over replicated data types to serve as the meta-theory for the 5G control plane protocols. Additionally, we shall derive an executable specification of a subset of the NAS protocol within an interactive theorem prover, IVy to illustrate how the protocol is amenable to verification within a decidable fragment of first-order logic. This research is a work in progress. Our proposal to describe the control-plane protocols using existing notions of replicated data types is speculative and we wish to obtain feedback from the community regarding our design choices, the inference of transactional isolation levels, and the safety and liveness properties of these protocols.