The traditional focus on protocol security has often overshadowed the importance of privacy, relegating it to a secondary objective rather than treating it as a distinct and critical aspect. Consequently, there is a noticeable lack of formal or semi-formal privacy verification analysis, and researchers have yet to establish a consensus on privacy terms and frameworks. Existing approaches to privacy proofs often rely on process-algebra equivalences, which can yield false attacks or inaccurate results. This has led to the adoption of approximate theoretical models. These approaches move away from overly idealized models, aiming to make their formalisms more practical and relevant to real-world scenarios.

We introduce the term ``identification-based protocols'' to encompass communication systems whereby the identities of entities are used for granting access to services or resources. Such protocols are predominantly cryptographic such as authentication key-exchange and identification schemes, however, they can also encompass non-cryptographic systems such as password-based access-control systems. This thesis will demonstrate that in practice, these protocols are ubiquitous in various domains, including the Internet, mobile networks, and the IoT. In fact, they are prevalent in nearly all networked applications. This extensive class of identity-based protocols is particularly vulnerable to privacy risks due to their inherent associating entities with their presence on a network, systems, or accessing a service.

To address the privacy challenges in such protocols/systems, this thesis introduces the TrackDev framework, a novel and comprehensive approach to specify and reason about privacy. The strength of TrackDev lies in its fine-grained definitions, enabling a detailed analysis of various notions of privacy. To this end, TrackDev considers multiple dimensions combined: whether the attacker is active or passive, whether an entity is trackable in its every single appearance on the network or just in a compound set thereof, and whether the entity can be explicitly or implicitly identified.

As a result, TrackDev provides a methodology for (formal) privacy verification that offers a more detailed analysis of the specific type or flavour of privacy being analysed, which helps overcome certain bottlenecks in traditional privacy verification. Furthermore, we mechanise the TrackDev framework in the Tamarin tool, demonstrating the advantages of TrackDev over existing state-of-the-art privacy verification.

To showcase the practicality of TrackDev, we conduct real-world case studies on the LoRaWAN Join and 5G procedures. Through these case studies, we not only identify vulnerabilities and attacks on these protocols but also propose effective patches to mitigate the privacy risks. Notably, one of our proposed privacy-preserving patches has been adopted by the LoRa Alliance for inclusion in the upcoming LoRaWAN v1.2.0 specifications.

These developments showcase the practical and theoretical relevance of our TrackDev framework for privacy specification and reasoning in identity-based systems.