Euro S&P 2023

Systematic Improvement of Access-Stratum Security in Mobile Networks

by Rhys Miller, Ioana Boureanu, Steve Wesemeyer, Zhili Sun, and Hemant Zope, presented at EURO S&P 2023.

The paper can be found here or download paper.

Summary

In mobile networks, the User Equipment (UE) secures some of the communication with its serving Radio Access Network (RAN) node (“base station”) via a set of keys known as Access Stratum (AS) keys. Unfortunately, the level of secrecy of these keys varies with the mobile procedures re-establishing them.

To improve the secrecy of the AS keys, we propose minimal changes to 5G & 4G handovers, i.e., the main AS-key establishment procedures. We show the minimality of our changes also via an implementation of one of our protocol in the 3GPP-compliant Open5GCore 5G testbed. We also cross-compare standard handovers with our amended handovers, systematically via MobTrustCom: a framework to quantify especially trust but also communication complexity in mobile networks. Moreover, we use Tamarin, a formal security-protocol verification tool, to prove no loss of “classical” security yet an increase in AS-keys’ secrecy brought by our improvements to handovers.

Finding 1

• We propose a series of protocols which modify the XN/X2 handover procedure (X2) handovers in a systematic, as well as minimal way w.r.t. the 3GPP specifications, in order to recover the backwards security for the AS keys.

Finding 2

• To ascertain the minimality of our changes, we implement our of extensions to the XN/X2 protocol in the well-known and 3GPP-compliant Open5GCore 5G network testbed; we show no loss of functionality or depreciation of efficiency.

Finding 3

• We carry out formal verification of all our proposed improvements to XN/X2. We show that XN/X2 does not have backwards security of the AS keys and that our protocols gain that, whilst losing no other security guarantees.

Finding 4

• We propose the MobTrustCom framework, motivated by measuring how much trust and what communication costs are associated to access-stratum security and potentially improvements to it in mobile networks. It provides fine-grained measures of trust, “split-trust” and explicit descriptions of communication costs in mobile networks. We apply MobTrustCom to some of the main protocols in 5G and 4G (handovers and other key-establishment protocols such as the Registration procedure (REG)) and compare our security-improving solutions amongst themselves, as well as against existing mobile procedures w.r.t. the MobTrustCom’s trust and communications cost.

Tamarin models

• Check out our most up-to-date Tamarin models: See models here