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.

ProVerif models

AKA protocol: anonymity 3GPP Fixed
AKA protocol: unlinkability 3GPP Fixed
Identification: anonymity 3GPP Fixed
Identification: unlinkability 3GPP Fixed
Paging: anonymity 3GPP Fixed
Paging: unlinkability 3GPP Fixed
All fixed processes running in parallel Anonymity Unlinkability

Press coverage