Formal Analysis of a TTP-Free Blacklistable Anonymous Credentials System

This paper firstly introduces a novel security definition for BLAC-like schemes (BLAC represents TTP-free BLacklistable Anonymous Credentials) in symbolic model using applied pi calculus, which is suitable for automated reasoning via formal analysis tools. We model the definitions of some common security properties: authenticity, non-framebility, mis-authentication resistance and privacy (anonymity and unlinkability). The case study of these security definitions is demonstrated by modelling and analyzing BLACR (BLAC with Reputation) system. We verify these security properties by Blanchet's ProVerif and a ZKP (Zero-Knowledge Proof) compiler developed by Backes et al.. In particular, we analyze the express-lane authentication in BLACR. The analysis discovers a known attack that can be carried out by any potential user to escape from being revoked as he wishes. We provide a revised variant that can be proved successfully by ProVerif, which also indicates that the fix provided by ExBLACR (Extending BLACR) is incorrect.