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

const bottom:bitstringbot.

(* We define the equivalence used internally by the command "move array" *)

define move_array_internal_macro(T) {

param N, NX, Neq.

equiv move_array(T)
      foreach i<=N do X <-R T; (foreach iX <= NX do OX() := return(X) |
                      	        foreach ieq <= Neq do Oeq(X':T) := return(X' = X))
<=(#Oeq / |T|)=> [manual,computational]
      foreach i<=N do (foreach iX <= NX do OX() := find[unique] j<=NX suchthat defined(Y[j]) then return(Y[j]) else Y <-R T; return(Y) |
              	       foreach ieq <= Neq do Oeq(X':T) := find[unique] j<=NX suchthat defined(Y[j]) then return(X' = Y[j]) else return(false)).

}

(***************************** Symmetric encryption *********************************************)


(* IND-CPA probabilistic symmetric encryption 
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   key: type of keys, must be "bounded"
   cleartext: type of cleartexts
   ciphertext: type of ciphertexts
   seed: type of random seeds for encryption, must be "fixed"

   kgen: key generation function 
   enc: encryption function
   dec: decryption function
   injbot: natural injection from cleartext to bitstringbot
   Z: function that returns for each cleartext a cleartext of the same length consisting only of zeroes.

   Penc(t, N, l): probability of breaking the IND-CPA property in time
   t for one key and N encryption queries with cleartexts of length at
   most l

   The types keyseed, key, cleartext, ciphertext, seed and the
   probability Penc must be declared before this macro is
   expanded. The functions kgen, enc, dec, injbot, and Z are declared
   by this macro. They must not be declared elsewhere, and they can be
   used only after expanding the macro.  
*)

define IND_CPA_sym_enc(keyseed, key, cleartext, ciphertext, seed, kgen, enc, dec, injbot, Z, Penc) { 

param N, N2.

fun enc(cleartext, key, seed): ciphertext.
fun kgen(keyseed):key.
fun dec(ciphertext, key): bitstringbot.

fun enc2(cleartext, key, seed): ciphertext.
fun kgen2(keyseed):key.

fun injbot(cleartext):bitstringbot [compos].
(* The function Z returns for each bitstring, a bitstring
   of the same length, consisting only of zeroes. *)
fun Z(cleartext):cleartext.

forall x:cleartext; injbot(x) <> bottom.
forall m:cleartext, r:keyseed, r2:seed; 
	dec(enc(m, kgen(r), r2), kgen(r)) = injbot(m).

equiv ind_cpa(enc)
       foreach i2 <= N2 do r <-R keyseed; 
       	       foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := 
	       	       return(enc(x, kgen(r), r2)) 
     <=(N2 * Penc(time + (N2-1)*(time(kgen) + N*time(enc, maxlength(x)) + N*time(Z, maxlength(x))), N, maxlength(x)))=> 
       foreach i2 <= N2 do r <-R keyseed; 
       	       foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := 
	       	       return(enc2(Z(x), kgen2(r), r2)).

}


(* IND-CPA and INT-CTXT probabilistic symmetric encryption 
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   key: type of keys, must be "bounded"
   cleartext: type of cleartexts
   ciphertext: type of ciphertexts
   seed: type of random seeds for encryption, must be "fixed"

   kgen: key generation function 
   enc: encryption function
   dec: decryption function
   injbot: natural injection from cleartext to bitstringbot
   Z: function that returns for each cleartext a cleartext of the same length consisting only of zeroes.

   Penc(t, N, l): probability of breaking the IND-CPA property in time
   t for one key and N encryption queries with cleartexts of length at
   most l
   Pencctxt(t, N, N', l, l'): probability of breaking the INT-CTXT property
   in time t for one key, N encryption queries, N' decryption queries with
   cleartexts of length at most l and ciphertexts of length at most l'.

   The types keyseed, key, cleartext, ciphertext, seed and the
   probabilities Penc, Pencctxt must be declared before this macro is
   expanded. The functions kgen, enc, dec, injbot, and Z are declared
   by this macro. They must not be declared elsewhere, and they can be
   used only after expanding the macro.
*)


define IND_CPA_INT_CTXT_sym_enc(keyseed, key, cleartext, ciphertext, seed, kgen, enc, dec, injbot, Z, Penc, Pencctxt) { 

param N, N2, N3.

fun enc(cleartext, key, seed): ciphertext.
fun kgen(keyseed):key.
fun dec(ciphertext, key): bitstringbot.

fun enc2(cleartext, key, seed): ciphertext.
fun kgen2(keyseed):key.

fun injbot(cleartext):bitstringbot [compos].
forall x:cleartext; injbot(x) <> bottom.

(* The function Z returns for each bitstring, a bitstring
   of the same length, consisting only of zeroes. *)
fun Z(cleartext):cleartext.

forall m:cleartext, r:keyseed, r2:seed; 
	dec(enc(m, kgen(r), r2), kgen(r)) = injbot(m).

	(* IND-CPA *)

equiv ind_cpa(enc)
       foreach i2 <= N2 do r <-R keyseed; 
       	       foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := 
	       	       return(enc(x, kgen2(r), r2))
     <=(N2 * Penc(time + (N2-1)*(time(kgen) + N*time(enc, maxlength(x)) + N*time(Z, maxlength(x))), N, maxlength(x)))=> 
       foreach i2 <= N2 do r <-R keyseed; 
       	       foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := 
	       	       return(enc2(Z(x), kgen2(r), r2)).

	(* INT-CTXT *)

equiv int_ctxt(enc)
      foreach i2 <= N2 do r <-R keyseed; (
      	      foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := return(enc(x, kgen(r), r2)) |
	      foreach i3 <= N3 do Odec(y:ciphertext) := return(dec(y,kgen(r))))
     <=(N2 * Pencctxt(time + (N2-1)*(time(kgen) + N*time(enc, maxlength(x)) + N3*time(dec,maxlength(y))), N, N3, maxlength(x), maxlength(y)))=> [computational] 
      foreach i2 <= N2 do r <-R keyseed [unchanged]; (
      	      foreach i <= N do r2 <-R seed [unchanged]; Oenc(x:cleartext) := z:ciphertext <- enc(x, kgen2(r), r2); return(z) |
	      foreach i3 <= N3 do Odec(y:ciphertext) := find j <= N suchthat defined(x[j],r2[j],z[j]) && z[j] = y then return(injbot(x[j])) else return(bottom)).

}

(* IND-CCA2 and INT-PTXT probabilistic symmetric encryption 
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   key: type of keys, must be "bounded"
   cleartext: type of cleartexts
   ciphertext: type of ciphertexts
   seed: type of random seeds for encryption, must be "fixed"

   kgen: key generation function 
   enc: encryption function
   dec: decryption function
   injbot: natural injection from cleartext to bitstringbot
   Z: function that returns for each cleartext a cleartext of the same length consisting only of zeroes.

   Penc(t, N, N', l, l'): probability of breaking the IND-CCA2 property
   in time t for one key, N encryption queries, N' decryption queries with
   cleartexts of length at most l and ciphertexts of length at most l'.
   Pencptxt(t, N, N', l, l'): probability of breaking the INT-PTXT property
   in time t for one key, N encryption queries, N' decryption queries with
   cleartexts of length at most l and ciphertexts of length at most l'.

   The types keyseed, key, cleartext, ciphertext, seed and the
   probabilities Penc, Pencctxt must be declared before this macro is
   expanded. The functions kgen, enc, dec, injbot, and Z are declared
   by this macro. They must not be declared elsewhere, and they can be
   used only after expanding the macro.
*)

define IND_CCA2_INT_PTXT_sym_enc(keyseed, key, cleartext, ciphertext, seed, kgen, enc, dec, injbot, Z, Penc, Pencptxt) { 

param N, N2, N3.

fun enc(cleartext, key, seed): ciphertext.
fun kgen(keyseed):key.
fun dec(ciphertext, key): bitstringbot.

fun enc2(cleartext, key, seed): ciphertext.
fun kgen2(keyseed):key.
fun dec2(ciphertext, key): bitstringbot.

fun injbot(cleartext):bitstringbot [compos].
forall x:cleartext; injbot(x) <> bottom.

(* The function Z returns for each bitstring, a bitstring
   of the same length, consisting only of zeroes. *)
fun Z(cleartext):cleartext.

forall m:cleartext, r:keyseed, r2:seed; 
	dec(enc(m, kgen(r), r2), kgen(r)) = injbot(m).

	(* IND-CCA2 *)

equiv ind_cca2(enc)
       foreach i2 <= N2 do r <-R keyseed; (
       	       foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := return(enc(x, kgen(r), r2)) |
               foreach i3 <= N3 do Odec(y:ciphertext) := return(dec2(y,kgen(r))))
     <=(N2 * Penc(time + (N2-1)*(time(kgen) + N*time(enc, maxlength(x)) + N*time(Z, maxlength(x)) + N3*time(dec,maxlength(y))), N, N3, maxlength(x), maxlength(y)))=> 
       foreach i2 <= N2 do r <-R keyseed; (
       	       foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := z:ciphertext <- enc2(Z(x), kgen2(r), r2); return(z) |
	       foreach i3 <= N3 do Odec(y:ciphertext) := find j <= N suchthat defined(x[j],r2[j],z[j]) && y = z[j] then return(injbot(x[j])) else return(dec2(y, kgen2(r)))).

	(* INT-PTXT *)

equiv int_ptxt(enc)
      foreach i2 <= N2 do r <-R keyseed; (
      	      foreach i <= N do r2 <-R seed; Oenc(x:cleartext) := return(enc(x, kgen(r), r2)) |
	      foreach i3 <= N3 do Odec(y:ciphertext) := return(dec(y,kgen(r)))) 
     <=(N2 * Pencptxt(time + (N2-1)*(time(kgen) + N*time(enc, maxlength(x)) + N*time(Z, maxlength(x)) + N3*time(dec,maxlength(y))), N, N3, maxlength(x), maxlength(y)))=> [computational] 
      foreach i2 <= N2 do r <-R keyseed [unchanged]; (
      	      foreach i <= N do r2 <-R seed [unchanged]; Oenc(x:cleartext) := return(enc(x, kgen(r), r2)) |
	      foreach i3 <= N3 do Odec(y:ciphertext) := 
				z <- dec2(y, kgen(r));
                                find j <= N suchthat defined(x[j]) && z = injbot(x[j]) then return(injbot(x[j])) else return(bottom)).

}

(* SPRP block cipher
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   key: type of keys, must be "bounded"
   blocksize: type of the input and output of the cipher, must be "fixed" and "large".
   (The modeling of SPRP block ciphers 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".)

   kgen: key generation function 
   enc: encryption function
   dec: decryption function

   Penc(t, N, N'): probability of breaking the SPRP property
   in time t for one key, N encryption queries, and N' decryption queries.

   The types keyseed, key, blocksize and the probability Penc must be
   declared before this macro is expanded. The functions kgen, enc,
   dec are declared by this macro. They must not be declared
   elsewhere, and they can be used only after expanding the macro.

 *)


define SPRP_cipher(keyseed, key, blocksize, kgen, enc, dec, Penc) {

param N, N2, N3.

fun enc(blocksize, key): blocksize.
fun kgen(keyseed):key.
fun dec(blocksize, key): blocksize.

forall m:blocksize, r:keyseed; 
	dec(enc(m, kgen(r)), kgen(r)) = m.

equiv sprp(enc)
       foreach i3 <= N3 do r <-R keyseed; (
       	       foreach i <= N do Oenc(x:blocksize) := return(enc(x, kgen(r))) |
	       foreach i2 <= N2 do Odec(m:blocksize) := return(dec(m, kgen(r))))
     <=(N3 * (Penc(time + (N3-1)*(time(kgen) + N*time(enc) + N2*time(dec)), N, N2) + (N+N2)*(N+N2-1)/|blocksize|))=>
       foreach i3 <= N3 do r <-R keyseed; (
       	       foreach i <= N do Oenc(x:blocksize) :=
		find[unique] j<=N suchthat defined(x[j],r2[j]) && x = x[j] then return(r2[j])
		orfind k<=N2 suchthat defined(r4[k],m[k]) && x = r4[k] then return(m[k])
		else r2 <-R blocksize; return(r2) |
	       foreach i2 <= N2 do Odec(m:blocksize) :=
		find[unique] j<=N suchthat defined(x[j],r2[j]) && m = r2[j] then return(x[j]) 
		orfind k<=N2 suchthat defined(r4[k],m[k]) && m = m[k] then return(r4[k]) 
		else r4 <-R blocksize; return(r4)).

}

(* PRP block cipher
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   key: type of keys, must be "bounded"
   blocksize: type of the input and output of the cipher, must be "fixed" and "large".
   (The modeling of PRP block ciphers 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. In
   other words, we model a PRF rather than a PRP, and apply the
   PRF/PRP switching lemma to make sure that this is sound. Then
   CryptoVerif needs to eliminate collisions between those random
   numbers, so blocksize must really be "large".)

   kgen: key generation function 
   enc: encryption function
   dec: decryption function

   Penc(t, N): probability of breaking the PRP property
   in time t for one key and N encryption queries.

   The types keyseed, key, blocksize and the probability Penc must be
   declared before this macro is expanded. The functions kgen, enc,
   dec are declared by this macro. They must not be declared
   elsewhere, and they can be used only after expanding the macro.

 *)


define PRP_cipher(keyseed, key, blocksize, kgen, enc, dec, Penc) {

param N, N2, N3.

fun enc(blocksize, key): blocksize.
fun kgen(keyseed):key.
fun dec(blocksize, key): blocksize.

forall m:blocksize, r:keyseed; 
	dec(enc(m, kgen(r)), kgen(r)) = m.

equiv prp(enc)
       foreach i3 <= N3 do r <-R keyseed; 
       	       foreach i <= N do Oenc(x:blocksize) := return(enc(x, kgen(r)))
     <=(N3 * (Penc(time + (N3-1)*(time(kgen) + N*time(enc)), N) + N * (N-1) / |blocksize|))=>
       foreach i3 <= N3 do r <-R keyseed; 
       	       foreach i <= N do Oenc(x:blocksize) := 
		find[unique] j<=N suchthat defined(x[j],r2[j]) && x = x[j] then return(r2[j])
		else r2 <-R blocksize; return(r2).

}

(* Ideal Cipher Model
   cipherkey: type of keys that correspond to the choice of the scheme, must be "fixed"
   key: type of keys (typically "large")
   blocksize: type of the input and output of the cipher, must be "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 such as
   	 (foreach iE <= qE do OencA(x:blocksize, ke:key) := return(enc(ck,x,ke)))
       | (foreach iD <= qD do OdecA(m:blocksize, kd:key) := return(dec(ck,m,kd)))
   where qE is the number of requests to the encryption oracle,
   qD the number of requests to the decryption oracle,
   ck the cipherkey.
   
   The types cipherkey, key, blocksize must be declared before this macro is
   expanded. The functions enc, dec are declared by this macro. They
   must not be declared elsewhere, and they can be used only after
   expanding the macro.

 *)

define ICM_cipher(cipherkey, key, blocksize, enc, dec) {

param Ne, Nd, Nck.

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

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

equiv icm(enc)
       foreach ick <= Nck do ck <-R cipherkey;
         (foreach ie <= Ne do Oenc(me:blocksize, ke:key) := return(enc(ck, me, ke)) |
          foreach id <= Nd do Odec(md:blocksize, kd:key) := return(dec(ck, md, kd)))
     <=((#Oenc+#Odec)*(#Oenc+#Odec-1)/|blocksize|)=> [computational]
       foreach ick <= Nck do 
         (foreach ie <= Ne do Oenc(me:blocksize, ke:key) :=
		find[unique] j<=Ne suchthat defined(me[j],ke[j],re[j]) && me = me[j] && ke = ke[j] then return(re[j]) 
		orfind k<=Nd suchthat defined(rd[k],md[k],kd[k]) && me = rd[k] && ke = kd[k] then return(md[k]) 
		else re <-R blocksize; return(re) |
          foreach id <= Nd do Odec(md:blocksize, kd:key) :=
		find[unique] j<=Ne suchthat defined(me[j],ke[j],re[j]) && md = re[j] && kd = ke[j] then return(me[j]) 
		orfind k<=Nd suchthat defined(rd[k],md[k],kd[k]) && md = md[k] && kd = kd[k] then return(rd[k]) 
		else rd <-R blocksize; return(rd)).

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

(*When CryptoVerif will support parametric processes 
param qE, qD [noninteractive].
let enc_dec_oracle(ck) = (foreach iE <= qE do OencA(x:blocksize, ke:key) := return(enc(ck,x,ke)))
                       | (foreach iD <= qD do OdecA(m:blocksize, kd:key) := return(dec(ck,m,kd))). 
*)

}


(*************************************** MACs ***************************************)


(* UF-CMA mac 
   mkeyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   mkey: type of keys, must be "bounded"
   macinput: type of inputs of MACs
   macres: type of result of MACs

   mkgen: key generation function 
   mac: MAC function
   check: verification function

   Pmac(t, N, N', l): probability of breaking the UF-CMA property in
   time t for one key, N MAC queries, N' verification queries for
   messages of length at most l.

   The types mkeyseed, mkey, macinput, macres and the probability Pmac
   must be declared before this macro is expanded. The functions
   mkgen, mac, check are declared by this macro. They must not be
   declared elsewhere, and they can be used only after expanding the
   macro.

*)

define UF_CMA_mac(mkeyseed, mkey, macinput, macres, mkgen, mac, check, Pmac) {

param N, N2, N3.

const mark: bitstring.

fun mac(macinput, mkey):macres.
fun check(macinput, mkey, macres): bool.
fun mkgen(mkeyseed):mkey.

fun mac2(macinput, mkey):macres.
fun check2(macinput, mkey, macres): bool.
fun mkgen2(mkeyseed):mkey.

forall m:macinput, r:mkeyseed;
	check(m, mkgen(r), mac(m, mkgen(r))).
forall m:macinput, r:mkeyseed;
	check2(m, mkgen2(r), mac2(m, mkgen2(r))).

equiv uf_cma(mac)
      foreach i3 <= N3 do r <-R mkeyseed;(
	 foreach i <= N do Omac(x: macinput):= return(mac(x, mkgen(r))) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) := return(check(m, mkgen(r), ma)))
     <=(N3 * Pmac(time + (N3-1)*(time(mkgen) + N*time(mac,maxlength(x)) + N2*time(check,maxlength(m),maxlength(ma))), N, N2, max(maxlength(x), maxlength(m))))=> [computational]
      foreach i3 <= N3 do r <-R mkeyseed [unchanged];(
	 foreach i <= N do Omac(x: macinput) := return(mac2(x, mkgen2(r))) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) :=
	    find j <= N suchthat defined(x[j]) && (m = x[j]) && check2(x[j], mkgen2(r), ma) then return(true) else return(false)).

equiv uf_cma_corrupt(mac)
      foreach i3 <= N3 do r <-R mkeyseed;(
	 foreach i <= N do Omac(x: macinput)[useful_change] := return(mac(x, mkgen(r))) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) [useful_change] := return(check(m, mkgen(r), ma)) |
	 Ocorrupt() [10] := return(r))
     <=(N3 * Pmac(time + (N3-1)*(time(mkgen) + N*time(mac,maxlength(x)) + N2*time(check,maxlength(m),maxlength(ma))), N, N2, max(maxlength(x), maxlength(m))))=> [manual,computational]
      foreach i3 <= N3 do r <-R mkeyseed [unchanged];(
	 foreach i <= N do Omac(x: macinput) := return(mac2(x, mkgen2(r))) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) :=
	    if defined(corrupt) then return(check2(m, mkgen2(r), ma)) else
	    find j <= N suchthat defined(x[j]) && (m = x[j]) && check2(x[j], mkgen2(r), ma) then return(true) else return(false) |
	 Ocorrupt() := let corrupt: bitstring = mark in return(r)).

}

(* SUF-CMA mac (strongly unforgeable MAC)
   The difference between a UF-CMA MAC and a SUF-CMA MAC is that, for a UF-CMA MAC, the adversary may
   easily forge a new MAC for a message for which he has already seen a MAC. Such a forgery is guaranteed 
   to be hard for a SUF-CMA MAC.
 
   mkeyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   mkey: type of keys, must be "bounded"
   macinput: type of inputs of MACs
   macres: type of result of MACs

   mkgen: key generation function 
   mac: MAC function
   check: verification function

   Pmac(t, N, N', l): probability of breaking the SUF-CMA property in
   time t for one key, N MAC queries, N' verification queries for
   messages of length at most l.

   The types mkeyseed, mkey, macinput, macres and the probability Pmac
   must be declared before this macro is expanded. The functions
   mkgen, mac, check are declared by this macro. They must not be
   declared elsewhere, and they can be used only after expanding the
   macro.

*)

define SUF_CMA_mac(mkeyseed, mkey, macinput, macres, mkgen, mac, check, Pmac) {

param N, N2, N3.

const mark: bitstring.

fun mac(macinput, mkey):macres.
fun check(macinput, mkey, macres): bool.
fun mkgen(mkeyseed):mkey.

fun mac2(macinput, mkey):macres.
fun mkgen2(mkeyseed):mkey.

forall m:macinput, r:mkeyseed;
	check(m, mkgen(r), mac(m, mkgen(r))).

equiv suf_cma(mac)
      foreach i3 <= N3 do r <-R mkeyseed;(
	 foreach i <= N do Omac(x: macinput) := return(mac(x, mkgen(r))) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) := return(check(m, mkgen(r), ma)))
     <=(N3 * Pmac(time + (N3-1)*(time(mkgen) + N*time(mac,maxlength(x)) + N2*time(check,maxlength(m),maxlength(ma))), N, N2, max(maxlength(x), maxlength(m))))=> [computational]
      foreach i3 <= N3 do r <-R mkeyseed [unchanged];(
	 foreach i <= N do Omac(x: macinput) := let ma2:macres = mac2(x, mkgen2(r)) in return(ma2) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) :=
	    find j <= N suchthat defined(x[j], ma2[j]) && (m = x[j]) && ma = ma2[j] then return(true) else return(false)).

equiv suf_cma_corrupt(mac)
      foreach i3 <= N3 do r <-R mkeyseed;(
	 foreach i <= N do Omac(x: macinput) [useful_change] := return(mac(x, mkgen(r))) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) [useful_change] := return(check(m, mkgen(r), ma)) |
	 Ocorrupt() [10] := return(r))
     <=(N3 * Pmac(time + (N3-1)*(time(mkgen) + N*time(mac,maxlength(x)) + N2*time(check,maxlength(m),maxlength(ma))), N, N2, max(maxlength(x), maxlength(m))))=> [manual,computational]
      foreach i3 <= N3 do r <-R mkeyseed [unchanged];(
	 foreach i <= N do Omac(x: macinput) := let ma2:macres = mac2(x, mkgen2(r)) in return(ma2) |
	 foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) :=
	    if defined(corrupt) then return(check(m, mkgen2(r), ma)) else
	    find j <= N suchthat defined(x[j], ma2[j]) && (m = x[j]) && ma = ma2[j] then return(true) else return(false) |
	 Ocorrupt() := let corrupt: bitstring = mark in return(r)).

}

