Cryptology ePrint Archive: Report 2016/270

Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model

Miguel Ambrona and Gilles Barthe and Benedikt Schmidt

Abstract: We develop a new method to automatically prove security statements in the Generic Group Model as they occur in actual papers. We start by defining (i) a general language to describe security definitions, (ii) a class of logical formulas that characterize how an adversary can win, and (iii) a translation from security definitions to such formulas. We prove a Master Theorem that relates the security of the construction to the existence of a solution for the associated logical formulas. Moreover, we define a constraint solving algorithm that proves the security of a construction by proving the absence of solutions.

We implement our approach in a fully automated tool, the $gga^{\infty}$ tool, and use it to verify different examples from the literature. The results improve on the tool by Barthe et al. (CRYPTO'14, PKC'15): for many constructions, $gga^{\infty}$ succeeds in proving standard (unbounded) security, whereas Barthe's tool is only able to prove security for a small number of oracle queries.

Category / Keywords: public-key cryptography / Automated analysis; Generic Group Model; Structure-Preserving Signatures; Synthesis

Original Publication (in the same form): IACR-EUROCRYPT-2016

Date: received 10 Mar 2016

Contact author: miguel ambrona at imdea org

Available format(s): PDF | BibTeX Citation

Version: 20160310:181210 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]