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

param N, N2.

proba Penc.

fun Z(cleartext):cleartext.
fun enc(cleartext, pkey, enc_seed): ciphertext.
fun skgen(keyseed):skey.
fun pkgen(keyseed):pkey.

(* part displayed in the paper starts here *)
fun dec(ciphertext, skey): bitstringbot.
fun injbot(cleartext):bitstringbot [data].

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

table cipher(cleartext, ciphertext).

equiv(ind_cca2(enc))
  k <-R keyseed; (
    Opk() := return(pkgen(k)) |
    foreach i2 <= N2 do Odec(c:ciphertext) :=
      return(dec(c, skgen(k))) |
    foreach i <= N do r <-R enc_seed;
      Oenc(m:cleartext) := return(enc(m, pkgen(k),r)))
<=(N * Penc(time + (N-1) * time(enc, maxlength(m)), N2))=>
  k <-R keyseed; (
   Opk() := return(pkgen(k)) |
   foreach i2 <= N2 do Odec(c:ciphertext) :=
     get cipher(m1, =c) in return(injbot(m1))
     else return(dec(c, skgen(k))) |
   foreach i <= N do r <-R enc_seed;
     Oenc(m:cleartext) :=
       c1 <- enc(Z(m), pkgen(k), r);
       insert cipher(m, c1); return(c1)).

process 0