Top

Journal of Cryptology

Published in:

18-12-2018

Automated Analysis of Cryptographic Assumptions in Generic Group Models

Authors: Gilles Barthe, Edvard Fagerholm, Dario Fiore, John Mitchell, Andre Scedrov, Benedikt Schmidt

Published in: Journal of Cryptology | Issue 2/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We initiate the study of principled, automated methods for analyzing hardness assumptions in generic group models, following the approach of symbolic cryptography. We start by defining a broad class of generic and symbolic group models for different settings—symmetric or asymmetric (leveled) k-linear groups—and by proving “computational soundness” theorems for the symbolic models. Based on this result, we formulate a very general master theorem that formally relates the hardness of a (possibly interactive) assumption in these models to solving problems in polynomial algebra. Then, we systematically analyze these problems. We identify different classes of assumptions and obtain decidability and undecidability results. Next, we develop and implement automated procedures for verifying the conditions of master theorems, and thus the validity of hardness assumptions in generic group models. The concrete outcome of this work is an automated tool which takes as input the statement of an assumption and outputs either a proof of its generic hardness or shows an algebraic attack against the assumption.

previous article Efficient RSA Key Generation and Threshold Paillier in the Two-Party Setting

next article Hardness-Preserving Reductions via Cuckoo Hashing

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

The tool is available at https://github.com/generic-group-analyzer/gga.

