Automated Analysis of Cryptographic Assumptions in Generic Group Models

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.

1 Introduction

Sophisticated abstractions have often been instrumental in recent breakthroughs in the design of cryptographic schemes. Bilinear maps are perhaps the most striking instance of such an abstraction; over the last fifteen years, they have been used for building advanced and previously unknown cryptographic schemes. Now it is believed that multilinear maps will lead to similar breakthroughs. Compared to the “classical” algebraic settings based on the purported hardness of the Factoring/RSA or Discrete-log/Diffie–Hellman problems, bilinear and multilinear maps indeed provide richer and more versatile algebraic structures that are particularly suitable for new constructions. At the same time, one unsettling consequence of using such sophisticated abstractions is a significant growth in the number of hardness assumptions used in security proofs. Moreover, these assumptions are not as well studied as their classical and standard counterparts. While it is widely acknowledged that this situation is far from ideal, relying on non-standard assumptions is sometimes the only known way to construct some new (or some efficient) cryptographic scheme, and hence it cannot be completely disregarded. A common view to resolving this dilemma is to develop principled, rigorous approaches for analyzing and comparing non-standard hardness assumptions.

This question has been previously considered in the literature, in which we identify at least two approaches. One approach is to devise assumptions that are general enough to be reused and allow for simple security proofs, and at the same time are shown to hold under more classical assumptions (e.g., [19, 42]). A second approach is to develop idealized models, such as the Generic Group [38, 41, 46] and the Generic Bilinear Group [13] models, and to provide (in the form of so-called master theorems) necessary and sufficient conditions for the security of an assumption in these models. Proving the hardness of an assumption in these models is essentially a way to rule out the possibility of algebraic attacks against the underlying algorithmic problem, and it can be considered the minimal level of guarantee we need to gain confidence in an assumption. Two prominent examples along this direction are the “Uber assumption” (aka “Master theorem”) of Boneh, Boyen and Goh [13, 18] and the Matrix Decisional Diffie–Hellman assumption family recently proposed by Escala et al. [22].

However, although these results are quite general, they can be quite difficult to apply. Indeed, in order to argue the hardness of an assumption using the Uber assumption in [13, 18] (resp. the Matrix-DDH assumption in [22]) one has to show the independence (resp. irreducibility) of certain polynomials contained in the statement of the assumption. A similar problem arises in the context of interactive assumptions such as [2, 36], in which the hardness crucially relies on the restrictions posed on the queries performed by the adversary. In summary, applying these general results to verify the validity of a given assumption is far from being a trivial task and may be error-prone, as witnessed by unfortunate failures [30, 48].

In this paper, we initiate the study of principled, automated methods for analyzing hardness assumptions in generic group models. Our main contribution is essentially threefold. First, we reformulate master theorems in the style of the celebrated “computational soundness” theorem of Abadi and Rogaway [1], and formally show that the problem of analyzing assumptions in the generic group reduces to solving problems in polynomial algebra. Second, we systematically analyze these problems: While we show that the most general problem is undecidable, we distill a set of properties (capturing most interesting cases) for which the problem is decidable. Finally, by applying tools from linear algebra, 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 an assumption and outputs either a proof of its generic hardness (along with concrete bounds) or shows an algebraic attack against the assumption.

1.1 An Overview of Our Contribution

The key contribution of our work is the development of automated decision procedures for testing the validity of hardness assumptions in generic group models. Toward this goal, we first settle a rigorous framework for carrying out this analysis. Basically, this framework consists of formalizing a class of generic group models and then stating a general master theorem. Finally, our decision procedures will be aimed at verifying the side conditions of our master theorem.

1.1.1 Generic Group Models

We formalize a broad class of generic group models capturing many interesting cases used in cryptography: symmetric and asymmetric k-linear groups, with both leveled and non-leveled maps, and with the possibility of modeling efficiently computable isomorphisms between the groups. For any experiment stated in these generic models, we generalize the commonly used step of applying the Schwartz–Zippel Lemma, and obtain a generic transformation (cf. Theorem 1) for switching from the generic group model experiment, in which variables are uniformly sampled in the underlying field, to a completely deterministic experiment that works in a corresponding symbolic group model.

1.1.2 A General Master Theorem

We give a general version of the Master theorem in [13] which can be stated in any of the generic group models mentioned above. We formulate an assumption as a list ${\varvec{L}}$ of Laurent polynomials in ${\mathbb {F}}_p[X_1,X_1^{-1}, \ldots , X_n,X_n^{-1}]$ where $X_1, \ldots , X_n$ is a set of random variables. In particular, a decisional (aka left-or-right) assumption is defined by two lists of Laurent polynomials ${\varvec{L}}$ and ${\varvec{L}}'$ (one for the “left” and one for the “right” distribution), and the assumption is said to hold if the adversary cannot distinguish whether it receives Laurent polynomials from ${\varvec{L}}$ or ${\varvec{L}}'$. Very informally, our Master theorem states that viewing ${\varvec{L}}$ and ${\varvec{L}}'$ as the generating sets of two vector spaces,² then the linear dependencies within ${\varvec{L}}$ and within ${\varvec{L}}'$ are the same. Previous master theorems [13, 22] considered only decisional assumptions with the real-or-random formulation in which the adversary is given a list of polynomials ${\varvec{L}}$ and either a “challenge” polynomial f or a fresh random variable Z.

Beyond obtaining a theorem that works in (leveled) k-linear groups, our general formulation allows us to capture virtually all decisional assumptions, based on k-linear groups (for any $k \ge 1$), that are used in cryptography. To mention some examples, assumptions captured by our theorem include the Matrix-DDH assumption [22], the k-BDH assumption [8], and recently proposed assumptions such as (n, k)-MMDHE [29].

Finally, we extend both the generic group model and our master theorem to the case of groups of composite order. This allows us to capture more cryptographic assumptions such as the Subgroup Decision assumption [17].

1.1.3 Automated Methods

Once we have settled the above framework, our goal is to develop a collection of automated methods to verify the side condition of the Master theorem for any given assumption stated in the framework. While the statement of the above side condition already suggests how to use linear algebra to make these checks, a crucial challenge is that in many important cases (e.g., $\ell$-BDHI, k-Lin) the size of the lists ${\varvec{L}}$ and ${\varvec{L}}'$ is a variable parameter. That is, to check that the side condition holds, one would have to do computations on a vector space of variable dimension: a challenging problem for automation.

We study this problem for three main categories of hardness assumptions: (1) nonparametric, (2) parametric, and (3) interactive. Nonparametric assumptions are non-interactive assumptions in which the number of inputs is fixed, the input polynomials are fixed, and the number of levels is fixed (examples include DDH, DBDH [15], as well as assumptions in k-linear groups for fixed k, e.g., 3-Lin in 3-linear groups). Conversely, an assumption is parametric if one or more of the above restrictions do not hold. Finally, interactive assumptions are those in which the adversary is granted access to additional oracles (in addition to the oracles for the algebraic operations). By carefully analyzing each of these categories, we obtain the following results summarized in Table 1.

Table 1 Summary of our automated analysis methods

For nonparametric assumptions, we show how to reduce the check on the side condition to computing the kernels of certain matrices (of fixed dimension) that are derived from the lists of polynomials in the assumption’s definition. Using computer algebra tools (SAGE [47]), we implement a decision procedure that shows a concrete hardness bound in the corresponding generic group model in the positive case, and an algebraic attack if the assumption does not hold.

Our methods for nonparametric assumptions offer a complete decision procedure to verify arbitrary instances of parametric assumptions where all the parameters have been fixed. This might be sufficient to test quickly a new assumption (and find attacks if any), but it is often desirable to obtain stronger guarantees that hold for all parameters. We show that, contrary to the nonparametric case, the side condition becomes undecidable in general. However, we identify a class of assumptions for which we develop an automated method. Our method focuses on the case in which the number of random variables is fixed, and the input elements are monomials. We show how to reduce the check of the side condition to an integer programming problem. Interestingly, we can show the following: If the degree of the monomials is not a linear polynomial, or the arity of the map is variable, then the problem is undecidable; otherwise (if the monomials have linear degree and the arity of the map is fixed), the problem is decidable. We implemented the translation procedure to integer programming problems and use SMT solvers to check satisfiability. For the decidable fragment of assumptions mentioned above, we obtain a complete decision procedure that also shows an attack if the assumption is invalid. For the undecidable fragment, our procedure successfully analyzes all significant examples from the literature.

Finally, we study interactive assumptions such as LRSW [36]. To analyze interactive assumptions, we first formulate an interactive version of our master theorem. Interestingly, once applying our general “computational soundness” theorem and switching to the symbolic model, our interactive master theorem essentially becomes a variant of the non-interactive master theorem, where some variables are under adversarial control. This allow us to apply similar techniques as for parametric assumptions. More specifically, we use SMT solvers and Gröbner bases computations as an incomplete method to show the validity of such assumptions and find attacks. For instance, our tool automatically proves the validity of LRSW [36] and exhibits attacks for m-LRSW [10]. Additionally, certain security definitions such as EUF-CMA are expressible as an interactive assumption, allowing our tool to automatically find attacks against a flawed SPS-EQ scheme of [27] as well as being used as a verification back end for synthesis of SPS schemes [6]. Similarly, reductions between computational assumptions such as CDH and Square-CDH can also be phrased as an interactive assumption, therefore allowing explicit reductions to be found automatically by the tool.

1.1.4 Limitations

While our master theorem is very general, our automated methods require to specify the assumptions in a concrete language, essentially to describe the distribution of the Laurent polynomials defining the assumption. Such language cannot support the expression of very abstract properties, and thus rules out a few examples. For instance, the definition of the Decision Multilinear No-Exact-Cover Assumption [24] is parameterized by an instance (with no solution) of the Exact-Cover NP-complete problem. Although fixing a specific Exact-Cover instance yields lists of polynomials which can be analyzed using our methods, a definition for any instance is too general. For a similar reason, our tool cannot handle the Matrix-DDH assumption in its full generality, unless one fixes a specific distribution for the matrix (e.g., k-Lin).

1.1.5 Discussion

Although well-studied standard assumptions should always be preferred when designing cryptographic schemes, the use of non-standard ones is not likely to stop. In this sense, we believe the study and development of rigorous methods for analyzing cryptographic assumptions is relevant, and that automated analysis tools can support cryptographers in multiple directions. Mainly, they provide a rigorous, fast way to test the validity of candidate assumptions in generic models by delegating this task to a machine. This is especially relevant in the recent setting of leveled multilinear maps, that have a rich algebraic structure and for which even simple assumptions may become difficult to analyze. We believe that the importance of such tools is motivated by the fact that proofs validating the hardness of an assumption in the generic group model fall exactly in the so-called “mundane part”³ of cryptographic proofs mentioned by Halevi [26], and constitute a perfect candidate of a proof to be delegated to a machine.

Our work shows the feasibility and relevance of developing automated methods to analyze assumptions in generic group models. It can also be seen as the first step toward analyzing cryptographic protocols directly in the generic model; we expect that such analyses would allow to discover subtle flaws in protocols and supplant existing methods based on symbolic cryptography.

1.2 Related Work

The problem of analyzing and comparing hardness assumptions has been earlier considered in the literature, e.g., [40]. In particular, we identify two main approaches in the previous work. The first approach aims to define generalized assumptions that reduce to standard ones. Examples of works in this direction include: the Square Diffie–Hellman assumption, shown to be equivalent to CDH by Maurer and Wolf [39]; the (P, Q)-Decisional Diffie–Hellman assumption of Bresson et al. [19] which is shown to reduce to DDH; and the decisional subspace problems of Okamoto–Takashima [42] that are reduced to DLin.

The other approach aims at directly analyzing assumptions by means of idealized models, such as the generic group model. This model was introduced by Nechaev [41] and further refined and generalized by Shoup [46], and Maurer [38]. Our work follows closely Maurer’s model, in which the main difference compared to previous proposals is to model the adversary’s access to group elements via handles instead of random bitstrings as in [41, 46]. These two models have been proven equivalent in [32]. Worth mentioning in this context is the semi-generic group model of Jager and Rupp [31]. This is a weaker version of the bilinear generic group model, and its basic idea is to model the base groups of pairings as generic groups, whereas the target group is given in the standard model.

Two works that address the problem of devising general assumptions in the generic group are the Master theorem of Boneh et al. [13] (generalized by Boyen [18]), and the Matrix-DDH assumption of Escala et al. [22]. Roughly speaking, the former provides a framework for arguing about the validity of several pairing-based assumptions in the generic group model, and it captures a significant fraction of assumptions in the literature. The latter is an assumption that subsumes classical problems like DDH or DLin and also introduces assumptions, such as k-Casc, that are proven hard in the generic k-linear group model. In [5, 7], Barthe, Cederquist and Tarento use the Coq proof assistant to formalize the Generic Group model, on its own and in conjunction with the Random Oracle model, and use their formalization to reason about the security of signed ElGamal encryption. Also worth mentioning is the work of Freeman [23] which extends the BBG Master theorem to challenges in the source group and uses the computer algebra system Magma to verify the side conditions required to prove two of the assumptions. Our work is also close to the line of work on automation of cryptographic proofs in both the computational and symbolic models, see [9] for an overview.

1.3 Preliminaries

In our work, we denote by $\lambda$ the security parameter. We use $\mathbb {G}_i$ to denote additive cyclic groups of prime order and $P_i$ to denote a generator of $\mathbb {G}_i$. For any element $Q=x P_i$, we denote with $x={ d }{\mathrm {log}}(Q)$ its discrete logarithm. We use ${{\varvec{a}}}$ or ${\varvec{v}}$ to denote vectors, ${{\varvec{a}}} \Vert {{\varvec{b}}}$ for the concatenation of two vectors, and ${{\varvec{a}}} \cdot {{\varvec{b}}}$ to denote their inner product. We denote the power set of S with $\mathcal {P}(S)$, the ith element of a list with L[i], the range $\{n,\ldots ,n+l\}$ with $[n,n+l]$, and [1, n] with [n]. A (multivariate) Laurent polynomial f over a field $\mathbb {F}$ is a polynomial where variables can take also negative powers, and we denote it as $f \in \mathbb {F}[X_1, X_1^{-1}, \ldots , X_n, X_n^{-1}]$.

