type pkey [bounded].
type skey [bounded].
type keyseed [large,fixed].
type cleartext.
type ciphertext.
type enc_seed [bounded].

proba Penc.

param N, N', N2, N3, N4.

fun enc(cleartext, pkey, enc_seed): ciphertext.
fun skgen(keyseed):skey.
fun pkgen(keyseed):pkey.
fun dec(ciphertext, skey): bitstringbot.
fun injbot(cleartext):bitstringbot [data].

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

equation forall m:cleartext, r:keyseed, r2:enc_seed; 
	dec(enc(m, pkgen(r), r2), skgen(r)) = injbot(m).

equiv(ind_cca2(enc))
       r <-R keyseed; (
           Opk() := return(pkgen(r)) |
	   foreach i2 <= N2 do Odec(c:ciphertext) := return(dec(c, skgen(r))) |
           foreach i <= N do r1 <-R enc_seed; Oenc(m:cleartext) := return(enc(m, pkgen(r),r1)))
     <=(N * Penc(time + (N-1) * time(enc, maxlength(m)), N2))=>
       r <-R keyseed; (
           Opk() := return(pkgen(r)) |
	   foreach i2 <= N2 do Odec(c:ciphertext) :=
                find j <= N suchthat defined(c1[j],m[j]) && c = c1[j] then return(injbot(m[j])) else
		return(dec(c, skgen(r))) |
	   foreach i <= N do r1 <-R enc_seed; Oenc(m:cleartext) :=
			c1:ciphertext <- enc(Z(m), pkgen(r), r1);
			return(c1)).

process 0