Formal Analysis of Selective Disclosure Attribute-Based Credential System in Applied Pi Calculus

摘要

We propose a general framework of formally verifying selective disclosure attribute-based credential system. The framework includes two modules: the first module allows user to receive a credential, which contains a list of attributes, from a trusted party, the second module allows user to convince a service provider with the credential. Particularly, the user can selectively disclose parts of the attributes according to the requirement of the service provider, while not revealing the rest of the attributes. We formalize the framework with applied Pi calculus. It can be used to check attribute-based credential system on security properties. In our experiments, we apply the framework to a concrete security protocol and successfully prove the authenticity properties in the protocol using Pro Verif.