(******************************* Public-key encryption *******************************)

(* IND-CCA2 probabilistic public-key encryption 
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   pkey: type of public keys, must be "bounded"
   skey: type of secret keys, must be "bounded"
   cleartext: type of cleartexts, must be "bounded" or "fixed" (the encryptions of *all* cleartexts of any length
   	      are assumed to be indistinguishable from each other).
   ciphertext: type of ciphertexts
   seed: type of random seeds for encryption, must be "fixed"

   pkgen: public-key generation function 
   skgen: secret-key generation function
   enc: encryption function
   dec: decryption function
   injbot: natural injection from cleartext to bitstringbot
   Z: a constant cleartext

   Penc(t, N): probability of breaking the IND-CCA2 property
   in time t for one key and N decryption queries.
   Penccoll: probability of collision between independently generated keys

   The types keyseed, pkey, skey, cleartext, ciphertext, seed and the
   probabilities Penc, Penccoll must be declared before this macro is
   expanded. The functions pkgen, skgen, enc, dec, injbot, and the
   constant Z are declared by this macro. They must not be declared
   elsewhere, and they can be used only after expanding the macro. 
*)


define IND_CCA2_public_key_enc(keyseed, pkey, skey, cleartext, ciphertext, seed, skgen, pkgen, enc, dec, injbot, Z, Penc, Penccoll) {

param N, N2, N3, N4.

fun enc(cleartext, pkey, seed): ciphertext.
fun skgen(keyseed):skey.
fun pkgen(keyseed):pkey.
fun dec(ciphertext, skey): bitstringbot.

fun enc2(cleartext, pkey, seed): ciphertext.
fun skgen2(keyseed):skey.
fun pkgen2(keyseed):pkey.
fun dec2(ciphertext, skey): bitstringbot.

fun injbot(cleartext):bitstringbot [compos].

const Z:cleartext.

forall m:cleartext, r:keyseed, r2:seed; 
	dec(enc(m, pkgen(r), r2), skgen(r)) = injbot(m).
forall m:cleartext, r:keyseed, r2:seed; 
	dec2(enc2(m, pkgen2(r), r2), skgen2(r)) = injbot(m).

equiv ind_cca2(enc)
       foreach i3 <= N3 do r <-R keyseed; (
           Opk() [2] := return(pkgen(r)) |
	   foreach i2 <= N2 do Odec(m:ciphertext) := return(dec(m, skgen(r))) |
           foreach i <= N do r1 <-R seed; Oenc(x1:cleartext) := return(enc(x1, pkgen(r),r1))) |
       foreach i4 <= N4 do r2 <-R seed; Oenc2(x:cleartext, y:pkey) [3] := return(enc(x,y,r2)) [all]
     <=((N3 * N + N4) * Penc(time + (N4+N-1) * time(enc) + (N3-1)*(time(pkgen) + time(skgen) + N2 * time(dec, maxlength(m)) + N * time(enc)), N2))=> 
       foreach i3 <= N3 do r <-R keyseed; (
           Opk() := return(pkgen2(r)) |
	   foreach i2 <= N2 do Odec(m:ciphertext) :=
                find j <= N suchthat defined(m1[j],x1[j]) && m = m1[j] then return(injbot(x1[j])) else
		find j <= N4 suchthat defined(m2[j],y[j],x[j]) &&
		y[j] = pkgen2(r) && m = m2[j] then return(injbot(x[j])) else return(dec2(m, skgen2(r))) |
	   foreach i <= N do r1 <-R seed; Oenc(x1:cleartext) :=
			m1:ciphertext <- enc2(Z, pkgen2(r), r1);
			return(m1)) |
       foreach i4 <= N4 do Oenc2(x:cleartext, y:pkey) :=
		find k <= N3 suchthat defined(r[k]) && y = pkgen2(r[k]) then
			(r2 <-R seed; 
			m2:ciphertext <- enc2(Z, y, r2);
			return(m2))
		else r3 <-R seed; return(enc(x,y,r3)).

collision r1 <-R keyseed; r2 <-R keyseed; 
	return(pkgen(r1) = pkgen(r2)) <=(Penccoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(pkgen2(r1) = pkgen2(r2)) <=(Penccoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(skgen(r1) = skgen(r2)) <=(Penccoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(skgen2(r1) = skgen2(r2)) <=(Penccoll)=> return(false).

}

(*************************************** Signatures ******************************)

(* UF-CMA probabilistic signatures 
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   pkey: type of public keys, must be "bounded"
   skey: type of secret keys, must be "bounded"
   signinput: type of inputs of signatures
   signature: type of signatures
   seed: type of random seeds for signatures, must be "fixed"

   pkgen: public-key generation function 
   skgen: secret-key generation function
   sign: signature function
   check: verification function

   Psign(t, N, l): probability of breaking the UF-CMA property
   in time t, for one key, N signature queries with messages of length
   at most l.
   Psigncoll: probability of collision between independently generated keys

   The types keyseed, pkey, skey, signinput, signature, seed and the
   probabilities Psign, Psigncoll must be declared before this macro
   is expanded. The functions pkgen, skgen, sign, and check are
   declared by this macro. They must not be declared elsewhere, and
   they can be used only after expanding the macro.  
*)

define UF_CMA_signature(keyseed, pkey, skey, signinput, signature, seed, skgen, pkgen, sign, check, Psign, Psigncoll) {

param N, N2, N3, N4.

const mark: bitstring.

fun sign(signinput, skey, seed): signature.
fun skgen(keyseed):skey.
fun pkgen(keyseed):pkey.
fun check(signinput, pkey, signature): bool.

fun sign2(signinput, skey, seed): signature.
fun skgen2(keyseed):skey.
fun pkgen2(keyseed):pkey.
fun check2(signinput, pkey, signature): bool.

forall m:signinput, r:keyseed, r2:seed; 
	check(m, pkgen(r), sign(m, skgen(r), r2)) = true.
forall m:signinput, r:keyseed, r2:seed; 
	check2(m, pkgen2(r), sign2(m, skgen2(r), r2)) = true.

equiv uf_cma(sign)
       foreach i3 <= N3 do r <-R keyseed; (
           Opk() [2] := return(pkgen(r)) |
	   foreach i2 <= N2 do r2 <-R seed; Osign(x: signinput) := return(sign(x, skgen(r), r2)) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) := return(check(m1, pkgen(r), si1))) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) [3] := return(check(m, y, si)) [all]
     <=(N3 * Psign(time + (N4+N-1) * time(check, max(maxlength(m1), maxlength(m)), max(maxlength(si1), maxlength(si))) + (N3-1)*(time(pkgen) + time(skgen) + N2 * time(sign, maxlength(x)) + N * time(check, maxlength(m1), maxlength(si1))), N2, maxlength(x)))=> [computational]
       foreach i3 <= N3 do r <-R keyseed [unchanged]; (
           Opk() := return(pkgen2(r)) |
	   foreach i2 <= N2 do r2 <-R seed [unchanged]; Osign(x: signinput) := return(sign2(x, skgen2(r), r2)) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) := 
                find j <= N2 suchthat defined(x[j]) && m1 = x[j] && check2(m1, pkgen2(r), si1) then return(true) else return(false)) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) :=
		find j <= N2, k <= N3 suchthat defined(x[j,k],r[k]) && y = pkgen2(r[k]) && m = x[j,k] && check2(m, y, si) then return(true) else
		find k <= N3 suchthat defined(r[k]) && y = pkgen2(r[k]) then return(false) else
		return(check(m,y,si)).

