The project investigates systems designed to offer privacy guarantees to on-line users, such as anonymity of payment, privacy of shopping preference, of email patterns and associations between correspondents, or candidate choice in an election. It aims to develop a taxonomy of anonymity and privacy properties within two verification formalisms (strand spaces and applied pi calculus) and to develop techniques for analysing protocols that are designed to provide such properties. We shall also analyse some well-known protocols, such as private authentication protocols and direct anonymous attestation protocol. This proposal builds on the acknowledged expertise of the University of Birmingham in the area of formal methods and verification.