Abstract or Summary:
Frequently, communication between two principals reveals their identities and presence to third parties. These privacy breaches can occur even if security protocols are in use; indeed, they may even be caused by security protocols. However, with some care, security protocols can provide authentication for principals that wish to communicate while protecting them from monitoring by third parties. We discuss the problem of private authentication and present two protocols for private authentication of mobile principals. Our protocols allow two mobile principals to communicate when they meet at a location if they wish to do so, without the danger of tracking by third parties. We also present the analysis of one of the protocols in the applied pi calculus.We establish authenticity and secrecy properties. Although such properties are fairly standard, their formulation in the applied pi calculus makes an original use of process equivalences. In addition, we treat identity-protection properties, thus exploring a formal model of privacy.