Cryptology ePrint Archive: Report 2017/983

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

Miguel Ambrona and Gilles Barthe and Romain Gay and Hoeteck Wee

Abstract: 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.

Category / Keywords: public-key cryptography / automated proofs, symbolic security, attribute-based encryption, generic group model

Original Publication (with minor differences): ACM Conference on Computer and Communications Security 2017

Date: received 5 Oct 2017

Contact author: rgay at di ens fr

Available format(s): PDF | BibTeX Citation

Version: 20171009:145658 (All versions of this report)

Short URL: ia.cr/2017/983