Research Article
Symbolic Analysis for Security of Roaming Protocols in Mobile Networks
@INPROCEEDINGS{10.1007/978-3-642-31909-9_29, author={Chunyu Tang and David Naumann and Susanne Wetzel}, title={Symbolic Analysis for Security of Roaming Protocols in Mobile Networks}, proceedings={Security and Privacy in Communication Networks. 7th International ICST Conference, SecureComm 2011, London, UK, September 7-9, 2011, Revised Selected Papers}, proceedings_a={SECURECOMM}, year={2012}, month={10}, keywords={Mobile networks GSM UMTS roaming protocols security authentication secrecy symbolic modeling automated analysis}, doi={10.1007/978-3-642-31909-9_29} }- Chunyu Tang
David Naumann
Susanne Wetzel
Year: 2012
Symbolic Analysis for Security of Roaming Protocols in Mobile Networks
SECURECOMM
Springer
DOI: 10.1007/978-3-642-31909-9_29
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.