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
[ Cryptology ePrint archive ]