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.