Formal Security Analyses of 5G Security Protocols in Diﬀerent Threat Models
Creators: name: Miller, Rhys
Publisher: name: University of Surrey
Year: 2024

description: As the 5th generation (5G) of mobile communication continues to evolve and is being deployed more widely, the security of 5G networks is of paramount importance. Importantly, unlike with cases such as the standardisation of version 1.3 of the TLS (Transport Layer Security) protocol in 2018, the standardisation of different revisions of 5G (and before it, of 4G, 3G), do not enjoy the academic scrutiny of formal security analysis, so one has to endeavour into this as revisions are published. In this thesis, we do just that: we do formal analysis of the main security protocols in 5G, in some of their latest revisions.<br>
description: <br>
description: In more detail, for User Equipments (UE), that is mobile devices, to connect to the network securely, a series of cryptographic protocols are used in silo as well as in combination. Primarily, these are authenticated key establishment (AKE) protocols. In this thesis, we are concerned with the formal security analysis of all of the AKE protocols used in mobile networks: 1. Registration; 2. Authentication Key Agreement (AKA); 3. Handovers; 4. AKMA (Authentication and Key Management for Application) . In all cases, we focus primarily on 5G, though some of our ﬁndings apply to the 4G as well. <br>
description: <br>
description: Firstly, we focus on Registration, Authentication Key Agreement (AKA), and Handovers. All these protocols are run between the UE, the Radio Access Network (RAN) nodes (a.k.a. ‘base stations’), and the Core (i.e., the servers of the network that the UE subscribes to). We model and analyse these protocols in isolation, in all their variants, as well as in sequential composition amongst themselves and amongst their variants. In the latter case, we refer to the composed procedure as the 5GAKE_stack. We scrutinise these protocols as well as 5GAKE_stack, in varying threat-models: 1. All parties being honest but subject to a Dolev-Yao attack; 2. The RAN nodes being corrupt; 3. The RAN nodes being ‘honest-but-curious’ (i.e., following the protocols, but aiming to get illicit insights/controls where possible). Considering the RAN in such a threat model is in keeping with the revealing of rogue base-stations [97], with the advent of small cells in 5G, as well as the simple fact that the RAN is often running proprietary, 3rd-party software.<br>
description: <br>
description: Secondly, we focus on the AKMA (Authentication and Key Management for Application) procedure. In this protocol, the mobile network proxies an AKE protocol between the UE and a 3rd-party called Application Function (AF), whilst the cryptographic material is all based on mobile-network keys. In this way, AFs (e.g., car manufacturers) authenticates and securely deliver data to UEs, e.g., smart cars, connected to a mobile network/providers. The threat of having 3rd-parties query mobile-network cryptographic data is palpable. Moreover, this protocol is under significant, on-going revisions by 3GPP, in the light of imminent adoptions. Thus, analysing the security of this protocol is important as well as timely.<br>
description: <br>
description: In what follows, we present our thirteen contributions in a topic by topic fashion.<br>
description: <br>
description: With respect to the formal analysis of the 5GAKE_stack, using formal verification in the so-called Dolev-Yao/symbolic model, in the Tamarin tool, we achieve the following.<br>
description: <br>
description: 1. We are the first to verify the composed procedure called the 5GAKE_stack.<br>
description: <br>
description: 2. We are the first to verify in fact the full Registration procedure.<br>
description: <br>
description: 3. We show that honest-but-curious RAN can force weaker versions of handovers without being detected, which in turn allows them to gain access to so-called security keys of the UEs that they normally should not obtain.<br>
description: <br>
description: 4. We show that rogue RAN can change billing data of the UE, e.g., giving someone unpaid service, without any detection if a part of the Core called SMF (Session Management Function) does not always implement PDU filtering, which is currently the case in 5G.<br>
description: <br>
description: With respect to the formal analysis of XN handovers, using formal verification in the so-called Dolev-Yao/symbolic model, in the Tamarin tool, we achieve the following.<br>
description: <br>
description: 5. We formally show that the RAN can control channel-securing keys called Access-Stratum (AS) keys beyond what is normal.<br>
description: <br>
description: 6. We propose provably-secure several variants of the XN handovers to amend this flow, all the while maintaining efficiency and backward-compatibility in mind.<br>
description: <br>
description: 7. Moreover, we pursue the following: we create a framework to measure trust and communication complexity, such as to compare variants of procedures amongst themselves, as well as our new variants of XN; in this way, we show that our proposal are worthwhile.<br>
description: <br>
description: 8. Finally, we extend this demonstration to the practical realms: we are the first implement XN handovers in 3GPP-compliant Open5GCore testbed, as well as our more-secure variants of XN.<br>
description: <br>
description: 9. Using this, we show that one of our variants brings to efficiency degradation to XN, on average.<br>
description: <br>
description: Now, we look at our findings with respect to the AKMA (Authentication and Key Management for Application) procedure. To analyse AKMA, we proceed in several steps.<br>
description: <br>
description: 10. Firstly, we propose PCS_AC (“post-compromise security with applications control”): a generic cryptographic framework for post-compromise security (PCS) which –for the first time in the context of PCS– considers attackers that do not control just keys, but also application controls (e.g., reset conditions, timers, etc.). As with all PCS models, our framework looks at whether attackers that control a key now can maintain this control or subsequent controls of keys in the future, or the protocol can ‘heal’ and the controls are lost. In PCS_AC, the application controls make the attacker power more subtle but also wider, as he/she/it may gain/lose knowledge of keys due to application flaws, rather than key leakage.<br>
description: <br>
description: 11. Secondly, we mechanise PCS_AC in the two state-of-the-art protocol verifiers, ProVerif and Tamarin, and we then apply it to AKMA.<br>
description: <br>
description: 12. Moreover, using our ProVerif and Tamarin mechanisations, we show that AKMA has a PCS flaw which is easily fixable. Our patch is called AKMA+, which we prove secure in the same ProVerif and Tamarin mechanisations.<br>
description: <br>
description: 13. Finally, we implement and test AKMA and AKMA+ on top of the Open5GCore test bed, and show no loss of efficiency, on average, between AKMA+ and AKMA.<br>
description: <br>
description: All our work has been disclosed to 3GPP, and we are working with them towards adoption of some of our measures.<br>