We are oversimplifying. More precisely, one has to consider lists \(\varvec{C}\) and \(\varvec{C}'\) containing all Laurent polynomials computable by doing multiplications over \({\varvec{L}}\) and \({\varvec{L}}'\), respectively, and then look at linear dependencies in \(\varvec{C}\) and \(\varvec{C}'\).

In [26], Halevi informally divides proofs in two categories (quoting): “Most (or all) cryptographic proofs have a creative part (e.g., describing the simulator or the reduction) and a mundane part (e.g., checking that the reduction actually goes through). It often happens that the mundane parts are much harder to write and verify, and it is with these parts that we can hope to have automated help.”

Considering Laurent polynomials as rational functions whose denominator is a monomial.

In this case, setting the number of queries to some constant c, e.g., \(c=1,2\), corresponds to looking for reductions that invoke the adversary c times.

These restrictions include the limitation to bilinear groups and to oracles that do not take as input group elements.

M. Abadi, P. Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 20(3):395 (2007).CrossRefMATH

M. Abdalla, D. Pointcheval, Interactive Diffie–Hellman assumptions with applications to password-based authentication, in A. Patrick, M. Yung, editors, FC 2005, vol. 3570 of LNCS (Springer, 2005), pp. 341–356

G. Ateniese, J. Camenisch, B. de Medeiros, Untraceable RFID tags via insubvertible encryption, in V. Atluri, C. Meadows, A. Juels, editors, ACM CCS 05 (ACM Press, 2005), pp. 92–101

C. E. Z. Baltico, D. Catalano, D. Fiore, R. Gay, Practical functional encryption for quadratic functions with applications to predicate encryption, in Advances in Cryptology—CRYPTO 2017 (2017).

G. Barthe, J. Cederquist, S. Tarento, A machine-checked formalization of the generic model and the random oracle model, in Automated Reasoning—Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4–8, 2004, Proceedings, pp. 385–399 (2004)

G. Barthe, E. Fagerholm, D. Fiore, A. Scedrov, B. Schmidt, M. Tibouchi, Strongly-optimal structure preserving signatures from type ii pairings: Synthesis and lower bounds, in J. Katz, editor, Public-Key Cryptography—PKC 2015, vol. 9020 of LNCS (Springer, Berlin, 2015), pp. 355–376

G. Barthe, S. Tarento, A machine-checked formalization of the random oracle model, in Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15–18, 2004, Revised Selected Papers (2004), pp. 33–49

K. Benson, H. Shacham, B. Waters, The k-BDH assumption family: Bilinear map cryptography from progressively weaker assumptions, in E. Dawson, editor, CT-RSA 2013, vol. 7779 of LNCS, (Springer, Feb. / Mar. 2013), pp. 310–325

B. Blanchet. Security protocol verification: Symbolic and computational models, in POST 2012, vol. 7215 of Lecture Notes in Computer Science (Springer, Heidelberg, 2012), pp. 3–29

10.

A. Boldyreva, C. Gentry, A. O’Neill, D. H. Yum, Ordered multisignatures and identity-based sequential aggregate signatures, with applications to secure routing, in P. Ning, S. D. C. di Vimercati, P. F. Syverson, editors, ACM CCS 07 (ACM Press, 2007), pp. 276–285

11.

A. Boldyreva, C. Gentry, A. O’Neill, D. H. Yum, Ordered multisignatures and identity-based sequential aggregate signatures, with applications to secure routing. Cryptology ePrint Archive, Report 2007/438, revised 21 Feb 2010 (2007)

12.

D. Boneh, X. Boyen. Short signatures without random oracles. In C. Cachin, J. Camenisch, editors, EUROCRYPT 2004, vol. 3027 of LNCS (Springer, 2004), pp. 56–73

13.

D. Boneh, X. Boyen, E.-J. Goh. Hierarchical identity based encryption with constant size ciphertext, in R. Cramer, editor, EUROCRYPT 2005, vol. 3494 of LNCS (Springer, 2005), pp. 440–456

14.

D. Boneh, X. Boyen, E.-J. Goh. Hierarchical identity based encryption with constant size ciphertext. Cryptology ePrint Archive, Report 2005/015 (2005)

15.

D. Boneh, M. K. Franklin, Identity-based encryption from the Weil pairing, in J. Kilian, editor, CRYPTO 2001, vol. 2139 of LNCS (Springer, 2001), pp. 213–229

16.

D. Boneh, C. Gentry, B. Waters. Collusion resistant broadcast encryption with short ciphertexts and private keys, in V. Shoup, editor, CRYPTO 2005, vol. 3621 of LNCS (Springer, 2005), pp. 258–275

17.

D. Boneh, E.-J. Goh, K. Nissim, Evaluating 2-DNF formulas on ciphertexts, in J. Kilian, editor, TCC 2005, vol. 3378 of LNCS (Springer, 2005), pp. 325–341

18.

X. Boyen. The uber-assumption family (invited talk), in S. D. Galbraith, K. G. Paterson, editors, PAIRING 2008, vol. 5209 of LNCS (Springer, 2008), pp. 39–56

19.

E. Bresson, Y. Lakhnech, L. Mazaré, B. Warinschi, A generalization of DDH with applications to protocol analysis and computational soundness, in A. Menezes, editor, CRYPTO 2007, vol. 4622 of LNCS (Springer, 2007), pp. 482–499

20.

H. Cohen, A course in computational algebraic number theory, vol. 138 of Graduate Texts in Mathematics (Springer, Berlin, 1993)

21.

L. De Moura, N. Bjørner, Z: An efficient smt solver, in Tools and Algorithms for the Construction and Analysis of Systems (Springer, 2008), pp. 337–340

22.

A. Escala, G. Herold, E. Kiltz, C. Ràfols, J. Villar. An algebraic framework for Diffie–Hellman assumptions, in R. Canetti, J. A. Garay, editors, CRYPTO 2013, Part II, vol. 8043 of LNCS (Springer, 2013), pp. 129–147

23.

D. M. Freeman, Converting pairing-based cryptosystems from composite-order groups to prime-order groups, in H. Gilbert, editor, EUROCRYPT 2010, vol. 6110 of LNCS (Springer, 2010), pp. 44–61

24.

S. Garg, C. Gentry, A. Sahai, B. Waters. Witness encryption and its applications, in D. Boneh, T. Roughgarden, J. Feigenbaum, editors, 45th ACM STOC (ACM Press, 2013), pp. 467–476

25.

K. Gjøsteen, Ø. Thuen. Password-based signatures, in Public Key Infrastructures, Services and Applications (Springer, 2012), pp. 17–33

26.

S. Halevi, A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005)

27.

C. Hanser, D. Slamanig, Structure-preserving signatures on equivalence classes and their application to anonymous credentials, in P. Sarkar, T. Iwata, editors, Advances in Cryptology—ASIACRYPT 2014, vol. 8873 of Lecture Notes in Computer Science (Springer, Berlin, 2014), pp. 491–511

28.

C. Hanser, D. Slamanig. Structure-preserving signatures on equivalence classes and their application to anonymous credentials, in P. Sarkar, T. Iwata, editors, Advances in Cryptology—ASIACRYPT 2014, vol. 8873 of Lecture Notes in Computer Science (Springer, Berlin, 2014), pp. 491–511

29.

S. Hohenberger, A. Sahai, B. Waters, Full domain hash from (leveled) multilinear maps and identity-based aggregate signatures, in R. Canetti, J. A. Garay, editors, CRYPTO 2013, Part I, vol. 8042 of LNCS (Springer, 2013), pp. 494–512

30.

J. Y. Hwang, D. H. Lee, M. Yung, Universal forgery of the identity-based sequential aggregate signature scheme, in W. Li, W. Susilo, U. K. Tupakula, R. Safavi-Naini, V. Varadharajan, editors, ASIACCS 09 (ACM Press, 2009), pp. 157–160

31.

