| The GSM (2G), UMTS (3G), and LTE (4G) mobile telephony protocols are all in active use, giving rise to a number of interoperation situations. This poses serious challenges in ensuring authentication and other security properties. Analyzing the security of all possible interoperation scenarios by hand is, at best, tedious undertaking. Model checking techniques provide an effective way to automatically find vulnerabilities in or to prove the security properties of security protocols.;Although the specifications address the interoperation cases between GSM and UMTS and the switching and mapping of established security context between LTE and previous technologies, there is not a comprehensive specification of which are the possible interoperation cases. Nor is there comprehensive specification of the procedures to establish security context (authentication and short-term keys) in the various interoperation scenarios. We systematically enumerate the cases, classifying them as allowed, disallowed, or uncertain with rationale based on detailed analysis of the specifications. We identify the authentication and key agreement procedure for each of the possible cases.;We formally model the pure GSM, UMTS, LTE authentication protocols, as well as all the interoperation scenarios, and analyze their security, in the symbolic model of cryptography, using the tool ProVerif. We find the previously known man-in-the-middle attack on GSM. For the interoperation scenarios, we find three kind of attacks: one is the false base station attack which is inherited from the GSM system; another attack is a similar false base station attack but with a 4G BS; the third one modifies the CMC message. Based on the proved and refuted properties, we compare the authenticity achieved in different scenarios, and we provide recommendations to improve the mobile telephony standards. |
