(* One-Encryption Key Exchange - forward secrecy

   This version assumes the following definition of freshness of an instance:
   - First, the instance has computed and accepted a session key.
   - Second, no Corrupt-query has been made by the adversary since the beginning of the game (before the session key is accepted).
   - Third, the instance has not been asked for a Reveal-query and if it has a partner, then its partner has not been asked for a Reveal-query.
   Test queries are allowed for fresh instances, hence we prove secrecy of session keys for fresh instances.
   We prove secrecy of sk_u, the session key of the user. Session keys of the server are then also secret, because all session keys of the server are session keys of the user by authentication of the user U to the server S. We prove this property using CDH.
*)

(* Proof indications *)

proof {
set autoMove = false;
allowed_collisions noninteractive^2/large;
   (* Allow eliminating collisions of probability q^2 / |Z|, q^2 / |G|, q^2 / |hash1|,
   where q is a number of queries (qH0, qH1, qE, qD, NS, NU, NP):
   |G|, |Z|, |hash1| are considered to be large
   q^3/|G| or q/|passwd| are not allowed.

   Since q \in O(t_A) and |Z| = |G|, we will get terms for probabilities of collisions
   O(t_A^2)/|hash1| + O(t_A^2)/|G|.

   *)
success; (* proof of event(acceptU(x,X,y,Ystar,a,k,u)) && event(acceptU(x,X,y,Ystar,a,k',u')) ==> u = u' *)
show_game;
insert after "OH(" "let concat(x01,x02,x03,x04,x05) = x1 in"; (* just after OH(..) := *)
crypto rom(h0);
insert after "OH_1" "let concat(x11,x12,x13,x14,x15) = x1_1 in"; (* just after OH_1(..):= *)
crypto rom(h1);
insert after "OS2" "if defined(xcorrupt) then else find j <= NU suchthat defined(X[j]) && X[j] = X_s then else find jh <= qH1 suchthat defined(x11[jh], x12[jh], x13[jh], x14[jh], r_7[jh]) && (U = x11[jh]) && (S = x12[jh]) && (X_s = x13[jh]) && (Y = x14[jh]) && (auth_s = r_7[jh]) then event_abort Auth"; (* just after OS2(..):= , in else branch of "if defined(xcorrupt) then" *)
simplify;
insert after "OC2" "if defined(xcorrupt) then";
crypto icm(enc);
show_game;
insert_event Encrypt after_nth 2 "pw0 = ke\\["; (* beginning of the branch "find ... && (pw0 = ke[..]) then .." in OC2, in else branch of "if defined(xcorrupt) then" *)
show_game;
crypto group_to_exp_strict(exp) *;
(* We rewrite the "find" at the beginning of OH_1, to capture exactly the
conditions that can be eliminated by CDH. The conditions are of the form: 
i,j suchthat defined(x[i], y[j]) && (x14 = exp(g, x[i])) && (x13 = exp(g, y[j])) && (x12 = S) && (x11 = U) && (x15 = exp(g, mult(x[i], y[j])))
for some exponents x,y. That allows eliminating similar conditions in the rest of the game.
- We test x15 = exp(g, mult(x[i], y[j])) as last condition, so that the test is executed only when x13 and x14 are the right public keys. CryptoVerif then realizes that the test is made for a single i,j for each hash query.
 *)
show_game;
insert before "find \\[unique\\] u_32 "
  "          if defined(xcorrupt) then else
          find ri_7 <= NU, ri_8 <= NU suchthat defined(x[ri_7], X[ri_7], x_3[ri_8]) && (x14 = exp(g, x_3[ri_8])) && (x13 = X[ri_7]) && (x12 = S) && (x11 = U) && (x15 = exp(g, mult(x_3[ri_8], x[ri_7]))) then
            event_abort cdh
          orfind ri_7 <= NU, ri_9 <= qD suchthat defined(x[ri_7], X[ri_7], x_2[ri_9]) && (x14 = exp(g, x_2[ri_9])) && (x13 = X[ri_7]) && (x12 = S) && (x11 = U) && (x15 = exp(g, mult(x_2[ri_9], x[ri_7]))) then
            event_abort cdh
          orfind ri_7 <= NU, ri_10 <= NS suchthat defined(x[ri_7], y[ri_10], X[ri_7], Y[ri_10]) && (x14 = Y[ri_10]) && (x13 = X[ri_7]) && (x12 = S) && (x11 = U) && (x15 = exp(g, mult(y[ri_10], x[ri_7]))) then
            event_abort cdh
          orfind ri_7 <= NU, ri_11 <= NP suchthat defined(x[ri_7], yp[ri_11], X[ri_7], Yp[ri_11]) && (x14 = Yp[ri_11]) && (x13 = X[ri_7]) && (x12 = S) && (x11 = U) && (x15 = exp(g, mult(yp[ri_11], x[ri_7]))) then
            event_abort cdh
          orfind ri_6 <= NP suchthat defined(yp[ri_6], xp[ri_6], Xp[ri_6], Yp[ri_6]) && (x14 = Yp[ri_6]) && (x13 = Xp[ri_6]) && (x12 = S) && (x11 = U) && (x15 = exp(g, mult(xp[ri_6], yp[ri_6]))) then
            event_abort cdh";
(* We rewrite the "find" at the beginning of OH in a similar way *)
insert before "find \\[unique\\] u_9 "
  "          if defined(xcorrupt) then else
          find ri_69 <= NU, ri_70 <= NU suchthat defined(X[ri_69], x[ri_69], x_3[ri_70]) && (x04 = exp(g, x_3[ri_70])) && (x03 = X[ri_69]) && (x02 = S) && (x01 = U) && (x05 = exp(g, mult(x_3[ri_70], x[ri_69]))) then
            event_abort cdh
          orfind ri_67 <= NU, ri_71 <= qD suchthat defined(X[ri_67], x[ri_67], x_2[ri_71]) && (x04 = exp(g, x_2[ri_71])) && (x03 = X[ri_67]) && (x02 = S) && (x01 = U) && (x05 = exp(g, mult(x_2[ri_71], x[ri_67]))) then
            event_abort cdh
          orfind ri_65 <= NU, ri_99 <= NS suchthat defined(X[ri_65], Y[ri_99], x[ri_65], y[ri_99]) && (x04 = Y[ri_99]) && (x03 = X[ri_65]) && (x02 = S) && (x01 = U) && (x05 = exp(g, mult(y[ri_99], x[ri_65]))) then
            event_abort cdh
          orfind ri_63 <= NU, ri_73 <= NP suchthat defined(X[ri_63], Yp[ri_73], x[ri_63], yp[ri_73]) && (x04 = Yp[ri_73]) && (x03 = X[ri_63]) && (x02 = S) && (x01 = U) && (x05 = exp(g, mult(yp[ri_73], x[ri_63]))) then
            event_abort cdh
          orfind ri_8 <= NP suchthat defined(Xp[ri_8],xp[ri_8],Yp[ri_8],yp[ri_8]) && (x04 = Yp[ri_8]) && (x03 = Xp[ri_8]) && (x02 = S) && (x01 = U) && (x05 = exp(g, mult(yp[ri_8], xp[ri_8]))) then
	    event_abort cdh";
simplify;
focus "query forall k: hash0, a: hash1, Ystar, X: G, y, x: host; inj-event(termS(x, X, y, Ystar, a, k)) ==> exists u <= NU; (inj-event(acceptU(x, X, y, Ystar, a, k, u)) || event(corrupt))", "query event(cdh) ==> false", "query event(cdh_1) ==> false", "query event(cdh_2) ==> false", "query event(cdh_3) ==> false", "query event(cdh_4) ==> false", "query event(cdh_5) ==> false", "query event(cdh_6) ==> false", "query event(cdh_7) ==> false", "query event(cdh_8) ==> false", "query event(cdh_9) ==> false", "query event(Auth) ==> false", "query event(Encrypt) ==> false";
SArename r_1; (* These case distinctions help proving authentication *)
SArename r_5;
SArename r_7;
SArename r_3;
success; (* Show authentication *)
success simplify; (* Removes corruption *)
simplify; (* Finish removing corruption tests *)
crypto cdh(exp);
crypto exp_to_group(exp) *;
show_game;
move array X_5; (* variable chosen at the end of OC2 and not used immediately *)
merge_arrays X_1 Y_1;
merge_branches;
move array X_2; (* variable chosen in OP and not used immediately *)
(*show_game;
merge_arrays X_1 Y_...;
merge_branches;*)
move array X_4; (* variable chosen in OS1 and not used immediately *)
(*show_game;
merge_arrays X_1 Y_1;*)
show_game;
insert before "find jh" "find jh' <= qH1, jd <= qD suchthat defined(x11[jh'], x12[jh'], x13[jh'], x14[jh'], r_27[jh'], m[jd], kd[jd], X_1[jd]) && (m[jd] = md_O_enc) && (U = x11[jh']) && (S = x12[jh']) && (X_s = x13[jh']) && (x14[jh'] = X_1[jd]) && (auth_s = r_27[jh'])  && (kd[jd] = pw0) then event_abort Auth2";
simplify;
merge_branches;
allowed_collisions noninteractive^2/large, small/password;
(* Allow eliminating collisions with probability 
   (NU + NS)/|passwd| since NU and NS are small and |passwd| is of size password.
   These collisions are not eliminated automatically because |passwd| is too small,
   they need to be explicitly requested by simplify coll_elim(variables: pw0) below.
 *)
simplify coll_elim(variables: pw0);
success;
(* All active queries are proved, we go back to before "focus" and prove secrecy of sk_u_secret and sk_p *)

insert before "find \\[unique\\] u_9 " "find ri_8 <= NP suchthat defined(xcorrupt, Xp[ri_8],xp[ri_8],Yp[ri_8],yp[ri_8]) && (x04 = Yp[ri_8]) && (x03 = Xp[ri_8]) && (x02 = S) && (x01 = U) && (x05 = exp(g, mult(yp[ri_8], xp[ri_8]))) then event_abort cdh_corrupt";
simplify;
crypto cdh(exp) [variables: xp -> a_1, x_4 -> b, yp -> b, x_2 -> b, x_3 -> b, x -> a_1 .];
success; (* Show secrecy of sk_p; secrecy of sk_u_secret remains to show *)

(* There are some tests on the value of K_s = X_s^y in the server, which are not allowed in CDH (they correspond to DDH queries).
   We eliminate them as much as we can.
   We find which query to H1 we are going to consider using auth_s, without testing on K_s (the "find" inserted below), then we test K_s
   only in that query, so that we have a single test on K_s: K_s = x15[uH].
   *)
insert after_nth 1 "K_s:" "find uH = ri_38 <= qH1 suchthat defined(r_7[ri_38], x11[ri_38], x12[ri_38], x13[ri_38], x14[ri_38], x15[ri_38]) && (auth_s = r_7[ri_38]) && (Y = x14[ri_38]) && (X_s = x13[ri_38]) && (S = x12[ri_38]) && (U = x11[ri_38]) then let accept_s = (K_s = x15[uH]) in if accept_s then";
simplify;
merge_branches; (* Remove a usage of K_s in a find that executes yield *)
SArename r_1; (* This case distinction makes it easier to know which references to K_s are under the test K_s = x15[uH] and which are not *)
out_game "g1occ.out" occ;
(* We replace tests K_s = ... with tests x15[uH] = ..., in evaluations of H0, both in oracle OH and in the server *)
replace 2165 "x15[uH[ri_8]]"; (* replace K_s[ri_8] with its value x15[uH[ri_8]] in OH, when r_57 is defined, so the test K_s = x15[uH] holds *)
replace 1213 "x15[uH]"; (* replace K_s with its value x15[uH] in the server, when the test K_s = x15[uH] holds *)
SArename r_7; (* These case distinctions help proving secrecy, like similar case distinctions helped proving authentication *)
SArename r_3;
(* guess the tested session and its partner, to apply CDH to a single pair of exponents *)
allowed_collisions ; (* Avoid eliminating collisions after guessing, because that would yield bigger probabilities of collisions *)
set guessRemoveUnique = true;
guess iU; (* guess iU = iU_tested, tested session of sk_u_secret *)
remove_assign binder sk_u_secret; (* make sure that sk_u_secret_1 is defined directly from a random, so that success simplify works *)
success simplify; (* removes code of the tested session, in cases in which sk_u_secret_1 is not defined *)
guess "u_74[iU_tested]"; (* guess u_74[iU_tested] = u_74_guessed, partner S of the tested session for U *)
insert after "OS1" "if iS = u_tested then"; (* test if iS = u_74_guessed at the beginning of the server *)
SArename x; (* SArename x, y => distinguish name in tested sessions from others
	       Name in tested sessions: x_11, y_2 *)
SArename y;
insert before_nth 1 "find u_9" "if defined(X[iU_tested], Y[u_tested], x_11[iU_tested], y_2[u_tested]) && (x04 = Y[u_tested]) && (x03 = X[iU_tested]) && (x02 = S) && (x01 = U) && (x05 = exp(g, mult(x_11[iU_tested], y_2[u_tested]))) then event_abort cdh_corrupt2"; (* introduce event cdh_corrupt2 in the hash oracle for the CDH of x,y in the tested sessions*)
simplify; 
success;  (* success proves secrecy, we still need to exclude cdh_corrupt2 *)
SArename K_s;
remove_assign binder K_s_5;
simplify;
guess "accept_s[u_tested]" no_test; (* guess the value of the test accept_s = (X_s^y = Z) in the server for y of the tested server session. That removes the last DDH query; we can then apply CDH *)
crypto cdh(exp) [variables: x_11 -> a_1, y_2 -> b . ]; (* apply cdh. *)
success
}

(* Parameter and type declarations *)

param NU, NS [small].
param NP [passive].

type Z [large, bounded].
type G [large, bounded].
type passwd [password, bounded].

type hash0 [fixed].
type hash1 [fixed,large].
type host [bounded].

(* Computational Diffie-Hellman *)

expand DH_good_group(G, Z, g, exp, exp', mult).
proba pCDH.
letproba pZero = 0.
expand CDH_RSR(G, Z, g, exp, exp, mult, pCDH, pZero).
   (* Using exp also after transformation, not exp', to be able to apply CDH several times *)

(* Ideal cipher model *)

type cipherkey [fixed].

expand ICM_cipher(cipherkey, passwd, G, enc, dec, enc_dec_oracle, qE, qD).

(* Hash functions in the random oracle model *)

type hashkey [fixed].

fun concat(host, host, G, G, G): bitstring [data].

expand ROM_hash(hashkey, bitstring, hash0, h0, hashoracle0, qH0).

expand ROM_hash_large(hashkey, bitstring, hash1, h1, hashoracle1, qH1).

(* Host names *)

const U : host.
const S : host.

(* Acceptation results *)

const AcceptHonest: bitstring.
fun AcceptAttacker(hash0): bitstring [data].

(* Queries *)

query secret sk_u_secret public_vars sk_p.
query secret sk_p public_vars sk_u_secret.

event termS(host, G, host, G, hash1, hash0).
event acceptU(host, G, host, G, hash1, hash0, NU).
event corrupt.

query x:host, X:G, y:host, Ystar:G, a: hash1, k:hash0, u <= NU;
	inj-event(termS(x,X,y,Ystar,a,k)) ==> inj-event(acceptU(x,X,y,Ystar,a,k,u)) || event(corrupt)
	public_vars sk_u_secret, sk_p.
query x:host, X:G, y:host, Ystar:G, a: hash1, k:hash0, k':hash0, u <= NU, u' <= NU;
	event(acceptU(x,X,y,Ystar,a,k,u)) && event(acceptU(x,X,y,Ystar,a,k',u')) ==> u = u'
	public_vars sk_u_secret, sk_p.

(* Client *)

let processU(hk0: hashkey, hk1: hashkey, ck: cipherkey, pw: passwd) =
	foreach iU <= NU do 
	OC1() :=
	x <-R Z;
	X:G <- exp(g,x);
	return(U, X);
	OC2(=S, Ystar_u: G) :=
	Y_u <- dec(ck, Ystar_u, pw);
	K_u <- exp(Y_u, x);
	auth_u: hash1 <- h1(hk1,concat(U,S,X,Y_u,K_u));
	sk_u: hash0 <- h0(hk0,concat(U,S,X,Y_u,K_u));
	event acceptU(U, X, S, Ystar_u, auth_u, sk_u, iU);
	return(auth_u);
	OC3() := 
	if defined(xcorrupt) then 
	  return(sk_u)
	else
	  sk_u_secret: hash0 <- sk_u.

(* Server *)

let processS(hk0: hashkey, hk1: hashkey, ck: cipherkey, pw: passwd) =
	foreach iS <= NS do 
	OS1(=U, X_s: G) :=
	y <-R Z;
	Y <- exp(g,y);
	Ystar <- enc(ck, Y, pw);
	return(S, Ystar);
	OS2(auth_s: hash1) :=
	K_s <- exp(X_s, y);
	if auth_s = h1(hk1,concat(U,S,X_s,Y,K_s)) then
	sk_s: hash0 <- h0(hk0,concat(U,S,X_s,Y,K_s));
	event termS(U, X_s, S, Ystar, auth_s, sk_s);
	find j <= NU suchthat defined(X[j], Ystar_u[j], auth_u[j], sk_u[j]) &&
	  X[j] = X_s && Ystar_u[j] = Ystar && auth_u[j] = auth_s && sk_u[j] = sk_s then
	  return(AcceptHonest)
	else
	  (* if defined(xcorrupt) then *) return(AcceptAttacker(sk_s)).


(* Sessions that are subject only to a passive attack.
   We send a transcript of the session *)

let processPassive(hk0: hashkey, hk1: hashkey, ck: cipherkey, pw: passwd) =
	foreach iP <= NP do 
	OP() :=
	xp <-R Z;
	Xp <- exp(g, xp);
	yp <-R Z;
	Yp <- exp(g, yp);
	Kp <- exp(g, mult(xp,yp));
	Ystarp <- enc(ck, Yp, pw);
	authp <- h1(hk1, concat(U, S, Xp, Yp, Kp));
	sk_p: hash0 <- h0(hk0, concat(U, S, Xp, Yp, Kp));
	return(U, Xp, S, Ystarp, authp).


(* Corruption *)

let processCorrupt(pw: passwd) =
        Ocorrupt() :=
	event corrupt();
	xcorrupt: bool <- true;
	return(pw).

process 
	Ostart() :=
	hk0 <-R hashkey;
	hk1 <-R hashkey;
	ck <-R cipherkey;
	pw0 <-R passwd;
	return;
	(run processU(hk0, hk1, ck, pw0) |
	 run processS(hk0, hk1, ck, pw0) |
	 run processPassive(hk0, hk1, ck, pw0) |
	 run processCorrupt(pw0) |
	 run enc_dec_oracle(ck) | run hashoracle0(hk0) | run hashoracle1(hk1))

(* Results

   The hash, encryption, and decryption queries are performed by the adversary,
   so qH0, qH1, qE, qD \in O(t_A).

   NP is the number of sessions of the protocol the adversary passively observes,
   NP << t_A

   NS and NU are the number of sessions of the server/user the adversary
   actively interferes with. NS, NU << NP.

   |Z| = |G| = p-1 where the Diffie-Hellman group has prime order p.
   (G excludes the neutral element, Z excludes 0.)

   We qE + qD + qH0 + qH1 + NS + NU + NP = O(t_A). 
   Let qH = qH0 + qH1

I can overapproximate the probabilities as follows:
Proved 
event(acceptU(x,X,y,Ystar,a,k,u)) && event(acceptU(x,X,y,Ystar,a,k',u')) ==> u = u'
with public variable sk_u_secret, sk_p up to probability NU^2/2|G|

Proved
inj-event(termS(x,X,y,Ystar,a,k)) ==> inj-event(acceptU(x,X,y,Ystar,a,k,u)) || event(corrupt)
with public variable sk_u_secret, sk_p up to probability
(NS + NU) / |passwd| + qH pCDH(time_1) + O(tA^2)/|G| + O(tA^2) / |hash1|

Proved secrecy of sk_p with public variable sk_u_secret up to probability 
(NS + NU) / |passwd| + qH (5 + 12 NU) pCDH(time_2) + O(tA^2)/|G| + O(tA^2) / |hash1|

Proved secrecy of sk_u_secret with public variable sk_p up to probability 
(NS + NU) / |passwd| + qH (5 + 12 NU + 2 NU NS) * pCDH(time_3) + O(tA^2)/|G| + O(tA^2) / |hash1|

*)


(* EXPECTED
All queries proved.
33.233s (user 33.165s + system 0.068s), max rss 197504K
END *)