A security model for anonymous credential systems

This paper proposes a formal model of the Bellare-Rogaway type [Bellare and Rogaway, 1994] that enables one to prove the security of an anonymous credential system in a complexity theoretic framework. The model abstracts away from how a specific instance of anonymous credential system achieves its goals; instead it defines what these goals are. The notions of credential unforgeability, non-transferability, pseudonym unlinkability and pseudonym owner protection are formally defined and the relationships between them are explored. The model is a step towards a formal treatment of the level of privacy protection that anonymous credential systems can and should achieve, both in terms of pseudonym unlinkability and user anonymity.