equation forall x:bool; not(not(x)) = x.
equation forall x:bool,y:bool; (not(x && y)) = (not(x) || not(y)).
equation forall x:bool,y:bool; (not(x || y)) = (not(x) && not(y)).
equation not(true) = false.
equation not(false) = true.
equation forall x:bool; (x = true) = x.
equation forall x:bool; (x <> false) = x.
equation forall x:bool; (x <> true) = not(x).
equation forall x:bool; (x = false) = not(x).
equation forall x,y,z:bool; ((x || y) && z) = ((x && z) || (y && z)).

const bottom:bitstringbot.

(******************************** Diffie-Hellman ***************************)

(* DH_basic defines a part common for most Diffie-Hellman assumptions.

   G: type of group elements (must be "bounded" or "nonuniform", and "large")
   Z: type of exponents (must be "bounded" or "nonuniform", and "large")

   g: generator 
   exp: the exponentiation function
   exp': symbol that replaces exp after game transformation
   mult: the multiplication function for exponents

   The types G and Z must be declared before expanding
   this macro.  The functions g, exp, exp', and mult are defined by this
   macro. They must not be declared elsewhere, and they can be used
   only after expanding the macro.
*)

def DH_basic(G, Z, g, exp, exp', mult) {

fun exp(G,Z): G.
fun exp'(G,Z): G.
const g:G.

fun mult(Z,Z): Z. 
equation builtin commut(mult).

(* exponents multiply *)

equation forall a:G, x:Z, y:Z;
  exp(exp(a,x), y) = exp(a, mult(x,y)).
equation forall a:G, x:Z, y:Z;
  exp'(exp'(a,x), y) = exp'(a, mult(x,y)).

}

(* DH_dist_random_group_element_vs_exponent says that the probability
   of distinguishing a random group element from an exponentiation
   exp(g,x) with a random exponent is at most PDist.  The other
   arguments are as in DH_basic and must all be defined before. *)

