Formal Verification of the 5G Inter-Operator Signaling Protocol

Abstract

This thesis analyzes the formal security properties of the PRotocol for N32 INterconnect Security (PRINS), specified by the 3rd Generation Partnership Project (3GPP) for the purposes of protecting signaling traffic between 5G mobile networks. An emerging technology that is believed to enable a plethora of novel and potentially critical applications, it is mandatory that 5G communication be effectively secured by design. Since inter-operator signaling exhibits specific functional requirements that existing security protocols fail to address, 3GPP defines this purpose-built protocol that has yet to undergo thorough analysis by the broader research community at the time of this writing. Formal methods have successfully been used to validate and improve several security protocols in the past. The nature of this approach to verifying a system’s correctness makes it particularly suited for detecting logical flaws in the underlying design. Semiautomated tools for formal verification further aid the discovery of issues that would be non-trivial to identify by manual analysis. As part of this thesis, the PRINS specification is assessed in detail in order to understand all related message flows and derive the intended security properties. Subsequently, they are transposed into a formalized representation and verified against a model of the protocol for the popular model checker ProVerif. Although no concrete attacks substantiate from the formal verification, it is shown that the 3GPP specification contains several inconsistencies and, most notably, a lack of clarity about what the protocol is supposed to achieve. This ambiguity may potentially lead to unreliable and therefore insecure implementations. Based on these findings, a number of improvements are suggested that can help make the specification more explicit and easier to understand.

Hans Christian Rudolph
Hans Christian Rudolph
Manager, Cyber Advisory