A symmetric k-linear group is a pair of groups $\mathbb {G}_1$ and $\mathbb {G}_2$ together with an admissible k-linear map $e:\mathbb {G}_1^k\rightarrow \mathbb {G}_2$. An asymmetric k-linear group is a sequence of groups $\mathbb {G}_1,\ldots ,\mathbb {G}_k,\mathbb {G}_{k+1}$ together with an admissible k-linear map $e:\mathbb {G}_1\times \cdots \times \mathbb {G}_k\rightarrow \mathbb {G}_{k+1}$. A k-linear map is said admissible if it is non-degenerate (i.e., there exist $P_1, \ldots , P_k$ such that $e(P_1, \ldots , P_k) \ne 1_{\mathbb {G}_{k+1}}$) and efficiently computable. For a k-linear map $e:\mathbb {G}_1\times \cdots \times \mathbb {G}_k\rightarrow \mathbb {G}_{k+1}$, we call $\mathbb {G}_{k+1}$ the target group and other groups $\mathbb {G}_i$source groups. We can further assume existence of isomorphisms $\mathbb {G}_i\rightarrow \mathbb {G}_j$ between source groups.

A symmetric leveled k-linear group is a sequence of groups $\mathbb {G}_1,\ldots ,\mathbb {G}_{k}$ together with bilinear maps $e:\mathbb {G}_i\times \mathbb {G}_j\rightarrow \mathbb {G}_{i+j}$ for $i,j\in [1,k]$ and $i+j\le k$. We say that $\mathbb {G}_n$ is the group at level n and call $\mathbb {G}_{k}$ the target group. An asymmetric leveled k-linear group is a collection of groups $\{\mathbb {G}_S\}$ for $S\in \mathcal {P}([k]) {\setminus } \{\emptyset \}$ together with bilinear maps $e_{S,T}:\mathbb {G}_S\times \mathbb {G}_T \rightarrow \mathbb {G}_{S\cup T}$ for all $S\cap T=\emptyset$.

2 Generic Group Models and Symbolic Group Models

In this section, we define a class of generic group models that captures the previously described group settings. Afterward, we define a symbolic group model where instead of computing with (randomly sampled) group elements, the challenger computes with (fixed) polynomials. We prove that this model is equivalent to the generic group model up to some usually small error.

2.1 Generic Group Models

A generic group model for a concrete group setting captures all operations that an adversary with black box access can perform.

Definition 1

A group setting is a tuple ${\mathcal {G}}{\mathcal {S}}=(p,\mathcal {G}, \varPhi , \mathcal {E})$ where $\mathcal {G}= \{\mathbb {G}_i\}_{i \in \mathcal {I}}$ is a set of cyclic groups of prime order p indexed by a totally ordered finite set $\mathcal {I}$, $\varPhi$ is a set of isomorphisms $\phi : \mathbb {G}_i \rightarrow \mathbb {G}_j$, and $\mathcal {E}$ is a set of maps, where for each $e\in \mathcal {E}$, there are an integer k and indices $i_1, \ldots , i_{k+1} \in \mathcal {I}$ s.t.$~\hbox { }\ e : \mathbb {G}_{i_1} \times \cdots \times \mathbb {G}_{i_k} \rightarrow \mathbb {G}_{i_{k+1}}$ is an admissible k-linear map.

The generic model for a group setting $(p,\mathcal {G}, \varPhi , \mathcal {E})$ and a distribution $\mathcal {D}$ on indexed sets $\{L_i\}_{i \in \mathcal {I}}$ of lists of elements of $\mathbb {G}_i$ is shown in Fig. 1. The challenger maintains lists ${\varvec{L}}=\{L_i\}_{i\in \mathcal {I}}$ where each list $L_i$ contains elements from $\mathbb {G}_i$. The lists are initialized by sampling from $\mathcal {D}$ and the adversary can apply the group operations, isomorphisms, and k-linear maps to list elements by providing the indices of elements as handles. For an operation $o : \mathbb {G}_{i_1} \times \cdots \times \mathbb {G}_{i_k} \rightarrow \mathbb {G}_{i_{k+1}}$, the corresponding oracle takes handles $h_1,\ldots ,h_k$, computes $a = o(a_1,\ldots ,a_k)$ for $a_j = L_{i_j}[h_j]$, appends a to $L_{i_{k+1}}$ and returns a’s handle $h=|L_{i_{k+1}}|$. Note that handles are not unique (i.e., several handles can point to the same group element), but the challenger provides an equality oracle to check if two handles refer to the same group element.

Fig. 1

Generic group model $\mathsf {Gen}^{{\mathcal {G}}{\mathcal {S}}}_{\mathcal {D}}$ for group setting ${\mathcal {G}}{\mathcal {S}}= (p,\mathcal {G}, \varPhi , \mathcal {E})$ and distribution $\mathcal {D}$

Remark 1

As mentioned in Sect. 1.2, our generic group model closely follows Maurer’s model [38]. We provide the adversary with access to the internal state variables of the challenger via handles, and we assume that the equality queries are “free,” in the sense that they do not count when measuring the computational complexity of the adversary.

Example 1

To model an asymmetric leveled k-linear map, we use the index set $\mathcal {I}= \mathcal {P}([k]) {\setminus } \{\emptyset \}$, $\varPhi = \emptyset$, and $\mathcal {E}= \{ e_{T,R} : \mathbb {G}_T \times \mathbb {G}_R \rightarrow \mathbb {G}_{T \cup R} \mid T,R \in \mathcal {I}\wedge T \cap R = \emptyset \}$.

Definition 2

For a list of lists ${\varvec{L}}= L_1, \ldots , L_k$ of Laurent polynomials in ${\mathbb {F}}_p[X_1,X_1^{-1},\ldots ,X_n,X_n^{-1}]$, where each list is assumed to contain the constant Laurent polynomial 1, we define the distribution $\mathcal {D}_{{\varvec{L}}}$ by the following procedure. Uniformly sample a point ${\varvec{x}} \in ({\mathbb {F}}_p^*)^n$ and return the list of lists ${\varvec{L}}' = L'_1, \ldots , L'_k$ where $L'_i = [ {f_1({\varvec{x}})} P_i, \ldots , {f_{|L_i|}({\varvec{x}})} P_i]$ for $f_j = L_i[j]$. A distribution $\mathcal {D}$ is polynomially induced if $\mathcal {D}= \mathcal {D}_{{\varvec{L}}}$ for some ${\varvec{L}}$.

Note that we sample nonzero elements in ${\mathbb {F}}_p$ to ensure that all Laurent polynomials can be evaluated without dividing by zero.

Most hardness assumptions in generic group models belong to the following classes of decisional, computational, or generalized extraction problems stated with respect to a group setting ${\mathcal {G}}{\mathcal {S}}$:

• Decisional problem for ${\mathcal {D}_{{\varvec{L}}}}$ and ${\mathcal {D}_{{\varvec{L}}'}}$: The adversary returns $b \in \{ 0,1 \}$ to distinguish the corresponding generic group models. We consider the event $b = 1$.

• Computational problem for ${\mathcal {D}_{{\varvec{L}}}}$, Laurent polynomial f, and group index i: We consider the event $L_i[h] = {f({\varvec{x}})}P_i$, where h is a handle returned by the adversary and ${\varvec{x}}$ is the random point sampled by $\mathcal {D}_{{\varvec{L}}}$.

• Generalized extraction problem for ${\mathcal {D}_{{\varvec{L}}}}$, integers n, m, group indices $i_1,\ldots ,i_m$, and Laurent polynomials ${H_1,\ldots ,H_k}$ and $G_1,\ldots ,G_l$: The adversary returns ${{\varvec{a}}} \in {\mathbb {F}}_p^n$ and handles $h_1,\ldots ,h_m$. We consider the event that, for all $i \in [k]$ and $j \in [l]$, the point ${\varvec{x}}$ sampled by $\mathcal {D}_{{\varvec{L}}}$ satisfies $\hbox { }\ H_i({\varvec{x}}, {{\varvec{a}}}, { d }{\mathrm {log}}(L_{i_1}[h_1]),\ldots ,{ d }{\mathrm {log}}(L_{i_m}[h_m])) = 0$ and $G_j({\varvec{x}}, {{\varvec{a}}}, { d }{\mathrm {log}}(L_{i_1}[h_1]),\ldots ,{ d }{\mathrm {log}}(L_{i_m}[h_m]))\ne 0$.

The above classification generalizes the one proposed by Maurer [38]. Precisely, in addition to decisional and computational assumptions, Maurer considered “straight” extraction problems (such as discrete logarithm) in which the adversary has to extract the random value x of a handle. Our class of generalized extraction problems captures extraction problems like discrete logarithm, but also captures problems like the Strong Diffie–Hellman (SDH) Problem [12]. Moreover, note that our class of generalized extraction problems contains the class of computational problems. Indeed, by setting $m=1$, $l=n=0$, and $H_1({{\varvec{x}}}, y) = f({{\varvec{x}}})-y$, we recover the event “$L_i[h] = {f({\varvec{x}})}P_i$” of computational problems.

Finally we note that the above classification considers only non-interactive problems where the adversary can only interact through the oracles described in Fig. 1 essentially for computing group operations, isomorphisms and k-linear maps. The case of interactive assumptions where the adversary has access to additional oracles that compute over the group elements stored in the lists is discussed in Sect. 5.

Example 2

Set $n=1$, $m=0$, then $H(X,a_1) = X - a_1$ encodes DLOG as a generalized extraction problem and $n=m=1$, $H(X,a_1,Y) = (X - a_1)Y - 1$ encodes SDH.

2.2 From Generic to Symbolic Group Models

The symbolic group model for a group setting $(p,\mathcal {G}, \varPhi , \mathcal {E})$ and a polynomially induced distribution $\mathcal {D}_{{\varvec{L}}}$ provides the same adversary interface as the corresponding generic group model. The difference is that, internally, the challenger now stores lists of Laurent polynomials in ${\mathbb {F}}_p[X_1,X_1^{-1},\ldots ,X_n,X_n^{-1}]$, where $X_1,\ldots ,X_n$ are the variables occurring in ${\varvec{L}}$. The oracles perform addition, negation, and equality checks in the ring. To define the polynomial operations corresponding to applications of isomorphisms and n-linear maps, observe that for all isomorphisms $\phi$ there is an $a \in {\mathbb {F}}_p^{\times }$ such that $\phi (g_i) = g_j^a$. We therefore define the oracle $\textsf {isom}_{\phi }(h)$ such that it computes $a\cdot L_i[h]$. Similarly, we define the oracle $\textsf {map}_{e}(h_1,\ldots ,h_k)$ such that it computes $a\cdot (L_{i_1}[h_1] \cdots L_{i_k}[h_k])$, for a such that $g_{i_{k+1}}^{a} = e(g_{i_1}, \ldots , g_{i_{k}})$. We also define symbolic versions S(E) of events E used to define decisional, computational, and generalized extraction problems. For decisional problems and computational problems, the symbolic event is equal to the generic event, i.e., $S(E)=E$. For generalized extraction problems, the event E is translated by replacing all arguments of the polynomials $H_j$ and $G_j$ that are of the form ${ d }{\mathrm {log}}(L_i[h])$ by $L_i[h]$. We denote the symbolic group model for a group setting ${\mathcal {G}}{\mathcal {S}}$ and a distribution $\mathcal {D}_{{\varvec{L}}}$ with $\mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}$ and the corresponding generic group model with $\mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}$.

To state our theorem, we define the maximal numerator degree for a given polynomially induced distribution $\mathcal {D}_{{\varvec{L}}}$, event E, and query-bound q, which we denote with $\hbox {mndeg}(\mathcal {D}_{{\varvec{L}}},E,q)$, as follows. Denote with S the set of all Laurent polynomials that can occur in the internal state of $\mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}$ and S(E) after q queries, denote with g their lowest common denominator,⁴ and denote with $S'$ the result of expressing all Laurent polynomials in S with denominator g. Then $\hbox {mndeg}(\mathcal {D}_{{\varvec{L}}},E,q)$ is defined as the maximal degree of a numerator in $S'$.

Theorem 1

Let $(p,\mathcal {G}, \varPhi , \mathcal {E})$ denote a group setting, where p is prime, $\mathcal {D}_{{\varvec{L}}}$ a polynomially induced distribution, $\mathcal {A}$ an adversary performing at most q queries, and E the winning event of a decisional, computational, or generalized extraction problem. If d is an upper bound on $\hbox {mndeg}(\mathcal {D}_{{\varvec{L}}},E,q)$, s is the sum of the sizes of the lists in ${\varvec{L}}$, and the event S(E) contains at most e equality tests, then

$$\begin{aligned} \left| {Pr\left[ \mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) : E \right] } - {Pr\left[ \mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) : S(E) \right] } \right| \le \left( \frac{(s + q)^2}{2} + e\right) \frac{d}{p - 1} \end{aligned}$$

where the probability is taken over the coins of $\mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}$ and $\mathcal {A}$.

Proof

First, observe that the number of equality checks between group elements (resp. Laurent polynomials) performed in $\mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}$ (resp. $\mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}$) is upper-bounded by $(s + q)^2/2 + e$. The adversary can perform at most $(s + q)^2/2$ distinct eq-queries since the lists ${\varvec{L}}$ contain $s+q$ Laurent polynomials and the evaluation of the event requires e equality checks. To perform the proof, we utilize a hybrid argument that replaces equality checks $f_1=f_2$ in $\mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A})$ by equality checks $f_1({\varvec{x}})=f_2({\varvec{x}})$ where ${\varvec{x}}$ is the random point required to compute $\mathcal {D}_{{\varvec{L}}}$. Since $f_i = h_i / g$ for a polynomial $h_i$ and the lowest common denominator g, we can then use the Schwartz–Zippel Lemma [44, 49] to bound the probability that $h_1 \ne h_2$ and $h_1({\varvec{x}}) = h_2({\varvec{x}})$.