T. Jager, A. Rupp, The semi-generic group model and applications to pairing-based cryptography, in M. Abe, editor, ASIACRYPT 2010, vol. 6477 of LNCS (Springer, 2010), pp. 539–556

32.

T. Jager, J. Schwenk, On the equivalence of generic group models, in J. Baek, F. Bao, K. Chen, X. Lai, editors, ProvSec 2008, vol. 5324 of LNCS (Springer, 2008), pp. 200–209

33.

D. Jovanović, L. De Moura, Solving non-linear arithmetic, in Automated Reasoning(Springer, 2012), pp. 339–354

34.

J. Katz, A. Sahai, B. Waters, Predicate encryption supporting disjunctions, polynomial equations, and inner products, in N. P. Smart, editor, EUROCRYPT 2008, vol. 4965 of LNCS (Springer, 2008), pp. 146–162

35.

J. Katz, A. Sahai, B. Waters, Predicate encryption supporting disjunctions, polynomial equations, and inner products. Journal of Cryptology, 26(2), 191–224 (2013)

36.

A. Lysyanskaya, R. L. Rivest, A. Sahai, S. Wolf, Pseudonym systems, in H. M. Heys, C. M. Adams, editors, SAC 1999, vol. 1758 of LNCS (Springer, 1999), pp 184–199

37.

J. V. Matijasevic, Enumerable sets are diophantine. Dokl. Akad. Nauk SSSR, 191, 279–282 (1970)MathSciNet

38.

U. M. Maurer, Abstract models of computation in cryptography (invited paper), in N. P. Smart, editor, 10th IMA International Conference on Cryptography and Coding, vol. 3796 of LNCS (Springer, 2005), pp. 1–12

39.

U. M. Maurer, S. Wolf. Diffie–Hellman oracles, in N. Koblitz, editor, CRYPTO’96, vol. 1109 of LNCS (Springer, 1996), pp. 268–282

40.

M. Naor, On cryptographic assumptions and challenges (invited talk), in D. Boneh, editor, CRYPTO 2003, vol. 2729 of LNCS (Springer, 2003), pp. 96–109

41.

V. I. Nechaev, Complexity of a determinate algorithm for the discrete logarithm. Mathematical Notes, 55(2), 165–172 (1994)MathSciNetCrossRefMATH

42.

T. Okamoto, K. Takashima, Fully secure functional encryption with general relations from the decisional linear assumption, in T. Rabin, editor, CRYPTO 2010, vol. 6223 of LNCS (Springer, 2010), pp. 191–208

43.

A. Robinson, Solution of a problem of tarski. Fundamenta Mathematicae, 47(2), 179–204 (1959)MathSciNetCrossRefMATH

44.

J. T. Schwartz, Fast probabilistic algorithms for verification of polynomial identities. Journal of the ACM, 27, 701–717 (1980)MathSciNetCrossRefMATH

45.

H. Shacham, A cramer-shoup encryption scheme from the linear assumption and from progressively weaker linear variants. Cryptology ePrint Archive, Report 2007/074 (2007). http://eprint.iacr.org/2007/074.

46.

V. Shoup, Lower bounds for discrete logarithms and related problems, in W. Fumy, editor, EUROCRYPT’97, vol. 1233 of LNCS (Springer, 1997), pp. 256–266

47.

W. Stein et al. Sage Mathematics Software (Version 5.12). The Sage Development Team (2013) http://www.sagemath.org

48.

M. Szydlo, A note on chosen-basis decisional Diffie–Hellman assumptions, in Financial Cryptography and Data Security (Springer, 2006), pp. 166–170

49.

R. Zippel, Probabilistic algorithms for sparse polynomials, in E. W. Ng, editor, EUROSM ’79, vol. 72 of Lecture Notes in Computer Science (Springer, 1979), pp. 216–226

Title: Automated Analysis of Cryptographic Assumptions in Generic Group Models
Authors: Gilles Barthe
Edvard Fagerholm
Dario Fiore
John Mitchell
Andre Scedrov
Benedikt Schmidt
Publication date: 18-12-2018
Publisher: Springer US
Published in: Journal of Cryptology / Issue 2/2019
Print ISSN: 0933-2790
Electronic ISSN: 1432-1378
DOI: https://doi.org/10.1007/s00145-018-9302-3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 2/2019

On Tight Security Proofs for Schnorr Signatures

Efficient RSA Key Generation and Threshold Paillier in the Two-Party Setting

Hardness-Preserving Reductions via Cuckoo Hashing

Cryptanalysis of the CLT13 Multilinear Map

From Physical to Stochastic Modeling of a TERO-Based TRNG

Non-black-box Simulation in the Fully Concurrent Setting, Revisited

Premium Partner