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 [2, 10] that are targeted to aid reasoning about authentication protocols, as well as from formal methods on PKIs [5, 6]. The family of protocols directly covered are built using selective disclosure certificates, blind signatures and oneway has functions as cryptographic primitives. The logic is able to proe 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 Holt and Seamons, specified in [4].
Citation:
Theodoros Balopoulos, Stephanos Gritzalis, "Towards a Logic of Privacy-Preserving Selective Disclosure Credential Protocols," dexa, pp.396, 14th International Workshop on Database and Expert Systems Applications (DEXA'03), 2003