equiv uf_cma_corrupt(sign)
       foreach i3 <= N3 do r <-R keyseed; (
           Opk() [useful_change] [2] := return(pkgen(r)) |
	   foreach i2 <= N2 do r2 <-R seed; Osign(x: signinput) [useful_change] := return(sign(x, skgen(r), r2)) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) [useful_change] := return(check(m1, pkgen(r), si1)) |
	   Ocorrupt() [10] := return(r)) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) [3] := return(check(m, y, si)) [all]
     <=(N3 * Psign(time + (N4+N-1) * time(check, max(maxlength(m1), maxlength(m)), max(maxlength(si1), maxlength(si))) + (N3-1)*(time(pkgen) + time(skgen) + N2 * time(sign, maxlength(x)) + N * time(check, maxlength(m1), maxlength(si1))), N2, maxlength(x)))=> [manual,computational]
       foreach i3 <= N3 do r <-R keyseed [unchanged]; (
           Opk() := return(pkgen2(r)) |
	   foreach i2 <= N2 do r2 <-R seed [unchanged]; Osign(x: signinput) := return(sign2(x, skgen2(r), r2)) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) := 
	        if defined(corrupt) then return(check2(m1, pkgen2(r), si1)) else
                find j <= N2 suchthat defined(x[j]) && m1 = x[j] && check2(m1, pkgen2(r), si1) then return(true) else return(false) |
	   Ocorrupt() := let corrupt: bitstring = mark in return(r)) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) :=
		find k <= N3 suchthat defined(r[k],corrupt[k]) && y = pkgen2(r[k]) then return(check2(m, y, si)) else
		find j <= N2, k <= N3 suchthat defined(x[j,k],r[k]) && y = pkgen2(r[k]) && m = x[j,k] && check2(m, y, si) then return(true) else
		find k <= N3 suchthat defined(r[k]) && y = pkgen2(r[k]) then return(false) else
		return(check(m,y,si)).

