We present a thorough experimental and formal analysis of users’ privacy in mobile telephony systems. In particular, we experimentally analyse the use of pseudonyms and point out weak deployed policies leading to some critical scenarios which make it possible to violate a user’s privacy. We also expose some protocol’s vulnerabilities resulting in breaches of the anonymity and/or user unlinkability. We show these breaches translate in actual attacks which are feasible to implement on real networks and discuss our prototype implementation. In order to countermeasure these attacks, we propose realistic solutions. Finally, we provide the theoretical framework for the automatic verification of the unlinkability and anonymity of the fixed 2G/3G procedures and automatically verify them using the ProVerif tool.