def DH_dist_random_group_element_vs_exponent(G, Z, g, exp, exp', mult, PDist) {

(* replace a random group element with an exponentiation, and conversely. *)

param N, N'.

equiv(group_to_exp_strict(exp))
      foreach iX <= N do X <-R G; (OX() := return(X) | foreach iXm <= N' do OXm(m:Z) [useful_change] := return(exp(X,m)))
<=(N * PDist)=> [computational]
      foreach iX <= N do x <-R Z; (OX() := return(exp(g,x)) | foreach iXm <= N' do OXm(m:Z) := return(exp(g,mult(x,m)))).

(* This equivalence is very general, apply it only manually, because
   otherwise it might be applied too often.  The equivalence above is
   particular case applied only when X is inside exp, and good for
   automatic proofs. *)

equiv(group_to_exp(exp))
      foreach iX <= N do X <-R G; OX() := return(X) 
<=(N * PDist)=> [manual, computational]    
      foreach iX <= N do x <-R Z; OX() := return(exp(g,x)).


equiv(exp_to_group(exp))
      foreach iX <= N do x <-R Z; OX() := return(exp(g,x))
<=(N * PDist)=> [computational]
      foreach iX <= N do X <-R G; OX() := return(X).

equiv(exp'_to_group(exp))
      foreach iX <= N do x <-R Z; OX() := return(exp'(g,x))
<=(N * PDist)=> [computational]
      foreach iX <= N do X <-R G; OX() := return(X).

}

(* DH_good_group defines Diffie-Hellman assumptions that hold
   when
   - G is a group of prime order q, with the neutral element excluded.
   - the set of exponents Z is {1, ..., q-1}
   - g is a generator of G
   - mult is the product modulo q in {1, ..., q-1}, i.e. in the group (Z/qZ)*

   Warnings: 
   * It may not be obvious when an element is received on the network
   whether it really belongs to the group G generated by g. That should 
   be checked for the results to apply.
   * Random choices of exponents must be made uniformly in {1, ..., q-1} 
   for the results to apply; random choices in G are also uniform.

   The arguments are as in DH_basic. 
*)

def DH_good_group(G, Z, g, exp, exp', mult) {

expand DH_basic(G, Z, g, exp, exp', mult).

(* Since the group has prime order, 
exp(x,y) = exp(x',y) implies x = x', by raising both sides to y^{-1}.
Note that y is invertible since it belongs to (Z/qZ)* with q prime. *)

equation forall x:G, x':G, y:Z; (exp(x,y) = exp(x',y)) = (x = x').
equation forall x:G, x':G, y:Z; (exp'(x,y) = exp'(x',y)) = (x = x').
equation forall x:G, x':Z, y:Z; (exp(x,y) = exp(g, mult(x',y))) = (x = exp(g,x')).
equation forall x:G, x':Z, y:Z; (exp'(x,y) = exp'(g, mult(x',y))) = (x = exp(g,x')).

(* Injectivity: Since G has prime order, all its elements x are generators.
   All elements x^y for y \in Z = { 1, ..., q-1 } are then distinct. *)

equation forall x:G, y:Z, y':Z; (exp(x,y) = exp(x,y')) = (y = y').
equation forall x:G, y:Z, y':Z; (exp'(x,y) = exp'(x,y')) = (y = y').

(* collision between products *)

(* The collision x.y = z happens when x = z/y
   (y is invertible since we work in (Z/qZ)* with q prime).
   Since z/y is independent of x, this has probability
   1/|Z| to happen. *)
collision x <-R Z; forall y: Z, z: Z; 
  return(mult(x,y) = z) <=(1/|Z|)=> return(false) if y independent-of x && z independent-of x. 

collision x <-R Z; y <-R Z; forall z: Z; 
  return(mult(x,y) = z) <=(1/|Z|)=> return(false) if z independent-of x || z independent-of y. 

(* The next collision groups 2 cases:
   - mult(x,y) = z with x, y independent of each other, seen above
   - mult(x,x) = z. This case is justified as follows.
   In (Z/qZ)*, half of the elements are square, and each square
   has 2 square roots. If z is not a square, the equality x.x = z is false.
   If z is a square z = x'.x', then x.x = x'.x' iff x = x' or x = -x' (mod q),
   so with probability 2/|Z|. *) 
collision x <-R Z; y <-R Z; [random_choices_may_be_equal] forall z: Z; 
  return(mult(x,y) = z) <=(2/|Z|)=> return(false) if z independent-of x || z independent-of y. 

(* The next collision is a consequence of the previous one, though this requires
   some reasoning.
   The random choices x1,y1,x2,y2 may be either independent of each other or equal
   (because the option "random_choices_may_be_equal" still makes sure that the 
   array indices of x1,y1,x2,y2 do not depend on x1,y1,x2,y2). 
   Hence x1 independent-of x2 actually implies that x2 is also independent of x1.
   
   The condition (x1 independent-of x2 || y1 independent-of y2) &&
	       (x1 independent-of y2 || y1 independent-of x2)
   yields 4 cases:
   1/ x1 independent-of x2 and x1 independent-of y2
   x2 and y2 independent of x1, so mult(x2,y2) independent of x1
   Apply previous collision with z = mult(x2,y2)

   2/ x1 independent-of x2 and y1 independent-of x2
   x1 and y1 independent of x2, so mult(x1,y1) independent of x2
   Apply previous collision with z = mult(x1,y1)

   3/ y1 independent-of y2 and x1 independent-of y2
   x1 and y1 independent of y2, so mult(x1,y1) independent of y2
   Apply previous collision with z = mult(x1,y1)

   4/ y1 independent-of y2 and y1 independent-of x2
   x2 and y2 independent of y1, so mult(x2,y2) independent of y1
   Apply previous collision with z = mult(x2,y2)

   The formulation below allows CryptoVerif to replace 
   mult(x1,y1) = mult(x2,y2)
   with a condition corresponding to 
   (x1 = x2 && y1 = y2) || (x1 = y2 && y1 = x2)
   where = here means that they are the same random choice (i.e. same 
   variable with the same indices). This condition is the negation
   of the independence condition
   (x1 independent-of x2 || y1 independent-of y2) &&
   (x1 independent-of y2 || y1 independent-of x2).
   It corresponds to the only case that makes the equality 
   succeed with non-negligible probability.  *)
collision x1 <-R Z; y1 <-R Z; x2 <-R Z; y2 <-R Z; [random_choices_may_be_equal]
  return(mult(x1,y1) = mult(x2,y2)) <=(2/|Z|)=> return(false)
	    if (x1 independent-of x2 || y1 independent-of y2) &&
	       (x1 independent-of y2 || y1 independent-of x2).

(* x is invertible since we work in (Z/qZ)* with q prime *)
equation forall x:Z, y:Z, y':Z; 
  (mult(x,y) = mult(x,y')) = (y = y').


(* The following properties are true, but CryptoVerif should be able
   to infer them from the equations above.

   If Y independent of x, g^x = Y succeeds for one value of x, 
   so with probability 1/|Z|. 
collision x <-R Z; forall Y: G;
	  return(exp(g, x) = Y) <=(1/|Z|)=> return(false) if Y independent-of x.
collision x <-R Z; forall Y: G;
	  return(exp'(g, x) = Y) <=(1/|Z|)=> return(false) if Y independent-of x.

   If Y independent of y, g^(x.y) = Y succeeds for one value of y, 
   so with probability 1/|Z|. 
collision x <-R Z; y <-R Z; forall Y: G;
	  return(exp(g, mult(x,y)) = Y) <=(1/|Z|)=> return(false) if Y independent-of y.
collision x <-R Z; y <-R Z; forall Y: G;
	  return(exp'(g, mult(x,y)) = Y) <=(1/|Z|)=> return(false) if Y independent-of y.
*)

(* X^x = Y 
   X is a generator of the group, so Y = X^y for some y
   independent of x. The equality X^x = Y = X^y holds only when
   x = y (mod q) with y independent of x,
   so this has probability 1/|Z| of happening. *)

collision x <-R Z; forall X: G, Y: G;
	  return(exp(X, x) = Y) <=(1/|Z|)=> return(false)
	  if X independent-of x && Y independent-of x.
collision x <-R Z; forall X: G, Y: G;
	  return(exp'(X, x) = Y) <=(1/|Z|)=> return(false)
	  if X independent-of x && Y independent-of x.

(* replace a random group element with an exponentiation, and conversely.
   This is valid because G is exactly the group generated by g of cardinal q,
   and Z = {1, ..., q-1} so when x varies in Z, exp(g,x) covers each element
   of G exactly once. *)

letproba PDist = 0.

expand DH_dist_random_group_element_vs_exponent(G, Z, g, exp, exp', mult, PDist).

}

(* Variant of CDH with random self reducibility.
   It may yield lower probabilities but requires the rerandomization to be feasible.

   pCDH(t): the probability of breaking the CDH assumption in time t
   pDistRerandom: the probability that rerandomization can be distinguished from the
   original distribution
          It is 0 when exponents are chosen uniformly in (Z/qZ)^*.
	  2^-126 for curve25519
	  2^-221 for curve448
   (see https://tools.ietf.org/html/draft-barnes-cfrg-mult-for-7748-00 for the rerandomization
   for curve25519 and curve448).

   Other arguments as in DH_basic.

   All arguments must be declared before this macro. *)

def CDH_RSR(G, Z, g, exp, exp', mult, pCDH, pDistRerandom) {

(* the CDH assumption *) 

param na, naDDH, nb, nbDDH, naDH9, nbDH9.

equiv(cdh(exp))
    foreach ia <= na do a <-R Z; (
      OA() := return(exp(g,a)) | 
      Oa() [10] := return(a) |
      foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) [useful_change] := return(m = exp(g, mult(b[j], a))) |
      foreach iaDH9 <= naDH9 do ODHa9(x:Z) [2] := return(exp(g, mult(a, x)))
    ) |
    foreach ib <= nb do b <-R Z; (
      OB() := return(exp(g,b)) |
      Ob() [10] := return(b) |
      foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) := return(m = exp(g, mult(a[j], b))) |
      foreach ibDH9 <= nbDH9 do ODHb9(x:Z) [2] := return(exp(g, mult(b, x)))
    )
<=((#ODDHa + #ODDHb) * (3*#Oa+1) * (3*#Ob+1) * pCDH(time + (na + nb + (optim-if #Oa = 0 && #Ob = 0 then 0 else #ODDHa + #ODDHb) + 1 + #ODHa9 + #ODHb9) * time(exp)) + (na + nb) * pDistRerandom)=> [computational]
    foreach ia <= na do a <-R Z [unchanged]; (
      OA() := return(exp'(g,a)) |
      Oa() := let ka:bool = true in return(a) |
      foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) := 
      	      if defined(kb[j]) then return(m = exp'(g, mult(b[j], a))) else 
              if defined(ka) then return(m = exp'(g, mult(b[j], a))) else return(false) |
      foreach iaDH9 <= naDH9 do ODHa9(x:Z) := return(exp'(g, mult(a, x)))
    ) |
    foreach ib <= nb do b <-R Z [unchanged]; (
      OB() := return(exp'(g,b)) |
      Ob() := let kb:bool = true in return(b) |
      foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) := 
      	      if defined(ka[j]) then return(m = exp'(g, mult(a[j], b))) else 
              if defined(kb) then return(m = exp'(g, mult(a[j], b))) else return(false) |
      foreach ibDH9 <= nbDH9 do ODHb9(x:Z) := return(exp'(g, mult(b, x)))
    ).

}

(* Ideal Cipher Model
   cipherkey: type of keys that correspond to the choice of the scheme, must be "bounded" or "nonuniform", typically "fixed".
   key: type of keys (typically "large")
   blocksize: type of the input and output of the cipher, must be "bounded" or "nonuniform" (to be able to generate random numbers from it; typically "fixed") and "large".
   (The modeling of the ideal cipher model is not perfect in that, in
   order to encrypt a new message, one chooses a fresh random number,
   not necessarily different from previously generated random
   numbers. Then CryptoVerif needs to eliminate collisions between
   those random numbers, so blocksize must really be "large".)

   enc: encryption function
   dec: decryption function
   WARNING: the encryption and decryption functions take 2 keys as
   input: the key of type cipherkey that corresponds to the choice of
   the scheme, and the normal encryption/decryption key. The cipherkey
   must be chosen once and for all at the beginning of the game and
   the encryption and decryption oracles must be made available to the
   adversary, by including a process enc_dec_oracle(ck) where
   ck is the cipherkey.
   qE is the number of calls of the encryption oracle
   qD is the number of calls of the decryption oracle
   
   The types cipherkey, key, blocksize must be declared before this
   macro is expanded. The functions enc, dec, the process
   enc_dec_oracle, and the parameters qE, qD are declared by this
   macro. They must not be declared elsewhere, and they can be used
   only after expanding the macro.

 *)

def ICM_cipher(cipherkey, key, blocksize, enc, dec, enc_dec_oracle, qE, qD) {

fun enc(cipherkey, blocksize, key): blocksize.
fun dec(cipherkey, blocksize, key): blocksize.

equation forall ck:cipherkey, m:blocksize, k:key;
        dec(ck, enc(ck, m, k), k) = m.
equation forall ck:cipherkey, m:blocksize, k:key; 
	enc(ck, dec(ck, m, k), k) = m.
equation forall ck:cipherkey, m1:blocksize, m2:blocksize, k:key;
        (dec(ck, m1, k) = dec(ck, m2, k)) = (m1 = m2).
equation forall ck:cipherkey, m1:blocksize, m2:blocksize, k:key; 
	(enc(ck, m1, k) = enc(ck, m2, k)) = (m1 = m2).

equiv(icm(enc)) special icm(("key", "msg", "local_key"), enc, dec,
       (ck, k, me, md, u), ("large")).

equiv(icm_partial(enc)) special icm_partial(("key", "msg", "local_key"), 
       enc, dec, (ck, k, me, md, u), ("large")) [manual].

(* The difference of probability is the probability of collision between two
random numbers in blocksize among the N+N2 chosen random numbers. *)

  param qE, qD [noninteractive].

let enc_dec_oracle(ck: cipherkey) =
    (foreach iE <= qE do Oenc(x:blocksize, ke:key) := return(enc(ck,x,ke)))
  | (foreach iD <= qD do Odec(m:blocksize, kd:key) := return(dec(ck,m,kd))).

}

(******************************* Hash functions (ROM) ****************************)

(* Hash function in the random oracle model
   key: type of the key of the hash function, which models the choice of the hash function, must be "bounded", typically "fixed"
   input%: type of the %-th input of the hash function
   output: type of the output of the hash function, must be "bounded" or "nonuniform" (typically "fixed").

   f: the hash function.
   WARNING: f is a keyed hash function.
   The key must be generated once and for all at the beginning of the game 
   and the hash oracle must be made available to the adversary,
   by including the process f_oracle(k) where k is the key.
   qH is the number of calls to f_oracle.

   The types key, input%, and output must be declared before
   this macro. The function f, the process f_oracle, and
   the parameter qH are defined by this macro. They must not
   be declared elsewhere, and they can be used only after expanding the
   macro.

 *)

def ROM_hash(key, input1, output, f, f_oracle, qH) {

fun f(key, input1):output.

equiv(rom(f)) special rom("key_first", f, (hk, r, x, y, z, u)).

equiv(rom_partial(f)) special rom_partial("key_first", f, (hk, r, x, y, z, u)) [manual].


param qH [noninteractive].

let f_oracle(k: key) = 
        foreach iH <= qH do
	OH(x1: input1) :=
        return(f(k, x1)).

}

(* ROM with large output.
    The only difference with ROM is that we eliminate collisions on the output.
    The interface is the same as for ROMs. *)

def ROM_hash_large(key, input1, output, f, f_oracle, qH) {

fun f(key, input1):output.

equiv(rom(f)) special rom("key_first", f, (hk, r, x, y, z, u), ("large")).

equiv(rom_partial(f)) special rom_partial("key_first", f, (hk, r, x, y, z, u), ("large")) [manual].


param qH [noninteractive].

let f_oracle(k: key) = 
        foreach iH <= qH do
	OH(x1: input1) :=
        return(f(k, x1)).

}