collision r1 <-R keyseed; r2 <-R keyseed; 
	return(pkgen(r1) = pkgen(r2)) <=(Psigncoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(pkgen2(r1) = pkgen2(r2)) <=(Psigncoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(skgen(r1) = skgen(r2)) <=(Psigncoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(skgen2(r1) = skgen2(r2)) <=(Psigncoll)=> return(false).

}

(* SUF-CMA probabilistic signatures 
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   pkey: type of public keys, must be "bounded"
   skey: type of secret keys, must be "bounded"
   signinput: type of inputs of signatures
   signature: type of signatures
   seed: type of random seeds for signatures, must be "fixed"

   pkgen: public-key generation function 
   skgen: secret-key generation function
   sign: signature function
   check: verification function

   Psign(t, N, l): probability of breaking the SUF-CMA property
   in time t, for one key, N signature queries with messages of length
   at most l.
   Psigncoll: probability of collision between independently generated keys

   The types keyseed, pkey, skey, signinput, signature, seed and the
   probabilities Psign, Psigncoll must be declared before this macro
   is expanded. The functions pkgen, skgen, sign, and check are
   declared by this macro. They must not be declared elsewhere, and
   they can be used only after expanding the macro.  
*)

define SUF_CMA_signature(keyseed, pkey, skey, signinput, signature, seed, skgen, pkgen, sign, check, Psign, Psigncoll) {

param N, N2, N3, N4.

const mark: bitstring.

fun sign(signinput, skey, seed): signature.
fun skgen(keyseed):skey.
fun pkgen(keyseed):pkey.
fun check(signinput, pkey, signature): bool.

fun sign2(signinput, skey, seed): signature.
fun skgen2(keyseed):skey.
fun pkgen2(keyseed):pkey.
fun check2(signinput, pkey, signature): bool.

forall m:signinput, r:keyseed, r2:seed; 
	check(m, pkgen(r), sign(m, skgen(r), r2)) = true.
forall m:signinput, r:keyseed, r2:seed; 
	check2(m, pkgen2(r), sign2(m, skgen2(r), r2)) = true.

equiv suf_cma(sign)
       foreach i3 <= N3 do r <-R keyseed; (
           Opk() [2] := return(pkgen(r)) |
	   foreach i2 <= N2 do r2 <-R seed; Osign(x: signinput) := return(sign(x, skgen(r), r2)) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) := return(check(m1, pkgen(r), si1))) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) [3] := return(check(m, y, si)) [all]
     <=(N3 * Psign(time + (N4+N-1) * time(check, max(maxlength(m), maxlength(m1)), max(maxlength(si), maxlength(si1))) + (N3-1)*(time(pkgen) + time(skgen) + N2 * time(sign, maxlength(x)) + N * time(check, maxlength(m1), maxlength(si1))), N2, maxlength(x)))=> [computational]
       foreach i3 <= N3 do r <-R keyseed [unchanged]; (
           Opk() := return(pkgen2(r)) |
	   foreach i2 <= N2 do r2 <-R seed [unchanged]; Osign(x: signinput) := let s: signature = sign2(x, skgen2(r), r2) in return(s) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) := 
                find j <= N2 suchthat defined(x[j],s[j]) && m1 = x[j] && si1 = s[j] then return(true) else return(false)) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) :=
		find j <= N2, k <= N3 suchthat defined(x[j,k],r[k],s[j,k]) && y = pkgen2(r[k]) && m = x[j,k] && si = s[j,k] then return(true) else
		find k <= N3 suchthat defined(r[k]) && y = pkgen2(r[k]) then return(false) else
		return(check(m,y,si)).