More formally, for $i=0,\ldots ,n$ with n the number of equality checks, we define the hybrid game $\mathsf {Hyb}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}\langle i \rangle$ and hybrid event $H\langle i \rangle (E)$ as the following modifications of $\mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}$ and S(E), respectively. Namely, let a random point ${\varvec{x}}$ be sampled on initialization. In the ith hybrid, we use $f_1 = f_2$ for the first i equality checks, and $f_1({\varvec{x}}) = f_2({\varvec{x}})$ for equality checks from $i + 1$ to n. Then

$$\begin{aligned} {Pr\left[ \mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) : E \right] } = {Pr\left[ \mathsf {Hyb}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}\langle 0 \rangle (\mathcal {A}) : H\langle 0 \rangle (E) \right] } \end{aligned}$$

and

$$\begin{aligned} {Pr\left[ \mathsf {Hyb}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}\langle n \rangle (\mathcal {A}) : H\langle n \rangle (E) \right] } = {Pr\left[ \mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) : S(E) \right] }. \end{aligned}$$

To complete the proof, we use the Schwartz–Zippel Lemma to prove that for all $i \in [n]$,

$$\begin{aligned} \left| {Pr\left[ \mathsf {Hyb}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}\langle i-1 \rangle (\mathcal {A}) : H\langle i-1 \rangle (E) \right] } - {Pr\left[ \mathsf {Hyb}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}\langle i \rangle (\mathcal {A}) : H\langle i \rangle (E) \right] } \right| \le \frac{d}{p-1}. \end{aligned}$$

The two games are equivalent unless the ith equality check returns different results in the left and the right experiment. This happens when $f_1-f_2\ne 0$ and $f_1({\varvec{x}})-f_2({\varvec{x}})=0$. The inequality is equivalent to $((h_1-h_2) / g) \ne 0$ for the lowest common denominator g and polynomials $h_i$. The equality is equivalent to $(h_1-h_2)({\varvec{x}}) = 0$ since $g({\varvec{x}}) \ne 0$. Hence, we obtain the bound from the Schwartz–Zippel Lemma since the degree of $h_1 - h_2$ is bounded by d and ${\varvec{x}}$ is sampled independently (of $h_1$ and $h_2$) and uniformly from $({\mathbb {F}}_p^*)^n$.

$\square$

By applying this theorem, we can therefore analyze the hardness of assumptions in the simpler symbolic model. We note that existing master theorems usually include a similar step in their proofs. Here we explicitly prove the equivalence of the $\mathsf {Gen}^{}_{}$ and $\mathsf {Sym}^{}_{}$ experiments. This stronger result is required for our decidability results.

3 Master Theorem for Non-interactive Assumptions

In this section, we state our master theorem for decisional, non-interactive problems. In Sect. 5, we give a master theorem for interactive assumptions which cover generalized extraction problems (and computational ones per Sect. 2).

To state our theorem, we first define the completion $\mathcal {C}({\varvec{L}})$ of a list ${\varvec{L}}$ with respect to the group setting $(p,\mathcal {G}, \varPhi , \mathcal {E})$. This notion will be instrumental to define the side condition of our master theorem. Intuitively speaking, given a list ${\varvec{L}}$, its completion $\mathcal {C}({\varvec{L}})$ is the list of all Laurent polynomials that can be computed by the adversary by applying isomorphisms and maps to Laurent polynomials in ${\varvec{L}}$.

We compute the completion $\mathcal {C}({\varvec{L}})$ of ${\varvec{L}}$ in two steps. In the first step, we compute the recipe lists$\{R_i\}_{i \in \mathcal {I}}$ using the algorithm given in Fig. 2. The elements of the recipe lists are monomials over the variables $W_{i,j}$ for $\hbox { }\ (i,j) \in \mathcal {I}\times [|L_i|]$. The monomials characterize which products of elements in ${\varvec{L}}$ the adversary can compute by applying isomorphisms and maps. The result of the first step is independent of the elements in the lists ${\varvec{L}}$ and only depends on the lengths of the lists. In the second step, we compute the actual Laurent polynomials from the recipes $\{R_i\}_{i \in \mathcal {I}}$ as

$$\begin{aligned} \mathcal {C}({\varvec{L}})_i = \left[ m_1({\varvec{L}}), \ldots , m_{|R_i|}({\varvec{L}})\right] ~\mathrm {for}~\left[ m_1, \ldots , m_{|R_i|}\right] = R_i \end{aligned}$$

where every $m_i$ is a monomial over the variables $W_{i,j}$ and $m_i({\varvec{L}})$ denotes the result of evaluating the monomial $m_i$ for the values $L_{i}[j]$ of the variables $W_{i,j}$.

To ensure that the computation of the recipes terminates, we restrict ourselves to group settings without cycles, defined as follows. We also assume that the group setting contains a target group. Formally, for a group setting $(p,\mathcal {G}, \varPhi , \mathcal {E})$, we define the weighted directed graph $G=(V,E)$ with $V=\mathcal {G}$ and E defined as follows. For each isomorphism $\mathbb {G}_i\rightarrow \mathbb {G}_j\in \varPhi$, there is an edge from $\mathbb {G}_i$ to $\mathbb {G}_j$ of weight 0. Similarly, given any $\mathbb {G}_{i_1}\times \cdots \times \mathbb {G}_{i_n}\rightarrow \mathbb {G}_{i_{n+1}}\in \mathcal {E}$, there are edges from $\mathbb {G}_{i_j}$ to $\mathbb {G}_{i_{n+1}}$ of weight 1 for $j \in [n]$. We assume that the graph G contains no loops of positive weight. Furthermore, we assume there is a unique $\mathbb {G}_t\in V$ called the target group, such that from any $\mathbb {G}_i\in V$ there is a path to $\mathbb {G}_t$ and $\mathbb {G}_t$ does not have any outgoing edges.

Fig. 2

Computation of lists of recipes $R_i$ for input lists $L_i$

Example 3

Assume we are given a leveled 3-linear map with inputs $L_1=[1,X]$ and $L_i=\emptyset$ for $i=2,3,4$. Then $S_1=\{ W_{1,1},W_{1,2}\}$ and $S_i=\emptyset$ for $i=2,3,4$. Since there are no isomorphisms, the body of the $\textsf {while }$loop reduces to the first $\textsf {foreach }$loop and to checking whether the sets are saturated. The completion algorithm proceeds as follows:

• First iteration of $\textsf {while }$:

  • $e:\mathbb {G}_1 \times \mathbb {G}_1\rightarrow \mathbb {G}_2:$$S_2 :=\{W_{1,1}^2,W_{1,1}W_{1,2},W_{1,2}^2\} \,(= S_1 \cdot S_1)$.

  • $e:\mathbb {G}_1 \times \mathbb {G}_2\rightarrow \mathbb {G}_3:$ $S_3 := \{W_{1,1}^3,W_{1,1}^2W_{1,2},W_{1,1}W_{1,2}^2,W_{1,2}^3\} \,( = S_1 \cdot S_2)$

  • $e:\mathbb {G}_2 \times \mathbb {G}_2 \rightarrow \mathbb {G}_4:$ $S_4 := \{W_{1,1}^4,W_{1,1}^3W_{1,2},W_{1,1}^2W_{1,2}^2,W_{1,1}W_{1,2}^3,W_{1,2}^4\} \,( = S_2 \cdot S_2)$

  • $e:\mathbb {G}_1 \times \mathbb {G}_3 \rightarrow \mathbb {G}_4:$ $S_4 := S_4\, (= S_1 \cdot S_3 \text {, does not add any new monomials})$

• Second iteration of $\textsf {while }$: Sets already saturated, does not add any new monomials.

To get the completions, we plug in $W_{1,1}=1$ and $W_{1,2}=X$:

$$\begin{aligned} L_1 = [1,X],\; L_2=[1,X,X^2],\; L_3=[1,X,X^2,X^3],\; L_4=[1,X,X^2,X^3,X^4] \end{aligned}$$

Theorem 2

Let ${\mathcal {G}}{\mathcal {S}}=(p,\{\mathbb {G}_i\}_{i \in \mathcal {I}}, \varPhi , \mathcal {E})$ denote a group setting, and $\mathcal {D}_{{\varvec{L}}}, \mathcal {D}_{{\varvec{L}}'}$ be polynomially induced distributions such that $|L_{i}| = |L'_{i}|$ for all $i \in \mathcal {I}$. We assume that the Laurent polynomials in the completion $\mathcal {C}({\varvec{L}})_t$ (resp. $\mathcal {C}({\varvec{L}}')_t$) are expressed using their lowest common denominator. Let t denote the index of the target group, let $s = \sum _{i\in \mathcal {I}} | L_{i} |$, let $r = |\mathcal {C}({\varvec{L}})_t|$, and let d denote an upper bound on the degrees of the numerators of the Laurent polynomials in $\mathcal {C}({\varvec{L}})_t$ and $\mathcal {C}({\varvec{L}}')_t$. If

$$\begin{aligned} \left\{ {{\varvec{a}}} \in {\mathbb {F}}_p^r \mid {{\varvec{a}}} \cdot \mathcal {C}({\varvec{L}})_t = 0 \right\} = \left\{ {{\varvec{a}}} \in {\mathbb {F}}_p^r \mid {{\varvec{a}}} \cdot \mathcal {C}({\varvec{L}}')_t = 0 \right\} , \end{aligned}$$

then

$$\begin{aligned} \left| {Pr\left[ \mathsf {Gen}^{{\mathcal {G}}{\mathcal {S}}}_{\mathcal {D}_{{\varvec{L}}}}(\mathcal {A}) = 1 \right] } - {Pr\left[ \mathsf {Gen}^{{\mathcal {G}}{\mathcal {S}}}_{\mathcal {D}_{{\varvec{L}}'}}(\mathcal {A}) = 1 \right] } \right| \le \frac{(s + q)^2d}{p-1} \end{aligned}$$

for all adversaries $\mathcal {A}$ that perform at most q operations.

Proof

By using a standard hybrid argument, we can apply our Theorem 1 to switch both experiments $\mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A})$ and $\mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}'}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A})$ from the generic group model to the symbolic group model. Hence, we obtain:

$$\begin{aligned} \left| {Pr\left[ \mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) = 1 \right] } - {Pr\left[ \mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) = 1 \right] } \right| \le \frac{(s + q)^2d}{2(p-1)}\\ \left| {Pr\left[ \mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}'}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) = 1 \right] } - {Pr\left[ \mathsf {Gen}^{\mathcal {D}_{{\varvec{L}}'}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) = 1 \right] } \right| \le \frac{(s + q)^2d}{2(p -1)}. \end{aligned}$$

This leaves us with bounding

