(* This file proves a version of INT-CTXT that allows corruption of keys
   from a version that does not. Both the assumption and the conclusion
   are indistinguishability properties without the [computational] 
   annotation. *)

def INT_CTXT_sym_enc_no_corrupt(key, cleartext, ciphertext, enc_seed, enc, enc_r, enc_r', dec, injbot, Z, Advintctxt) { 

param N, N'.

fun enc_r(cleartext, key, enc_seed): ciphertext.
fun dec(ciphertext, key): bitstringbot.

fun enc_r'(cleartext, key, enc_seed): ciphertext.

fun injbot(cleartext):bitstringbot [data].
equation 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.

(* The encryption function is probabilistic *)
letfun enc(m: cleartext, k: key) =
       new r: enc_seed; enc_r(m, k, r).

equation forall m:cleartext, k:key, r:enc_seed; 
	dec(enc_r(m, k, r), k) = injbot(m).

	(* INT-CTXT *)

equiv(int_ctxt(enc))
      new k: key; (
      	! i <= N new r: enc_seed; Oenc(x:cleartext) := return(enc_r(x, k, r)) |
	! i' <= N' Odec(y:ciphertext) [useful_change] := return(dec(y,k)))
     <=(Advintctxt(time, N, N', maxlength(x), maxlength(y)))=> 
      new k: key; (
      	! i <= N new r: enc_seed; Oenc(x:cleartext) := let z:ciphertext = enc_r(x, k, r) in return(z) |
	! i' <= N' Odec(y:ciphertext) := find j <= N suchthat defined(x[j],z[j]) && z[j] = y then return(injbot(x[j])) else return(bottom)).

}

type key [bounded].
type cleartext.
type ciphertext.
type enc_seed [bounded].
proba Advintctxt.

expand INT_CTXT_sym_enc_no_corrupt(key, cleartext, ciphertext, enc_seed, enc, enc_r, enc_r', dec, injbot, Z, Advintctxt).

proof {
insert after "Ocorrupt" "let corrupt = true in";
insert after "Oenc" "let z = enc_r(x,k,r) in";
use_variable z;
insert after "Odec" "if defined(corrupt) then else find j <= N suchthat defined(x[j],z[j]) && z[j] = y then else if dec(y,k) <> bottom then event_abort distinguish else";
simplify;
replace at_nth 3 1 "{[0-9]+}dec(" "bottom";
remove_assign useless;
start_from_other_end;
insert before "return(bottom)" "if dec(y_1, k) <> bottom then event_abort distinguish else";
success; (* Proves equivalence; event(distinguish) ==> false remains to prove *)
success simplify; (* Remove compromise *)
auto (* Use ciphertext integrity and conclude *)
}


param N, N'. 

query_equiv(int_ctxt_corrupt(enc))
      new k: key; (
      	! i <= N new r: enc_seed; Oenc(x:cleartext) := return(enc_r(x, k, r)) |
	! i' <= N' Odec(y:ciphertext) := return(dec(y,k)) |
	Ocorrupt() := return(k))
     <=(?)=> 
      new k: key; (
      	! i <= N new r: enc_seed; Oenc(x:cleartext) := let z:ciphertext = enc_r(x, k, r) in return(z) |
	! i' <= N' Odec(y:ciphertext) :=
	    if defined(corrupt) then return(dec(y,k)) else
	    find j <= N suchthat defined(x[j],z[j]) && z[j] = y then return(injbot(x[j])) else return(bottom) |
	Ocorrupt() := let corrupt: bool = true in return(k))

(* EXPECTED
All queries proved.
0.052s (user 0.048s + system 0.004s), max rss 16808K
END *)