equiv suf_cma_corrupt(sign)
       foreach i3 <= N3 do r <-R keyseed; (
           Opk() [useful_change] [2] := return(pkgen(r)) |
	   foreach i2 <= N2 do r2 <-R seed; Osign(x: signinput) [useful_change] := return(sign(x, skgen(r), r2)) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) [useful_change] := return(check(m1, pkgen(r), si1)) |
	   Ocorrupt() [10] := return(r)) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) [3] := return(check(m, y, si)) [all]
     <=(N3 * Psign(time + (N4+N-1) * time(check, max(maxlength(m), maxlength(m1)), max(maxlength(si), maxlength(si1))) + (N3-1)*(time(pkgen) + time(skgen) + N2 * time(sign, maxlength(x)) + N * time(check, maxlength(m1), maxlength(si1))), N2, maxlength(x)))=> [manual,computational]
       foreach i3 <= N3 do r <-R keyseed [unchanged]; (
           Opk() := return(pkgen2(r)) |
	   foreach i2 <= N2 do r2 <-R seed [unchanged]; Osign(x: signinput) := let s: signature = sign2(x, skgen2(r), r2) in return(s) |
	   foreach i <= N do Ocheck(m1: signinput, si1:signature) := 
	        if defined(corrupt) then return(check2(m1, pkgen2(r), si1)) else
                find j <= N2 suchthat defined(x[j],s[j]) && m1 = x[j] && si1 = s[j] then return(true) else return(false) |
	   Ocorrupt() := let corrupt: bitstring = mark in return(r)) |
       foreach i4 <= N4 do Ocheck2(m: signinput, y: pkey, si: signature) :=
		find k <= N3 suchthat defined(r[k],corrupt[k]) && y = pkgen2(r[k]) then return(check2(m, y, si)) else
		find j <= N2, k <= N3 suchthat defined(x[j,k],r[k],s[j,k]) && y = pkgen2(r[k]) && m = x[j,k] && si = s[j,k] then return(true) else
		find k <= N3 suchthat defined(r[k]) && y = pkgen2(r[k]) then return(false) else
		return(check(m,y,si)).

