Unlinkability, as standardised by ISO 15408, is formalised as an equivalence problem between a normal network and one where it is impossible to reuse identities between sessions. A notion of process equivalence, bisimilarity, is introduced along with its characteristic modal logic. The modal logic is applied to analyse known vulnerabilities in various implementations of ePassport protocols. Unlinkability of EMV is also analysed and exercises consider unlinkability of further protocols. Finally, a protocol is developed that satisfies unlinkability and also various authentication properties, plus a strong confidentiality property – forward secrecy. The verification of all properties of this showcase protocol is automated.