Paper 2016/270

Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model

Miguel Ambrona, 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.

Metadata
Available format(s)
PDF
Category
Public-key cryptography
Publication info
Published by the IACR in EUROCRYPT 2016
Keywords
Automated analysisGeneric Group ModelStructure-Preserving SignaturesSynthesis
Contact author(s)
miguel ambrona @ imdea org
History
2016-03-10: received
Short URL
https://ia.cr/2016/270
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2016/270,
      author = {Miguel Ambrona and Gilles Barthe and Benedikt Schmidt},
      title = {Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model},
      howpublished = {Cryptology ePrint Archive, Paper 2016/270},
      year = {2016},
      note = {\url{https://eprint.iacr.org/2016/270}},
      url = {https://eprint.iacr.org/2016/270}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.