collision r1 <-R keyseed; r2 <-R keyseed; 
	return(pkgen(r1) = pkgen(r2)) <=(Psigncoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(pkgen2(r1) = pkgen2(r2)) <=(Psigncoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(skgen(r1) = skgen(r2)) <=(Psigncoll)=> return(false).
collision r1 <-R keyseed; r2 <-R keyseed; 
	return(skgen2(r1) = skgen2(r2)) <=(Psigncoll)=> return(false).

}

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

(* 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 "fixed"
   hashinput: type of the input of the hash function
   hashoutput: type of the output of the hash function, must be "fixed" and "large"

   hash: the hash function.
   WARNING: hash 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 a process such as
      foreach iH <= qH do OH(x:hashinput) := return(hash(k,x))
   where k is the key, qH the number of requests to the hash oracle.

   The types key, hashinput, and hashoutput must be declared before
   this macro. The function hash is defined by this macro. It must not
   be declared elsewhere, and it can be used only after expanding the
   macro.


 *)

define ROM_hash(key, hashinput, hashoutput, hash (*, hashoracle, qH*)) {

param Nh, N, Neq.

fun hash(key, hashinput):hashoutput.

equiv rom(hash)
      foreach ih <= Nh do k <-R key;
        (foreach i <= N do OH(x:hashinput) := return(hash(k,x)) |
         foreach ieq <= Neq do Oeq(x':hashinput, r':hashoutput) := return(r' = hash(k,x')))
       <=(#Oeq / |hashoutput|)=> [computational]
      foreach ih <= Nh do 
        (foreach i <= N do OH(x:hashinput) := 
	   find[unique] u <= N suchthat defined(x[u],r[u]) && x= x[u] then return(r[u]) else r <-R hashoutput; return(r) |
         foreach ieq <= Neq do Oeq(x':hashinput, r':hashoutput) := 
           find[unique] u <= N suchthat defined(x[u],r[u]) && x' = x[u] then return(r' = r[u]) else
	   return(false)).

(* When CryptoVerif will support parametric processes
param qH [noninteractive].
let hashoracle(k) = 
        foreach iH <= qH do
	OH(x:hashinput) :=
	return(hash(k,x)).
*)
}

(* Collision resistant hash function 
   key: type of the key of the hash function, must be "fixed"
   hashinput: type of the input of the hash function
   hashoutput: type of the output of the hash function

   hash: the hash function.
   Phash: probability of breaking collision resistance.
   WARNING: A collision resistant hash function is a keyed hash function.
   The key must be generated once and for all at the beginning of the game,
   and immediately made available to the adversary.

   The types key, hashinput, hashoutput, and the probability Phash
   must be declared before this macro.  The function hash is defined
   by this macro. It must not be declared elsewhere, and it can be
   used only after expanding the macro.

 *)

define CollisionResistant_hash(key, hashinput, hashoutput, hash, Phash) {

fun hash(key, hashinput):hashoutput.

collision k <-R key; forall x:hashinput, y:hashinput;
	return(hash(k,x) = hash(k,y)) <=(Phash(time))=> return(x = y).

}

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

(* Computational Diffie-Hellman 
   G: type of group elements (must be "fixed" and "large", of cardinal a prime q)
   Z: type of exponents (must be "fixed" and "large", supposed to be 
   {1, ..., q-1})

   g: a generator of the group
   exp: the exponentiation function
   mult: the multiplication function for exponents, product modulo q in
   {1, ..., q-1}, i.e. in the group (Z/qZ)*

   pCDH: the probability of breaking the CDH assumption

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

*)

define CDH(G, Z, g, exp, mult, pCDH) {

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

fun mult(Z,Z): Z [commut]. 

(* exponents multiply *)

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

(* injectivity *)

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

(* collision between products *)

collision x1 <-R Z; x2 <-R Z; x3 <-R Z; x4 <-R Z; 
  return(mult(x1,x2) = mult(x3,x4)) <=(1/|Z|)=> return(false). 

forall x:Z, y:Z, y':Z; 
  (mult(x,y) = mult(x,y')) = (y = y').

(* 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)))
<=(0)=> [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) 
<=(0)=> [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))
<=(0)=> [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))
<=(0)=> [computational]
      foreach iX <= N do X <-R G; OX() := return(X).

(* the CDH assumption *) 

const mark: bitstring.

param na, naDDH, nb, nbDDH.

