Abstract
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 p , 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 p .