1. Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions 2017 ABE CCS FormalVerification
    Miguel Ambrona, Gillis Barthe, Romain Gay, and Hoeteck Wee
    [View PDF on acmccs.github.io]
    [Show BibTex Citation]

    author = {Ambrona, Miguel and Barthe, Gilles and Gay, Romain and Wee, Hoeteck},
    title = {Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions},
    year = {2017},
    isbn = {9781450349468},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    url = {https://doi.org/10.1145/3133956.3134088},
    doi = {10.1145/3133956.3134088},
    booktitle = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security},
    pages = {647–664},
    numpages = {18},
    keywords = {automated proofs, symbolic security, attribute-based encryption, generic group model},
    location = {Dallas, Texas, USA},
    series = {CCS ’17}

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.