equiv cdh(exp)
    foreach ia <= na do a <-R Z; (
      OA() := return(exp(g,a)) | 
      Oa() [3] := return(a) |
      foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) [useful_change] := return(m = exp(g, mult(b[j], a)))
    ) |
    foreach ib <= nb do b <-R Z; (
      OB() := return(exp(g,b)) |
      Ob() [3] := return(b) |
      foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) := return(m = exp(g, mult(a[j], b)))
    )
<=((#ODDHa + #ODDHb) * max(1, 7.4*#Oa) * max(1, 7.4*#Ob) * pCDH(time + (na + nb + #ODDHa + #ODDHb) * time(exp)))=> [computational]
    foreach ia <= na do a <-R Z [unchanged]; (
      OA() := return(exp'(g,a)) |
      Oa() := let ka:bitstring = mark in return(a) |
      foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) := 
      	      find u<=nb suchthat defined(kb[u],b[u]) && b[j] = b[u] 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 ib <= nb do b <-R Z [unchanged]; (
      OB() := return(exp'(g,b)) |
      Ob() := let kb:bitstring = mark in return(b) |
      foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) := 
      	      find u<=na suchthat defined(ka[u],a[u]) && a[j] = a[u] 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)
    ).

}

(* Decisional Diffie-Hellman 
   G: type of group elements (must be "fixed" and "large", of cardinal a prime q)
   Z: type of exponents (must be "fixed" and "large", supposed to be 
   {1, ..., q-1})

   g: a generator of the group
   exp: the exponentiation function
   mult: the multiplication function for exponents, product modulo q in
   {1, ..., q-1}, i.e. in the group (Z/qZ)*

   pDDH: the probability of breaking the DDH assumption

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

define DDH(G, Z, g, exp, mult, pDDH) {

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

fun mult(Z,Z): Z [commut]. 

(* exponents multiply *)

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

(* injectivity *)

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

(* collision between products *)

collision x1 <-R Z; x2 <-R Z; x3 <-R Z; x4 <-R Z; 
  return(mult(x1,x2) = mult(x3,x4)) <=(1/|Z|)=> return(false). 

forall x:Z, y:Z, y':Z; 
  (mult(x,y) = mult(x,y')) = (y = y').

(* 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)))
<=(0)=> [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) 
<=(0)=> [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))
<=(0)=> [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))
<=(0)=> [computational]
      foreach iX <= N do X <-R G; OX() := return(X).

(* the DDH assumption *) 

const mark: bitstring.
event ev_abort.

param na, naDH, nb, nbDH.

equiv ddh(exp)
    foreach ia <= na do a <-R Z; (
      OA() := return(exp(g,a)) | 
      Oa() [3] := return (a) |
      foreach iaDH <= naDH do ODHa(j<=nb) [useful_change] := return (exp(g, mult(b[j], a)))
    ) |
    foreach ib <= nb do b <-R Z; (
      OB() := return (exp(g,b)) |
      Ob() [3] := return(b) |
      foreach ibDH <= nbDH do ODHb(j<=na) := return(exp(g, mult(a[j], b)))
    )
