Paper 2017/983

Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions

Miguel Ambrona, Gilles Barthe, Romain Gay, and Hoeteck Wee


Attribute-based encryption (ABE) is a cryptographic primitive which supports fine-grained access control on encrypted data, making it an appealing building block for many applications. In this paper, we propose, implement, and evaluate fully automated methods for proving security of ABE in the Generic Bilinear Group Model (Boneh, Boyen, and Goh, 2005, Boyen, 2008), an idealized model which admits simpler and more efficient constructions, and can also be used to find attacks. Our method is applicable to Rational-Fraction Induced ABE, a large class of ABE that contains most of the schemes from the literature, and relies on a Master Theorem, which reduces security in the GGM to a (new) notion of symbolic security, which is amenable to automated verification using constraint- based techniques. We relate our notion of symbolic security for Rational-Fraction Induced ABE to prior notions for Pair Encodings. Finally, we present several applications, including automated proofs for new schemes.

Available format(s)
Public-key cryptography
Publication info
Published elsewhere. MINOR revision.ACM Conference on Computer and Communications Security 2017
automated proofssymbolic securityattribute-based encryptiongeneric group model
Contact author(s)
rgay @ di ens fr
2017-10-09: received
Short URL
Creative Commons Attribution


      author = {Miguel Ambrona and Gilles Barthe and Romain Gay and Hoeteck Wee},
      title = {Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions},
      howpublished = {Cryptology ePrint Archive, Paper 2017/983},
      year = {2017},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.