Anonymity guarantees of the UMTS/LTE authentication and connection protocol

The UMTS/LTE protocol for mobile phone networks has been designed to offer a limited form of anonymity for mobile phone users. In this paper, we quantify precisely what this limited form of anonymity actually provides via a formal security model. The model considers an execution where the home and roaming network providers are considered as one entity. We consider two forms of anonymity, one where the mobile stations under attack are statically selected before the execution, and a second where the adversary selects these stations adaptively. We prove that the UMTS/LTE protocol meets both of these security definitions. Our analysis requires new assumptions on the underlying keyed functions for UMTS, namely that a set of pseudorandom functions are “agile”. This assumption, while probably true, has not previously been brought to the fore.