Towards a logic of privacy-preserving selective disclosure credential protocols

This paper presents a first approach towards a logic suited for protocols aiming to achieve selective disclosure of credentials while preserving privacy. The analysis draws from the BAN and related logics by M. Burrows et al (1990) and P. Syverson and I. Cervesanto (2001) that are targeted to aid reasoning about authentication protocols, as well as from formal methods on PKIs by C. Liu et al (2000, 2001) . The families of protocols directly covered are built using selective disclosure certificates, blind signatures and one-way has functions as cryptographic primitives. The logic is able to prove that if the protocol´s credentials are properly constructed and signed by trusted issuers, they should convince a verifier; furthermore, it provides a framework on which mechanized attacks against privacy may be attempted by an automatic theorem prover. The runner example is a protocol by J.E. Holt and K.E. Seamons (2002).