Identity and Security in 5G Authentication

Abstract

In this thesis, we study the provision and protection of user identity in the 5G Authentication and Key Agreement (5G-AKA) protocol. We present two variations of the protocol: the first mitigates a family of de-anonymization attacks that aim to defeat the privacy-protection features of 5G-AKA. It does so by replacing a fixed user identity with a sequence of ephemeral identifiers. This variant is designed to be fully backwards compatible with the existing 5G-AKA authentication message formats, which allows it to be used in roaming scenarios without changes to the visited network. The second protocol is a realization of "Bring Your Own Identity" (BYOI) for 5G-AKA, allowing subscribers to authenticate with an identity provisioned by an external provider. This is accomplished by composing 5G-AKA with OAuth 2.0, a de-facto standard for third-party authorization online. We built and verified a formal model of each protocol using Tamarin, a theorem-prover tool for security protocols. From this, we note some limitations of existing formalizations of secrecy and authentication properties, and propose improvements. Finally, we present an implementation of our BYOI protocol over a simulated 5G system, and show it works against Google's OAuth 2.0 API. We discuss some practical considerations arising from the implementation.