$$\begin{aligned} \left| {Pr\left[ \mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) = 1 \right] } - {Pr\left[ \mathsf {Sym}^{\mathcal {D}_{{\varvec{L}}'}}_{{\mathcal {G}}{\mathcal {S}}}(\mathcal {A}) = 1 \right] } \right| . \end{aligned}$$

However, note that the view of the adversary $\mathcal {A}$ in this symbolic game essentially depends on the equality queries that are performed on all Laurent polynomials computed by $\mathcal {A}$ and stored by the challenger. A key observation is that the completion $\mathcal {C}({\varvec{L}})$ can be seen as the generating set of a vector space V that describes all the Laurent polynomials computable by the adversary starting from the polynomials in ${\varvec{L}}$. So every Laurent polynomial $v \in V$ can be expressed as a linear combination of Laurent polynomials in $\mathcal {C}({\varvec{L}})_t$ (i.e., $v = {\varvec{\lambda }} \cdot \mathcal {C}({\varvec{L}})_t$ for some ${\varvec{\lambda }}$) and $\{ {{\varvec{a}}} \in {\mathbb {F}}_p^r \mid {{\varvec{a}}} \cdot \mathcal {C}({\varvec{L}})_t = 0 \}$ is the kernel of this linear map. Note that by our assumption that each $L_i$ contains the unit element, $\mathcal {C}({\varvec{L}})_t$ contains all the Laurent polynomials in $\mathcal {C}({\varvec{L}})_i$ for any i and similarly for $\mathcal {C}({\varvec{L}}')_t$ and $\mathcal {C}({\varvec{L}}')_i$. Therefore, all possible non-trivial relations in the generators of V are reflected in the completions of the target groups. Hence, the validity of our side condition essentially says that the equalities seen by the adversary in both games (i.e., w.r.t. lists ${\varvec{L}}$ and ${\varvec{L}}'$) are the same. Namely, the adversary gets an identical view in the two experiments.

To see this, let us suppose by contradiction that there exist an adversary that distinguishes the two symbolic game executions. We will show that this implies the side condition must be false.

Since the only difference in the adversary’s view can be a different outcome of equality queries, consider the case where the adversary has two handles $h_1, h_2$ that point to Laurent polynomials $f_1, f_2$ in the left game (i.e., with list ${\varvec{L}}$) and $f'_1, f'_2$ in the right game (i.e., with list ${\varvec{L}}'$), and assume that the equality query has a different outcome, namely $\textsf {eq}_{i}(h_1,h_2)=1$ in the left game, i.e., $f_1 = f_2$ and $\textsf {eq}_{i}(h_1,h_2)=0$ in the right game, i.e., $f'_1 \ne f'_2$. In both experiments, the polynomial $f_l$ and $f'_l$ can be expressed using the same linear combination of elements in their respective completion, i.e., for $l=1,2$, we have $f_{l} = {\varvec{\lambda }}_l \cdot \mathcal {C}({\varvec{L}})_t$ whereas $f'_{l} = {\varvec{\lambda }}_l \cdot \mathcal {C}({\varvec{L}}')_t$. However, this means that $({\varvec{\lambda }}_1 - {\varvec{\lambda }}_2) \cdot \mathcal {C}({\varvec{L}})_t = 0$, whereas $({\varvec{\lambda }}_1 - {\varvec{\lambda }}_2) \cdot \mathcal {C}({\varvec{L}}')_t \ne 0$, which contradicts the side condition. $\square$

Note that deciding the side condition is sufficient for deciding the hardness of the corresponding decisional problem for a fixed group setting and fixed distributions. Either the side condition is satisfied or there exists an ${{\varvec{a}}} \in {\mathbb {F}}_p^r$ that is included in one of the sets, but not in the other one. In the first case, the distinguishing advantage is upper-bounded by the $\epsilon$ given above. In the second case, we can construct an adversary that distinguishes the two symbolic models with probability 1, which implies that it distinguishes the corresponding generic models with probability $1 - \epsilon$. Note that for real-or-random assumptions where the adversary is given ${\hat{{\varvec{L}}}}$ and must distinguish f from a fresh variable Z in the target group $\mathbb {G}_t$, our side condition simplifies to $\sum _{j=1}^r a_j \mathcal {C}({\hat{{\varvec{L}}}})_{t}[j] \ne f$ for all ${{\varvec{a}}} \in {\mathbb {F}}_p^r$. This is similar to the independence condition in the BBG master theorem [14].

4 Automated Analysis of Non-interactive Assumptions

In this section, we present methods for automatically verifying or falsifying the hardness of decisional assumptions. As mentioned earlier, our master theorem is stated with respect to a fixed group setting and fixed distributions. To consider multiple group settings or distributions at once, we define a decisional assumption $\mathbb {A}$ as a possibly infinite set of triples $({\mathcal {G}}{\mathcal {S}}, \mathcal {D}_{{\varvec{L}}}, \mathcal {D}_{{\varvec{L}}'})$. $\mathbb {A}$ is generically hard if the distinguishing probability is upper-bounded by $\epsilon$ in Theorem 2 for all triples in $\mathbb {A}$.

We distinguish between nonparametric assumptions and parametric assumptions. An assumption is nonparametric if only the concrete groups, isomorphisms, and n-linear maps vary, but the structure of the group setting and the lists ${\varvec{L}}$ and ${\varvec{L}}'$ defining the distributions remain fixed. This captures assumptions such as “3-lin is generically hard in groups with a symmetric 3-linear map.” Conversely, an assumption is parametric if one or more of these restrictions do not hold.

4.1 Nonparametric Assumptions

We perform the following computations over $\mathbb {Z}$ to decide the hardness of a decisional assumption defined by lists ${\varvec{L}}$ and ${\varvec{L}}'$ for all group settings ${\mathcal {G}}{\mathcal {S}}$ with a given index set and types of isomorphisms and n-linear maps.

• 1. Initialize the set T of distinguishing tests and the set E of exceptional primes to the empty set $\emptyset$.

• 2. Compute the completions $\mathcal {C}({\varvec{L}})$ and $\mathcal {C}({\varvec{L}}')$ and set ${\overline{L}}_t:= \mathcal {C}({\varvec{L}})_t$, $\overline{L'}_t:= \mathcal {C}({\varvec{L}}')_t$ where t is the index of the target group.

• 3. Compute a generating set K of the $\mathbb {Z}$-module $\{ {{\varvec{a}}} \in \mathbb {Z}^{|{\overline{L}}_t|} \mid {{\varvec{a}}} \cdot {\overline{L}}_t= 0\}$ as follows:

  • (a) Represent all Laurent polynomials $g \in {\overline{L}}_t$ as vectors ${{\varvec{v}}}_{{{\varvec{1}}}},\ldots , {{\varvec{v}}}_{{{\varvec{n}}}}$ and denote by M the matrix, where row i is ${{\varvec{v}}}_{{{\varvec{i}}}}$ with respect to the basis $\textit{monomials}({\overline{L}}_t)$.

  • (b) Compute the Hermite Normal Form [20] N of M and read off a generating set K of the left kernel from N and the transformation matrix. Set $E := E\cup F$ where F is the set of integer factors of pivots of N.

  Perform the same steps for $\overline{L'}_t$ to obtain $M'$ and $K'$.

• 4. Check for every ${\varvec{k}} \in K$ if ${\varvec{k}} M' = {{\varvec{0}}}$. If ${\varvec{k}} M' = {{{\varvec{c}}}} \ne 0$, then set $T := T \cup {\varvec{k}}$ and $E := E \cup F$ where F denotes the set of integer factors that are in common among the entries of ${{{\varvec{c}}}}$. Perform the same steps for $K'$ and M.

• 5. Compute distinguishing probability $\epsilon$ from degrees in ${\overline{L}}_t$ and ${\overline{L}}_t'$.

• 6. If T is empty, return that distinguishing probability is upper-bounded by $\epsilon$ except (possibly) for primes in E. If T is nonempty, return that using the tests in T, an adversary can distinguish with probability $1 - \epsilon$ except (possibly) for primes in E.

Note that performing division-free computations over $\mathbb {Z}$ allows us to track the set of exceptional primes, which we return. We have implemented this algorithm in a tool that takes a group setting and two sequences of group elements as input and decides if the corresponding decisional assumption is hard returning $\epsilon$, E, and the distinguishing tests T (if nonempty).

Example 4

We show that the following assumption is insecure in a bilinear group using our method. This is just a slight modification of DDH where not all inputs are monomials, since it better highlights how the algorithm works. Let ${\varvec{L}}=[[1,X,Y,XY+Y],[]]$ and ${\varvec{L}}'=[[1,X,Y,Z],[]]$. Using the notation above, we have that

$$\begin{aligned} \begin{array}{ccllllllllll} {\overline{L}}_2 &{} = &{} [1, &{} X, &{} Y, &{} XY+Y, &{} X^2, &{} XY, &{} X^2Y+XY, &{} Y^2, &{} XY^2+Y^2, &{} X^2Y^2+2XY^2+Y^2]\\ {\overline{L}}'_2 &{} = &{} [1, &{} X, &{} Y, &{} Z, &{} X^2, &{} XY, &{} XZ, &{} Y^2,&{} YZ, &{} Z^2] \end{array} \end{aligned}$$

To compute the left kernels, we choose the following monomial bases:

$$\begin{aligned} \mathbb {B}&= (1,X,Y,XY,X^2,Y^2,XY^2,X^2Y^2)\\ \mathbb {B}'&= (1,X,Y,Z,X^2,XY,XZ,Y^2,YZ,Z^2) \end{aligned}$$

We obtain the matrices

$$\begin{aligned} M = \left[ \begin{array}{ccccccccc} 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 \\ 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 1 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 1 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 2 &{}\quad 1 \\ \end{array} \right] ,\quad M'= \left[ \begin{array}{cccccccccc} 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 \\ \end{array} \right] \end{aligned}$$

$M'$ is the identity matrix, so it is already in HNF and has trivial kernel. The HNF for M and its transformation matrix K are

$$\begin{aligned} N= \left[ \begin{array}{ccccccccc} 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0\\ 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0\\ 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0\\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0\\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0\\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0\\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0\\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0\\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1\\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \end{array} \right] ,\quad K= \left[ \begin{array}{cccccccccc} 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad -1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad -1 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad -1 &{}\quad 1 &{}\quad 0 \\ 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 1 &{}\quad -2 &{}\quad 1 \\ 0 &{}\quad 0 &{}\quad 1 &{}\quad -1 &{}\quad 0 &{}\quad 1 &{}\quad 0 &{}\quad 0 &{}\quad 0 &{}\quad 0 \end{array} \right] \end{aligned}$$

The generators of the kernel are the rows of the matrix K corresponding to the zero rows of the HNF, N, of M. All the pivots of N are 1, so there are no exceptional primes. Thus, the kernel is generated by ${{\varvec{a}}} = (0,0,1,-1,0,1,0,0,0,0)$ and ${{\varvec{a}}}$ denotes the relation $L_1[3]-L_1[4]+e(L_1[2],L_1[3])=0$. We also have that ${{\varvec{a}}}M' = {{\varvec{a}}}\ne {\varvec{0}}$, so this relation is not present in ${\overline{L}}_2'$. Furthermore, ${{\varvec{a}}}$ is not zero modulo any prime, so there are no exceptional primes. In addition to what is shown here, our software keeps track of how each element of ${\overline{L}}_2$ was constructed, so it can print out the formulas for all algebraic attacks against the assumption.

4.2 Parametric Assumptions

For parametric decisional assumptions, we restrict ourselves to the real-or-random case and to polynomials instead of Laurent polynomials. The approach can also be adapted to handle computational assumptions. We distinguish parametricity in two dimensions. First, an assumption may be parameterized by range limits$l_1, \ldots , l_m$ (ranging over $\mathbb {N}$) that determine the size of the adversary input. To express such assumptions, we use range expressions$\forall r_1 \in [\alpha _1,\beta _1], \ldots r_t \in [\alpha _t,\beta _t]\cdot h_{r_1,\ldots ,r_t}$, where all $\alpha _i$ and $\beta _i$ are polynomials over range limits, and polynomials $h_{r_1,\ldots ,r_t}$ can use the range indices$r_i$ in the exponent.

We will denote range expressions with capital letter R.

Example 5

To better understand the use of range expressions, consider the case of the l-DHE assumption in a group (without bilinear maps). The input is $(g, g^{x}, \ldots , g^{x^{l}}, g^{x^{l+2}}, \ldots , g^{x^{2l}})$ and the problem is to distinguish $g^{x^{l+1}}$ from a random group element. Symbolically, the problem is defined by range limit l, and by the following range expressions $M_1, M_2$ and challenge polynomial f:

$$\begin{aligned} M_1=\forall i\in [0,l]\cdot X^i,\quad M_2=\forall j\in [0,l-2]\cdot X^{l+2+j},\quad f=X^{l+1}. \end{aligned}$$

Second, the group setting of an assumption may be parameterized by an arityk for the k-linear maps: this captures the maximum number of multiplications that can be performed, and it allows us to consider the case of leveled k-linear groups.

Parametricity in the input size allows us to analyze assumptions such as “l-DHE is hard for all l.” Parametricity in the arity allows us to analyze assumptions such as “2-BDH is hard for all k-linear groups.” Combining both types of parametricity allows us to analyze assumptions such as “k-lin is hard in k-linear groups” or “(l, k)-MMDHE is hard for all l and $k\ge 3$.”

The way we handle parametric assumptions is based on a trivial observation. Let $S_1,\ldots ,S_n$ be not necessarily distinct sets of monomials and $T_i$ be the free $\mathbb {Z}$-module generated by $S_i$. Then a polynomial f belongs to the free $\mathbb {Z}$-module generated by $T_1\cdots T_n$ if and only if all its terms belong to $S_1\cdots S_n$ up to multiplication by a constant in $\mathbb {Z}$. Therefore, we need to define products of range expressions as well as methods to check whether a monomial is an instance of a range expression. Additionally, we must assume that all inputs are monomials.

We assume a real-or-random decisional assumption in a (leveled) k-linear group where the challenge polynomial g is in the target group, and the adversary input is expressed using range expressions $R_1, \ldots , R_n$ on the levels $\lambda _1, \ldots , \lambda _n$. Here $\lambda _i$ is either of the form c or of the form $k - c$ for a constant $c \in \mathbb {N}$. Furthermore, we assume that the assumption uses random variables ${{\varvec{X}}}$ and range limits ${\varvec{l}}$. To simplify the presentation, we will use the notation ${{\varvec{X}}}^{{\varvec{f}}} = X_1^{f_1}\cdots X_m^{f_m}$. Then the ranges are of the form

$$\begin{aligned} R_i = \forall r_{i,1}\in [\alpha _{i,1},\beta _{i,1}],\ldots ,r_{i,t_i}\in [\alpha _{i,t_i},\beta _{i,t_i}]\cdot {{\varvec{X}}}^{{{\varvec{f}}}_{{{\varvec{i}}}}} \\ \end{aligned}$$

where every $\alpha _{i,j}$ and $\beta _{i,j}$ is a polynomial over ${\varvec{l}}$ and every $f \in {\varvec{f}}_i$ is a polynomial over k, ${\varvec{l}}$, and $r_{i,1}, \ldots , r_{i,t_i}$. The challenge polynomial is of the form $g = \sum _{i=1}^w c_i {{\varvec{X}}}^{{{\varvec{u}}}_{{\varvec{i}}}}$. Using the independence condition derived from Theorem 2, it follows that real distribution and the random distribution are indistinguishable iff there is a monomial ${{\varvec{X}}}^{{{{\varvec{u}}}_{{\varvec{i}}}}}$ that is not an element of the completion of the $R_i$.

To check this condition, we proceed in two steps. In the first step, we compute a single range expression ${\overline{R}}$ that denotes the completion of the $R_i$ in the target group. In the second step, we check for each ${{\varvec{X}}}^{{{{\varvec{u}}}_{{\varvec{i}}}}}$ whether ${{\varvec{X}}}^{{{{\varvec{u}}}_{{\varvec{i}}}}} \in {\overline{R}}$, by encoding the required equalities of the exponent-polynomials into a set of diophantine (in)equalities. We then show that satisfiability checking for such constraints is undecidable in general. Nevertheless, we identify two decidable fragments and demonstrate that SMT solvers can handle most instances derived from practical cryptographic assumptions, even those that are not in the decidable fragments.

If the range expressions $R_1, \ldots , R_n$ denote the sets $S_1, \ldots , S_n$, then the completion ${\overline{R}}$ of $R_1, \ldots , R_n$ in the target group must denote the set

$$\begin{aligned} \bigcup _{{{\varvec{\delta }}} \in \mathbb {N}^n \text { s.t. } \sum _{i=1}^n \delta _i \cdot \lambda _i = k} S_1^{\delta _1} \cdots S_n^{\delta _n} \end{aligned}$$

where $S S' = \{ s s' \mid s \in S, s' \in S' \}$ and $S^{\delta } = \{ \prod _{i=1}^{\delta } s_i | s_1 \in S, \ldots , s_{\delta } \in S\}$. We therefore define multiplication of range expressions with distinct range indices as

$$\begin{aligned}&\left( \forall r_1 \in [\alpha _{1},\beta _{1}],\ldots , r_t \in [\alpha _{t},\beta _{t}]\cdot {{\varvec{X}}}^{{\varvec{f}}}\right) \left( \forall r_1'\in \left[ \alpha '_1,\beta _1'\right] ,\ldots ,r_s'\in \left[ \alpha '_{t'},\beta _{t'}'\right] \cdot {{\varvec{X}}}^{{\varvec{f}}'}\right) \\&\quad = \forall r_1\in [\alpha _{1},\beta _{1}],\ldots ,r_t\in [\alpha _{t},\beta _{t}], r_1'\in \left[ \alpha '_1,\beta _1'\right] ,\ldots ,r_s'\in \left[ \alpha '_{t'},\beta '_{t'}\right] \cdot {{\varvec{X}}}^{{\varvec{f}} + {\varvec{f}}'}. \end{aligned}$$

To define the $\delta$-fold product of a range expression, we restrict ourselves to exponent-polynomials that can be expressed as linear polynomials in range indices, i.e., exponents that can be expressed as $f + g$ such that g is a polynomial in $\mathbb {Z}[{\varvec{l}},k]$ and $f = \sum _{j=1}^{t} r_{j} \,\phi _j({\varvec{l}},k)$ for polynomials $\phi _j$ in $\mathbb {Z}[{\varvec{l}},k]$. The $\delta$-fold product is then defined as

$$\begin{aligned}&\left( \forall r_1\in \left[ \alpha _1,\beta _1\right] ,\ldots ,r_m\in \left[ \alpha _t,\beta _t\right] \cdot {{\varvec{X}}}^{{\varvec{f}}+{\varvec{g}}}\right) ^\delta \\&\quad = \forall r_1\in \left[ \delta \alpha _1,\delta \beta _1\right] ,\ldots ,r_m\in \left[ \delta \alpha _t,\delta \beta _t\right] \cdot {{\varvec{X}}}^{{\varvec{f}}+\delta {\varvec{g}}}. \end{aligned}$$

Given range expressions $R_1, \ldots , R_n$, we can now compute ${\overline{R}}$ by introducing fresh variables $\delta _1, \ldots , \delta _n$, computing the range expressions $R_i^{\delta _i}$, and then computing the product of these range expressions.

The remaining task is now to check if

$$\begin{aligned} {{\varvec{X}}}^{{\varvec{u}}} \in \left( \forall r_{1}\in \left[ \alpha _{1},\beta _{1}\right] ,\ldots ,r_{t}\in \left[ \alpha _{t},\beta _{t}\right] \cdot {{\varvec{X}}}^{{\varvec{f}}}\right) = {\overline{R}} \end{aligned}$$

where ${\varvec{u}} \in \mathbb {Z}[{\varvec{l}},k]^m$, $\alpha _i,\beta _i \in \mathbb {Z}[{{\varvec{\delta }}}, {\varvec{l}}]$, ${\varvec{f}} \in \mathbb {Z}[{\varvec{l}},k,r_1,\ldots ,r_t]^m$, and $\hbox { }\ \sum _{i=1}^n \delta _i \cdot \lambda _i = k$. To achieve this, we compute the following set of integer constraints that is satisfiable iff ${{\varvec{X}}}^{{\varvec{u}}} \in {\overline{R}}$:

$$\begin{aligned} \left\{ \begin{array}{ll} 0\le \delta _i &{} \quad \text { for } i \in [1,n] \\ \alpha _i \le r_i \le \beta _i &{}\quad \text { for } i \in [1,t] \\ u_i = f_i, &{}\quad \text { for } i \in [1,m] \\ \sum _{i=1}^n \delta _i\lambda _i = k &{} \end{array} \right. \end{aligned}$$

If we allow for both types of parametricity, it is possible to reduce Hilbert’s 10th problem to the generic hardness of cryptographic assumptions expressed as previously described. This yields the following theorem.

Theorem 3

The problem of establishing the hardness of parametric assumptions in the generic group model is undecidable, even if all exponent-polynomials are linear in range limits, range indices, and the arity.

The proof of Theorem 3 can be found in “Appendix.” By introducing additional restrictions, we obtain a class of parametric assumptions for which the problem is decidable.

Theorem 4

For all parametric assumptions such that all exponent-polynomials $f_{i,j}$ and range bounds $\alpha _{i,j}$ and $\beta _{i,j}$ in the input are linear, and either (1) the arity k is fixed or (2) the assumption does not contain range limits $l_i$ and the input exponent-polynomials do not use k, establishing the hardness in the generic group model is decidable.

Proof

(Sketch) In both cases, we transform the constraint system into a system of linear constraints. Note that the first type of constraint is already linear. In the first case, the arity k is fixed and we can eliminate the variables $\delta _i$ by performing a case distinction since there are only finitely many possible values. Then, the constraints of the first and fourth type are constant and the constraints of the second and third type are linear. If there are no range limits, then the range bounds are constants and we can eliminate the range indices by expanding all range expressions into finite sets of monomials. Then the constraints of the second type are constant and we can linearize the constraints of the last type using Proposition 1. For constraints of the third type, every $u_i$ is a linear polynomial in $\mathbb {Z}[k]$ and every $f_i$ is a linear polynomial in $\mathbb {Z}[{{\varvec{\delta }}},k]$. $\square$

Proposition 1

The equation $\sum _{i=1}^t \delta _i\lambda _i = k$ can always be split into a finite number of cases, where the remaining equation is linear.

Proof

The variables $\lambda _i$ are by definition either of the form $c_i$ or $k-c_i$, where $c_i$ is a constant. In the former case $\delta _ic_i$ is a first-degree term. In the latter case, $\delta _i(k-c_i)$ is a degree two term. By arranging terms, we may write the equation in the form

$$\begin{aligned} \sum _{i=1}^r \delta _ic_i + \sum _{i=r+1}^t \delta _i(k-c_i) = k. \end{aligned}$$

Write $c = \max \{c_i\mid i=r+1,\ldots ,t\}$, so that

$$\begin{aligned} (k-c) \sum _{i=r+1}^t \delta _i = \sum _{i=r+1} \delta _i(k-c) \le \sum _{i=r+1}^t \delta _i(k-c_i) \le k \end{aligned}$$

and therefore

$$\begin{aligned} \sum _{i=r+1}^t \delta _i \le \frac{k}{k-c} \le \frac{c+1}{c+1-c}=c+1. \end{aligned}$$

This shows that there are a finite number of possible values for $\delta _{r+1},\ldots ,\delta _t$. This leads to at most ${c+t-r \atopwithdelims ()t-r-1}$ possible choices for $\delta _{r+1},\ldots ,\delta _t$. $\square$

We have implemented this method in our tool and use Z3 [21] to check the constraints. Our experiments confirm that Z3 can prove most assumptions taken from the literature, even those outside the decidable fragment.

Example 6

Consider the decisional l-BDHE [16] problem in a symmetric bilinear group with map $e:\mathbb {G}_0\times \mathbb {G}_0\rightarrow \mathbb {G}_1$. The inputs are $(h,g,g^x,g^{x^2},\ldots ,g^{x^l},g^{x^{l+2}},\ldots , g^{x^{2l}})$. Writing $h=g^y$, the problem is to distinguish $e(h,g)^{x^{l+1}}=e(g,g)^{yx^{l+1}}$ from a random group element. Symbolically, the problem is defined by the input

$$\begin{aligned}&M_1=1,\quad M_2=Y,\quad M_3=\forall i\in [0,l]\cdot X^i,\quad M_4=\forall j\in [0,l-2]\cdot X^{l+2+j},\\&g=YX^{l+1}, \end{aligned}$$

where the $M_i$ are all at level 1 with the challenge at level 2. Therefore, we compute

$$\begin{aligned} M_1^{\delta _1}&= 1\\ M_2^{\delta _2}&= Y^{\delta _2}\\ M_3^{\delta _3}&= \forall i\in [0,\delta _3 l]\cdot X^i\\ M_4^{\delta _4}&= \forall j\in [0,\delta _4(l-2)]\cdot X^{j+\delta _4(l+2)}\\ M_1^{\delta _1} M_2^{\delta _2} M_3^{\delta _3} M_4^{\delta _4}&= \forall i\in [0,\delta _3 l],\, j\in [0,\delta _4(l-2)] \cdot X^{i+j+\delta _4(l+2)}Y^{\delta _2} \end{aligned}$$

This yields the following set of constraints

$$\begin{aligned} \left\{ \begin{array}{l} 0\le \delta _1,\delta _2,\delta _3,\delta _4\\ 0\le i \le \delta _3 l\\ 0\le j \le \delta _4(l-2)\\ l+1 = i+j+\delta _4(l+2)\\ 1 = \delta _2\\ \delta _1+\delta _2+\delta _3+\delta _4 = 2 \end{array} \right. . \end{aligned}$$

The fourth (resp. fifth) equation corresponds to taking the degrees of both sides of the equation $YX^{l+1} = M_1^{\delta _1} M_2^{\delta _2} M_3^{\delta _3} M_4^{\delta _4}$ with respect to X (resp. Y). In this case, the system trivially linearizes, since there are only finitely many possible values for the $\delta _i$, $i=1,\ldots ,4$.

5 Interactive Assumptions

In this section, we present our methods for the analysis of interactive assumptions such as LRSW [36]. We focus on assumptions where exactly one additional oracle $\mathcal {O}$ is provided to the adversary, and the problem is a generalized extraction problem. In the remainder, we fix a group setting ${\mathcal {G}}{\mathcal {S}}=(p,\{\mathbb {G}\}_{i \in \mathcal {I}},\varPhi ,\mathcal {E})$ and a distribution $\mathcal {D}_{{\varvec{L}}}$. We use ${{\varvec{X}}}$ to denote the variables occurring in ${\varvec{L}}$ and ${\varvec{x}}$ to denote the point sampled by $\mathcal {D}_{{\varvec{L}}}$.

5.1 Master Theorem for Interactive Assumption

Our first step is to generalize the generic group and symbolic group models to the interactive setting. In order to do this, we need to give precise definitions of our oracles that we can mathematically work with. We first note that an oracle operates as follows:

• 1. It takes as input parameters elements in ${\mathbb {F}}_p$ and handles to group elements.

• 2. It returns handles to group elements that are computed from the input parameters, values randomly sampled by $\mathcal {D}_{{\varvec{L}}}$ and elements in ${\mathbb {F}}_p$ randomly sampled by the oracle.

In the symbolic model, the oracle has the same interface, except that instead of internally sampling a new value, it creates a new formal variable. Instead of handles to group elements, it returns handles to formal Laurent polynomials in the ring augmented with the new formal variables.

Formally an oracle is therefore given as follows.

Definition 3

An oracle is a tuple $\mathcal {O}=(q', n, m, {\varvec{w}}, {\varvec{F}}, {\varvec{v}})$, where the different parts are defined as follows:

• $q'$ is the number of oracle queries allowed,

• n is the number of variables $A_1,\ldots ,A_n$ in ${\mathbb {F}}_p$ taken as scalar input parameters,

• m is the number of values $Y_1,\ldots ,Y_m$ sampled in ${\mathbb {F}}_p$ by the oracle,

• ${\varvec{w}}$ is a vector of indices in $\mathcal {I}$ describing the handle input parameters $Z_i$ and the groups they belong to,

• ${\varvec{F}}$ is a vector of Laurent polynomials in ${\mathbb {F}}_p[{{\varvec{X}}},{{\varvec{X}}}^{-1},{{\varvec{A}}},{{\varvec{A}}}^{-1},{{\varvec{Y}}},{{\varvec{Y}}}^{-1},{\varvec{Z}},{\varvec{Z}}^{-1}]$ describing the oracle return values, and

• ${\varvec{v}}$ is a vector of indices in $\mathcal {I}$ describing the groups they belong to.

Assume that ${\varvec{F}}=(F_1,\ldots ,F_n)$ and ${\varvec{v}}=(i_1,\ldots ,i_n)$ and a query is made with scalar parameters ${{\varvec{a}}}$ and handle parameters ${\varvec{z}}$. Denote by ${\varvec{x}}$ the discrete logarithms of the elements of ${{\varvec{X}}}$ with respect to their respective group generator. Similarly, we set ${\varvec{z}}' = ({ d }{\mathrm {log}}(L_{w_1}[z_1]),\ldots ,{ d }{\mathrm {log}}(L_{w_r}[z_r]))$, where the discrete logarithm of $L_{w_i}[z_i]$ is taken with respect to the generator $P_{w_i}$. In the generic group model, the oracle appends $F_j({\varvec{x}}, {{\varvec{a}}},{\varvec{y}},{\varvec{z}}')P_{i_j}$ to $L_{i_j}$ and returns handles for $j \in [n]$. In the symbolic model, instead of sampling values for the $Y_i$, the oracle creates fresh new variables $Y_i'$ for each $Y_i$. Writing ${{\varvec{Y}}}'=(Y_1',\ldots ,Y_m')$ and ${\varvec{Z}}' = (L_{w_1}[z_1],\ldots ,L_{w_r}[z_r])$ the oracle appends the Laurent polynomial $F_j({{\varvec{X}}},{{\varvec{a}}},{{\varvec{Y}}}',{\varvec{Z}}')$ to $L_{i_j}$ and returns handles for $j \in [n]$. Note that in many cases, it is useful to consider only oracles defined such that the oracle return value can be computed by using suitable pairings instead of taking discrete logarithms.

Since Theorem 1 captures generalized extraction problems and can be generalized to oracle queries, we can analyze such assumptions in the symbolic group model as before. As mentioned earlier, the symbolic version of the winning event can be obtained by plugging in the polynomials $L_{i_j}[h_j]$ for the variables $Z_j$ instead of using the discrete logarithm.

5.1.1 Interactive Master Theorem

To define the interactive master theorem, we introduce the notion of parametric completion. The parametric completion of ${\varvec{L}}$ with respect to a group setting ${\mathcal {G}}{\mathcal {S}}$ and an oracle $\mathcal {O}$ defined by $(q', n, m, {\varvec{w}}, {\varvec{F}}, {\varvec{v}})$ is a family $L_i$ of lists of Laurent polynomials defined as follows. Assume that in the oracle definition, ${\varvec{F}}$ consists of Laurent polynomials in

$$\begin{aligned} {\mathbb {F}}_p\left[ {{\varvec{X}}},{{\varvec{X}}}^{-1},{{\varvec{A}}},{{\varvec{A}}}^{-1},{{\varvec{Y}}},{{\varvec{Y}}}^{-1},{\varvec{Z}},{\varvec{Z}}^{-1}\right] \end{aligned}$$

and define the sets of variables

$$\begin{aligned} \mathcal {A}= \{A_{i,j}\}_{i\in [n],j\in [q']} \text { and } \mathcal {Y}= \{Y_{i,j}\}_{i\in [m], j\in [q']}. \end{aligned}$$

The parametric completion then consists of lists of Laurent polynomials in

$$\begin{aligned} {\mathbb {F}}_p\left[ {{\varvec{X}}},{{\varvec{X}}}^{-1},\mathcal {A},\mathcal {A}^{-1},\mathcal {Y},\mathcal {Y}^{-1},\mathcal {C}\right] \end{aligned}$$

according to the algorithm described in Fig. 3. The variables $\mathcal {C}$ are fresh variables created during the completion calculation, which represent the handle parameters chosen by the adversary. Their meaning becomes apparent in the following example.

Fig. 3

Parametric completion w.r.t. an oracle

Example 7

Assume that our group setting contains the single group $\mathbb {G}$ and an oracle that on input $z_1\in \mathbb {G}$ returns $z_1^2$. Further assume that the adversary input consists of the generator $P$ and the group element $x_1\,P$ for a randomly sampled $x_1 \in {\mathbb {F}}_p$. The oracle would be defined by the single polynomial $F_1(X_1,Z_1)=Z_1^2$ and the input distribution would be defined by the list $L_1=[1,X_1]$ of polynomials. There is only one input list with no isomorphism or pairing, so the standard completion does not add any elements. On the first query, we have $|L_1| = 2$, so we get

$$\begin{aligned} Z_1' = C_{1,1,1}1 + C_{1,1,2}X_1 \end{aligned}$$

and

$$\begin{aligned} F_1' = \left( C_{1,1,1}1 + C_{1,1,2}X_1\right) ^2. \end{aligned}$$

This implies that after one query $L_1 = [1,X_1,(C_{1,1,1}1 + C_{1,1,2}X_1)^2]$. Since the values of the $C_{\cdot ,\cdot ,\cdot }$ are chosen by the adversary, we see that anything computable by the adversary is a linear combination of the elements of L under some choices of the values of the $C_{\cdot ,\cdot ,\cdot }$. This can trivially be proven by induction. Given one more query, we would have

$$\begin{aligned} L_1 = \left[ 1,X_1,\left( C_{1,1,1}1 + C_{1,1,2}X_1\right) ^2, \left( C_{1,2,1} + C_{1,2,2}X_1 + C_{1,2,3}\left( C_{1,1,1}1 + C_{1,1,2}X_1\right) ^2\right) ^2\right] . \end{aligned}$$

This also shows that given an oracle that takes group handle parameters, we can typically only handle problems for small numbers of oracle queries due to a combinatorial explosion in the number of constraints that our solver extracts from the problem. The number of constraints depends on the number of terms in the expanded expressions in $L_1$.

To state our interactive master theorem, we exploit that in the symbolic model, we can translate a generalized extraction problem to an equivalent generalized extraction problem where the adversary returns only elements in ${\mathbb {F}}_p$ and no handles. This is simply, because the setting is completely deterministic and because the adversary can return a handle to a polynomial element if and only if the polynomial is in the span of the completion. Therefore, instead of returning the handle to the polynomial, the adversary can return the coefficients in the linear combination that constructs the polynomials from the completion and we can modify the winning condition accordingly. More precisely, let $\mathcal {C}^{\mathcal {O}}({\varvec{L}}) = {\overline{L}}_{i_1},\ldots ,{\overline{L}}_{i_l}$ denote the lists in the parametric completion. Assume now that the winning condition in the generalized extraction problem has a polynomial of the form

$$\begin{aligned} H\left( {{\varvec{X}}},\mathcal {Y},{{\varvec{B}}},h_1,\ldots ,h_n\right) , \end{aligned}$$

where $h_j$ is a handle to some element in $L_{i_j}$. We replace H in the winning condition by

$$\begin{aligned} H'\left( {{\varvec{X}}},\mathcal {Y},{{\varvec{B}}},{{\varvec{\alpha }}}_1,\ldots ,{{\varvec{\alpha }}}_n\right) = H\left( {{\varvec{X}}},\mathcal {Y},{{\varvec{B}}},{{\varvec{\alpha }}}_1\cdot {\overline{L}}_{i_1},\ldots ,{{\varvec{\alpha }}}_n\cdot {\overline{L}}_{i_n}\right) , \end{aligned}$$

i.e., a handle to a polynomial is replaced by requiring the actual linear combination that computes it from the completion. Renaming variables, we can therefore assume in the symbolic case that the polynomials in the generalized extraction problem are of the form

$$\begin{aligned} H\left( {{\varvec{X}}},\mathcal {Y},{{\varvec{B}}}\right) . \end{aligned}$$

Finally, we note that an attack strategy in the symbolic model is given with respect to the sampled variables ${{\varvec{X}}}$ and $\mathcal {Y}$ that are treated as formal variables. Any attack in the symbolic model requires a sequence of oracle queries, which is represented by instantiating $\mathcal {A}$ and $\mathcal {C}$ with some concrete values chosen by the adversary. We can encode the strategy directly in the polynomials in the generalized extraction problem by writing polynomials in the form

$$\begin{aligned} H({{\varvec{X}}},\mathcal {Y},{{\varvec{B}}},\mathcal {A},\mathcal {C}), \end{aligned}$$

i.e., we plug $\mathcal {A}$ and $\mathcal {C}$ into the parametric completion before plugging in for ${{\varvec{X}}}$, $\mathcal {Y}$ and ${{\varvec{B}}}$.

Theorem 5

Let ${\mathcal {G}}{\mathcal {S}}$ denote a group setting and let $\mathcal {D}_{{\varvec{L}}}$ denote a polynomially induced distribution. Consider the $({\hat{n}},{\hat{m}},{\varvec{j}},{\varvec{H}},{\varvec{G}})$-extraction problem in the generic and symbolic group models for ${\mathcal {G}}{\mathcal {S}}$, $\mathcal {D}_{{\varvec{L}}}$, and the oracle defined by $(q', n, m, {\varvec{w}}, {\varvec{F}}, {\varvec{v}})$. Let ${\varvec{H}}'$ and ${\varvec{G}}'$ denote the translations of ${\varvec{H}}$ and ${\varvec{G}}$ with respect to this model that do not use handles. Then the problem is symbolically hard if there are no vectors ${{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}}$ over ${\mathbb {F}}_p$ satisfying

$$\begin{aligned} \left( \bigwedge \nolimits _{j=1}^{|{\varvec{H}}'|} H'_j\left( {{\varvec{X}}}, \mathcal {Y}, {{\varvec{b}}},{{\varvec{a}}},{{\varvec{c}}}\right) = 0 \right) \wedge \left( \bigwedge \nolimits _{j=1}^{|{\varvec{G}}'|} G'_j\left( {{\varvec{X}}}, \mathcal {Y}, {{\varvec{b}}},{{\varvec{a}}},{{\varvec{c}}}\right) \ne 0 \right) \text {.} \end{aligned}$$

In this case, the winning probability for the generic version is upper-bounded by

$$\begin{aligned} \left( \frac{(s + q + q' l)^2}{2} + e \right) \frac{d}{p - 1}, \end{aligned}$$

where p is the group order, $l = |{\varvec{F}}|$ is the number of oracle return values, s is the sum of the sizes of the lists in ${\varvec{L}}$, q the number of queries to the group operation oracles, $q'$ the number of queries to $\mathcal {O}$ and $e = |{\varvec{H}}'| + |{\varvec{G}}'|$. Finally, d is an upper bound on the degree of the numerators (in ${{\varvec{X}}}$ and ${{\varvec{Y}}}$) for all Laurent polynomials stored by the corresponding symbolic model and occurring in ${\varvec{H}}'$ and ${\varvec{G}}'$ when the polynomials are written with respect to a common denominator of minimal degree.

Proof

We use Theorem 1 to switch to the symbolic model which is equivalent up to the $\epsilon$-bound stated in the theorem. Here, we take into account that each of the $q'$ oracle calls adds l group elements to the lists and that the winning condition contains $e=|{\varvec{H}}| + |{\varvec{G}}|$ equality checks. Then, we show that if the side-condition is false, then there exists a symbolic adversary that wins with probability one. If the side condition is true, then the winning probability in the symbolic model is always zero. To see why this is the case, first observe that an adversary that wins must query $\mathcal {O}$ with parameters ${{{\varvec{a}}}}_\mathbf{1},\ldots ,{{{\varvec{a}}}}_{{{\varvec{q}}'}}$ and return ${{\varvec{b}}}$ and ${\varvec{h}}$ such that the equalities H and the inequalities G are satisfied. As mentioned in Sect. 5, we can get an equivalent characterization of the winning condition using “handle-free” polynomials $H'$ and $G'$. For such polynomials, the side condition of the theorem exactly mirrors the winning condition. $\square$

5.2 Automated Analysis

We have developed two methods for the automated analysis of interactive assumptions. Our first method deals with the bounded case, i.e., where the maximum number of oracle queries $q'$ is fixed. In addition to giving the possibility of analyzing interactive assumptions in scenarios where the adversary is known to perform a given limited number queries, there are two more applications of particular use. The first one is to find attacks based on some constant number of queries, which is useful to test assumptions, as we do, e.g., for m-LRSW assumption [10] with 2 oracle queries. The second application is that reductions between computational assumptions, such as CDH and Square-CDH, can also be phrased as an interactive assumption, therefore allowing explicit reductions to be found automatically by the tool.⁵ Our second method can instead deal with the more general case where the number of queries performed by the adversary is not a priori bounded. This allows us to capture interactive assumptions such as LRSW [36] for which one can argue validity for every (polynomial) number of queries. As a limitation, however, this second method can establish invalidity of an assumption but is not able to find an explicit attack.

5.2.1 Our Method for Bounded Number of Queries

We first describe our method for the bounded case, i.e., where the number of oracle queries $q'$ is fixed. Informally, we use Gröbner basis techniques and SMT solvers to prove that there is either (1) no solution for all primes, (2) no solution for all primes except for some bad primes, (3) a solution over the rationals which can be converted into an attack for almost all primes, or (4) a solution over $\mathbb {C}$. Even though we only encountered cases (1–3) in practice, case (4) is the reason for the incompleteness of our algorithm since the existence of a solution over $\mathbb {C}$ does not imply the existence of solutions over ${\mathbb {F}}_p$.

• 1. We translate a given assumption to a group setting ${\mathcal {G}}{\mathcal {S}}$, a list of polynomials ${\varvec{L}}$, an oracle description $(q', n, m, {\varvec{w}}, {\varvec{F}}, {\varvec{v}})$, and an extraction problem $({\hat{n}},{\hat{m}},\{i_1,\ldots ,i_m\},{\varvec{H}},{\varvec{G}})$.

• 2. We compute the parametric completion for a fixed $q'$ and translate the extraction polynomials ${\varvec{H}},{\varvec{G}}$ to obtain handle-free versions ${\varvec{H}}'$ and ${\varvec{G}}'$.

• 3. We extract the coefficients ${\varvec{f}}_i, {\varvec{g}}_j$ of the polynomials $H_i',G_j'$ represented as polynomials in $(\mathbb {Z}[{{\varvec{A}}},{{\varvec{B}}},{{\varvec{C}}}])[{{\varvec{X}}},{{\varvec{Y}}}]$. Writing ${\varvec{f}}_i=(f_{i,1},\ldots ,f_{i,n_i})$ and ${\varvec{g}}_j=(g_{j,1},\ldots ,g_{j,m_j})$, where $f_{i,s},g_{j,r}\in \mathbb {Z}[{{\varvec{A}}},{{\varvec{B}}},{{\varvec{C}}}]$, we note that the side condition of Theorem 5 is satisfied iff there are no points ${{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}}$ over ${\mathbb {F}}_p$ such that for all $i \in [|{\varvec{H}}'|]$, $s\in [n_i]$, $f_{i,s}({{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}})=0$, and for all $j \in [|{\varvec{G}}'|]$ there is some $s\in [m_j]$ such that $g_{j,s}({{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}})\ne 0$.

• 4. We use the Rabinowitch trick to transfer inequalities to equalities by defining for each $g_{j,s}({{\varvec{A}}},{{\varvec{B}}},{{\varvec{C}}})$ the polynomial ${\widetilde{g}}_{j,s}({{\varvec{A}}},{{\varvec{B}}},{{\varvec{C}}})D_{j,s}-1$ and set $\phi _j = {\widetilde{g}}_{j,1}\cdots {\widetilde{g}}_{j,m_j}$.

• 5. It is not hard to see that (over ${\mathbb {F}}_p$)

  $$\begin{aligned}&\left\{ ({{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}}) \mid \bigwedge _{i,s} f_{i,s}({{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}}) = 0 \wedge \bigwedge _j \bigvee _s g_{j,s}({{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}}) \ne 0\right\} \\&\quad = \left\{ ({{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}}) \mid \exists {\varvec{d}}. \bigwedge _{i,s} f_{i,s}\left( {{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}}\right) = 0 {}\wedge {} \bigwedge _j \phi _j\left( {{\varvec{a}}},{{\varvec{b}}},{{\varvec{c}}},d_{j,1},\ldots ,d_{j,m_j}\right) = 0\right\} . \end{aligned}$$

• 6. Let ${\mathcal {J}}$ be the ideal generated by the polynomials $f_{i,s}$ and $\phi _j$ over $\mathbb {Z}$. We compute a Gröbner basis I of the ideal ${\mathcal {J}}$. We can then conclude as follows (for all adversaries performing up to q queries):

  • (a) If $I=(1)$, i.e., the Gröbner basis of ${\mathcal {J}}$ contains 1, then return assumption is hard for all primes p. Indeed, by Hilbert’s Nullstellensatz, this means that the ideal ${\mathcal {J}}$ does not have any zero, and by the transformation of the previous steps, this is exactly the condition for the assumption to be hard (by Theorem 5).

  • (b) If I contains a constant $n\ne 1$, then return assumption is hard except for B consisting of all primes that divide n.

  • (c) If I does not contain a constant, we know that there is a solution over the complex numbers. We then try to find a solution over the rationals using a combination of primary decomposition of ideals, linear algebra, and model finding using SMT solvers. If we find a solution, we return the solution which describes an attack that works for almost all primes p. If we do not find a solution, then we return “unknown.”

To summarize, our method is sound, i.e., whenever we return an attack or “hard except for B,” then this is a valid conclusion. It is incomplete because the existence of a solution over the complex numbers does not imply the existence of a solution over ${\mathbb {F}}_p$. On the other hand, no solution over $\mathbb {C}$ implies no solutions over ${\mathbb {F}}_p$ when p is large enough. This is a consequence of the compactness theorem of first-order logic in the form of Robinson’s principle [43].

5.2.2 Our Method for Unbounded Number of Queries

Our method for the unbounded case proceeds similarly to the bounded method. The main difference is that we use symbolic variants of the steps since the number of queries $q'$ is not fixed. More concretely, we encode the hardness of the assumption into a formula in the theory of nonlinear arithmetic over $\mathbb {C}$ with uninterpreted function symbols, which we use to encode parameters used in queries and returned by the adversary. We use Z3 to prove the unsatisfiability of these formulas exploiting the support for nonlinear arithmetic over the reals [33] by encoding complex numbers as pairs of reals. In our experiments, Z3 can prove the unsatisfiability of formulas obtained from most valid assumptions in seconds.

• 1. We translate a given assumption to a group setting ${\mathcal {G}}{\mathcal {S}}$, a list of polynomials ${\varvec{L}}$, an oracle description $(q',n,m,{\varvec{w}}, {\varvec{F}}, {\varvec{v}})$, and an extraction problem $({\hat{n}},{\hat{m}},{\varvec{j}},{\varvec{H}},{\varvec{G}})$.

• 2.1 We use ranges, indexed random variables, and indexed parameter variables to compute a symbolic parameterized completion. Concretely, instead of extending the lists $L_{i_j}$ with polynomials

  $$\begin{aligned} F_j({{\varvec{X}}},Y_{1,1},\ldots , Y_{m,1},A_{1,1},\ldots , A_{n,1}), \ldots , F_j({{\varvec{X}}},Y_{1,q'},\ldots , Y_{m,q'},A_{1,q'},\ldots , A_{n,q'}) \end{aligned}$$

  for $j \in [|{\varvec{F}}|]$, we extend the lists $L_{i_j}$ with the formal expressions

  $$\begin{aligned} \forall v \in [q']\cdot F_j({{\varvec{X}}},Y_{1,v},\ldots , Y_{m,v},A_{1,v},\ldots , A_{n,v}) \end{aligned}$$

  for $j \in [|{\varvec{F}}|]$ where $q'$ is a variable, and $Y_{1,v},\ldots ,Y_{m,v},A_{1,v},\ldots , A_{n,v}$ are random variables indexed by v. Using the definition of multiplication given in Sect. 4.2, we then perform the completion with respect to n-linear maps symbolically.

• 2.2 In the translation of ${\varvec{H}}$ and ${\varvec{G}}$ that gets rid of the handles, we must now use formal sums and indexed parameters $C_i$. For example, all linear combinations of elements of the range given above are captured by the symbolic expression

  $$\begin{aligned} \sum _{v \in [q']} C_v F_j({{\varvec{X}}},Y_{1,v},\ldots , Y_{m,v},A_{1,v},\ldots , A_{n,v})\text {.} \end{aligned}$$

• 3. We can rewrite the resulting expressions to obtain symbolic polynomials in $(\mathbb {Z}[{{\varvec{A}}},{{\varvec{B}}},{{\varvec{C}}}])[{{\varvec{X}}},{{\varvec{Y}}}]$ where ${{\varvec{B}}}$ is a finite set of normal variables, ${{\varvec{Y}}}$ and ${{\varvec{A}}}$ are finite sets of indexed variables, and ${{\varvec{C}}}$ is a finite set of normal and indexed variables. Extracting the coefficients, we now also obtain all-quantified (in)equalities like $\forall v \in [q']\cdot C_{1,v} * C_{2,v} = 0$ or $\forall u \in [q']\cdot C_{3,v} * D_{2,v} - 1 = 0$.

• 4. We translate these constraints directly into the theory of nonlinear arithmetic over the complex numbers and use interpreted function symbols $f : \mathbb {Z}\rightarrow \mathbb {C}$ to model the indexed variables. These variables arise because we consider an unbounded number of queries. For example, the winning condition can contain an unbounded number of parameters queried to the oracle.

As mentioned before, we use Z3 [21] for satisfiability checking.

6 Assumptions in Composite-Order Groups

In this section, we describe how to extend our method to composite-order groups, following ideas in Katz et al. [34] and Boyen [18]. However, we do not restrict ourselves to the case of bilinear maps, i.e., we also support more general group settings, which includes multilinear maps and leveled multilinear maps. Contrary to what is typical in cryptography, we use additive notation for all groups in this section, since it allows us to use cleaner notation for polynomially induced distributions.

6.1 Composite-Order Bilinear Groups

We consider group settings generated by algorithms $\mathsf {GroupGen}$ that take a security parameter $\lambda$ in unary representation and return a group setting ${\mathcal {G}}{\mathcal {S}}=(N,\mathcal {G}, \varPhi , \mathcal {E})$ where N is the product of distinct primes $p_1,\ldots ,p_k$, each greater than $2^{\lambda }$, $\mathcal {G}= \{\mathbb {G}_i\}_{i \in \mathcal {I}}$ is a family of cyclic groups of composite-order N, $\varPhi$ is a set of isomorphisms $\phi : \mathbb {G}_i \rightarrow \mathbb {G}_j$, and $\mathcal {E}$ is a set of admissible l-linear maps $e : \mathbb {G}_{i_1} \times \cdots \times \mathbb {G}_{i_l} \rightarrow \mathbb {G}_{i_{l+1}}$. Additionally, $\mathsf {GroupGen}$ returns the prime factors $p_1,\ldots ,p_k$ of N as well as for each group $\mathbb {G}_i$ generators $P_{i,1},\ldots ,P_{i,k}$ for the prime order subgroups. We assume that for a given group generator $\mathsf {GroupGen}$, the index set $\mathcal {I}$, the number k of primes, and the types of isomorphisms and maps are fixed. We also assume that for each group $\mathbb {G}_i$, its description includes the generator $P_i = P_{i,1}+\cdots +P_{i,k}$. Finally, we assume that the isomorphisms and maps are compatible with the generators, e.g., for $e : \mathbb {G}_i \times \mathbb {G}_j \rightarrow \mathbb {G}_t$, it holds that $e(P_{i,r}, P_{j,r}) = P_{t,r}$.

An important property satisfied by bilinear pairings in our group settings is that $e(P_{i,r},P_{j,s})=0$ for $r\ne s$. This is called the canceling property of composite-order pairings and follows from the fact that

$$\begin{aligned} p_re(P_{i,r},P_{j,s}) = e(p_rP_{i,r},P_{j,s})=e(0,P_{j,s})=0. \end{aligned}$$

Analogously, $p_{s}e(P_{i,r},P_{j,s})=0$, so choosing $a,b\in \mathbb {Z}$, s.t. $ap_r+bp_s=1$, we get

$$\begin{aligned} e(P_{i,r},P_{j,s}) = (ap_r+bp_s)e(P_{i,r},P_{j,s}) = ap_re(P_{i,r},P_{j,s}) + bp_se(P_{i,r},P_{j,s}) = 0. \end{aligned}$$

The implication of the canceling property is that computing a general pairing $e:\mathbb {G}_i\times \mathbb {G}_j \rightarrow \mathbb {G}_t$ has the form

$$\begin{aligned} e\left( a_1P_{i,1} + \cdots + a_kP_{i,k},b_1P_{j,1} + \cdots + b_kP_{j,k}\right) = a_1b_1P_{t,1} + \cdots + a_kb_kP_{t,k}. \end{aligned}$$

for $a_i,b_i\in \mathbb {Z}$, $i=1,\ldots ,k$. Clearly, the same argument generalizes to multilinear pairings of higher arity. From the perspective of our tool, this means that we can process composite-order groups as lists of tuples and compute pairings by multiplying the tuples component by component.

6.2 Generic and Symbolic Model for Composite-Order Bilinear Groups

In the composite-order case, the generic group model is not defined for a concrete group setting, but the group setting is sampled on initialization. For a group generator $\mathsf {GroupGen}$, a security parameter $\lambda$, and a distribution $\mathcal {D}$, we denote the corresponding generic group model with $\mathsf {Gen}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}}$. To define a symbolic version of this model, we restrict ourselves to polynomially induced distributions, which we define as follows for composite-order group settings.

Definition 4

Let ${\mathcal {G}}{\mathcal {S}}=(N=p_1 \cdots p_k,\mathcal {G}, \varPhi , \mathcal {E})$ be a composite-order group setting as defined above. Let ${\varvec{L}}=\{L_i\}_{i\in \mathcal {I}}$ be a set of lists where each list element is a tuple of polynomials in $(\mathbb {F}_{p_1}[X_1,\ldots ,X_n],\ldots ,\mathbb {F}_{p_k}[X_1,\ldots ,X_n])$. Furthermore, each list in ${\varvec{L}}$ is assumed to contain the constant tuple $(1,\ldots ,1)$. We define a distribution $\mathcal {D}_{{\varvec{L}}}$ on $\mathcal {G}= \{\mathbb {G}_i\}_{i\in \mathcal {I}}$ as follows. Uniformly sample a point ${\varvec{x}}\in \mathbb {Z}_N$, where $N=p_1\cdots p_k$, and return ${\varvec{L}}' = \{L'_i\}_{i\in \mathcal {I}}$, where $L_i' = [\sum _{j=1}^{k} f_j({\varvec{x}}) P_{i,j} \mid (f_1,\ldots ,f_k)\leftarrow L_i]$. We say that a distribution $\mathcal {D}$ on $\{\mathbb {G}_i\}_{i\in \mathcal {I}}$ is polynomially induced if $\mathcal {D}= \mathcal {D}_{{\varvec{L}}}$ for some ${\varvec{L}}$.

We note that the definition of decisional, computational and generalized extraction problems directly translate to the product group setting.

Example 8

The Subgroup Decision Problem for 3 primes is defined as follows. A group generator returns $({\mathcal {G}}{\mathcal {S}},\{p_1,p_2,p_3\},\{g_{p_1},g_{p_2},g_{p_3}\},\{h_{p_1},h_{p_2},h_{p_3}\})\leftarrow \mathsf {GroupGen}(\lambda )$, where the group setting is ${\mathcal {G}}{\mathcal {S}}=(N=p_1p_2p_3,\{\mathbb {G},\mathbb {G}_T\},\emptyset ,\{e:\mathbb {G}\times \mathbb {G}\rightarrow \mathbb {G}_T\})$ and we assume that the description of $\mathbb {G}$ and $\mathbb {G}_T$ in the group setting includes generators $g=g_{p_1}+g_{p_2}+g_{p_3}$ and $h=h_{p_1}+h_{p_2}+h_{p_3}$. Our compatibility assumption, then translates to $e(g_{p_i},g_{p_i}) = h_{p_i}$, $e(g_{p_i},g_{p_j}) = 0$, $i\ne j$, and $e(g,g) = h$.

Using the additive notation in the definition above, the adversary is then given $ag_{p_1}$, $bg_{p_3}$, where $a,b\leftarrow \mathbb {Z}_N$, as well as ${\mathcal {G}}{\mathcal {S}}$ and has to distinguish between $T_0 = cg_{p_1}+dg_{p_2}$ and $T_1 = cg_{p_1}$, where $c,d\leftarrow \mathbb {Z}_N$. We denote the distribution that samples $T_i$ by $\mathcal {D}_i$ for $i=0,1$. Following our definition, the distribution $\mathcal {D}_0$ is described by the list of tuples of polynomials $L = [(1,1,1),(a,0,0),(0,0,b),(c,d,0)]$ and $L_T=[(1,1,1)]$ in $\mathbb {Z}[a,b,c,d]^3$, where the tuples (1, 1, 1) corresponds to the generators g and h given as part of the group description. $\mathcal {D}_1$ is described similarly, except that $L = [(1,1,1),(a,0,0),(0,0,b),(c,0,0)]$.

6.2.1 From Generic to Symbolic Group Models

We define the symbolic group model $\mathsf {Sym}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}_{{\varvec{L}}}}$ for a group generator $\mathsf {GroupGen}$, a security parameter $\lambda$ and a polynomially induced distribution $\mathcal {D}_{{\varvec{L}}}$ as follows.

• Sample primes $p_1,\ldots ,p_k$ according to the same distribution as $\mathsf {GroupGen}$.

• Internally store lists of vectors of polynomials in $\mathbb {Z}_N[X_1,\ldots ,X_n]^k$ where $X_1,\ldots ,X_n$ are the variables occurring in ${\varvec{L}}$ and $N=p_1\cdots p_k$.

• The oracles perform addition, negation, and equality checks in the product ring of the polynomial rings.

• The oracle $\textsf {isom}_{\phi }(h)$ copies elements from one list to another.

• The oracle $\textsf {map}_{e}(h_1,\ldots ,h_k)$ appends the product of the source list elements to the target list.

Example 9

The symbolic version of the Subgroup Decision Problem for 3 primes in Example 8 is defined by letting the internal state of the oracle be initialized to $L = [(1,1,1),(a,0,0),(0,0,b),(c,d,0)]$ and $L_T=[(1,1,1)]$ in $\mathbb {Z}_N[a,b,c,d]^3$, where N is the order of the groups in the corresponding group setting.

We now prove that it is hard to distinguish the generic group model and the corresponding symbolic group model under the assumption that it is hard to factor the composite numbers N sampled by $\mathsf {GroupGen}$.

Theorem 6

Let $\lambda$ be a security parameter and let ${\mathcal {G}}{\mathcal {S}}=(N,\mathcal {G}, \varPhi ,\mathcal {E})$ denote a group setting obtained by running $\mathsf {GroupGen}(\lambda )$, where each $\mathbb {G}\in \mathcal {G}$ is cyclic of order $N=p_1\cdots p_k$, where the $p_i$, $i=1,\ldots ,k$ are distinct primes of size $\lambda$. Let $\mathcal {D}_{{\varvec{L}}}$ be a polynomially induced distribution, $s=\sum _{i\in \mathcal {I}}|L_i|$ and q the total number of queries performed by an adversary $\mathcal {A}$, then

$$\begin{aligned} \left| \Pr \left[ \mathsf {Gen}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}_{{\varvec{L}}}}(\mathcal {A})=1\right] -\Pr \left[ \mathsf {Sym}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}_{{\varvec{L}}}}(\mathcal {A})=1\right] \right| \le \frac{(s+q)^2d}{2p_\mathrm{min}} + \varepsilon (\lambda ), \end{aligned}$$

where $p_\mathrm{min} = \min {(p_1, \ldots , p_k)}$ and $\varepsilon (\lambda )$ is an upper bound on the probability that $\mathcal {A}$ succeeds in factoring N.

Proof

Translating composite-order assumptions in a group setting ${\mathcal {G}}{\mathcal {S}}=(N,\mathcal {G},\varPhi ,\mathcal {E})$, where the initial state of the generic group is sampled by a polynomially induced distribution $\mathcal {D}_{{\varvec{L}}}$, to a symbolic model is based on the following sequence of games.

Game 0::

Generic group game.

Game 1::

Replace the internal representations of the groups by the additive group $\mathbb {Z}_{p_1}\times \cdots \times \mathbb {Z}_{p_k}$.

Game 2::

Replace all sampled elements by formal variables and sample values for them in $\mathbb {Z}_N$. Replace the internal representation of the groups by $(\mathbb {Z}_{p_1}[{{\varvec{X}}}],\ldots ,\mathbb {Z}_{p_k}[{{\varvec{X}}}])$, where ${{\varvec{X}}}$ denotes the set of formal variables. Perform equality checks on tuples of polynomials evaluated at the sampled values.

Game 3::

Replace the equality check oracle in the previous game to perform an equality check on the tuples of formal polynomials.

Game 4::

Replace the polynomial computations to happen over $(\mathbb {Z}_N[{{\varvec{X}}}],\ldots ,\mathbb {Z}_N[{{\varvec{X}}}])$

We note that Games 0–2 are identically distributed. Next, we argue that the distinguishing probability of Games 2 and 3 can be bounded based on the random choice of ${{\varvec{x}}} \in \mathbb {Z}_N$. In fact, a difference between the two games occurs only when there is an equality query that is answered positively in Game 2 and negatively in Game 3, i.e., there are two k-tuples of polynomials $f, f' \in (\mathbb {Z}_{p_1}[{{\varvec{X}}}],\ldots ,\mathbb {Z}_{p_k}[{{\varvec{X}}}])$ such that $f \ne f'$ but $f_j({{\varvec{x}}}) = f'_j({{\varvec{x}}}) \in \mathbb {Z}_{p_j}$. If $f \ne f'$, then there exists at least one index $j \in [k]$ such that $f_j \ne f'_j$ over $\mathbb {Z}_{p_j}[{{{\varvec{X}}}}]$. Let d be the highest degree of any polynomial appearing as a component of a k-tuple. Then the probability that, for this j, $f_j \ne f'_j$ but $f_j({{\varvec{x}}}) = f'_j({{\varvec{x}}}) \in \mathbb {Z}_{p_j}$ is, by Schwartz–Zippel, bounded above by $d/p_j$, over the random choice of ${{\varvec{x}}} \in \mathbb {Z}_N$ (in fact, by the Chinese Remainder Theorem, the value of each variable X modulo $p_i$ is independent of the value modulo $p_j$ for $i\ne j$). Let q be the number of queries and $s=\sum _{i\in \mathcal {I}}|L_i|$ the total initial lengths of the internal lists: The number of polynomial tuples in the problem is then limited by $s+q$. Since $p_j \ge p_\mathrm{min}$, we have that the distinguishing probability of Games 2 and 3 is upper-bounded by

$$\begin{aligned} \frac{(s+q)^2d}{2p_\mathrm{min}}. \end{aligned}$$

To conclude the proof, we note that any adversary that can distinguish between Games 3 and 4 can be used to efficiently factor N, which gives us the second term in the bound.

$\square$

6.3 Master Theorem

Let $\mathcal {D}_{{\varvec{L}}}$ and $\mathcal {D}_{{\varvec{L}}'}$ be two polynomially induced distributions such that $|L_i|=|L_i'|$ for all i. In what follows, we derive a condition under which

$$\begin{aligned} \left| \Pr \left[ \mathsf {Sym}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}_{{\varvec{L}}}}(\mathcal {A})=1\right] - \Pr \left[ \mathsf {Sym}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}_{{\varvec{L}}'}}(\mathcal {A})=1\right] \right| =0 . \end{aligned}$$

In the game $\mathsf {Sym}^{}_{}$, computing pairings corresponds to component-wise multiplication of tuples. This allows us to directly extend our concept of completion to tuples. From Example 3, we directly see that computing the completion for tuples can be done in exactly the same way, except that we plug in tuple values for the freshly chosen variables. In the composite-order symbolic model, the completion on the product group structure similarly records the possible elements that the adversary may compute from the inputs. It follows that the left and right version of Game 4 are equally distributed if

$$\begin{aligned} \left\{ {{\varvec{\alpha }}}\in \mathbb {Z}_N^r\mid {{\varvec{\alpha }}}\cdot \mathcal {C}({\varvec{L}})_t \right\} = \left\{ {{\varvec{\alpha }}}\in \mathbb {Z}_N^r\mid {{\varvec{\alpha }}}\cdot \mathcal {C}({\varvec{L}}')_t \right\} , \end{aligned}$$

where $r=|\mathcal {C}({\varvec{L}})_t|=|\mathcal {C}({\varvec{L}}')_t|$.

Finally, by combining Theorem 6 and the above argument, we obtain the following version of the master theorem for the composite-order setting:

Theorem 7

Let $\lambda$ be a security parameter and let ${\mathcal {G}}{\mathcal {S}}=(N,\mathcal {G}, \varPhi ,\mathcal {E})$ denote a group setting obtained by running $\mathsf {GroupGen}(\lambda )$, where each $\mathbb {G}\in \mathcal {G}$ is cyclic of order $N=p_1\cdots p_k$, where the $p_i$, $i=1,\ldots ,k$ are distinct primes of size $\lambda$. Let $\mathcal {D}_{{\varvec{L}}}, \mathcal {D}_{{\varvec{L}}'}$ be polynomially induced distributions such that $|L_{i}| = |L'_{i}|$ for all $i \in \mathcal {I}$. Let t denote the index of the target group, $s = \sum _{i\in \mathcal {I}} | L_{i} |$, $r = |\mathcal {C}({\varvec{L}})_t|$, let d denote an upper bound for the total degrees of the polynomials in the completions of the lists, and let q be the total number of queries performed by an adversary $\mathcal {A}$. If

$$\begin{aligned} \left\{ {{\varvec{a}}} \in \mathbb {Z}_N^r \mid {{\varvec{a}}} \cdot \mathcal {C}({\varvec{L}})_t = 0 \right\} = \left\{ {{\varvec{a}}} \in \mathbb {Z}_N^r \mid {{\varvec{a}}} \cdot \mathcal {C}({\varvec{L}}')_t = 0 \right\} , \end{aligned}$$

then

$$\begin{aligned} \left| \Pr \left[ \mathsf {Gen}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}_{{\varvec{L}}}}(\mathcal {A})=1\right] - \Pr \left[ \mathsf {Gen}^{\mathsf {GroupGen},\lambda }_{\mathcal {D}_{{\varvec{L}}'}}(\mathcal {A})=1\right] \right| \le \frac{(s+q)^2d}{p_\mathrm{min}} + 2\varepsilon (\lambda ). \end{aligned}$$

where $p_\mathrm{min} = \min {(p_1, \ldots , p_k)}$ and $\varepsilon (\lambda )$ is an upper bound on the probability that $\mathcal {A}$ succeeds in factoring N.

6.4 Nonparametric and Non-interactive Assumptions

The algorithm in Sect. 4.1 extends directly with one simple modification. For the polynomials in the closure, a basis is given by all the monomials appearing in the closure. We just need to extend this to tuples, i.e., for any element $(P_1,\ldots ,P_k)$ in the closure and any monomial M appearing in $P_i$, we add $(0,\ldots ,0,M,0,\ldots ,0)$ to the basis, where M is in the ith position. In the resulting basis, we can express all the polynomial tuples in the closure and the algorithm extends with no further modifications.

7 Implementation and Case Studies

We have developed a tool that implements the described methods. The tool uses Sage [47] as a back end for linear and commutative algebra and Z3 [21] as a back end for model-finding and unsatisfiability proofs. Table 2 shows a selection of case studies analyzed by our tool and the result. It is worth mentioning that the extension of our results for supporting Laurent polynomials that was introduced in this extended version was necessary to capture structure preserving signature schemes, such as those listed in Table 2.

Table 2 Analysis for various assumptions from the literature

8 Conclusion

In this paper, we initiated the study of automated methods for analyzing the hardness of cryptographic assumptions in generic group models. A concrete outcome of our work are a collection of automated procedures implemented in a publicly available tool that can verify the generic hardness of a large class of cryptographic assumptions. Our current methods can deal in a quite satisfactory way (offering a complete decision procedure that can also find attacks) with nonparametric assumptions and interactive bounded computational assumptions. On the other hand, there are classes of assumptions that are currently out of reach of our methods. One interesting case is that of interactive decisional assumptions: While a formulation of a master theorem for this class of problems (with some restrictions⁶) has been given recently by Baltico et al. [4], the development of automated decision procedures for this setting seems a hard task and is an open problem. A second case is that of parametric and interactive assumptions for groups of composite order.

Appendix: Automated Analysis of Non-interactive Assumptions

1.1 Undecidability of Simultaneous Degree and Arity Parametricity

To prove the theorem, we show that a Diophantine problem can be encoded into a parametric assumption where both the range limits and the arity of the map are parametric. This means that deciding hardness of such parametric assumptions would imply a decision algorithm for the Diophantine problem, which however is undecidable by Matiyasevich’s theorem [37].

First, we observe that given a Diophantine problem, by introducing new variables, we can always reduce the equation to a system of the following form

$$\begin{aligned} \left\{ \begin{array}{l} c_1X_1+\cdots +c_nX_n = d\\ X_i = X_j \cdot X_k \end{array} \right. \end{aligned}$$

(1)

where there is only one equation of the first form, while there can be several equations of the form $X_i = X_j \cdot X_k$.

In what follows, we show that this system can always be encoded in the set of equations

$$\begin{aligned} \left\{ \begin{array}{ll} 0\le \delta _i &{}\quad \text { for } i \in [1,n] \\ \alpha _i \le r_i \le \beta _i &{}\quad \text { for } i \in [1,t] \\ u_i = f_i, &{}\quad \text { for } i \in [1,m] \\ \sum \limits _{i=1}^n \delta _i\lambda _i = k &{} \end{array} \right. \end{aligned}$$

by appropriate choice of decision function and input polynomials. We note that for undecidability, it is enough to look for solutions over the naturals, since the general case over the integers reduces to this by independently replacing each variable X by $\pm X$ and checking all the possible equations over the naturals.

We now show how to encode the system (1) as a range and arity parametric assumption with all inputs at level one and the decision polynomial being a monomial at the target level.

First, we look at the linear relation $c_1X_1+\cdots +c_nX_n=d$. Let $l_1,\ldots ,l_n$ be fresh range limit variables. We add the input monomial

$$\begin{aligned} M = Z_1^{c_1l_1+\cdots +c_nl_n}Z_2 \end{aligned}$$

as input, where $Z_1,Z_2$ are freshly introduced variables not used in any other input monomial. Conversely, we add to the decision polynomial f the factors

$$\begin{aligned} Z_1^dZ_2. \end{aligned}$$

The degree equations corresponding to the variables $Z_1$ and $Z_2$ are now

$$\begin{aligned} \left\{ \begin{array}{l} d = \delta \left( c_1l_1+\cdots +c_nl_n\right) \\ 1 = \delta \end{array} \right. , \end{aligned}$$

which encode $d=c_1l_1+\cdots +c_nl_n$.

Second, having switched variables in (1) to range limits, we look at an equation $l_i=l_j\cdot l_m$. Again, we let $Z_1,Z_2$ be new fresh variables and add the input monomial $M = Z_1Z_2^{l_m}$. Conversely, we multiply f with the factors $Z_1^{l_j}Z_2^{l_i}$. The degree equations now become

$$\begin{aligned} \left\{ \begin{array}{l} l_j = \delta \\ l_i = \delta \cdot l_m \end{array} \right. , \end{aligned}$$

which gives us precisely $l_i = l_j\cdot l_m$. Since k is not used anywhere in the input or f it only appears in the first equation in the system (1). Therefore, k can grow unbounded, so $\sum _{i=1}^t\delta _i \le k$ adds no restrictions on the $\delta _i$ except what was forced by our computations above. Similarly, range indices are never used, so no limitations are forced on the range limits except that they are positive. Therefore, we have encoded the system (1) under the sole requirement that $l_i\in \mathbb {N}$ for each i while only placing restrictions on the other variables that can be trivially independently satisfied.

Example 10

To encode the equation $3XY^2+Z^2=0$ as an assumption, we first write the equation in the form

$$\begin{aligned} \left\{ \begin{array}{l} 3l_5 + l_6 = 0\\ l_4 = l_2\cdot l_2\\ l_5 = l_1\cdot l_4\\ l_6 = l_3 \cdot l_3, \end{array} \right. \end{aligned}$$

where we have used $X=l_1$, $Y=l_2$ and $Z=l_3$. The assumption then becomes the following: for all k, given $M_1 = Z_1^{3l_5+l_6}Z_2$, $M_2=Z_3Z_4^{l_2}$, $M_3=Z_5Z_6^{l_4}$, and $M_4=Z_7Z_8^{l_3}$ at level 1, we cannot distinguish $Z_2Z_3^{l_2}Z_4^{l_4}Z_5^{l_1}Z_6^{l_5}Z_7^{l_3}Z_8^{l_6}$ from random at level k, where the $Z_i$ have been uniformly randomly sampled.

As can be seen, the assumption is unnatural, since it defines range limits, but does not actually have any range indices that uses them. Therefore, it remains open to find well-defined restrictions on the inputs that still allows deciding the constraint system.