One of the goals of mobile telephone protocols is to deny third parties the ability to link communication sessions with subscribers' identities. We have been investigating security and privacy in mobile telephone protocols, both in theory using formal methods and in practice by capturing real network communication.
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.
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.