(* 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 *)