Abstract
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 protocols in the 3GPP-compliant Open5GCore 5G testbed. We also systematically cross-compare standard handovers with our amended handovers using 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.