(* This file proves properties of a handshake with pre-shared key
and Diffie-Hellman, in the presence of corruption of the pre-shared key.
It proves forward secrecy of the exchanged key.
Secrecy is proved both on the client side and on the server side.

This example can be considered as a very simplified version of the TLS 1.3
handshake with pre-shared key and Diffie-Hellman (PSK-DHE). *)

channel cStart, cC0, cC1, cC2, cC3, cS1, cS2, cS3, 
	cCorrupt.

param Nc,Ns.

(* We separate the proof from the beginning between an authentication-like
   property (for which we can ignore corruption) and the final properties 
   we want to prove. *)

proof {
insert before "let k_secret_c" "find j3 <= Ns suchthat defined(X'[j3], Y[j3]) && X = X'[j3] && Y' = Y[j3] then else event_abort client_break_auth";
insert before "let k_secret_s" "find j4 <= Nc suchthat defined(X[j4]) && X' = X[j4] then else event_abort server_break_auth";
(* First, prove that client_break_auth and server_break_auth happen with
   negligible probability.
   That shows a form of authentication. *)
focus "query event(client_break_auth) ==> false", "query event(server_break_auth) ==> false";
(* Since these events never happen when the PSK is corrupted, we can remove
   the corruption of the PSK. This is what "success simplify" does. *)
success simplify;
(* Then the proof relies on the secrecy of the pre-shared key and the 
   random oracle assumption *)
crypto rom(H);
crypto splitter(split3) *;
move array part1;
success; (* All active queries proved. Going back to the last focus command. *)
(* At this point, we have proved that client_break_auth and server_break_auth
   never happen.
   We now prove the queries mentioned in the input file. We can consider that
   the PSK is corrupted for this proof. The proof relies on the random oracle 
   assumption and GDH. *) 
out_game "g1.out";
(* We distinguish whether the received exponential comes from the
   honest interlocutor or not, first in the server. *)
insert after "in(cS1" "find j' <= Nc suchthat defined(X[j']) && X' = X[j'] then";
(* There are now two occurrences of Y in the server; we rename them to
   distinct names. *)
SArename Y;
out_game "g2.out";
(* We distinguish whether the received exponential comes from the
   honest interlocutor or not, now in the client. *)
insert after "in(cC2" "find j'' <= Ns suchthat defined(Y_2[j''], X'[j'']) && X = X'[j''] && Y' = Y_2[j''] then";
simplify;
(* Then we apply random oracle, gap Diffie-Hellman to show that the adversary
   cannot obtain the output of the random oracle in honest sessions,
   split the obtained random output of the random oracle, and conclude *)
crypto rom(H);
simplify;
out_game "g3.out";
crypto gdh(exp) [variables: x -> a, y_2 -> b .];
crypto splitter(split3) *;
success
}


type key [large, fixed].

type Z [large, bounded, nonuniform].
type G [large, bounded, nonuniform].

(* Gap Diffie-Hellman assumption. Moreover, the group is a prime-order
group. *)

expand DH_good_group(G, Z, g, exp, exp', mult).

proba pGDH.
letproba pDistRerandom = 0.
expand GDH_RSR(G, Z, g, exp, exp', mult, pGDH, pDistRerandom).

(* Random oracle *)

type hashkey [large,fixed].
type three_keys [large,fixed].
expand ROM_hash_large_4(hashkey, G, G, G, key, three_keys, H, hashoracle, qH).

type tuple3keys_t.
expand random_split_3(three_keys, key, key, key, tuple3keys_t, tuple3keys, split3).

(* Secrecy of the key *)

query secret k_secret_c.
query secret k_secret_s.

(* The protocol itself *)

let Client(hk: hashkey, psk: key) = 
    !ic <= Nc
    in(cC0[ic],());
    new x:Z;
    let X = exp(g,x) in
    out(cC1[ic], X);
    in(cC2[ic],(Y':G, k_s: key));
    let tuple3keys(k_c', k_s', k') = split3(H(hk, exp(Y',x), X, Y', psk)) in
    if k_s = k_s' then
    if defined(corruptedPSK) then
       out(cC3[ic], k_c')
    else
       (* We prove that k' is secret *)
       let k_secret_c: key = k' in
       out(cC3[ic], k_c').

let Server(hk: hashkey, psk: key) = 
   !is <= Ns
   in(cS1[is], X': G);
   new y: Z;
   let Y = exp(g,y) in
   let tuple3keys(k_c, k_s, k) = split3(H(hk, exp(X',y), X', Y, psk)) in
   out(cS2[is],(Y, k_s));
   in(cS3[is], k_c': key);
   if k_c = k_c' then
   if defined(corruptedPSK) then yield else
   (* We prove that k is secret *)
   let k_secret_s: key = k.

let corruptPSK(psk: key) =
   in(cCorrupt, ());
   let corruptedPSK: bool = true in
   out(cCorrupt, psk).

process 
  in(cStart,());
  new hk: hashkey; (* Key that models the choice of the random oracle *)
  new psk: key;
  out(cStart,());
  (Client(hk, psk) | 
   Server(hk, psk) |
   corruptPSK(psk) | 
   hashoracle(hk))

(* EXPECTED
All queries proved.
0.272s (user 0.260s + system 0.012s), max rss 28404K
END *)