Welcome to the resource topic for 2016/270
Title:
Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model
Authors: Miguel Ambrona, Gilles Barthe, 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.
ePrint: https://eprint.iacr.org/2016/270
Talk: https://www.youtube.com/watch?v=kSB-3ekGXfU
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .