Publications

CCS 2012

New privacy issues in mobile telephony: fix and verification.

Myrto Arapinis, Loretta Mancini, Eike Ritter, Mark Ryan

Nico Golde, Kevin Redon, Ravishankar Borgaonkar

Proceedings of the 19th ACM Conference on Computer and Communications Security.

Abstract

Mobile telephony equipment is carried daily by billions of subscribers everywhere they go. Avoiding linkability of subscribers by third parties, and protecting the privacy of those subscribers is one of the goals of mobile telecommunication protocols. We use formal methods to model and analyse the security properties of 3G protocols. We expose two novel threats to users' privacy in 3G telephony systems, which make it possible to trace and identify mobile telephony subscribers, and we demonstrate the feasibility of a low-cost implementation of these attacks. We propose fixes to these privacy issues, which also take into account and solve other privacy attacks known from the literature. We successfully prove that our privacy-friendly fixes satisfy the desired unlinkability and anonymity properties using the automatic verification tool ProVerif.

Pdf - Related Material - Slides

Hotspot

Pseudonyms in mobile telephony systems: good principles but weak implementations.

Myrto Arapinis, Loretta Mancini, Eike Ritter, Mark Ryan

Abstract

Mobile telephony systems employ a mechanism to change pseudonyms (called TMSIs) in order to provide user privacy against third party eavesdroppers. A new pseudonym is assigned by executing the TMSI reallocation procedure in cyphered mode. However, the 3GPP standard only gives some guidelines about the frequency and circumstances of the reallocation, and leaves space for weak implementations. To motivate a theoretical investigation, we capture and analyse real networks communications to understand the level of privacy currently provided by real network operators. We identify and discuss scenarios that threaten user privacy and discover a linkability attack on the TMSI reallocation procedure. We confirm the presence of the conditions necessary to perform the attack on real implementations adopted by major network operators. Moreover, we formally prove the unlinkability of a fixed version of the TMSI reallocation procedure. We prove that an ideal version of the protocol and the fixed protocol satisfy labelled bisimilarity by building a symmetric relation and proving it satisfies the three conditions of labelled bisimilarity.

Related Material

Eprint

Formal Analysis of UMTS Privacy

Abstract

The ubiquitous presence of mobile communication devices and the continuous development of mobile data applications, which results in high level of mobile devices’ activity and exchanged data, often transparent to the user, makes privacy preservation an important feature of mobile telephony systems. We present a formal analysis of the UMTS Authentication and Key Agreement protocol, using the applied pi-calculus and the ProVerif tool. We formally verify the model with respect to privacy properties. We show a linkability attack which makes it possible, for individuals with low-cost equipment, to trace UMTS subscribers. The attack exploits information leaked by poorly designed error messages.