ASIACCS 2022
The 5G Key-Establishment Stack: In-Depth Formal Verification
by Rhys Miller, Ioana Boureanu, Steve Wesemeyer, Chris Newton, presented at ASIACCS 2022.
The paper can be found here or download paper.
Summary
We formally analyse the security of each 5G authenticated key- establisment (AKE) procedures: the 5G registration, the 5G authentication and key agreement (AKA) and 5G handovers. We also study the security of their composition, which we call the 5GAKE_stack. Our security analysis focuses on aspects of multi-party AKEs that occur in the 5GAKE_stack. We also look at the consequences this AKE (in)security has over critical mobile-networks’ objects such as the Protocol Data Unit (PDU) sessions, which are used to bill sub- scribers and ensure quality of service as per their contracts/plans.
In our assessments, we augment the standard Dolev-Yao model with different levels of trust and threat by considering honest, honest-but-curious, as well as completely rogue radio nodes. We formally prove security in the first case, and insecurity in the latter two as well as making formal recommendations on this. We carry out our formal analysis using the Tamarin-Prover.
Lastly, we also present an emulator of the 5GAKE_stack. This can be a useful “5G API”-like tool for the community to experiment with the 5GAKE_stack, since the 5G networks are not yet fully deployed and mobile networks are proprietary and closed “loops”.
Finding # 1
-
We formally show that honest-but-curious 5G base stations (gNBs) can collectively and systematically maintain the lack of backwards security in handovers: i.e., these gNBs follow the specification, but purposedly choose to run the least secure configuration of handovers’ key-establishment such as to gain and keep an illicit ability to decrypt users’ traffic.
-
It is well known (e.g., 3GPP TS 33.501 version 16.6.0 Release 16) that so-called horizontal key-derivation in handovers offers no backwards secrecy/security, allowing base stations (gNBs) which served a user in the past to decrypt this user’s traffic in the future, when said user is no longer served by said gNB. We formally show that a group of honest-but-curious gNBs can prolong/maintain this lower security, thus allowing them be unhindered in continuing to decrypt and read users’ traffic they should not have access to.
In the 5G era, when access-stratum traffic contains so many types of information, this is a serious issue!
Recommendation A
-
To counteract this security issue we show, we recommend that, in 5G, one of the following measures are taken:
-
Only vertical key derivation in handovers be allowed.
-
User equipments keep state and not accept more than 2 horizontal key derivations in a row, especially if an un-used session-key called “NH” is present.
Finding # 2
-
We formally show that malicious (protocol-deviating) 5G base stations can affect positively or negatively the quality-of-service (QoS) and billing of a user when routing them out to the internet, if the so-called UPFs (User Plane Functions) do not apply certain package filtering rules.
-
At the end of each execution of a handover and/or of a registration, the SMF (Session Management Function) instructs UPFs as to the QoS and billing data for each subscriber, yet the configuration on the UPFs may be such that when it routes subscribers out, filtering of packages (i.e., PDU – Protocol Data Unit) may not be applied, that is, it is optional. See 3GPP TS 29.244 version 16.6.0, sections 5.7 and 5.8. We formally show that this optionality allows the gNBs to alter/choose the QoS and the usage/billing data (i.e., the PDU-session data) of users, at will.
This is a serious issue in 5G, as complex payment-plans/contracts and usage are and will be in place, and “bumping up or down” someone’s service or bill is therefore of consequence!
Recommendation B
- To counteract this security issue, we recommend that packet filtering by UPFs be made mandatory in 5G.
Finding # 3
- We formally verify the Registration, AKA, and handovers, composed sequentially and concurrently. We formally show that, in presence of non-malicious gNBs, these procedures run correctly or securely w.r.t. authentication and channel security!
Other aspects
- We follow the specifications (3GPP TS 33.501 version 16.6.0 Release 16) closely and create an emulator for 5G handovers, which can serve as an API for those interested in them.
Tamarin models
- Check out our most up-to-date models: See models here
Code
- Check out our emulator for 5G handovers: See Emulator here