  We study the 5G-AKA authentication protocol described in the 5G mobile
communication standards. This version of AKA tries to achieve a better privacy
than the 3G and 4G versions through the use of asymmetric randomized
encryption. Nonetheless, we show that except for the IMSI-catcher attack, all
known attacks against 5G-AKA privacy still apply.
  Next, we modify the 5G-AKA protocol to prevent these attacks, while
satisfying the cost and efficiency constraints of the 5G-AKA protocol. We then
formally prove that our protocol is sigma-unlinkable. This is a new security
notion, which allows for a fine-grained quantification of a protocol privacy.
Our security proof is carried out in the Bana-Comon indistinguishability logic.
We also prove mutual authentication as a secondary result.
