This paper focuses on the privacy of communication between two or more mobile interlocutors (principals), and protecting their messages and their identities from third parties (a situation that can arise in mobile telephony and mobile computing). The protection is considered to be against an active adversary (as in security described by Needham-Schroder protocols).

Abadi and Fournet provide a definition of a privacy property (first informally, then in a process calculus). This property implies that each principal may reveal and prove its identity to certain other principals, and hide it from the rest. The main contribution of the paper consists of the construction of two protocols that allow the principals to authenticate with chosen interlocutors, while hiding their identities from others.

The paper spans 50 pages. The first section is a general overview of the subject. Section 2 defines and discusses the privacy properties defined by the authors. Section 3 presents the general assumptions on which the protocols rely. Section 4 develops two protocols, and some optimizations and extensions. The first protocol uses digital signatures, and requires that principals have loosely synchronized clocks. It is based on the Denning-Sacco public key protocol [1], and its corrected version [2]. The second protocol uses only encryption, and avoids the synchronization requirements, at the cost of an extra message.

Section 5 explains the applied pi calculus (an extension of pi calculus), and gives some examples. Section 6 constructs a formal model of the second protocol using the applied pi calculus. Section 7 addresses (in two theorems) the authenticity and secrecy properties of this model of the second protocol. In section 8, the theoretical analysis is concentrated on privacy properties. The results show that the standard authenticity, secrecy, and privacy (identity protection) properties are covered by the protocol. Some applications of this identity protection are developed in subsection 8.3. Section 9 discusses some related problems and related work (including, in particular, work on message untraceability). Section 10 concludes the paper. An appendix contains proofs for the main claims of sections 7 and 8.

The paper is considered by the authors to be a contribution to the formal study of security protocols and of their properties.