TY - GEN

T1 - A Formal Security Analysis of Hyperledger AnonCreds

AU - Fraser, Ashley

AU - Schneider, Steve

PY - 2025/2/12

Y1 - 2025/2/12

N2 - In an anonymous credential system, users collectcredentials from issuers, and can use their credentials to gen-erate privacy-preserving identity proofs that can be shownto third-party verifiers. Since the introduction of anonymouscredentials by Chaum in 1985, there has been promisingadvances with respect to system design, security analysisand real-world implementations of anonymous credentialsystems.In this paper, we examine Hyperledger AnonCreds, ananonymous credential system that was introduced in 2017and is currently undergoing specification. Despite beingimplemented in deployment-ready identity system platforms,there is no formal security analysis of the HyperledgerAnonCreds protocol. We rectify this, presenting syntax anda security model for, and a first security analysis of, theHyperledger AnonCreds protocol. In particular, we demon-strate that Hyperledger AnonCreds is correct, and satisfiesnotions of unforgeability and anonymity. We conclude witha discussion on the implications of our findings, highlightingthe importance of rigorous specification efforts to supportsecurity evaluation of real-world cryptographic protocols.

AB - In an anonymous credential system, users collectcredentials from issuers, and can use their credentials to gen-erate privacy-preserving identity proofs that can be shownto third-party verifiers. Since the introduction of anonymouscredentials by Chaum in 1985, there has been promisingadvances with respect to system design, security analysisand real-world implementations of anonymous credentialsystems.In this paper, we examine Hyperledger AnonCreds, ananonymous credential system that was introduced in 2017and is currently undergoing specification. Despite beingimplemented in deployment-ready identity system platforms,there is no formal security analysis of the HyperledgerAnonCreds protocol. We rectify this, presenting syntax anda security model for, and a first security analysis of, theHyperledger AnonCreds protocol. In particular, we demon-strate that Hyperledger AnonCreds is correct, and satisfiesnotions of unforgeability and anonymity. We conclude witha discussion on the implications of our findings, highlightingthe importance of rigorous specification efforts to supportsecurity evaluation of real-world cryptographic protocols.

M3 - Conference contribution/Paper

BT - IEEE Euro S&P 2025

ER -