(* This file proves properties of the handshake with pre-shared key and Diffie-Hellman, in the presence of corruption of the pre-shared key. It proves secrecy, authentication, and unique channel identifier properties, provided the pre-shared key is not corrupted yet during the handshake. In particular, this proves forward secrecy. Secrecy is proved both on the client side and on the server side. On the server side, secrecy of sats is proved when the server sends the ServerFinished message, before it receives the ClientFinished message. This property is useful for proving security of 0.5RTT messages, by composition with the record protocol. In principle, this proof should be done in the presence of PSK handshakes without DHE, even if we do not prove properties for the latter. We omit them here as a first step and leave the full proof for future work. *) channel io1, io1', io2, io2', io3, io4, io5, io6, io7, io8, io9, io10, io11, io12, io13, io14, io15, io16, io17, io18, io19, io20, io11', io12', io13', io14', io21, io22, io23, io24, io25, io26, io27, io28, io29, io30, dhe_io1, dhe_io1', dhe_io2, dhe_io2', dhe_io3, dhe_io4, dhe_io5, dhe_io6, dhe_io7, dhe_io8, dhe_io9, dhe_io10, dhe_io11, dhe_io12, dhe_io13, dhe_io14, dhe_io15, dhe_io16, dhe_io17, dhe_io18, dhe_io19, dhe_io20, dhe_io11', dhe_io12', dhe_io13', dhe_io14', dhe_io18', dhe_io19', dhe_io21, dhe_io22, dhe_io23, dhe_io24, dhe_io25, dhe_io26, dhe_io27, dhe_io28, dhe_io29, dhe_io30, dhe_io31, cCorrupt1, cCorrupt2. param N1,N5,N6, N7,N8,N9,N10,N11,N12, N13,N14,N15,N16. (* I separate the proof from the beginning between an auth.-like property (for which we can ignore corruption) and the final properties we want to prove. *) proof { insert before_nth 3 "ClientTerm1" "find j3 <= N7 suchthat defined(s_sfl_dhe[j3]) && c_sfl = s_sfl_dhe[j3] then"; insert_event client_break_auth before_nth 4 "ClientTerm1"; insert before_nth 2 "ServerAcceptDHE" "find j4 <= N2 suchthat defined(gx_1[j4]) && (sgx = gx_1[j4]) then"; insert_event server_break_auth before_nth 3 "ServerAcceptDHE"; simplify; (* expand the inserted c_sfl = s_sfl_dhe[j3] to make comparisons between exponentials appear. Must be done early to take fully advantage of GDH. *) (* First, prove that client_break_auth and server_break_auth never happen. That shows a form of authentication. *) focus "query event(client_break_auth)", "query event(server_break_auth)"; (* 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 is fairly similar to the one for PSKDHE without corruption (We use random oracles instead of PRFs because we need HKDF_extract_DHE to be a random oracle to apply GDH in the other proof.) *) crypto rom(HKDF_extract_zero_salt); crypto rom(Derive_Secret_psk_binder_key); crypto rom(HKDF_extract_DHE); crypto rom(Derive_Secret_cets_eems); crypto suf_cma(mac) *; crypto prf2 *; crypto splitter(split2) *; crypto prf_fin_key_iv *; crypto prf3 *; crypto suf_cma(mac) *; success; (* All active queries proved. Going back to the last focus command. *) (* At this point, I have proved that client_break_auth and server_break_auth never happen. I now prove the queries mentioned in the input file. I can consider that the PSK is corrupted for this proof. The proof is then fairly similar to the proof of the initial handshake. (It relies on GDH.) *) out_game "g1.out"; insert after "new sr_" "find j' <= N2 suchthat defined(gx_1[j']) && sgx = gx_1[j'] then"; (* gy_1 is the value of gy in the server *) SArename gy_1; out_game "g2.out"; insert after_nth 1 "let sil_" "find j'' <= N7 suchthat defined(gy_2[j''], sgx[j'']) && gx_1 = sgx[j''] && cgy = gy_2[j''] then"; crypto rom(HKDF_extract_DHE); remove_assign binder s; remove_assign binder s_1; simplify; out_game "g3.out"; crypto gdh(exp) [variables: x_3 -> a, y_13 -> b .]; crypto prf2 *; crypto splitter(split2) *; crypto prf_fin_key_iv *; crypto prf3 *; crypto splitter(split3) *; crypto suf_cma(mac) *; simplify; success } type key [large, fixed]. type extracted [large, fixed]. type Z [large, bounded, nonuniform]. type elt [large, bounded, nonuniform]. fun element2key(elt): key [data]. fun elt2bitstring(elt): bitstring [data]. (* Gap Diffie-Hellman assumption. Moreover, the probability that exp(g, x) = Y for random x and Y independent of x is at most PCollKey1, and the probability that exp(g, mult(x,y)) = Y where x and y are independent random private keys and Y is independent of x or y is at most PCollKey2. *) expand DH_basic(elt, Z, G, exp, exp', mult). proba PCollKey1. proba PCollKey2. expand DH_proba_collision(elt, Z, G, exp, exp', mult, PCollKey1, PCollKey2). proba pGDH. proba pDistRerandom. expand GDH_RSR(elt, Z, G, exp, exp', mult, pGDH, pDistRerandom). letfun dh_keygen() = new x:Z; (x,exp(G,x)). param N, N', N'', N2, N3, N4. type hashkey [large,fixed]. type two_keys [large,fixed]. (* HKDF_extract_zero_salt(psk) = HKDF_extract(0,psk), that is, HKDF_extract with salt argument 0, is a random oracle. *) expand ROM_hash_large(hashkey, key, extracted, HKDF_extract_zero_salt, hashoracle, qH). (* HKDF_extract_DHE(EarlySecret,dh_elt) is a random oracle *) expand ROM_hash_large_2(hashkey, extracted, elt, extracted, HKDF_extract_DHE, hashoracle3, qH3). (* Derive_Secret_psk_binder_key(EarlySecret) = Derive_secret(EarlySecret, "psk_binder_key", empty_log) is a random oracle *) expand ROM_hash_large(hashkey, extracted, key, Derive_Secret_psk_binder_key, hashoracle4, qH4). (* Derive_Secret_cets_eems(EarlySecret, log) = concat(Derive_secret(EarlySecret, "client_ets", log), Derive_secret(EarlySecret, "eems", log)) is a random oracle *) expand ROM_hash_large_2(hashkey, extracted, bitstring, two_keys, Derive_Secret_cets_eems, hashoracle5, qH5). (* These oracles can be considered as independent random oracles, and independent from other PRFs that we use below, having distinct domains: The calls to DeriveSecret use different tags, and use a domain of HMAC different from the calls to HKDF_extract (different length). The EarlySecret has a negligible probablity of being 0, we can exclude this value. The dh_elt is supposed to be different from 0. Can be achieved by excluding the 0 value for Curve25519. *) (* We use the lemma proved in KeySchedule2.cv *) fun Derive_Secret_cs_hts(extracted,bitstring):two_keys. fun HKDF_extract_zero(extracted):extracted. (* HKDF_extract_zero(x) = HKDF_extract(x,0) *) proba Pprf2. equiv(prf2) !N3 new k: extracted; (!N O1(log:bitstring) := return(Derive_Secret_cs_hts(k, log)) | O2() := return(HKDF_extract_zero(k))) <=(N3 * Pprf2(time + (N3-1)*(time(HKDF_extract_zero) + N * time(Derive_Secret_cs_hts, maxlength(log))), N))=> !N3 (!N O1(log:bitstring) := find[unique] j<=N suchthat defined(log[j],r[j]) && log = log[j] then return(r[j]) else new r: two_keys; return(r) | O2() := new r': extracted; return(r')). type tuple2keys_t. expand random_split_2(two_keys, key, key, tuple2keys_t, tuple2keys, split2). (* We use the lemma proved in KeySchedule3.cv *) type three_keys [large, fixed]. fun Derive_Secret_cs_ats_exp(extracted, bitstring): three_keys. fun Derive_Secret_rms(extracted, bitstring): key. proba Pprf3. equiv(prf3) !N3 new k: extracted; (!N O1(log:bitstring) := return(Derive_Secret_cs_ats_exp(k, log)) | !N' O2(log': bitstring) := return(Derive_Secret_rms(k, log'))) <=(N3 * Pprf3(time + (N3-1)*(N' * time(Derive_Secret_rms, maxlength(log')) + N * time(Derive_Secret_cs_ats_exp, maxlength(log))), N, N'))=> !N3 (!N O1(log:bitstring) := find[unique] j<=N suchthat defined(log[j],r[j]) && log = log[j] then return(r[j]) else new r: three_keys; return(r) | !N' O2(log':bitstring) := find[unique] j'<=N' suchthat defined(log'[j'],r'[j']) && log' = log'[j'] then return(r'[j']) else new r': key; return(r')). type tuple3keys_t. expand random_split_3(three_keys, key, key, key, tuple3keys_t, tuple3keys, split3). (* We use the lemma proved in HKDFexpand.cv *) fun HKDF_expand_fin_label(key): key. fun HKDF_expand_key_label(key): key. fun HKDF_expand_iv_label(key): key. proba Pprf_fin_key_iv. equiv(prf_fin_key_iv) !N3 new r: key; (O1() := return(HKDF_expand_fin_label(r)) | O2() := return(HKDF_expand_key_label(r)) | O3() := return(HKDF_expand_iv_label(r))) <=(N3 * Pprf_fin_key_iv(time + (N3-1)*(time(HKDF_expand_fin_label) + time(HKDF_expand_key_label) + time(HKDF_expand_iv_label))))=> !N3 (O1() := new r1: key; return(r1) | O2() := new r2: key; return(r2) | O3() := new r3: key; return(r3)). (* SUF-CMA MAC The MAC is actually a combination of a hash followed by a MAC. It is easy to see that the combination is SUF-CMA provided the MAC is SUF-CMA and the hash is collision resistant. *) (* Avoid the systematic transformation of mac(m,k) = m' into check(m, k, m') because it prevents the proof of some correspondences. (The equality between the arguments of two events is transformed into check, from which CryptoVerif does not infer back the equality when the MAC key is not secret.) *) def SUF_CMA_det_mac_v2(mkey, macinput, macres, mac, Pmac) { fun mac(macinput, mkey):macres. fun mac'(macinput, mkey):macres. equiv(suf_cma(mac)) foreach i3 <= N3 do k <-R mkey;( foreach i <= N do Omac(x: macinput) := return(mac(x, k)) | foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) := return(mac(m, k) = ma)) <=(N3 * Pmac(time + (N3-1)*(N*time(mac,maxlength(x)) + N2*time(mac,maxlength(m))), N, N2, 0, max(maxlength(x), maxlength(m))))=> [computational] foreach i3 <= N3 do k <-R mkey [unchanged];( foreach i <= N do Omac(x: macinput) := let ma2:macres = mac'(x, k) in return(ma2) | foreach i2 <= N2 do Ocheck(m: macinput, ma: macres) := find j <= N suchthat defined(x[j], ma2[j]) && (m = x[j]) && ma = ma2[j] then return(true) else return(false)). } proba Pmac. expand SUF_CMA_det_mac_v2(key, bitstring, bitstring, mac, (* check, *) Pmac). (* Message formats *) type nonce [large, fixed]. type certificate. fun ClientHelloOut(nonce,bitstring): bitstring [data]. fun ClientHelloIn(nonce,bitstring,bitstring,bitstring): bitstring [data]. fun ServerHelloIn(nonce,bitstring): bitstring [data]. fun ServerHelloOut(nonce): bitstring [data]. fun ClientHelloOutDHE(nonce, elt, bitstring): bitstring [data]. fun ClientHelloInDHE(nonce, elt, bitstring, bitstring, bitstring): bitstring [data]. fun ServerHelloInDHE(nonce, elt, bitstring): bitstring [data]. fun ServerHelloOutDHE(nonce, elt): bitstring [data]. fun ServerFinishedIn(bitstring,bitstring): bitstring [data]. fun ServerFinishedOut(bitstring): bitstring [data]. fun ClientFinishedOut(bitstring): bitstring [data]. fun ClientFinishedIn(bitstring,bitstring): bitstring [data]. (* Logs *) fun ClientHelloBinderLogInfo(nonce,bitstring): bitstring [data]. fun ClientHelloBinderLogInfoDHE(nonce,elt,bitstring): bitstring [data]. fun ClientHelloLogInfo(bitstring,bitstring,bitstring): bitstring [data]. fun ServerHelloLogInfo(bitstring,nonce,bitstring): bitstring [data]. fun ServerHelloLogInfoDHE(bitstring,nonce,elt,bitstring): bitstring [data]. fun ServerBeforeFinishedLogInfo(bitstring,bitstring): bitstring [data]. fun ServerFinishedLogInfo(bitstring,bitstring): bitstring [data]. fun ClientBeforeFinishedLogInfo(bitstring, bitstring): bitstring [data]. fun ClientFinishedLogInfo(bitstring, bitstring): bitstring [data]. equation forall cr: nonce, l: bitstring, cr': nonce, gx: elt, l': bitstring; ClientHelloBinderLogInfo(cr,l) <> ClientHelloBinderLogInfoDHE(cr',gx,l'). (* Tables *) table c_table(nonce, bitstring, bitstring, bitstring). table cdhe_table(nonce, elt, bitstring, bitstring, bitstring). (* Secrecy of the key *) query secret cdhe_cats public_vars cdhe_sats, cdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query secret cdhe_sats public_vars cdhe_cats, cdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query secret cdhe_ems public_vars cdhe_cats, cdhe_sats, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query secret sdhe_cats public_vars sdhe_sats, sdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query secret sdhe_sats public_vars sdhe_cats, sdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query secret sdhe_ems public_vars sdhe_cats, sdhe_sats, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query secret cdhe_resumption_secret public_vars cdhe_cats, cdhe_sats, cdhe_ems, sdhe_cats, sdhe_sats, sdhe_ems, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query secret sdhe_resumption_secret public_vars cdhe_cats, cdhe_sats, cdhe_ems, sdhe_cats, sdhe_sats, sdhe_ems, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. (* Authentication of the server to the client *) event ClientTermDHE(bitstring,bitstring). event ServerAcceptDHE(bitstring,bitstring, N7). query log4: bitstring, keys: bitstring, i <= N7; inj-event(ClientTermDHE(log4, keys)) ==> inj-event(ServerAcceptDHE(log4, keys, i)) public_vars (*c_cats, c_sats, c_ems, s_cats, s_sats, s_ems, *) cdhe_cats, cdhe_sats, cdhe_ems, sdhe_cats, sdhe_sats, sdhe_ems, (*c_resumption_secret, s_resumption_secret, *)cdhe_resumption_secret, sdhe_resumption_secret, (*c_cets, c_eems, s_cets, s_eems, *) cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query log4: bitstring, s_keys: bitstring, s_keys': bitstring, i <= N7, i' <= N7; event(ServerAcceptDHE(log4, s_keys, i)) && event(ServerAcceptDHE(log4, s_keys', i')) ==> i = i' public_vars cdhe_cats, cdhe_sats, cdhe_ems, sdhe_cats, sdhe_sats, sdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. (* Authentication of the client to the server *) event ServerTermDHE(bitstring,bitstring). event ClientAcceptDHE(bitstring,bitstring, N2). query log7: bitstring, keys: bitstring, i <= N2; inj-event(ServerTermDHE(log7, keys)) ==> inj-event(ClientAcceptDHE(log7, keys, i)) public_vars cdhe_cats, cdhe_sats, cdhe_ems, sdhe_cats, sdhe_sats, sdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. query log7: bitstring, c_keys: bitstring, c_keys': bitstring, i <= N2, i' <= N2; event(ClientAcceptDHE(log7, c_keys, i)) && event(ClientAcceptDHE(log7, c_keys', i')) ==> i = i' public_vars cdhe_cats, cdhe_sats, cdhe_ems, sdhe_cats, sdhe_sats, sdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. (* Early authentication - these are limited authentication properties guaranteed by the MAC - We do not prove it here, see the version without PSK corruption for this property. *) event ServerEarlyTermDHE(nonce,elt,bitstring,bitstring). event ClientEarlyAcceptDHE(nonce,elt,bitstring,bitstring). (* Unique channel identifier *) event ClientTerm1(bitstring, bitstring, bitstring). event ServerTerm1(bitstring, bitstring, bitstring). query sfl: bitstring, c_cfl: bitstring, s_cfl: bitstring, c_keys: bitstring, s_keys: bitstring; event(ClientTerm1(sfl, c_cfl, c_keys)) && event(ServerTerm1(sfl, s_cfl, s_keys)) ==> c_cfl = s_cfl && c_keys = s_keys public_vars cdhe_cats, cdhe_sats, cdhe_ems, sdhe_cats, sdhe_sats, sdhe_ems, cdhe_resumption_secret, sdhe_resumption_secret, cdhe_cets, cdhe_eems, sdhe_cets, sdhe_eems. letfun send_client_hello1() = new cr:nonce; cr. type send_client_hello2_res_t. fun send_client_hello2_succ(nonce, bitstring, bitstring, tuple2keys_t): send_client_hello2_res_t [data]. letfun send_client_hello2(hk5: hashkey, earlySecret: extracted, binder_key: key, cr: nonce, log1: bitstring, log1': bitstring) = let chbl = ClientHelloBinderLogInfo(cr,log1) in let binder = mac(chbl, binder_key) in let chl = ClientHelloLogInfo(chbl, binder, log1') in let cets_eems = Derive_Secret_cets_eems(hk5, earlySecret, chl) in send_client_hello2_succ(cr, binder, chl, split2(cets_eems)). type keys_res_t. fun keys_succ(extracted, key, key, key, key, key, key): keys_res_t [data]. const keys_fail: keys_res_t. equation forall x1: extracted, x2: key, x3: key, x4: key, x5: key, x6: key, x7: key; keys_succ(x1,x2,x3,x4,x5,x6,x7) <> keys_fail. letfun recv_server_hello(handshakeSecret: extracted, sil:bitstring) = let ServerHelloLogInfo(chl,sr,l2) = sil in (let tuple2keys(client_hts, server_hts) = split2(Derive_Secret_cs_hts(handshakeSecret,sil)) in (let client_hk = HKDF_expand_key_label(client_hts) in let server_hk = HKDF_expand_key_label(server_hts) in let client_hiv = HKDF_expand_iv_label(client_hts) in let server_hiv = HKDF_expand_iv_label(server_hts) in let cfk = HKDF_expand_fin_label(client_hts) in let sfk = HKDF_expand_fin_label(server_hts) in let masterSecret = HKDF_extract_zero(handshakeSecret) in keys_succ(masterSecret,client_hk,server_hk,client_hiv,server_hiv,cfk,sfk) ) else keys_fail ) else keys_fail. type recv_server_finished_res_t. fun recv_server_finished_succ(tuple3keys_t): recv_server_finished_res_t [data]. const recv_server_finished_fail: recv_server_finished_res_t. equation forall x1: tuple3keys_t; recv_server_finished_succ(x1) <> recv_server_finished_fail. letfun recv_server_finished(sil:bitstring, masterSecret:extracted, sfk: key, m:bitstring, log3:bitstring) = let scvl = ServerBeforeFinishedLogInfo(sil, log3) in let sfl = ServerFinishedLogInfo(scvl,m) in let cs_ats_exp = Derive_Secret_cs_ats_exp(masterSecret,sfl) in if mac(scvl,sfk) = m then recv_server_finished_succ(split3(cs_ats_exp)) else recv_server_finished_fail. letfun send_client_finished(log:bitstring, cfk:key) = mac(log,cfk). letfun get_resumption_secret(masterSecret: extracted, cfl: bitstring) = Derive_Secret_rms(masterSecret, cfl). type recv_client_hello_res_t. fun recv_client_hello_succ(nonce, bitstring, tuple2keys_t): recv_client_hello_res_t [data]. const recv_client_hello_fail: recv_client_hello_res_t. equation forall x1: nonce, x2: bitstring, x3: tuple2keys_t; recv_client_hello_succ(x1, x2, x3) <> recv_client_hello_fail. letfun recv_client_hello(hk5: hashkey, earlySecret: extracted, binder_key: key, cr:nonce, log1: bitstring, binder: bitstring, log1': bitstring) = let chbl = ClientHelloBinderLogInfo(cr,log1) in if mac(chbl, binder_key) = binder then ( let chl = ClientHelloLogInfo(chbl, binder, log1') in let cets_eems = Derive_Secret_cets_eems(hk5, earlySecret, chl) in new sr:nonce; recv_client_hello_succ(sr,chl,split2(cets_eems)) ) else recv_client_hello_fail. letfun onertt_hs_keys(sil:bitstring,handshakeSecret:extracted) = let tuple2keys(client_hts, server_hts) = split2(Derive_Secret_cs_hts(handshakeSecret,sil)) in ( let client_hk = HKDF_expand_key_label(client_hts) in let server_hk = HKDF_expand_key_label(server_hts) in let client_hiv = HKDF_expand_iv_label(client_hts) in let server_hiv = HKDF_expand_iv_label(server_hts) in let cfk = HKDF_expand_fin_label(client_hts) in let sfk = HKDF_expand_fin_label(server_hts) in let masterSecret = HKDF_extract_zero(handshakeSecret) in keys_succ(masterSecret, client_hk, server_hk, client_hiv, server_hiv, cfk, sfk) ) else keys_fail. letfun send_server_finished(scvl:bitstring,sfk:key) = mac(scvl, sfk). letfun onertt_data_keys(masterSecret: extracted, sfl:bitstring) = split3(Derive_Secret_cs_ats_exp(masterSecret,sfl)). type check_client_finished_res_t. fun check_client_finished_succ(key): check_client_finished_res_t [data]. const check_client_finished_fail: check_client_finished_res_t. equation forall x1: key; check_client_finished_succ(x1) <> check_client_finished_fail. letfun check_client_finished(masterSecret: extracted, ccvl:bitstring,cfin:bitstring,cfk:key) = if mac(ccvl,cfk) = cfin then ( let cfl = ClientFinishedLogInfo(ccvl, cfin) in let resumption_secret = Derive_Secret_rms(masterSecret, cfl) in check_client_finished_succ(resumption_secret) ) else check_client_finished_fail. (* Functions modified for the version with DHE *) type send_client_hello1DHE_res_t. fun send_client_hello1DHE_succ(nonce, Z, elt): send_client_hello1DHE_res_t [data]. letfun send_client_hello1DHE() = new cr:nonce; new x:Z; let gx = exp(G,x) in send_client_hello1DHE_succ(cr,x,gx). type send_client_hello2DHE_res_t. fun send_client_hello2DHE_succ(nonce, Z, elt, bitstring, bitstring, tuple2keys_t): send_client_hello2DHE_res_t [data]. letfun send_client_hello2DHE(hk5: hashkey, earlySecret: extracted, binder_key: key, cr: nonce, x:Z, gx: elt, log1: bitstring, log1': bitstring) = let chbl = ClientHelloBinderLogInfoDHE(cr,gx,log1) in let binder = mac(chbl,binder_key) in let chl = ClientHelloLogInfo(chbl, binder, log1') in let cets_eems = Derive_Secret_cets_eems(hk5, earlySecret, chl) in send_client_hello2DHE_succ(cr,x,gx, binder, chl, split2(cets_eems)). letfun recv_server_helloDHE(hk: hashkey, earlySecret: extracted, sil:bitstring, x:Z) = let ServerHelloLogInfoDHE(chl,sr,gy,l2) = sil in (let s = exp(gy,x) in let handshakeSecret = HKDF_extract_DHE(hk, earlySecret, s) in let tuple2keys(client_hts, server_hts) = split2(Derive_Secret_cs_hts(handshakeSecret,sil)) in ( let client_hk = HKDF_expand_key_label(client_hts) in let server_hk = HKDF_expand_key_label(server_hts) in let client_hiv = HKDF_expand_iv_label(client_hts) in let server_hiv = HKDF_expand_iv_label(server_hts) in let cfk = HKDF_expand_fin_label(client_hts) in let sfk = HKDF_expand_fin_label(server_hts) in let masterSecret = HKDF_extract_zero(handshakeSecret) in keys_succ(masterSecret,client_hk,server_hk,client_hiv,server_hiv,cfk,sfk) ) else keys_fail ) else keys_fail. type recv_client_helloDHE_res_t. fun recv_client_helloDHE_succ(nonce, elt, extracted, bitstring, tuple2keys_t): recv_client_helloDHE_res_t [data]. const recv_client_helloDHE_fail: recv_client_helloDHE_res_t. equation forall x1: nonce, x2: elt, x3: extracted, x4: bitstring, x5: tuple2keys_t; recv_client_helloDHE_succ(x1, x2, x3, x4, x5) <> recv_client_helloDHE_fail. letfun recv_client_helloDHE(hk: hashkey, hk5: hashkey, earlySecret: extracted, binder_key: key, cr:nonce, gx:elt, log1: bitstring, binder: bitstring, log1': bitstring) = let chbl = ClientHelloBinderLogInfoDHE(cr,gx,log1) in if mac(chbl, binder_key) = binder then ( let chl = ClientHelloLogInfo(chbl, binder, log1') in let cets_eems = Derive_Secret_cets_eems(hk5, earlySecret, chl) in new sr:nonce; new y: Z; let gy = exp(G,y) in let s = exp(gx,y) in let handshakeSecret = HKDF_extract_DHE(hk,earlySecret,s) in recv_client_helloDHE_succ(sr,gy,handshakeSecret,chl,split2(cets_eems)) ) else recv_client_helloDHE_fail. (* PSKDHE *) let ClientDHE(hk3: hashkey, hk5: hashkey, earlySecret: extracted, binder_key: key) = !i2 <= N2 in(dhe_io1,cdhe_log1: bitstring); let send_client_hello1DHE_succ(cr: nonce, x: Z, cgx: elt) = send_client_hello1DHE() in out(dhe_io1', (cr,cgx)); (* Give cr,cgx to the adversary, so that it can compute binders for other PSKs (in cdhe_log1') and add them to the ClientHello message *) in(dhe_io2', cdhe_log1': bitstring); let send_client_hello2DHE_succ(cdhe_cr:nonce,x:Z,cgx':elt, cdhe_binder: bitstring, chl: bitstring, cets_eems: tuple2keys_t) = send_client_hello2DHE(hk5, earlySecret, binder_key, cr, x, cgx, cdhe_log1, cdhe_log1') in let tuple2keys(cdhe_cets: key, cdhe_eems: key) = cets_eems in event ClientEarlyAcceptDHE(cdhe_cr, cgx', cdhe_log1, cdhe_binder); (* We drop 0-RTT since we can prove nothing more for it (no forward secrecy) *) out(dhe_io2,ClientHelloOutDHE(cdhe_cr,cgx',cdhe_binder)); in(dhe_io3,ServerHelloInDHE(sr,cgy,log2)); let sil = ServerHelloLogInfoDHE(chl,sr,cgy,log2) in let keys_succ(masterSecret:extracted,client_hk:key,server_hk:key,client_hiv:key,server_hiv:key,cfk:key,sfk:key) = recv_server_helloDHE(hk3,earlySecret,sil,x) in out(dhe_io4,(client_hk, server_hk, client_hiv, server_hiv)); in(dhe_io5,(ServerFinishedIn(log3,m), ClientAuth: bool, log4: bitstring)); let recv_server_finished_succ(tuple3keys(cats, sats, ems)) = recv_server_finished(sil,masterSecret,sfk,m,log3) in let scvl = ServerBeforeFinishedLogInfo(sil,log3) in let c_sfl : bitstring = ServerFinishedLogInfo(scvl,m) in let ccvl = ClientBeforeFinishedLogInfo(c_sfl,log4) in let cfin = send_client_finished(ccvl,cfk) in let cfl = ClientFinishedLogInfo(ccvl, cfin) in let resumption_secret = get_resumption_secret(masterSecret, cfl) in let honestsession = if defined(corruptedPSK) then ( find j2 <= N7 suchthat defined(s_sfl_dhe[j2]) && c_sfl = s_sfl_dhe[j2] then (* The server has the same cs_ats_exp in session j2. *) true else false ) else true in event ClientTerm1((cdhe_cr,cgx',cdhe_log1,cdhe_binder,cdhe_log1',sr,cgy,log2,log3,m),(log4,cfin),(client_hk,server_hk,client_hiv,server_hiv,cfk,sfk,cats,sats,ems,resumption_secret)); if honestsession then ( let cdhe_sats: key = sats in (* We prove that cdhe_cats, cdhe_sats, cdhe_ems and cdhe_resumption_secret are secret We compose - with the record protocol with secret sdhe_sats (ClientTermDHE is event e2) - with the record protocol with secret cdhe_cats (ClientAcceptDHE is event e1) - with the PSK/PSKDHE handshake with secret cdhe_resumption_secret (ClientAcceptDHE is event e1) *) event ClientTermDHE((cdhe_cr,cgx',cdhe_log1,cdhe_binder,cdhe_log1',sr,cgy,log2,log3,m),(client_hk,server_hk,client_hiv,server_hiv,cfk,sfk,cats,cdhe_sats,ems)); event ClientAcceptDHE((cdhe_cr,cgx',cdhe_log1,cdhe_binder,cdhe_log1',sr,cgy,log2,log3,m,log4,cfin),(client_hk,server_hk,client_hiv,server_hiv,cfk,sfk,cats,cdhe_sats,ems,resumption_secret),i2); let cdhe_cats: key = cats in let cdhe_ems: key = ems in let cdhe_resumption_secret: key = resumption_secret in out(dhe_io6, ClientFinishedOut(cfin)) ) else (* Output the final message, and the secrets. We do not prove security for these sessions We compose with a process that publishes the final message and runs - the record protocol sender-side for cats, - the record protocol receiver side for c_sats and - the client-side handshake with pre-shared key for resumption_secret, with no security claim, by eliminating private communications *) out(dhe_io7, (ClientFinishedOut(cfin), (resumption_secret, cats, sats, ems))). let ServerDHE(hk3: hashkey, hk5: hashkey, earlySecret: extracted, binder_key: key) = !i7 <= N7 in(dhe_io9,ClientHelloInDHE(sdhe_cr: nonce, sgx: elt, sdhe_log1: bitstring, sdhe_binder: bitstring, sdhe_log1': bitstring)); let recv_client_helloDHE_succ(sr:nonce,sgy:elt,handshakeSecret:extracted, chl: bitstring, cets_eems: tuple2keys_t) = recv_client_helloDHE(hk3,hk5,earlySecret,binder_key,sdhe_cr,sgx,sdhe_log1,sdhe_binder,sdhe_log1') in event ServerEarlyTermDHE(sdhe_cr,sgx,sdhe_log1,sdhe_binder); let tuple2keys(sdhe_cets: key, sdhe_eems: key) = cets_eems in out(dhe_io10,ServerHelloOutDHE(sr,sgy)); (* We drop 0-RTT since we can prove nothing more for it (no forward secrecy) *) in(dhe_io11,log2:bitstring); let sil = ServerHelloLogInfoDHE(chl,sr,sgy,log2) in let keys_succ(masterSecret: extracted, client_hk:key, server_hk: key, client_hiv: key, server_hiv: key, cfk: key, sfk: key) = onertt_hs_keys(sil,handshakeSecret) in out(dhe_io12,(client_hk, server_hk, client_hiv, server_hiv)); in(dhe_io13,log3:bitstring); let scvl = ServerBeforeFinishedLogInfo(sil,log3) in let m = send_server_finished(scvl,sfk) in let s_sfl_dhe : bitstring = ServerFinishedLogInfo(scvl,m) in let tuple3keys(cats, sats, ems) = onertt_data_keys(masterSecret,s_sfl_dhe) in let honestsession = if defined(corruptedPSK) then ( find j <= N2 suchthat defined(cgx[j]) && sgx = cgx[j] then true else false ) else true in (* We prove that sdhe_sats is secret, already here for 0.5-RTT We then compose with the record protocol, with secret sdhe_sats (ServerAcceptDHE is event e1) *) if honestsession then ( event ServerAcceptDHE((sdhe_cr,sgx,sdhe_log1,sdhe_binder,sdhe_log1',sr,sgy,log2,log3,m),(client_hk,server_hk,client_hiv,server_hiv,cfk,sfk,cats,sats,ems),i7); let sdhe_sats: key = sats in out(dhe_io18,ServerFinishedOut(m)); in(dhe_io19,ClientFinishedIn(log4, cfin)); let ccvl = ClientBeforeFinishedLogInfo(s_sfl_dhe,log4) in let check_client_finished_succ(resumption_secret: key) = check_client_finished(masterSecret,ccvl,cfin,cfk) in event ServerTerm1((sdhe_cr,sgx,sdhe_log1,sdhe_binder,sdhe_log1',sr,sgy,log2,log3,m),(log4,cfin),(client_hk,server_hk,client_hiv,server_hiv,cfk,sfk,cats,sats,ems,resumption_secret)); (* We prove that sdhe_cats, sdhe_ems, and sdhe_resumption_secret are secret We compose with the record protocol for sdhe_cats and with the PSK/PSKDHE handshake for s_resumption_secret *) let sdhe_cats: key = cats in let sdhe_ems: key = ems in let sdhe_resumption_secret: key = resumption_secret in (* We compose - with the record protocol with secret cdhe_cats (ServerTermDHE is event e2) and - with the PSK/PSKDHE handshake with secret cdhe_resumption_secret (ServerTermDHE is event e2) *) event ServerTermDHE((sdhe_cr,sgx,sdhe_log1,sdhe_binder,sdhe_log1',sr,sgy,log2,log3,m,log4,cfin),(client_hk,server_hk,client_hiv,server_hiv,cfk,sfk,sdhe_cats,sdhe_sats,sdhe_ems,sdhe_resumption_secret)); out(dhe_io30, ()) ) else (* We leak sats. We compose with a process that outputs the ServerFinished message, and runs the record protocol sender-side with sats, with no security claim, by eliminating private communications *) out(dhe_io18',(ServerFinishedOut(m), sats)); in(dhe_io19',ClientFinishedIn(log4, cfin)); let ccvl = ClientBeforeFinishedLogInfo(s_sfl_dhe,log4) in let check_client_finished_succ(resumption_secret: key) = check_client_finished(masterSecret,ccvl,cfin,cfk) in event ServerTerm1((sdhe_cr,sgx,sdhe_log1,sdhe_binder,sdhe_log1',sr,sgy,log2,log3,m),(log4,cfin),(client_hk,server_hk,client_hiv,server_hiv,cfk,sfk,cats,sats,ems,resumption_secret)); (* Output the secrets. We do not prove security for these sessions We compose with a process that runs - the record protocol receiver-side for cats, - the record protocol sender side for sats and - the server-side handshake with pre-shared key for resumption_secret, with no security claim, by eliminating private communications *) out(dhe_io31, (resumption_secret, cats, sats, ems)). let corruptPSK(psk: key) = in(cCorrupt1, ()); let corruptedPSK: bool = true in out(cCorrupt2, psk). (* For a first step, we consider only the version with DHE *) process in(io20,()); new hk: hashkey; (* Key that models the choice of the random oracle HKDF_extract_zero_salt *) new hk3: hashkey; (* Key that models the choice of the random oracle HKDF_extract_DHE *) new hk4: hashkey; (* Key that models the choice of the random oracle Derive_Secret_psk_binder_key *) new hk5: hashkey; (* Key that models the choice of the random oracle Derive_Secret_cets_eems *) new psk: key; let earlySecret = HKDF_extract_zero_salt(hk, psk) in let binder_key = Derive_Secret_psk_binder_key(hk4, earlySecret) in (* handshake secret for the PSK variant without DHE *) out(io21,()); ((in(io22, ()); out(io23, ()); ((in(io24, ()); out(io25, ()); ClientDHE(hk3, hk5, earlySecret, binder_key)) | (in(io26, ()); out(io27, ()); ServerDHE(hk3, hk5, earlySecret, binder_key)) | corruptPSK(psk))) | hashoracle(hk) | hashoracle3(hk3) | hashoracle4(hk4) | hashoracle5(hk5)) (* This code is equivalent to: in(io20,()); new hk: hashkey; new hk2: hashkey; new hk3: hashkey; new hk4: hashkey; new hk5: hashkey; out(io21,()); ((in(io22, ()); new psk: key; out(io23, ()); ((in(io24, ()); let earlySecret = HKDF_extract_zero_salt(hk, psk) in let binder_key = Derive_Secret_psk_binder_key(earlySecret) in out(io25, ()); ClientDHE) | (in(io26, ()); let earlySecret = HKDF_extract_zero_salt(hk, psk) in let binder_key = Derive_Secret_psk_binder_key(earlySecret) in out(io27, ()); ServerDHE))) | hashoracle(hk) | hashoracle2(hk2) | hashoracle3(hk3) | hashoracle4(hk4) | hashoracle5(hk5)) The version above is easier to verify for CryptoVerif, because let earlySecret = HKDF_extract_zero_salt(hk, psk) in let binder_key = Derive_Secret_psk_binder_key(earlySecret) in are called once, and before calls to the hash oracle by the adversary, so it is easy to show that they generate fresh random values, shared by ClientDHE, ServerDHE. The commented version is the one we use for the composition results. *) (* EXPECTED All queries proved. 99.568s (user 99.476s + system 0.092s), max rss 232304K END *)