Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - [Extended Abstract].
Chunyu Tang, David A. Naumann, Susanne Wetzel · 2011
Abstract. Both GSM (2G) and UMTS (3G) wireless standards are deployed worldwide. Like the 4G standard now appearing, these standards provide for mobile devices with differing capabilities to roam between providers or technologies. This poses serious challenges in ensuring authentication and other security properties. Automated analysis of security properties is needed to cope with the large number of possible scenarios. While some attacks exploit weaknesses in cryptographic functions, many attacks exploit flaws or other features of the protocol design. The latter attacks can be found using symbolic (Dolev-Yao) models. This paper demonstrates the use of a fully automatic tool to exhaustively analyze symbolic models of GSM, UMTS, and the respective roaming protocols. The results include the demonstration of known attacks as well as the confirmation of expected properties.