group_setting 3.

sample V,W.
input [V,W] in G1.

oracle o1(M:G2) =
  sample R;
  return [ R ] in G1,
         [ R, M*V + R^2 + W] in G2.

win (wM:G2, wR1:G1, wR2:G2, wS:G2) =
    (forall i: wM <> M_i /\ wR1 = wR2 /\ wS = V*wM + wR1*wR2 + W).

Group type

The tool is designed to be used on cryptographic schemes defined over bilinear groups. You must specify in your input file the group type where your construction is defined. There are three different settings in a bilinear group:

• Type I: $\mathbb{G}_{1} = \mathbb{G}_{2}$.
  This is also known as the symmetric setting. There is only one group, because the two groups are the same. This is the default setting if it is not specified in the input file.
• Type II: $\mathbb{G}_{1} \neq \mathbb{G}_{2}$, but there is an efficiently computable isomorphism $\psi: \mathbb{G}_{2} \rightarrow \mathbb{G}_{1}$.
  This implies that from an element in $\mathbb{G}_{2}$, it should be easy to compute an element in $\mathbb{G}_{1}$ with the same discrete logarithm . On the other hand, it is supposed to be hard to compute $\psi^{-1}$, the inverse isomorphism.
• Type III: $\mathbb{G}_{1} \neq \mathbb{G}_{2}$.
  This is also known as the asymmetric setting. There is no efficiently computable isomorphism between $\mathbb{G}_{1}$ and $\mathbb{G}_{2}$. Although this isomorphism exists (both groups have order $p$), it cannot be computed efficiently.

To specify the group type, you must include the following line in the input file:

group_setting n.

where n must be replaced with 1, 2 or 3.

Adversary input

This part of the input file allows to define what is given to the adversary in the beginning of the security game. Usually, we specify the public parameters and public keys in this part. The syntax is the following:

sample V1,V2,...,Vk.
input [P1,P2,...,Pm] in G1,
      [Q1,Q2,...,Qn] in G2.

The previous syntax represents the fact of sampling variables $$V_1,\dots,V_k \stackrel{\$}{\leftarrow} \mathbb{Z}_{p}^{*}$$ and giving to the adversary access to elements $$g_{1}^{P_1}, \dots, g_{1}^{P_m}, g_{2}^{Q_1}, \dots, g_{2}^{Q_n}$$ where $P_1,\dots,P_m,Q_1,\dots,Q_n$ are Laurent polynomials over the previously defined variables $V_1,\dots,V_k$ with coefficients in $\mathbb{Z}_{p}$.

• As variable names you can use arbitrarily long strings consisting of alphanumeric symbols: A-Z + a-z + 0-9
• To define polynomials you can use integers and variables, combined with symbols + - * ^ ( ).

This part of the input file is not a requirement, you may define security experiments where no initial information is given to the adversary.

Oracle definition

Here, we define the Oracle that the adversary can call in the security experiment. For instance, a Signing Oracle when we analyze a Signature Scheme. For this we must define the Oracle input, the randomness defined in the Oracle execution and the Oracle output. The syntax is the following:

oracle o1(I1:S1,...,Ik:Sk) = 
  sample R1,...,Rl;
  return [ P1,...,Pm ] in G1,
         [ Q1,...,Qn ] in G2.

• The oracle name must start with o and can be followed by an arbitrary string, consisting of alphanumeric characters: A-Z + a-z + 0-9
• The Oracle input is defined by a list of typed variables.
  Variables $I_{1},\dots,I_{k}$ are defined by alphanumeric strings, using: A-Z + a-z + 0-9
  Every set $S_{1},\dots, S_{k}$ must be G1, G2 or Fp, corresponding to $\mathbb{G}_{1}$, $\mathbb{G}_{2}$ and $\mathbb{Z}_{p}$ respectively.
• For random variable names, $R_{1},\dots, R_{l}$, you can use strings consisting of alphanumeric symbols: A-Z + a-z + 0-9
• For output polynomials $P_{1},\dots,P_{m},Q_{1},\dots,Q_{n}$ you can use integers and previously defined variables (either from the adversary input or Oracle random variables), combined with symbols + - * ^ ( ).

The oracle definition is required. If your security experiment does not give Oracle access to the adversary you can write:

oracle o1() =
  return [ ] in G1.

As an example, the Oracle definition from above:

oracle o1(M:G2) =
  sample R;
  return [ R ] in G1,
         [ R, M*V + R^2 + W] in G2.

Represents the fact that the adversary sends $M \in \mathbb{G}_{2}$ to the Oracle, which samples a random variable $r \stackrel{\$}{\leftarrow} \mathbb{Z}_{p}$ and outputs three group elements (a valid signature for $M$): $$g_{1}^{r}, \ \ \ \ \ \ \ g_{2}^{r}, \ \ \ \ \ \ \ \text{ and } \ \ \ \ M^{v}\cdot g_{2}^{r^{2}} \cdot g_{2}^{w}$$

Winning conditions

Here, we define the security statements that should be reached by the adversary to win the game and thus, if there is no way she can reach them, the security experiment is secure. The syntax is the following:

win (F1:S1,...,Fk:Sk) = 
  ( exp1  /\  exp2  /\ ... /\ expn ).

where:

• Elements $F_{1},\dots,F_{k}$ represent the forgery in the computational experiment. You must specify the type $S_i$ (G1, G2 or Fp) of every forgery element $F_i$.
• The winning conditions are defined by a conjunction of expressions. Expression can be equalities or inequalities and must have the following form:
  

  forall i1,...,ik: P = Q

  forall i1,...,ik: P <> Q

  • $i_{1},\dots,i_{k}$ are index variables. You can define them using arbitrary alphanumeric strings where the first symbol must be one of the following characters: i, j, k, l. You can also define two index variables sharing the same name, with the ' symbol. The syntax is name'n where n must be an integer. For example, i'1 and i'2 will share the name $i$ and will be printed in $\LaTeX{}$ form as $i_{1}$ and $i_{2}$.
  • $P$ and $Q$ are Laurent polynomials with coefficient in $\mathbb{Z}_{p}$, over all previous variables: adversary input variables, forgery variables, oracle input variables and random variables in the oracle. Variables, as explained above, are defined by alphanumeric strings. However, every oracle variable must be indexed (by a single index corresponding to the number of the Oracle query that involves the variable). This is done with the _ symbol. The syntax is V_i, where V is the variable name and i is an index variable.
    Additionally, $P$ and $Q$ may include summation terms. The syntax for a summation is:

    (sum i1,...,ik: M)

    where $i_{1},\dots,i_{k}$ are index variables and $M$ is a Laurent monomial.
  
  We note that, when the expression does not depend on index variables, the forall token can be omitted and the expression becomes P = Q or P <> Q.

These expressions allow us to express the conditions of the security experiment. For example, to establish that the forgery must be on a new message, different from all messages sent to the Oracle, we can write:

forall i: wM <> M_i