<=((#ODHa + #ODHb) * na * nb * pDDH(time + (na + nb + #ODHa + #ODHb) * time(exp)))=>
    foreach ia <= na do a <-R Z; (
      OA() := return(exp'(g,a)) |
      Oa() := 
         find uaDH <= naDH suchthat defined(ka'[uaDH]) then event ev_abort else
	 find ubDH <= nbDH, ub <= nb suchthat defined(kb'[ubDH, ub], a'[ubDH, ub]) && a'[ubDH, ub] = a then event ev_abort else
         let ka:bitstring = mark in return(a) |
      foreach iaDH <= naDH do ODHa(j<=nb) := 
      	 let b':Z = b[j] in
	 find u<=nb suchthat defined(kb[u],b[u]) && b' = b[u] then return(exp'(g, mult(b', a))) else 
         if defined(ka) then return(exp'(g, mult(b', a))) else 
	 let ka':bitstring = mark in
         find vaDH <= naDH suchthat defined(b'[vaDH],ca[vaDH]) && b' = b'[vaDH] then return(ca[vaDH]) else
         find vbDH <= nbDH, vb <= nb suchthat defined(b[vb], a'[vbDH, vb], cb[vbDH, vb]) && b' = b[vb] && a = a'[vbDH, vb] then return(cb[vbDH, vb]) else
	 ca <-R G; return(ca)
    ) |
    foreach ib <= nb do b <-R Z; (
      OB() := return(exp'(g,b)) |
      Ob() := 
         find ubDH <= nbDH suchthat defined(kb'[ubDH]) then event ev_abort else
	 find uaDH <= naDH, ua <= na suchthat defined(ka'[uaDH, ua], b'[uaDH, ua]) && b'[uaDH, ua] = b then event ev_abort else
         let kb:bitstring = mark in return(b) |
      foreach ibDH <= nbDH do ODHb(j<=na) := 
         let a':Z = a[j] in
	 find u<=na suchthat defined(ka[u],a[u]) && a' = a[u] then return(exp'(g, mult(a', b))) else 
         if defined(kb) then return(exp'(g, mult(a', b))) else 
	 let kb':bitstring = mark in
         find vbDH <= nbDH suchthat defined(a'[vbDH],cb[vbDH]) && a' = a'[vbDH] then return(cb[vbDH]) else
         find vaDH <= naDH, va <= na suchthat defined(a[va], b'[vaDH, va], ca[vaDH, va]) && a' = a[va] && b = b'[vaDH, va] then return(ca[vaDH, va]) else
	 cb <-R G; return(cb)
    ).

}

(********************************* Miscellaneous ***************************)

(* One-way trapdoor permutation 
   seed: type of random seeds to generate keys, must be "fixed"
   pkey: type of public keys, must be "bounded"
   skey: type of secret keys, must be "bounded"
   D: type of the input and output of the permutation, must be "fixed"

   pkgen: public-key generation function
   skgen: secret-key generation function
   f: the permutation (taking as argument the public key)
   invf: the inverse permutation of f (taking as argument the secret key,
         i.e. the trapdoor)

   POW(t): probability of breaking the one-wayness property
   in time t, for one key and one permuted value.

   The types seed, pkey, skey, D, and the probability POW must be
   declared before this macro. The functions pkgen, skgen, f, invf
   are defined by this macro. They must not be declared elsewhere, and
   they can be used only after expanding the macro. 
*)

define OW_trapdoor_perm(seed, pkey, skey, D, pkgen, skgen, f, invf, POW) {

param nK, nF, n1.

const mark:bitstring.
fun pkgen(seed):pkey.
fun pkgen'(seed):pkey.
fun skgen(seed):skey.
fun f(pkey, D):D.
fun f'(pkey, D):D.
fun invf(skey, D):D.

(* invf is the inverse of f *)

forall r:seed, x:D; invf(skgen(r), f(pkgen(r), x)) = x.

(* f is the inverse of invf *)

forall r:seed, x:D; f(pkgen(r), invf(skgen(r), x)) = x.

(* Injectivity of f *)

forall k:pkey, x:D, x':D; (f(k,x) = f(k,x')) = (x = x').
forall k:pkey, x:D, x':D; (f'(k,x) = f'(k,x')) = (x = x').

(* injectivity of invf *)

forall k:skey, x:D, x':D; (invf(k,x) = invf(k,x')) = (x = x').

(* f/invf are inverse permutations; use this to remove some
   occurrences of invf in equality tests *)

forall r:seed, x:D, x':D; 
	(x' = invf(skgen(r),x)) = (f(pkgen(r),x') = x).

(* We can permute the distribution, for uniformly distributed random
   numbers x. Do that only when x is used in invf(skgen(r),x) *)

equiv remove_invf(f)
      foreach iK <= nK do r <-R seed; (
	Opk() := return(pkgen(r)) |
	foreach iF <= nF do x <-R D; 
		(Oant() := return(invf(skgen(r),x)) | 
	         Oim() := return(x)))
<=(0)=> [computational]
      foreach iK <= nK do r <-R seed [unchanged]; (
	Opk() := return(pkgen(r)) |
	foreach iF <= nF do x <-R D; 
		(Oant() := return(x) |
                 Oim() := return(f(pkgen(r), x)))).

(* One-wayness *)

equiv ow(f)
      foreach iK <= nK do r <-R seed; (
	Opk() := return(pkgen(r)) |
	foreach iF <= nF do x <-R D; 
		(Oy() := return(f(pkgen(r), x)) |
		 foreach i1 <= n1 do Oeq   (x' : D) := return(x' = x) |
		 Ox() := return(x)))
<=(nK * nF * POW(time + (nK-1) * time(pkgen) + (#Oy-1) * time(f)))=> [computational]
      foreach iK <= nK do r <-R seed [unchanged]; (
	Opk() := return(pkgen'(r)) |
	foreach iF <= nF do x <-R D [unchanged]; 
		(Oy() := return(f'(pkgen'(r), x)) |
		 foreach i1 <= n1 do Oeq(x':D) := 
	           if defined(k) then return(x' = x) else return(false) |
		 Ox() := let k:bitstring = mark in return(x))).

}

(* One-way trapdoor permutation, with random self-reducibility. 
   Same as above, but with a smaller probability of attack
*)

define OW_trapdoor_perm_RSR(seed, pkey, skey, D, pkgen, skgen, f, invf, POW) {

param nK, nF, n1.

const mark:bitstring.
fun pkgen(seed):pkey.
fun pkgen'(seed):pkey.
fun skgen(seed):skey.
fun f(pkey, D):D.
fun f'(pkey, D):D.
fun invf(skey, D):D.

(* invf is the inverse of f *)

forall r:seed, x:D; invf(skgen(r), f(pkgen(r), x)) = x.

(* f is the inverse of invf *)

forall r:seed, x:D; f(pkgen(r), invf(skgen(r), x)) = x.

(* Injectivity of f *)

forall k:pkey, x:D, x':D; (f(k,x) = f(k,x')) = (x = x').
forall k:pkey, x:D, x':D; (f'(k,x) = f'(k,x')) = (x = x').

(* injectivity of invf *)

forall k:skey, x:D, x':D; (invf(k,x) = invf(k,x')) = (x = x').

(* f/invf are inverse permutations; use this to remove some
   occurrences of invf in equality tests *)

forall r:seed, x:D, x':D; 
	(x' = invf(skgen(r),x)) = (f(pkgen(r),x') = x).

(* We can permute the distribution, for uniformly distributed random
   numbers x. Do that only when x is used in invf(skgen(r),x) *)

equiv remove_invf(f)
      foreach iK <= nK do r <-R seed; (
	Opk() := return(pkgen(r)) |
	foreach iF <= nF do x <-R D; 
		(Oant() := return(invf(skgen(r),x)) | 
	         Oim() := return(x)))
<=(0)=> [computational]
      foreach iK <= nK do r <-R seed [unchanged]; (
	Opk() := return(pkgen(r)) |
	foreach iF <= nF do x <-R D; 
		(Oant() := return(x) |
                 Oim() := return(f(pkgen(r), x)))).

(* One-wayness *)

equiv ow_rsr(f)
      foreach iK <= nK do r <-R seed; (
	Opk() := return(pkgen(r)) |
	foreach iF <= nF do x <-R D; 
		(Oy() := return(f(pkgen(r), x)) |
		 foreach i1 <= n1 do Oeq   (x' : D) := return(x' = x) |
		 Ox() := return(x)))
<=(max(nK, 4 * #Ox) * POW(time + (nK-1) * time(pkgen) + (#Oy-1) * time(f)))=> [computational]
      foreach iK <= nK do r <-R seed [unchanged]; (
	Opk() := return(pkgen'(r)) |
	foreach iF <= nF do x <-R D [unchanged]; 
		(Oy() := return(f'(pkgen'(r), x)) |
		 foreach i1 <= n1 do Oeq(x':D) := 
	           if defined(k) then return(x' = x) else return(false) |
		 Ox() := let k:bitstring = mark in return(x))).

}

(* Pseudo random function (PRF) 
   keyseed: type of key seeds, must be "fixed" (to be able to generate random numbers from it), typically large.
   key: type of keys, must be "bounded"
   input: type of the input of the PRF.
   output: type of the output of the PRF, must be "fixed".

   kgen: key generation function 
   f: PRF function

   Pprf(t, N, l): probability of breaking the PRF property
   in time t, for one key, N queries to the PRF of length at most l.

   The types keyseed, key, input, output and the probability Pprf must
   be declared before this macro is expanded. The functions kgen and f
   are declared by this macro. They must not be declared elsewhere,
   and they can be used only after expanding the macro.

*)

define PRF(keyseed, key, input, output, kgen, f, Pprf) {

param N, N2, N3.

fun f(key, input): output.
fun kgen(keyseed):key.

equiv prf(f)
       foreach i3 <= N3 do r <-R keyseed; foreach i <= N do Of(x:input) := return(f(kgen(r), x))
     <=(N3 * Pprf(time + (N3-1)*(time(kgen) + N * time(f, maxlength(x))), N, maxlength(x)))=>
       foreach i3 <= N3 do r <-R keyseed; foreach i <= N do Of(x:input) :=
		find[unique] j<=N suchthat defined(x[j],r2[j]) && x = x[j] then return(r2[j])
		else r2 <-R output; return(r2).

}

(* Xor
   D: domain on which xor applies 
   xor: the exclusive or function

   The type D must be declared before this macro is expanded. The function
   xor is declared by this macro. It must not be declared elsewhere,
   and it can be used only after expanding the macro.

   This model of xor is not fully satisfactory. In particular, associativity
   is missing.
 *)

define Xor(D, xor) {

param nx.

fun xor(D,D):D [commut].

(* Xor self-cancels *)

forall x:D,y:D; xor(x, xor(x,y)) = y.

(* Xor is injective *)

forall x:D,y:D,z:D; (xor(x,z) = xor(y,z)) = (x = y).

(* Xor is a one-time pad *)

equiv remove_xor(xor)
      foreach ix <= nx do a <-R D; Oxor(x:D) := return(xor(a,x))
      <=(0)=> [computational]
      foreach ix <= nx do a <-R D; Oxor(x:D) := return(a).

}