A Systematic Study of Practical & Formal Privacy in the 5G AKMA Procedure

We systematically scrutinise all the facets of privacy in the 5G delegated-authentication procedure called AKMA (Authentication and Key Management for Applications based on 3GPP credentials in the 5G Systems). We define, in general terms, a privacy-threat model and privacy requirements for this protocol. Using these definitions, we find numerous privacy failings in the AKMA protocol. We propose a patch, called AKMA<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">p</sup>, which imposes minimal changes on AKMA, yet it attains all our privacy requirements. We also formalise and analyse all of this in terms of formal privacy-verification in the Dolev-Yao model; to this end, we use the Tamarin prover to systematically carried out our formal analyses of AKMA and AKMA<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">p</sup>.