(* Model of WireGuard by Benjamin Lipp and Bruno Blanchet, Inria Paris. This file generates several CryptoVerif scripts using the m4 preprocessor. It considers the case in which the psk may be corrupted at some point, and proves forward secrecy with respect to the compromise of the psk. It uses the following settings: - Compromise settings: m4_S_i_compr When this macro is defined, the long-term secret key S_i_priv of the initiator can be dynamically compromised. m4_S_r_compr When this macro is defined, the long-term secret key S_r_priv of the responder can be dynamically compromised. m4_E_i_compr When this macro is defined, the ephemeral E_i_priv of the initiator is compromised. m4_E_r_compr When this macro is defined, the ephemeral E_r_priv of the responder is compromised. - Other settings: m4_AB When this macro is defined, the script models sessions in which A is the initiator and B is the responder. When it is not defined, the script also models sessions in which B is the initiator and A is the responder (the ephemerals are always compromised for these sessions; it does not prove security for these sessions; security holds by symmetry). m4_replay_prot When this macro is defined, the first message is protected against replays using the timestamp. m4_zero_test When this macro is defined, the process fails in case a Diffie-Hellman shared secret is zero. m4_uniquesession_chbinding_weakUKS When this macro is defined, the long-term keys secret keys are compromised from the beginning and the psk is received from the adversary. CryptoVerif proves session uniqueness, channel binding for the hash, and a weak version of resistance to unknown key share attacks (long-term keys equal modulo pow8). m4_first_msg_auth When this macro is defined, the script proves authentication of the first message. For this to hold, the long-term secret keys must not be compromised at the moment the first message is received. For simplicity, we assume that the long-term secret keys are never compromised; compromising them after event rcvd1 is executed clearly does not affect the truth of the correspondence. When this macro is not defined, it proves all other security properties. The proof indications need to be adapted to the various settings. We use the following 3 combinations -Dm4_S_i_compr -Dm4_S_r_compr -Dm4_E_i_compr -Dm4_S_r_compr -Dm4_S_i_compr -Dm4_E_r_compr with in addition m4_AB defined or not, m4_replay_prot defined or not, and m4_zero_test defined. The other combinations may not work. The case in which both ephemerals are compromised, and the long-term keys are never compromised is proved by the file WG.25519.m4.cv: the psk is not needed in this case, security just relies on the long-term keys. m4_uniquesession_chbinding_weakUKS and m4_first_msg_auth are proved in WG.25519.m4.cv. *) (* To speed up proofs of correspondences *) set casesInCorresp = false. (* To speed up the proof *) set autoMergeBranches = false. (* To save memory *) set forgetOldGames = true. (* The macro m4_out_game outputs the current game to a file. The file name contains a number that is increased at each output. *) define(`m4_gamenumber', 0) define(`m4_out_game',`define(`m4_gamenumber', incr(m4_gamenumber))out_game "m4_name.m4_gamenumber.out.cv" occ') (* m4_if_zero(x,y) expands to "if is_zero(x) then y else" when m4_zero_test is defined *) ifdef(`m4_zero_test',` define(`m4_if_zero',`if is_zero($1) then $2 else') ', ` define(`m4_if_zero',`') ') (* Proof indications *) (* Define variable names *) ifdef(`m4_AB',` define(`m4_S_i_pub_rcvd', `S_i_pub_rcvd_2') define(`m4_E_r_pub_rcvd', `E_r_pub_rcvd_1') define(`m4_E_i_pub', `E_i_pub_2') define(`m4_E_i_pub_rcvd', `E_i_pub_rcvd_2') ifdef(`m4_E_i_compr',` define(`m4_gdh_i_priv', `S_A_priv -> a') ',` ifdef(`m4_E_r_compr',` define(`m4_gdh_i_priv', `E_i_priv_9 -> a, E_i_priv_8 -> a, E_i_priv_6 -> a') ',` define(`m4_gdh_i_priv', `E_i_priv_5 -> a, E_i_priv_4 -> a') ') ') ifdef(`m4_E_r_compr',` define(`m4_gdh_r_priv', `S_B_priv -> b') ',` ifdef(`m4_E_i_compr',` define(`m4_gdh_r_priv', `E_r_priv_52 -> b, E_r_priv_51 -> b, E_r_priv_49 -> b, E_r_priv_48 -> b, E_r_priv_47 -> b, E_r_priv_45 -> b, E_r_priv_56 -> b, E_r_priv_55 -> b, E_r_priv_53 -> b') ',` define(`m4_gdh_r_priv', `E_r_priv_48 -> b, E_r_priv_47 -> b, E_r_priv_46 -> b, E_r_priv_45 -> b, E_r_priv_50 -> b, E_r_priv_49 -> b') ') ') ',` define(`m4_S_i_pub_rcvd', `S_i_pub_rcvd_4') define(`m4_E_r_pub_rcvd', `E_r_pub_rcvd_2') define(`m4_E_i_pub', `E_i_pub_4') define(`m4_E_i_pub_rcvd', `E_i_pub_rcvd_3') ifdef(`m4_E_i_compr',` define(`m4_gdh_i_priv', `S_A_priv -> a') ',` ifdef(`m4_E_r_compr',` define(`m4_gdh_i_priv', `E_i_priv_15 -> a, E_i_priv_14 -> a, E_i_priv_12 -> a') ',` define(`m4_gdh_i_priv', `E_i_priv_11 -> a, E_i_priv_10 -> a') ') ') ifdef(`m4_E_r_compr',` define(`m4_gdh_r_priv', `S_B_priv -> b') ',` ifdef(`m4_E_i_compr',` define(`m4_gdh_r_priv', `E_r_priv_85 -> b, E_r_priv_84 -> b, E_r_priv_82 -> b, E_r_priv_81 -> b, E_r_priv_80 -> b, E_r_priv_78 -> b, E_r_priv_89 -> b, E_r_priv_88 -> b, E_r_priv_86 -> b') ',` define(`m4_gdh_r_priv', `E_r_priv_81 -> b, E_r_priv_80 -> b, E_r_priv_79 -> b, E_r_priv_78 -> b, E_r_priv_83 -> b, E_r_priv_82 -> b') ') ') ') proof { (* put the event init_break_auth in the initiator, when it is supposed to talk to the honest responder, the psk is not corrupted, and still E_r does not match one generated by the honest responder in a session in which it talks to the honest initiator. *) ifdef(`m4_E_r_compr', ` insert before "rcvd2" "if defined(psk_is_corrupted) then else find j5 <= n_S suchthat defined(E_r_pub[j5],m4_S_i_pub_rcvd[j5]) && pow8(m4_E_r_pub_rcvd) = pow8(E_r_pub[j5]) && m4_S_i_pub_rcvd[j5] = S_A_pub then else event_abort init_break_auth"; ',` (* the test honest_session already distinguishes whether the psk is corrupted, so we do not need to distinguish it again *) insert before_nth 2 "rcvd2" "find j5 <= n_S suchthat defined(E_r_pub[j5],m4_S_i_pub_rcvd[j5]) && pow8(m4_E_r_pub_rcvd) = pow8(E_r_pub[j5]) && m4_S_i_pub_rcvd[j5] = S_A_pub then else event_abort init_break_auth"; ') m4_out_game; (* put the event resp_break_auth in the responder, when it is supposed to talk to the honest initiator, the psk is not corrupted, and still E_i does not match one generated by the honest initiator in a session in which it talks to the honest responder. *) ifdef(`m4_E_i_compr', ` insert before_nth 4 "injbot(plaintext" "if defined(psk_is_corrupted) then else find j7 <= n_S suchthat defined(m4_E_i_pub[j7],S_X_pub[j7]) && pow8(m4_E_i_pub_rcvd) = pow8(m4_E_i_pub[j7]) && S_X_pub[j7] = S_B_pub then"; insert_event resp_break_auth after_nth 8 "injbot(plaintext"; ', `ifdef(`m4_E_r_compr', ` (* the test honest_session already distinguishes whether the psk is corrupted, so we do not need to distinguish it again *) insert before_nth 5 "injbot(plaintext" "find j7 <= n_S suchthat defined(m4_E_i_pub[j7],S_X_pub[j7]) && pow8(m4_E_i_pub_rcvd) = pow8(m4_E_i_pub[j7]) && S_X_pub[j7] = S_B_pub then"; insert_event resp_break_auth after_nth 7 "injbot(plaintext"; ', ` insert before_nth 6 "injbot(plaintext" "find j7 <= n_S suchthat defined(m4_E_i_pub[j7],S_X_pub[j7]) && pow8(m4_E_i_pub_rcvd) = pow8(m4_E_i_pub[j7]) && S_X_pub[j7] = S_B_pub then"; insert_event resp_break_auth after_nth 8 "injbot(plaintext"; ') ') m4_out_game; simplify; (* We first prove that init_break_auth and resp_break_auth happen with negligible probability *) focus "query event(init_break_auth)", "query event(resp_break_auth)"; success simplify; (* remove the compromise of the psk, since these events never happen when the psk is compromised *) m4_out_game; (* Distinguish whether the responder received an E_i that comes from the honest initiator *) insert after "in(c_init2resp_recv\\[" "find i <= n_S suchthat defined(m4_E_i_pub[i]) && m4_E_i_pub_rcvd = m4_E_i_pub[i] then"; simplify; m4_out_game; (* We apply the ROM assumptions in the order rom3, rom2, rom1 the reduce the number of case distinctions made by CryptoVerif. Since rom2 and rom3 are called after rom1, if we applied rom1 first, that would copy the calls to rom2 and rom3 for each case distinguished by rom1, and thus creates many more calls and case distinctions to make in rom2 and rom3. Appliying them in the reverse order avoids that. In the random oracle rom3 provided to the adversary, distinguish whether the argument of rom3 is a 7-tuple in which the components 2, 3, 5, 6 are elements of the subgroup of curve25519 generated by the base point. In all calls to rom3 made in the protocol, this property is satisfied because these components are Diffie-Hellman shared secrets computed as X_pub^Y_priv where Y_priv is a multiple of 8. Hence, calls made by the adversary that do not satisfy this condition cannot collide with calls made in the protocol. *) insert after "in(ch1_rom3" "let rom3_input(x1_rom3, G8_to_G(x2_rom3), G8_to_G(x3_rom3), x4_rom3, G8_to_G(x5_rom3), G8_to_G(x6_rom3), v_psk) = x_rom3 in"; (* Apply the ROM assumption to rom3 *) crypto rom(rom3_intermediate); (* Similar case distinction to the above, adapted to the calls to rom2 made in the protocol *) insert after "in(ch1_rom2" "let rom2_input(x1_rom2, G8_to_G(x2_rom2), G8_to_G(x3_rom2)) = x_rom2 in"; (* Apply the ROM assumption to rom2 *) crypto rom(rom2_intermediate); (* Similar case distinction to the above, adapted to the calls to rom1 made in the protocol *) insert after "in(ch1_rom1" "let rom1_input(x1_rom1, G8_to_G(x2_rom1)) = x_rom1 in"; (* Apply the ROM assumption to rom1 *) crypto rom(rom1_intermediate); (* Unset useKnownEqualitiesWithFunctionsInMatching and elsefindFactsInSimplify for speed. They are not necessary in this part of the proof. *) set useKnownEqualitiesWithFunctionsInMatching = false; set elsefindFactsInSimplify = false; (* Split the 4 random keys returned by rom3. The indication ** means that we apply splitter(concat_four_keys) as many times as we can, without performing a full simplification between each application. Avoiding that simplification here and for the ind_cpa transformation saves about 12% of the runtime. *) m4_out_game; crypto splitter(concat_four_keys) **; (* avoid trying SA renaming variables in case the next int_ctxt does not work immediately. The proof also works without that indication, but slower. *) set noAdviceCrypto = true; (* Apply ciphertext integrity for the AEAD scheme *) crypto int_ctxt(enc) *; success; (* no nonce reuse and init_break_auth and resp_break_auth *) (* Back to before focus *) (* Useful when using Curve25519 because we need to apply equalities pow8(..) = pow8(..) when testing whether a term matches another term, and CryptoVerif would not apply them by default. However, that is costly. *) set useKnownEqualitiesWithFunctionsInMatching = true; set elsefindFactsInSimplify = true; m4_out_game; (* Case distinctions *) (* We say that two public keys are X_pub and Y_pub are "equivalent" when X_pub^8 = Y_pub^8, written in CryptoVerif pow8(X_pub) = pow8(Y_pub). Such equivalent public keys yield the same Diffie-Hellman shared secrets because all secret keys are multiple of 8. *) ifdef(`m4_E_i_compr',`',` (* E_i_pub_sent is E_i_pub, avoid using 2 different variables, so that when we SArename E_i_pub, that also distinguishes cases on E_i_pub_sent. *) remove_assign binder E_i_pub_sent; ') ifdef(`m4_E_r_compr',` (* When E_r is compromised, we rely on the security of S_r. Distinguish whether the received S_r_pub (S_X_pub) is equivalent the honest one S_B_pub *) insert after "in(c_config_initiator\\[" "if pow8(S_X_pub) = pow8(S_B_pub) then"; ') ifdef(`m4_E_i_compr',` (* When E_i is compromised, we rely on the security of S_i. Distinguish whether the received S_i_pub is equivalent the honest one S_A_pub *) insert after "let injbot(G_to_bitstring(m4_S_i_pub_rcvd: G_t))" "if pow8(m4_S_i_pub_rcvd) = pow8(S_A_pub) then"; ') (* Distinguish whether the ephemeral m4_E_i_pub_rcvd received by the responder is equivalent to an ephemeral (m4_E_i_pub) generated by the honest initiator. This case distinction is useful when E_i_priv is not compromised, and also when E_r_priv is not compromised (in this case, we use it to show that we decrypt static_i_enc with the same key as the encryption key) *) insert after "in(c_init2resp_recv\\[" "find i <= n_S suchthat defined(m4_E_i_pub[i]) && pow8(m4_E_i_pub_rcvd) = pow8(m4_E_i_pub[i]) then"; (* Use different names for the ephemeral E_i_pub of the initiator, depending on the cases distinguished above *) SArename m4_E_i_pub; m4_out_game; ifdef(`m4_E_r_compr',`',` (* Distinguish whether the ephemeral m4_E_r_pub_rcvd received by the initiator is equivalent to an ephemeral E_r_pub generated by the honest responder. This case distinction is useful only when E_r_priv is not compromised. *) insert after_nth 2 "in(c_resp2init_recv\\[" "find j <= n_S suchthat defined(E_r_pub[j]) && pow8(m4_E_r_pub_rcvd) = pow8(E_r_pub[j]) then"; insert after_nth 1 "in(c_resp2init_recv\\[" "find j <= n_S suchthat defined(E_r_pub[j]) && pow8(m4_E_r_pub_rcvd) = pow8(E_r_pub[j]) then"; SArename E_r_pub; ') (* End of case distinctions *) m4_out_game; simplify; m4_out_game; (* We apply the ROM assumptions in the order rom3, rom2, rom1 the reduce the number of case distinctions made by CryptoVerif. Since rom2 and rom3 are called after rom1, if we applied rom1 first, that would copy the calls to rom2 and rom3 for each case distinguished by rom1, and thus creates many more calls and case distinctions to make in rom2 and rom3. Appliying them in the reverse order avoids that. In the random oracle rom3 provided to the adversary, distinguish whether the argument of rom3 is a 7-tuple in which the components 2, 3, 5, 6 are elements of the subgroup of curve25519 generated by the base point. In all calls to rom3 made in the protocol, this property is satisfied because these components are Diffie-Hellman shared secrets computed as X_pub^Y_priv where Y_priv is a multiple of 8. Hence, calls made by the adversary that do not satisfy this condition cannot collide with calls made in the protocol. *) insert after "in(ch1_rom3" "let rom3_input(x1_rom3, G8_to_G(x2_rom3), G8_to_G(x3_rom3), x4_rom3, G8_to_G(x5_rom3), G8_to_G(x6_rom3), v_psk) = x_rom3 in"; (* Apply the ROM assumption to rom3 *) crypto rom(rom3_intermediate); m4_out_game; (* Similar case distinction to the above, adapted to the calls to rom2 made in the protocol *) insert after "in(ch1_rom2" "let rom2_input(x1_rom2, G8_to_G(x2_rom2), G8_to_G(x3_rom2)) = x_rom2 in"; (* Apply the ROM assumption to rom2 *) crypto rom(rom2_intermediate); m4_out_game; (* Similar case distinction to the above, adapted to the calls to rom1 made in the protocol *) insert after "in(ch1_rom1" "let rom1_input(x1_rom1, G8_to_G(x2_rom1)) = x_rom1 in"; (* Apply the ROM assumption to rom1 *) crypto rom(rom1_intermediate); m4_out_game; (* Apply the gap Diffie-Hellman assumption. The previous case distinctions allow us to isolate Diffie-Hellman shared secrets that the adversary cannot compute because he does not have the two secret shares. The ROM assumptions applied before make comparisons with these Diffie-Hellman shared secrets appear. *) crypto gdh(exp_div8) [variables: m4_gdh_i_priv, m4_gdh_r_priv .]; (* Unset useKnownEqualitiesWithFunctionsInMatching and elsefindFactsInSimplify for speed. They are not necessary in the rest of the proof. *) set useKnownEqualitiesWithFunctionsInMatching = false; set elsefindFactsInSimplify = false; m4_out_game; (* Split the 4 random keys returned by rom3. The indication ** means that we apply splitter(concat_four_keys) as many times as we can, without performing a full simplification between each application. Avoiding that simplification here and for the ind_cpa transformation saves about 12% of the runtime. *) crypto splitter(concat_four_keys) **; success; (* unknown key-share *) simplify; m4_out_game; (* avoid trying SA renaming variables in case the next int_ctxt does not work immediately. The proof also works without that indication, but it is slower. *) set noAdviceCrypto = true; (* Apply ciphertext integrity for the AEAD scheme *) crypto int_ctxt(enc) *; success; (* no nonce reuse + authentication *) simplify; (* Apply IND-CPA of the AEAD scheme *) crypto ind_cpa(enc) **; success (* secrecy of secret_bit (message indistinguishability) *) } param n_S, n_M. (**** Gap Diffie-Hellman ****) type G_t [bounded,large]. (* type of public keys *) type G8_t [bounded,large]. (* type of { X^k, X \in F_p } *) fun G_to_bitstring(G_t): bitstring [data]. type Z_t [bounded,large,nonuniform]. (* type of exponents (must be "bounded" and "large", is the set of multiples of k prime to qq' modulo kqq'.) *) const dummy_z: Z_t. (* placeholder when we do not compromise the ephemerals *) proba P_GDH. (* probability of breaking the GDH assumption *) proba P_DistRerandom. (* Page 7 in the Noise paper, rev 33: The public_key either encodes some value in a large prime-order group (which may have multiple equivalent encodings), or is an invalid value. *) expand DH_X25519( (* types *) G_t, (* Public keys *) Z_t, (* Exponents *) (* variables *) g, (* base point *) exp, (* exponentiation function *) mult, (* multiplication function for exponents *) G8_t, g8, exp_div8, exp_div8', (* a symbol that replaces exp_div8 after game transformation *) pow8, G8_to_G, is_zero, is_zero8 ). expand GDH_RSR( (* types *) G8_t, (* Group elements *) Z_t, (* Exponents *) (* variables *) g8, (* a generator of the group *) exp_div8, (* exponentiation function *) exp_div8', (* a symbol that replaces exp_div8 after game transformation *) mult, (* multiplication function for exponents *) (* probabilities *) P_GDH, (* probability of breaking the GDH assumption *) P_DistRerandom (* probability of distinguishing a rerandomized key from an honest generated key, 2^{-125} for Curve25519 *) ). letfun DH(group_element: G_t, exponent: Z_t) = exp(group_element, exponent). (**** Symmetric encryption ****) type key_t [large,fixed]. fun key_to_bitstring(key_t): bitstring [data]. type psk_t [large,fixed]. (* 32 byte pre-shared symmetric key *) const psk_0: psk_t. (* pre-shared key with all zeros, *) (* used in case the WireGuard user *) (* did not provide a psk. *) type nonce_t [large,fixed]. (* 12 byte counter nonce for AEAD. *) const nonce_0: nonce_t. (* const value for the zero nonce *) const empty_bitstring : bitstring. (* const value for the empty bitstring that will be encrypted *) proba P_enc. proba P_encctxt. expand AEAD_nonce( (* types *) key_t, (* keys *) bitstring, (* plaintext *) bitstring, (* ciphertext *) bitstring, (* additional data *) nonce_t, (* nonces *) (* functions *) enc, (* encryption: enc(plaintext, additional data, key, nonce): ciphertext *) dec, (* decryption: dec(ciphertext, additional data, key, nonce): bitstringbot *) injbot, (* injection from plaintext to bitstringbot: injbot(plaintext): bitstringbot *) Zero, (* returns a plaintext of same length, consisting of zeros: Zero(plaintext): plaintext *) (* probabilities *) P_enc, (* breaking IND-CPA *) P_encctxt (* breaking INT-CTXT *) ). (**** Hash and HKDF ****) type hashkey_t [fixed]. type hashoutput_t [large,fixed]. fun hashoutput_to_bitstring(hashoutput_t): bitstring [data]. (* This models the derivation of a first intermediate symmetric key. *) type rom1_input_t. fun rom1_input(G_t, G_t): rom1_input_t [data]. expand ROM_hash_refactored( (* types *) hashkey_t, (* key of the hash function, models the choice of the hash function *) rom1_input_t, (* input type *) key_t, (* output type *) (* functions *) rom1_intermediate, (* name of the random oracle hash function: rom1(hashkey_t, rom2_input_t): key_t *) (* processes *) rom1_oracle, (* name of the oracle that will be available to the attacker *) (* variables *) r_rom1, x_rom1, (* channels for random oracle *) ch1_rom1, ch2_rom1, (* parameters *) N_qH1 (* number of queries to the oracle by the attacker *) ). letfun rom1(hk: hashkey_t, x1_rom1: G_t, x2_rom1: G_t) = rom1_intermediate(hk, rom1_input(x1_rom1, x2_rom1)). (* This models the derivation of a second intermediate symmetric key. *) type rom2_input_t. fun rom2_input(G_t, G_t, G_t): rom2_input_t [data]. expand ROM_hash_refactored( (* types *) hashkey_t, (* key of the hash function, models the choice of the hash function *) rom2_input_t, (* input type *) key_t, (* output type *) (* functions *) rom2_intermediate, (* Name of the random oracle hash function: rom2(hashkey_t, rom2_input_t): key_t *) (* processes *) rom2_oracle, (* Name of the oracle that will be available to the attacker. *) (* variables *) r_rom2, x_rom2, (* channels for random oracle *) ch1_rom2, ch2_rom2, (* parameters *) N_qH2 (* Number of queries to the oracle by the attacker. *) ). letfun rom2(hk: hashkey_t, x1_rom2: G_t, x2_rom2: G_t, x3_rom2: G_t) = rom2_intermediate(hk, rom2_input(x1_rom2, x2_rom2, x3_rom2)). (* This models the derivation of * a third intermediate symmetric key along with * a token that has the same length as a key and * the two * transport data keys. This makes it 4 variables we derive based on 7 input variables. A random oracle is used to derive an intermediate type. We define functions to retrieve the four individual parts and equivalence that shows that all the four parts are indepently random. *) type rom3_input_t. fun rom3_input(G_t, G_t, G_t, G_t, G_t, G_t, psk_t): rom3_input_t [data]. type four_keys_t [large,fixed]. expand ROM_hash_refactored( (* types *) hashkey_t, (* Key of the hash function, models the choice of the hash function. *) rom3_input_t, (* input type *) four_keys_t, (* intermediary output type of the actual random *) (* oracle *) (* functions *) rom3_intermediate, (* name of the random oracle hash function, *) (* returning the intermediate type: *) (* rom3_intermediate(hashkey_t, rom3_input_t): four_keys_t *) (* processes *) rom3_oracle, (* name of the oracle available to the attacker *) (* variables *) r_rom3, x_rom3, (* channels for random oracle *) ch1_rom3, ch2_rom3, (* parameters *) N_qH3 (* number of queries to the oracle by the attacker *) ). (* wrapper around the random oracle hash function, *) (* returning the concatenation of 4 keys: *) (* rom3(hashkey_t, G_t, G_t, G_t, G_t, G_t, G_t, psk_t): four_keys_t *) letfun rom3(hk: hashkey_t, e_i: G_t, es: G_t, ss: G_t, e_r: G_t, ee: G_t, se: G_t, v_psk: psk_t) = rom3_intermediate(hk, rom3_input(e_i, es, ss, e_r, ee, se, v_psk)). expand split_4( (* types *) four_keys_t, (* intermediary output type of the actual random *) (* oracle *) key_t, (* All the 4 parts to extract have type key_t *) key_t, key_t, key_t, (* functions *) concat_four_keys, (* function that concatenates the four parts. *) (* variables *) tau, (* Names of the variables used when applying the equivalence *) k, (* This makes the games in the proof much more readable. *) T_i_send, T_i_recv ). (* A collision resistant hash function is used for chaining hashes with parts of the protocol transcript. To the previous hash output, the next part of the transcript is appended. We model this as being a hash function that has two arguments, the first being of type hashoutput and the second of bitstring. *) proba P_hash. (* probability of breaking collision resistance *) expand CollisionResistant_hash_2( (* types *) hashkey_t, (* key of the hash function, models the choice of *) (* the hash function *) hashoutput_t, (* first argument that gets hashed. See the comment *) (* just above this macro for an explanation. *) bitstring, (* second argument that gets hashed. *) hashoutput_t, (* output type of the hash function *) (* functions *) hash, (* name of the hash function: *) (* hash(hashkey_t, hashoutput_t, bitstring): hashoutput_t *) (* processes *) hash_oracle, (* name of the oracle that will make available the *) (* hash key to the attacker *) (* parameters *) P_hash (* probability of breaking collision resistance *) ). (* constants used in the transcript hashing *) const hash_construction_identifier : hashoutput_t. (* This is hash( hash("Noise_IK…") || "WireGuard v1 …" ), and it's *) (* the same for all parties, so no need to calculate it with hash() *) (* channel names *) channel c_start. channel c_config_initiator. channel c_init2resp_send, c_resp2init_recv. channel c_init2resp_recv, c_resp2init_send. channel c_keyconfirm_send, c_keyconfirm_recv, c_wait_before_2nd_part. channel c_N_init_send_config, c_N_resp_send_config. channel c_N_init_send, c_N_resp_send. channel c_N_resp_recv, c_N_init_recv. channel c_N_resp_recv_res, c_N_init_recv_res. channel c_publickeys. channel c_corrupt_S_i, c_corrupt_S_r, c_corrupt_psk. channel c_config_initiator_sw. channel c_init2resp_send_sw, c_resp2init_recv_sw. channel c_init2resp_recv_sw, c_resp2init_send_sw. channel c_keyconfirm_send_sw, c_keyconfirm_recv_sw, c_wait_before_2nd_part_sw. channel c_N_init_send_config_sw, c_N_resp_send_config_sw. channel c_N_init_send_sw, c_N_resp_send_sw. channel c_N_resp_recv_sw, c_N_init_recv_sw. channel c_N_resp_recv_res_sw, c_N_init_recv_res_sw. (* WireGuard specific types *) type G_set_t. (* set of public keys *) fun is_in(G_t, G_set_t): bool. type counter_t [fixed]. (* 8 byte counter in the data message *) const counter_0: counter_t. (* constant for counter with value 0 *) fun counter_to_nonce(counter_t) : nonce_t [data]. (* This is [data] because it is an injection, from 8 byte counters to 12 bytes nonces. *) type msg_type_t [fixed]. (* 1 byte msg type field *) const msg_type_init2resp: msg_type_t. const msg_type_resp2init: msg_type_t. const msg_type_data: msg_type_t. const msg_type_cookie_reply: msg_type_t. type reserved_t [fixed]. (* 3 byte reserved field *) const reserved: reserved_t. type session_index_t [fixed]. (* 4 byte session identifier field *) type timestamp_t [fixed]. (* 12 byte timestamps *) fun timestamp_to_bitstring(timestamp_t): bitstring [data]. table rcvd_timestamps(G_t, G_t, timestamp_t). (* In the security game we want to be able to abort if the attacker wants us to encrypt with an already used nonce. *) type side. const is_initiator: side. const is_responder: side. const is_initiator_sw: side. const is_responder_sw: side. (* the bitstring is used as tuple (side, replication_index) *) table sent_counters(bitstring, counter_t). table rcvd_counters(bitstring, counter_t). (* Convenience wrappers around hash that take care of type conversion. *) letfun mix_hash_G(key_hash: hashkey_t, prev_hash: hashoutput_t, value: G_t) = hash(key_hash, prev_hash, G_to_bitstring(value)). letfun mix_hash_bitstring(key_hash: hashkey_t, prev_hash: hashoutput_t, value: bitstring) = hash(key_hash, prev_hash, value). letfun mix_hash_key(key_hash: hashkey_t, prev_hash: hashoutput_t, value: key_t) = hash(key_hash, prev_hash, key_to_bitstring(value)). (* Convenience wrappers for enc and dec that take care of type conversions. *) letfun enc_G(group_element: G_t, current_hash: hashoutput_t, k: key_t, n: nonce_t) = enc(G_to_bitstring(group_element), hashoutput_to_bitstring(current_hash), k, n). letfun dec_ad_hash(ciphertext: bitstring, current_hash: hashoutput_t, k: key_t, n: nonce_t) = dec(ciphertext, hashoutput_to_bitstring(current_hash), k, n). letfun enc_timestamp(timestamp: timestamp_t, current_hash: hashoutput_t, k: key_t, n: nonce_t) = enc(timestamp_to_bitstring(timestamp), hashoutput_to_bitstring(current_hash), k, n). letfun enc_bitstring(plaintext: bitstring, current_hash: hashoutput_t, k: key_t, n: nonce_t) = enc(plaintext, hashoutput_to_bitstring(current_hash), k, n). (* Define a function for choosing from two attacker-provided plaintexts based on a bit. Also, defines some equations on it so CryptoVerif is able to reason about it. *) expand boolean_choice_for_encryption( (* types *) bitstring, (* type of the values *) (* functions *) Zero, (* the Zero function provided by the encryption scheme. *) (* Needed for some equations about the function. *) test (* Name of the choice function: *) (* test(bool, bitstring, bitstring): bitstring *) ). event sent1( G_t, (* S_r_pub *) (* values sent in the first protocol message *) G_t, (* initiator's ephemeral public key *) bitstring, (* msg.static *) G_t, (* S_i_pub *) bitstring, (* msg.timestamp *) timestamp_t (* timestamp in the clear *) ). event rcvd1( bool, (* true if talking to initiator *) G_t, (* S_r_pub *) (* values sent in the first protocol message *) G_t, (* initiator's ephemeral public key *) bitstring, (* msg.static *) G_t, (* S_i_pub *) bitstring, (* msg.timestamp *) timestamp_t (* timestamp in the clear *) ). event initiator_uniq_Tir( n_S, (* initiator replication index *) key_t (* T_i_send = T_r_recv *) ). event initiator_uniq_Tri( n_S, (* initiator replication index *) key_t (* T_i_recv = T_r_send *) ). event initiator_uniq_pubmsg( n_S, (* initiator replication index *) (* values sent in the first protocol message *) G_t, (* initiator's ephemeral public key *) bitstring, (* msg.static *) bitstring, (* msg.timestamp *) (* values sent in the second protocol message, that have not yet been sent in the first *) G_t, (* responder's ephemeral public key *) bitstring (* encrypted empty bitstring *) ). event initiator_imb( (* session keys *) key_t, (* T_i_send = T_r_recv *) key_t, (* T_i_recv = T_r_send *) (* ephemeral public keys *) G_t, (* initiator's ephemeral public key *) G_t, (* responder's ephemeral public key *) (* static public keys *) G_t, G_t ). event responder_uniq_Tir( n_S, (* responder replication index *) key_t (* T_i_send = T_r_recv *) ). event responder_uniq_Tri( n_S, (* responder replication index *) key_t (* T_i_recv = T_r_send *) ). event responder_uniq_pubmsg( n_S, (* responder replication index *) (* values sent in the first protocol message *) G_t, (* initiator's ephemeral public key *) bitstring, (* msg.static *) bitstring, (* msg.timestamp *) (* values sent in the second protocol message, that have not yet been sent in the first *) G_t, (* responder's ephemeral public key *) bitstring (* encrypted empty bitstring *) ). event responder_imb( (* session keys *) key_t, (* T_i_send = T_r_recv *) key_t, (* T_i_recv = T_r_send *) (* ephemeral public keys *) G_t, (* initiator's ephemeral public key *) G_t, (* responder's ephemeral public key *) (* static public keys *) G_t, G_t ). event initiator_H7( G_t, (* S_i_pub *) G_t, (* S_r_pub *) G_t, (* E_i_pub *) G_t, (* E_r_pub *) timestamp_t, (* timestamp in the clear *) psk_t, (* pre-shared key *) key_t, (* T_i_send = T_r_recv *) key_t, (* T_i_recv = T_r_send *) hashoutput_t (* hash *) ). event responder_H7( G_t, (* S_i_pub *) G_t, (* S_r_pub *) G_t, (* E_i_pub *) G_t, (* E_r_pub *) timestamp_t, (* timestamp in the clear *) psk_t, (* pre-shared key *) key_t, (* T_i_send = T_r_recv *) key_t, (* T_i_recv = T_r_send *) hashoutput_t (* hash *) ). event sent2( G_t, (* S_r_pub *) (* values sent in the first protocol message *) G_t, (* initiator's ephemeral public key *) bitstring, (* msg.static *) G_t, (* S_i_pub in the clear *) bitstring, (* msg.timestamp *) timestamp_t, (* timestamp in the clear *) (* values sent in the second protocol message, that have not yet been sent in the first *) (*session_index_t,*) (* responder's session index *) G_t, (* responder's ephemeral public key *) bitstring, (* encrypted empty bitstring *) key_t, key_t ). event rcvd2( G_t, (* S_r_pub *) (* values sent in the first protocol message *) G_t, (* initiator's ephemeral public key *) bitstring, (* msg.static *) G_t, (* S_i_pub in the clear *) bitstring, (* msg.timestamp *) timestamp_t, (* timestamp in the clear *) (* values sent in the second protocol message, that have not yet been sent in the first *) G_t, (* responder's ephemeral public key *) bitstring, (* encrypted empty bitstring *) key_t, key_t ). event sent_msg_initiator( G_t, (* S_r_pub *) (* values sent in the first protocol message *) G_t, (* initiator's ephemeral public key *) bitstring, (* msg.static *) G_t, (* S_i_pub in the clear *) bitstring, (* msg.timestamp *) timestamp_t, (* timestamp in the clear *) (* values sent in the second protocol message, that have not yet been sent in the first *) G_t, (* responder's ephemeral public key *) bitstring, (* encrypted empty bitstring *) key_t, key_t, (* new and non-constant values in the transport data message *) counter_t, (* the attacker-provided nonce *) bitstring, (* the ciphertext *) bitstring (* the plaintext *) ). event rcvd_msg_responder(G_t, G_t, bitstring, G_t, bitstring, timestamp_t, G_t, bitstring, key_t, key_t, counter_t, bitstring, bitstring). event sent_msg_responder(G_t, G_t, bitstring, G_t, bitstring, timestamp_t, G_t, bitstring, key_t, key_t, counter_t, bitstring, bitstring). event rcvd_msg_initiator(G_t, G_t, bitstring, G_t, bitstring, timestamp_t, G_t, bitstring, key_t, key_t, counter_t, bitstring, bitstring). ifdef(`m4_uniquesession_chbinding_weakUKS',` (* Session uniqueness, channel binding, and a weak version of resistance to unknown key share attacks (see below) can be proved in a model with all keys (psk, long-term, and ephemeral) compromised. *) (* Session uniqueness 1. Single session with same key *) query i_init <= n_S, i_init2 <= n_S, (* key calculated by the protocol. *) Tir: key_t; event(initiator_uniq_Tir(i_init, Tir)) && event(initiator_uniq_Tir(i_init2, Tir)) ==> i_init = i_init2. query i_init <= n_S, i_init2 <= n_S, (* key calculated by the protocol. *) Tri: key_t; event(initiator_uniq_Tri(i_init, Tri)) && event(initiator_uniq_Tri(i_init2, Tri)) ==> i_init = i_init2. query i_resp <= n_S, i_resp2 <= n_S, (* key calculated by the protocol. *) Tir: key_t; event(responder_uniq_Tir(i_resp, Tir)) && event(responder_uniq_Tir(i_resp2, Tir)) ==> i_resp = i_resp2. query i_resp <= n_S, i_resp2 <= n_S, (* key calculated by the protocol. *) Tri: key_t; event(responder_uniq_Tri(i_resp, Tri)) && event(responder_uniq_Tri(i_resp2, Tri)) ==> i_resp = i_resp2. (* 2. Single session with same public messages *) query i_init <= n_S, i_init2 <= n_S, (* Values sent in the first protocol message. *) E_i_pub: G_t, static_i_enc: bitstring, timestamp_i_enc: bitstring, (* Values sent in the second protocol message, that have not yet been sent in the first. *) E_r_pub_rcvd: G_t, empty_bitstring_enc_rcvd: bitstring; event(initiator_uniq_pubmsg(i_init, E_i_pub, static_i_enc, timestamp_i_enc, E_r_pub_rcvd, empty_bitstring_enc_rcvd)) && event(initiator_uniq_pubmsg(i_init2, E_i_pub, static_i_enc, timestamp_i_enc, E_r_pub_rcvd, empty_bitstring_enc_rcvd)) ==> i_init = i_init2. query i_resp <= n_S, i_resp2 <= n_S, (* Values sent in the first protocol message. *) E_i_pub_rcvd: G_t, static_i_enc_rcvd: bitstring, timestamp_i_enc_rcvd: bitstring, (* Values sent in the second protocol message, that have not yet been sent in the first. *) E_r_pub: G_t, empty_bitstring_enc: bitstring; event(responder_uniq_pubmsg(i_resp, E_i_pub_rcvd, static_i_enc_rcvd, timestamp_i_enc_rcvd, E_r_pub, empty_bitstring_enc)) && event(responder_uniq_pubmsg(i_resp2, E_i_pub_rcvd, static_i_enc_rcvd, timestamp_i_enc_rcvd, E_r_pub, empty_bitstring_enc)) ==> i_resp = i_resp2. (* Channel binding *) query S_i_pub: G_t, S_i_pub_rcvd : G_t, S_X_pub : G_t, S_r_pub : G_t, E_i_pub_sent : G_t, E_i_pub_rcvd : G_t, E_r_pub_rcvd : G_t, E_r_pub_sent : G_t, timestamp_i: timestamp_t, timestamp_i_rcvd: timestamp_t, Q_i: psk_t, Q_r: psk_t, T_i_send: key_t, T_r_recv: key_t, T_i_recv: key_t, T_r_send: key_t, H7: hashoutput_t; event(initiator_H7(S_i_pub, S_X_pub, E_i_pub_sent, E_r_pub_rcvd, timestamp_i, Q_i, T_i_send, T_i_recv, H7)) && event(responder_H7(S_i_pub_rcvd, S_r_pub, E_i_pub_rcvd, E_r_pub_sent, timestamp_i_rcvd, Q_r, T_r_recv, T_r_send, H7)) ==> (S_i_pub = S_i_pub_rcvd) && (S_X_pub = S_r_pub) && (E_i_pub_sent = E_i_pub_rcvd) && (E_r_pub_rcvd = E_r_pub_sent) && (timestamp_i = timestamp_i_rcvd) && (Q_i = Q_r) && (T_i_send = T_r_recv) && (T_i_recv = T_r_send). (* Resistance against Unknown Key-Share attacks. We prove a weaker version when all keys are compromised (pow8(S_i_pub) = pow8(S_i_pub_rcvd) && pow8(S_r_pub) = pow8(S_r_pub_rcvd)) *) query (* We prove resistance againts an unknown key-share attack even in the dishonest case (keys compromised, talking to the attacker. *) (* The keys calculated by the protocol. *) T_i_send: key_t, T_i_recv: key_t, (* Ephemerals. *) E_i_pub: G_t, E_i_pub_rcvd: G_t, E_r_pub: G_t, E_r_pub_rcvd: G_t, (* Static keys. *) S_i_pub: G_t, S_i_pub_rcvd: G_t, S_r_pub: G_t, S_r_pub_rcvd: G_t; event(responder_imb(T_i_send, T_i_recv, E_i_pub_rcvd, E_r_pub, S_i_pub_rcvd, S_r_pub)) && event(initiator_imb(T_i_send, T_i_recv, E_i_pub, E_r_pub_rcvd, S_i_pub, S_r_pub_rcvd)) ==> E_i_pub = E_i_pub_rcvd && E_r_pub = E_r_pub_rcvd && pow8(S_i_pub) = pow8(S_i_pub_rcvd) && pow8(S_r_pub) = pow8(S_r_pub_rcvd). ',` ifdef(`m4_first_msg_auth',` (* Prove authentication of the first protocol message Holds when the static keys are not compromised (at the moment the first message is received); the ephemeral keys may be compromised. *) (* With the timestamp cache, the first protocol message is not replayable. Without the timestamp cache, we can still prove that the first message was at some point created by the initiator *) query S_r_pub: G_t, (* values sent in the first protocol message *) E_i_pub: G_t, static_i_enc: bitstring, S_i_pub: G_t, timestamp_i_enc: bitstring, timestamp_i: timestamp_t; ifdef(`m4_replay_prot',` inj-event(rcvd1(true, S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i)) ==> inj-event(sent1(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i)).',` event(rcvd1(true, S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i)) ==> event(sent1(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i)). ') ',` (* Prove all other properties *) (* For correctness, use WG.25519.correctness.m4.cv *) (* Secrecy *) query secret secret_bit. (* Resistance against Unknown Key-Share attacks. *) query (* We prove resistance againts an unknown key-share attack even in the dishonest case (keys compromised, talking to the attacker. *) (* The keys calculated by the protocol. *) T_i_send: key_t, T_i_recv: key_t, (* Ephemerals *) E_i_pub: G_t, E_i_pub_rcvd: G_t, E_r_pub: G_t, E_r_pub_rcvd: G_t, (* Static keys. *) S_i_pub: G_t, S_i_pub_rcvd: G_t, S_r_pub: G_t, S_r_pub_rcvd: G_t; event(responder_imb(T_i_send, T_i_recv, E_i_pub_rcvd, E_r_pub, S_i_pub_rcvd, S_r_pub)) && event(initiator_imb(T_i_send, T_i_recv, E_i_pub, E_r_pub_rcvd, S_i_pub, S_r_pub_rcvd)) ==> E_i_pub = E_i_pub_rcvd && E_r_pub = E_r_pub_rcvd && S_i_pub = S_i_pub_rcvd && S_r_pub = S_r_pub_rcvd. (* Initiator can authenticate the responder. *) query S_r_pub: G_t, (* values sent in the first protocol message *) E_i_pub: G_t, static_i_enc: bitstring, S_i_pub: G_t, timestamp_i_enc: bitstring, timestamp_i: timestamp_t, (* values sent in the second protocol message, that have not yet been sent in the first *) E_r_pub: G_t, empty_bitstring_enc: bitstring, T_i_send: key_t, T_i_recv: key_t; inj-event(rcvd2(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub, empty_bitstring_enc, T_i_send, T_i_recv)) ==> inj-event(sent2(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub, empty_bitstring_enc, T_i_send, T_i_recv)). query S_r_pub: G_t, (* values sent in the first protocol message *) E_i_pub: G_t, static_i_enc: bitstring, S_i_pub: G_t, timestamp_i_enc: bitstring, timestamp_i: timestamp_t, (* values sent in the second protocol message, that have not yet been sent in the first *) E_r_pub: G_t, empty_bitstring_enc: bitstring, (* new and non-constant values in the transport data message *) counter: counter_t, (* the attacker-provided nonce *) ciphertext: bitstring, (* the ciphertext *) plaintext: bitstring, (* the plaintext *) T_r_recv: key_t, T_r_send: key_t; inj-event(rcvd_msg_responder(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub, empty_bitstring_enc, T_r_recv, T_r_send, counter, ciphertext, plaintext)) ==> inj-event(sent_msg_initiator(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub, empty_bitstring_enc, T_r_recv, T_r_send, counter, ciphertext, plaintext)). query S_r_pub: G_t, (* values sent in the first protocol message *) E_i_pub: G_t, static_i_enc: bitstring, S_i_pub: G_t, timestamp_i_enc: bitstring, timestamp_i: timestamp_t, (* values sent in the second protocol message, that have not yet been sent in the first *) E_r_pub: G_t, empty_bitstring_enc: bitstring, (* new and non-constant values in the transport data message *) counter: counter_t, (* the attacker-provided nonce *) ciphertext: bitstring, (* the ciphertext *) plaintext: bitstring, (* the plaintext *) T_i_send: key_t, T_i_recv: key_t; inj-event(rcvd_msg_initiator(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub, empty_bitstring_enc, T_i_send, T_i_recv, counter, ciphertext, plaintext)) ==> inj-event(sent_msg_responder(S_r_pub, E_i_pub, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub, empty_bitstring_enc, T_i_send, T_i_recv, counter, ciphertext, plaintext)). ') ') (* Type definitions for return values of functions that prepare or process messages prepare1res_t is an "option" type: prepare1succ(...) is the success case prepare1fail is the failure case The disequation prepare1succ(x1,x2,x3,x4,x5,x6,x7,x8) <> prepare1fail guarantees that there is no confusion between these two cases. *) type prepare1res_t. fun prepare1succ(session_index_t, Z_t, G_t, bitstring, bitstring, G_t, G_t, hashoutput_t): prepare1res_t [data]. const prepare1fail: prepare1res_t. equation forall x1: session_index_t, x2: Z_t, x3: G_t, x4: bitstring, x5: bitstring, x6: G_t, x7: G_t, x8: hashoutput_t; prepare1succ(x1,x2,x3,x4,x5,x6,x7,x8) <> prepare1fail. type process1res_t. fun process1succ(G_t, G_t, G_t, hashoutput_t, timestamp_t):process1res_t [data]. const process1fail: process1res_t. equation forall x1: G_t, x2: G_t, x3: G_t, x4: hashoutput_t, x5: timestamp_t; process1succ(x1,x2,x3,x4,x5) <> process1fail. type prepare2res_t. fun prepare2succ(session_index_t, Z_t, G_t, key_t, key_t, hashoutput_t, bitstring):prepare2res_t [data]. const prepare2fail: prepare2res_t. equation forall x1: session_index_t, x2: Z_t, x3: G_t, x4: key_t, x5: key_t, x6: hashoutput_t, x7: bitstring; prepare2succ(x1,x2,x3,x4,x5,x6,x7) <> prepare2fail. type process2res_t. fun process2succ(key_t, key_t, hashoutput_t):process2res_t [data]. const process2fail: process2res_t. equation forall x1: key_t, x2: key_t, x3: hashoutput_t; process2succ(x1,x2,x3) <> process2fail. type preparemsgres_t. fun preparemsgsucc(bitstring, bitstring):preparemsgres_t [data]. const preparemsgfail: preparemsgres_t. equation forall x1: bitstring, x2: bitstring; preparemsgsucc(x1,x2) <> preparemsgfail. type processmsgres_t. fun processmsgsucc(bitstring):processmsgres_t [data]. const processmsgfail: processmsgres_t. equation forall x: bitstring; processmsgsucc(x) <> processmsgfail. (* Prepare the first message e, es, s, ss, {t} *) letfun prepare1( key_hash: hashkey_t, key_rom1: hashkey_t, key_rom2: hashkey_t, S_X_pub_rcvd: G_t, S_i_priv: Z_t, S_i_pub: G_t, timestamp_i: timestamp_t) = new I_i: session_index_t; new E_i_priv: Z_t; (* TODO Why are we not using DH here? *) let E_i_pub: G_t = exp(g, E_i_priv) in let H_i1: hashoutput_t = mix_hash_G(key_hash, hash_construction_identifier, S_X_pub_rcvd) in let H_i2: hashoutput_t = mix_hash_G(key_hash, H_i1, E_i_pub) in let es_i: G_t = DH(S_X_pub_rcvd, E_i_priv) in m4_if_zero(es_i, prepare1fail) let k_i2: key_t = rom1(key_rom1, E_i_pub, es_i) in let static_i_enc: bitstring = enc_G(S_i_pub, H_i2, k_i2, nonce_0) in let H_i3: hashoutput_t = mix_hash_bitstring(key_hash, H_i2, static_i_enc) in let ss_i: G_t = DH(S_X_pub_rcvd, S_i_priv) in m4_if_zero(ss_i, prepare1fail) let k_i3: key_t = rom2(key_rom2, E_i_pub, es_i, ss_i) in let timestamp_i_enc: bitstring = enc_timestamp(timestamp_i, H_i3, k_i3, nonce_0) in let H_i4: hashoutput_t = mix_hash_bitstring(key_hash, H_i3, timestamp_i_enc) in prepare1succ(I_i, E_i_priv, E_i_pub, static_i_enc, timestamp_i_enc, es_i, ss_i, H_i4). (* Process a received first message *) letfun process1( key_hash: hashkey_t, key_rom1: hashkey_t, key_rom2: hashkey_t, allowed_peers: G_set_t, S_r_priv: Z_t, S_r_pub: G_t, E_i_pub_rcvd: G_t, static_i_enc_rcvd: bitstring, timestamp_i_enc_rcvd: bitstring ) = let H_r1: hashoutput_t = mix_hash_G(key_hash, hash_construction_identifier, S_r_pub) in let H_r2: hashoutput_t = mix_hash_G(key_hash, H_r1, E_i_pub_rcvd) in let es_r: G_t = DH(E_i_pub_rcvd, S_r_priv) in m4_if_zero(es_r, process1fail) let k_r2: key_t = rom1(key_rom1, E_i_pub_rcvd, es_r) in let injbot(G_to_bitstring(S_i_pub_rcvd: G_t)) = dec_ad_hash(static_i_enc_rcvd, H_r2, k_r2, nonce_0) in ( if is_in(S_i_pub_rcvd, allowed_peers) then ( let H_r3: hashoutput_t = mix_hash_bitstring(key_hash, H_r2, static_i_enc_rcvd) in let ss_r: G_t = DH(S_i_pub_rcvd, S_r_priv) in m4_if_zero(ss_r, process1fail) let k_r3: key_t = rom2(key_rom2, E_i_pub_rcvd, es_r, ss_r) in let injbot(timestamp_to_bitstring(timestamp_i_rcvd: timestamp_t)) = dec_ad_hash(timestamp_i_enc_rcvd, H_r3, k_r3, nonce_0) in ( let H_r4: hashoutput_t = mix_hash_bitstring(key_hash, H_r3, timestamp_i_enc_rcvd) in process1succ(es_r, ss_r, S_i_pub_rcvd, H_r4, timestamp_i_rcvd) ) else ( (* timestamp did not decrypt *) process1fail ) ) else ( (* peer not allowed *) process1fail ) ) else ( (* static did not decrypt *) process1fail ). (* Prepare the second message e, ee, se, psk, {} *) letfun prepare2( key_hash: hashkey_t, key_rom3: hashkey_t, S_i_pub_rcvd: G_t, E_i_pub_rcvd: G_t, H_r4: hashoutput_t, es_r: G_t, ss_r: G_t, Q: psk_t) = new I_r: session_index_t; new E_r_priv: Z_t; let E_r_pub: G_t = exp(g, E_r_priv) in let ee_r: G_t = DH(E_i_pub_rcvd, E_r_priv) in m4_if_zero(ee_r, prepare2fail) let se_r: G_t = DH(S_i_pub_rcvd, E_r_priv) in m4_if_zero(se_r, prepare2fail) let H_r5: hashoutput_t = mix_hash_G(key_hash, H_r4, E_r_pub) in let concat_four_keys(tau_r4: key_t, k_r4: key_t, T_r_recv: key_t, T_r_send: key_t) = rom3(key_rom3, E_i_pub_rcvd, es_r, ss_r, E_r_pub, ee_r, se_r, Q) in ( let H_r6: hashoutput_t = mix_hash_key(key_hash, H_r5, tau_r4) in let empty_bitstring_r_enc: bitstring = enc_bitstring(empty_bitstring, H_r6, k_r4, nonce_0) in let H_r7: hashoutput_t = mix_hash_bitstring(key_hash, H_r6, empty_bitstring_r_enc) in prepare2succ(I_r, E_r_priv, E_r_pub, T_r_recv, T_r_send, H_r7, empty_bitstring_r_enc) ) else ( prepare2fail ). (* Process a received second message *) letfun process2( key_hash: hashkey_t, key_rom3: hashkey_t, E_i_priv: Z_t, E_i_pub: G_t, S_i_priv: Z_t, S_i_pub: G_t, E_r_pub_rcvd: G_t, empty_bitstring_r_enc_rcvd: bitstring, H_i4: hashoutput_t, es_i: G_t, ss_i: G_t, Q: psk_t) = let ee_i: G_t = DH(E_r_pub_rcvd, E_i_priv) in m4_if_zero(ee_i, process2fail) let se_i: G_t = DH(E_r_pub_rcvd, S_i_priv) in m4_if_zero(se_i, process2fail) let H_i5: hashoutput_t = mix_hash_G(key_hash, H_i4, E_r_pub_rcvd) in let concat_four_keys(tau_i4: key_t, k_i4: key_t, T_i_send: key_t, T_i_recv: key_t) = rom3(key_rom3, E_i_pub, es_i, ss_i, E_r_pub_rcvd, ee_i, se_i, Q) in ( let H_i6: hashoutput_t = mix_hash_key(key_hash, H_i5, tau_i4) in let injbot(=empty_bitstring) = dec_ad_hash(empty_bitstring_r_enc_rcvd, H_i6, k_i4, nonce_0) in ( let H_i7: hashoutput_t = mix_hash_bitstring(key_hash, H_i6, empty_bitstring_r_enc_rcvd) in process2succ(T_i_send, T_i_recv, H_i7) ) else ( (* empty_bitstring_r_enc_rcvd did not decrypt *) process2fail ) ) else ( (* weird case where the rom3 pattern matching did not work - actually never happens *) process2fail ). (* Prepare the payload messages *) letfun prepare_msg( side_index: bitstring, secret_bit_I: bool, plaintext_0: bitstring, plaintext_1: bitstring, counter: counter_t, T_i_send: key_t) = if Zero(plaintext_0) = Zero(plaintext_1) then ( get sent_counters(=side_index, =counter) in preparemsgfail else insert sent_counters(side_index, counter); let plaintext = test(secret_bit_I, plaintext_0, plaintext_1) in let ciphertext = enc(plaintext, empty_bitstring, T_i_send, counter_to_nonce(counter)) in preparemsgsucc(ciphertext, plaintext) ) else ( preparemsgfail ). (* Process the payload messages *) letfun process_msg( side_index: bitstring, counter_rcvd: counter_t, ciphertext_rcvd: bitstring, T_i_recv: key_t) = get rcvd_counters(=side_index, =counter_rcvd) in processmsgfail else insert rcvd_counters(side_index, counter_rcvd); let injbot(plaintext) = dec(ciphertext_rcvd, empty_bitstring, T_i_recv, counter_to_nonce(counter_rcvd)) in ( processmsgsucc(plaintext) ) else ( (* decryption failed *) processmsgfail ). (* The initiator *) let initiator(key_hash: hashkey_t, key_rom1: hashkey_t, key_rom2: hashkey_t, key_rom3: hashkey_t, S_i_priv: Z_t, S_i_pub: G_t, S_r_pub: G_t, secret_bit_I: bool, psk_ir: psk_t) = ! i_N_init_parties <= n_S (* Receive the public key of the responder we should communicate *) (* with, and the timestamp the initiator should use. *) in(c_config_initiator, (S_X_pub: G_t, timestamp_i: timestamp_t, psk_other: psk_t)); let Q = if S_X_pub = S_r_pub then psk_ir else psk_other in let prepare1succ(I_i: session_index_t, E_i_priv: Z_t, E_i_pub_sent: G_t, static_i_enc: bitstring, timestamp_i_enc: bitstring, es_i: G_t, ss_i: G_t, H_i4: hashoutput_t) = prepare1(key_hash, key_rom1, key_rom2, S_X_pub, S_i_priv, S_i_pub, timestamp_i) in ifdef(`m4_first_msg_auth',` event sent1(S_X_pub, E_i_pub_sent, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i); ') out(c_init2resp_send, (ifdef(`m4_E_i_compr',`E_i_priv',`dummy_z'), (msg_type_init2resp, reserved, I_i, E_i_pub_sent, static_i_enc, timestamp_i_enc))); (* Receive two plaintexts for the indistinguishability game of the third protocol message aka key confirmation message. *) in(c_resp2init_recv, (plaintext_0: bitstring, plaintext_1: bitstring, (=msg_type_resp2init, =reserved, I_r_rcvd: session_index_t, =I_i, E_r_pub_rcvd: G_t, empty_bitstring_r_enc_rcvd: bitstring))); let process2succ(T_i_send: key_t, T_i_recv: key_t, H_i7: hashoutput_t) = process2(key_hash, key_rom3, E_i_priv, E_i_pub_sent, S_i_priv, S_i_pub, E_r_pub_rcvd, empty_bitstring_r_enc_rcvd, H_i4, es_i, ss_i, Q) in event initiator_uniq_Tir(i_N_init_parties, T_i_send); event initiator_uniq_Tri(i_N_init_parties, T_i_recv); event initiator_uniq_pubmsg(i_N_init_parties, E_i_pub_sent, static_i_enc, timestamp_i_enc, E_r_pub_rcvd, empty_bitstring_r_enc_rcvd); event initiator_imb(T_i_send, T_i_recv, E_i_pub_sent, E_r_pub_rcvd, S_i_pub, S_X_pub); event initiator_H7(S_i_pub, S_X_pub, E_i_pub_sent, E_r_pub_rcvd, timestamp_i, Q, T_i_send, T_i_recv, H_i7); let honest_session = ifdef(`m4_S_r_compr',`if defined(psk_is_corrupted) then (find j <= n_S suchthat defined(E_r_pub[j]) && pow8(E_r_pub_rcvd) = pow8(E_r_pub[j]) then (* This means we have an honest E_r. *) true else false) else (S_X_pub = S_r_pub)',`(S_X_pub = S_r_pub)') in if not(honest_session) then out(c_keyconfirm_send, (T_i_send, T_i_recv)) (* The adversary can run the rest of the session by himself *) else event rcvd2(S_X_pub, E_i_pub_sent, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub_rcvd, empty_bitstring_r_enc_rcvd, T_i_send, T_i_recv); let preparemsgsucc(ciphertext_keyconfirmation: bitstring, plaintext_keyconfirmation: bitstring) = prepare_msg((is_initiator, i_N_init_parties), secret_bit_I, plaintext_0, plaintext_1, counter_0, T_i_send) in event sent_msg_initiator(S_X_pub, E_i_pub_sent, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub_rcvd, empty_bitstring_r_enc_rcvd, T_i_send, T_i_recv, counter_0, ciphertext_keyconfirmation, plaintext_keyconfirmation); out(c_keyconfirm_send, (msg_type_data, reserved, I_r_rcvd, counter_0, ciphertext_keyconfirmation)); (( ! i_Nis<=n_M in(c_N_init_send_config, (plaintext_data_0: bitstring, plaintext_data_1: bitstring, counter: counter_t)); let preparemsgsucc(ciphertext_data_send: bitstring, plaintext_data_send: bitstring) = prepare_msg((is_initiator, i_N_init_parties), secret_bit_I, plaintext_data_0, plaintext_data_1, counter, T_i_send) in event sent_msg_initiator(S_X_pub, E_i_pub_sent, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub_rcvd, empty_bitstring_r_enc_rcvd, T_i_send, T_i_recv, counter, ciphertext_data_send, plaintext_data_send); out(c_N_init_send, (msg_type_data, reserved, I_r_rcvd, counter, ciphertext_data_send)) )|( ! i_Nir<=n_M in(c_N_init_recv, (=msg_type_data, =reserved, =I_i, counter_rcvd: counter_t, ciphertext_data_rcvd: bitstring)); let processmsgsucc(plaintext_data_rcvd: bitstring) = process_msg((is_initiator, i_N_init_parties), counter_rcvd, ciphertext_data_rcvd, T_i_recv) in event rcvd_msg_initiator(S_X_pub, E_i_pub_sent, static_i_enc, S_i_pub, timestamp_i_enc, timestamp_i, E_r_pub_rcvd, empty_bitstring_r_enc_rcvd, T_i_send, T_i_recv, counter_rcvd, ciphertext_data_rcvd, plaintext_data_rcvd) )). (* The responder *) let responder(key_hash: hashkey_t, key_rom1: hashkey_t, key_rom2: hashkey_t, key_rom3: hashkey_t, S_r_priv: Z_t, S_i_pub: G_t, S_r_pub: G_t, secret_bit_R: bool, psk_ir: psk_t) = ! i_N_resp_parties <= n_S in(c_init2resp_recv, (psk_other: psk_t, allowed_peers: G_set_t, (=msg_type_init2resp, =reserved, I_i_rcvd: session_index_t, E_i_pub_rcvd: G_t, static_i_enc_rcvd: bitstring, timestamp_i_enc_rcvd: bitstring))); let process1succ(es_r: G_t, ss_r: G_t, S_i_pub_rcvd: G_t, H_r4: hashoutput_t, timestamp_i_rcvd: timestamp_t) = process1( key_hash, key_rom1, key_rom2, allowed_peers, S_r_priv, S_r_pub, E_i_pub_rcvd, static_i_enc_rcvd, timestamp_i_enc_rcvd) in let Q = if S_i_pub_rcvd = S_i_pub then psk_ir else psk_other in ifdef(`m4_replay_prot',` get rcvd_timestamps(=S_r_pub, =S_i_pub_rcvd, =timestamp_i_rcvd) in yield else insert rcvd_timestamps(S_r_pub, S_i_pub_rcvd, timestamp_i_rcvd); ') ifdef(`m4_first_msg_auth',` event rcvd1(pow8(S_i_pub_rcvd) = pow8(S_i_pub), S_r_pub, E_i_pub_rcvd, static_i_enc_rcvd, S_i_pub_rcvd, timestamp_i_enc_rcvd, timestamp_i_rcvd); ') let prepare2succ(I_r: session_index_t, E_r_priv: Z_t, E_r_pub_sent: G_t, T_r_recv: key_t, T_r_send: key_t, H_r7: hashoutput_t, empty_bitstring_enc: bitstring) = prepare2(key_hash, key_rom3, S_i_pub_rcvd, E_i_pub_rcvd, H_r4, es_r, ss_r, Q) in event sent2(S_r_pub, E_i_pub_rcvd, static_i_enc_rcvd, S_i_pub_rcvd, timestamp_i_enc_rcvd, timestamp_i_rcvd, E_r_pub_sent, empty_bitstring_enc, T_r_recv, T_r_send); event responder_uniq_Tir(i_N_resp_parties, T_r_recv); event responder_uniq_Tri(i_N_resp_parties, T_r_send); event responder_uniq_pubmsg(i_N_resp_parties, E_i_pub_rcvd, static_i_enc_rcvd, timestamp_i_enc_rcvd, E_r_pub_sent, empty_bitstring_enc); event responder_imb(T_r_recv, T_r_send, E_i_pub_rcvd, E_r_pub_sent, S_i_pub_rcvd, S_r_pub); event responder_H7(S_i_pub_rcvd, S_r_pub, E_i_pub_rcvd, E_r_pub_sent, timestamp_i_rcvd, Q, T_r_recv, T_r_send, H_r7); out(c_resp2init_send, (ifdef(`m4_E_r_compr',`E_r_priv',`dummy_z'), (msg_type_resp2init, reserved, I_r, I_i_rcvd, E_r_pub_sent, empty_bitstring_enc))); (* First data transport message is key confirmation. *) in(c_keyconfirm_recv, (=msg_type_data, =reserved, =I_r, counter_keyconfirmation: counter_t, ciphertext_keyconfirmation_rcvd: bitstring)); (* This means we have an honest E_i. In this case it cannot be corrupted, because we never corrupt S_i and E_i at the same time. Thus, the attacker cannot get the secret key, because E_i_priv is secret. *) let honest_session = ifdef(`m4_S_i_compr',`if defined(psk_is_corrupted) then (find j <= n_S suchthat defined(E_i_pub_sent[j],S_X_pub[j]) && pow8(E_i_pub_rcvd) = pow8(E_i_pub_sent[j]) && S_X_pub[j] = S_r_pub && S_i_pub_rcvd = S_i_pub then true else false) else (S_i_pub_rcvd = S_i_pub)',`(S_i_pub_rcvd = S_i_pub)') in if not(honest_session) then out(c_wait_before_2nd_part, (T_r_recv, T_r_send)) (* The adversary can run the rest of the session by himself *) else let processmsgsucc(plaintext_keyconfirmation_rcvd: bitstring) = process_msg((is_responder, i_N_resp_parties), counter_keyconfirmation, ciphertext_keyconfirmation_rcvd, T_r_recv) in event rcvd_msg_responder(S_r_pub, E_i_pub_rcvd, static_i_enc_rcvd, S_i_pub_rcvd, timestamp_i_enc_rcvd, timestamp_i_rcvd, E_r_pub_sent, empty_bitstring_enc, T_r_recv, T_r_send, counter_keyconfirmation, ciphertext_keyconfirmation_rcvd, plaintext_keyconfirmation_rcvd); out(c_wait_before_2nd_part, ()); (( ! i_Nrs<=n_M in(c_N_resp_send_config, (plaintext_0: bitstring, plaintext_1: bitstring, counter: counter_t)); let preparemsgsucc(ciphertext_data_send: bitstring, plaintext_data_send: bitstring) = prepare_msg((is_responder, i_N_resp_parties), secret_bit_R, plaintext_0, plaintext_1, counter, T_r_send) in event sent_msg_responder(S_r_pub, E_i_pub_rcvd, static_i_enc_rcvd, S_i_pub_rcvd, timestamp_i_enc_rcvd, timestamp_i_rcvd, E_r_pub_sent, empty_bitstring_enc, T_r_recv, T_r_send, counter, ciphertext_data_send, plaintext_data_send); out(c_N_resp_send, (msg_type_data, reserved, I_i_rcvd, counter, ciphertext_data_send)) )|( ! i_Nrr<=n_M in(c_N_resp_recv, (=msg_type_data, =reserved, =I_r, counter_rcvd: counter_t, ciphertext_data_rcvd: bitstring)); let processmsgsucc(plaintext_data_rcvd: bitstring) = process_msg((is_responder, i_N_resp_parties), counter_rcvd, ciphertext_data_rcvd, T_r_recv) in event rcvd_msg_responder(S_r_pub, E_i_pub_rcvd, static_i_enc_rcvd, S_i_pub_rcvd, timestamp_i_enc_rcvd, timestamp_i_rcvd, E_r_pub_sent, empty_bitstring_enc, T_r_recv, T_r_send, counter_rcvd, ciphertext_data_rcvd, plaintext_data_rcvd) )). (* Swapped initiator and responder - we prove no security properties for these sessions *) (* Copy of prepare2 because we need to change the name of the variable E_r_pub to avoid a confusion with that variable in I->R case. *) letfun prepare2_sw( key_hash: hashkey_t, key_rom3: hashkey_t, S_i_pub_rcvd: G_t, E_i_pub_rcvd: G_t, H_r4: hashoutput_t, es_r: G_t, ss_r: G_t, Q: psk_t) = new I_r: session_index_t; new E_r_priv: Z_t; let E_r_pub_sw: G_t = exp(g, E_r_priv) in let ee_r: G_t = DH(E_i_pub_rcvd, E_r_priv) in m4_if_zero(ee_r, prepare2fail) let se_r: G_t = DH(S_i_pub_rcvd, E_r_priv) in m4_if_zero(se_r, prepare2fail) let H_r5: hashoutput_t = mix_hash_G(key_hash, H_r4, E_r_pub_sw) in let concat_four_keys(tau_r4: key_t, k_r4: key_t, T_r_recv: key_t, T_r_send: key_t) = rom3(key_rom3, E_i_pub_rcvd, es_r, ss_r, E_r_pub_sw, ee_r, se_r, Q) in ( let H_r6: hashoutput_t = mix_hash_key(key_hash, H_r5, tau_r4) in let empty_bitstring_r_enc: bitstring = enc_bitstring(empty_bitstring, H_r6, k_r4, nonce_0) in let H_r7: hashoutput_t = mix_hash_bitstring(key_hash, H_r6, empty_bitstring_r_enc) in prepare2succ(I_r, E_r_priv, E_r_pub_sw, T_r_recv, T_r_send, H_r7, empty_bitstring_r_enc) ) else ( prepare2fail ). let initiator_swapped(key_hash: hashkey_t, key_rom1: hashkey_t, key_rom2: hashkey_t, key_rom3: hashkey_t, S_i_priv: Z_t, S_i_pub: G_t, S_r_pub: G_t, secret_bit_I: bool, psk_ir: psk_t) = ! i_N_init_parties <= n_S (* Receive the public key of the responder we should communicate *) (* with, and the timestamp the initiator should use. *) in(c_config_initiator_sw, (S_X_pub_sw: G_t, timestamp_i: timestamp_t, psk_other: psk_t)); let Q = if S_X_pub_sw = S_r_pub then psk_ir else psk_other in let prepare1succ(I_i: session_index_t, E_i_priv: Z_t, E_i_pub_sent_sw: G_t, static_i_enc: bitstring, timestamp_i_enc: bitstring, es_i: G_t, ss_i: G_t, H_i4: hashoutput_t) = prepare1(key_hash, key_rom1, key_rom2, S_X_pub_sw, S_i_priv, S_i_pub, timestamp_i) in out(c_init2resp_send_sw, (E_i_priv (* Always compromise ephemeral *), (msg_type_init2resp, reserved, I_i, E_i_pub_sent_sw, static_i_enc, timestamp_i_enc))); (* Receive two plaintexts for the indistinguishability game of the third protocol message aka key confirmation message. *) in(c_resp2init_recv_sw, (plaintext_0: bitstring, plaintext_1: bitstring, (=msg_type_resp2init, =reserved, I_r_rcvd: session_index_t, =I_i, E_r_pub_rcvd: G_t, empty_bitstring_r_enc_rcvd: bitstring))); let process2succ(T_i_send: key_t, T_i_recv: key_t, H_i7: hashoutput_t) = process2(key_hash, key_rom3, E_i_priv, E_i_pub_sent_sw, S_i_priv, S_i_pub, E_r_pub_rcvd, empty_bitstring_r_enc_rcvd, H_i4, es_i, ss_i, Q) in out(c_keyconfirm_send_sw, (T_i_send, T_i_recv)). (* The adversary can run the rest of the session by himself *) let responder_swapped(key_hash: hashkey_t, key_rom1: hashkey_t, key_rom2: hashkey_t, key_rom3: hashkey_t, S_r_priv: Z_t, S_i_pub: G_t, S_r_pub: G_t, secret_bit_R: bool, psk_ir: psk_t) = ! i_N_resp_parties <= n_S in(c_init2resp_recv_sw, (psk_other: psk_t, allowed_peers: G_set_t, (=msg_type_init2resp, =reserved, I_i_rcvd: session_index_t, E_i_pub_rcvd: G_t, static_i_enc_rcvd: bitstring, timestamp_i_enc_rcvd: bitstring))); let process1succ(es_r: G_t, ss_r: G_t, S_i_pub_rcvd: G_t, H_r4: hashoutput_t, timestamp_i_rcvd: timestamp_t) = process1( key_hash, key_rom1, key_rom2, allowed_peers, S_r_priv, S_r_pub, E_i_pub_rcvd, static_i_enc_rcvd, timestamp_i_enc_rcvd) in let Q = if S_i_pub_rcvd = S_i_pub then psk_ir else psk_other in ifdef(`m4_replay_prot',` get rcvd_timestamps(=S_r_pub, =S_i_pub_rcvd, =timestamp_i_rcvd) in yield else insert rcvd_timestamps(S_r_pub, S_i_pub_rcvd, timestamp_i_rcvd); ') let prepare2succ(I_r: session_index_t, E_r_priv: Z_t, E_r_pub_sent: G_t, T_r_recv: key_t, T_r_send: key_t, H_r7: hashoutput_t, empty_bitstring_enc: bitstring) = prepare2_sw(key_hash, key_rom3, S_i_pub_rcvd, E_i_pub_rcvd, H_r4, es_r, ss_r, Q) in out(c_resp2init_send_sw, (E_r_priv (* Always compromise ephemeral *), (msg_type_resp2init, reserved, I_r, I_i_rcvd, E_r_pub_sent, empty_bitstring_enc), (T_r_recv, T_r_send))). (* The adversary can run the rest of the session by himself *) (* Corruption processes: the adversary uses them to corrupt the long-term keys dynamically *) let corrupt_psk(psk: psk_t) = in(c_corrupt_psk, ()); let psk_is_corrupted: bool = true in out(c_corrupt_psk, psk). process in(c_start, ()); new psk: psk_t; new key_hash: hashkey_t; new key_rom1: hashkey_t; new key_rom2: hashkey_t; new key_rom3: hashkey_t; new S_A_priv: Z_t; let S_A_pub = exp(g, S_A_priv) in new S_B_priv: Z_t; let S_B_pub = exp(g, S_B_priv) in (* Secret bit for the indistinguishability game. *) new secret_bit : bool; (* hand over control to the attacker *) out(c_publickeys, (ifdef(`m4_S_i_compr',`S_A_priv',`S_A_pub'), ifdef(`m4_S_r_compr',`S_B_priv',`S_B_pub'))); (initiator(key_hash, key_rom1, key_rom2, key_rom3, S_A_priv, S_A_pub, S_B_pub, secret_bit, psk) | responder(key_hash, key_rom1, key_rom2, key_rom3, S_B_priv, S_A_pub, S_B_pub, secret_bit, psk) | ifdef(`m4_AB',`',` (* Swapped initiator and responder *) initiator_swapped(key_hash, key_rom1, key_rom2, key_rom3, S_B_priv, S_B_pub, S_A_pub, secret_bit, psk) | responder_swapped(key_hash, key_rom1, key_rom2, key_rom3, S_A_priv, S_B_pub, S_A_pub, secret_bit, psk) | ') rom1_oracle(key_rom1) | rom2_oracle(key_rom2) | rom3_oracle(key_rom3) | hash_oracle(key_hash) | corrupt_psk(psk) ) ifdef(`m4_AB',` ifdef(`m4_replay_prot',` ifdef(`m4_S_i_compr',` ifdef(`m4_S_r_compr',` (* WG.25519.psk_dyn.AB.S_i_compr.S_r_compr.replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 1 All queries proved. 1369.632s (user 1368.104s + system 1.528s), max rss 610060K END *) ',` (* WG.25519.psk_dyn.AB.S_i_compr.E_r_compr.replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 2 All queries proved. 910.124s (user 908.756s + system 1.368s), max rss 401432K END *) ') ',` (* WG.25519.psk_dyn.AB.E_i_compr.S_r_compr.replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 3 All queries proved. 3050.044s (user 3047.180s + system 2.864s), max rss 1213328K END *) ') ',` ifdef(`m4_S_i_compr',` ifdef(`m4_S_r_compr',` (* WG.25519.psk_dyn.AB.S_i_compr.S_r_compr.no_replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 4 All queries proved. 781.512s (user 780.180s + system 1.332s), max rss 530484K END *) ',` (* WG.25519.psk_dyn.AB.S_i_compr.E_r_compr.no_replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 5 All queries proved. 531.324s (user 530.420s + system 0.904s), max rss 353152K END *) ') ',` (* WG.25519.psk_dyn.AB.E_i_compr.S_r_compr.no_replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 6 All queries proved. 1343.364s (user 1340.896s + system 2.468s), max rss 1212112K END *) ') ') ',` ifdef(`m4_replay_prot',` ifdef(`m4_S_i_compr',` ifdef(`m4_S_r_compr',` (* WG.25519.psk_dyn.AB-BA.S_i_compr.S_r_compr.replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 7 All queries proved. 1774.216s (user 1771.616s + system 2.600s), max rss 841696K END *) ',` (* WG.25519.psk_dyn.AB-BA.S_i_compr.E_r_compr.replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 8 All queries proved. 1300.364s (user 1298.504s + system 1.860s), max rss 800780K END *) ') ',` (* WG.25519.psk_dyn.AB-BA.E_i_compr.S_r_compr.replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 9 All queries proved. 3754.168s (user 3750.096s + system 4.072s), max rss 1835236K END *) ') ',` ifdef(`m4_S_i_compr',` ifdef(`m4_S_r_compr',` (* WG.25519.psk_dyn.AB-BA.S_i_compr.S_r_compr.no_replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 10 All queries proved. 987.000s (user 984.828s + system 2.172s), max rss 733500K END *) ',` (* WG.25519.psk_dyn.AB-BA.S_i_compr.E_r_compr.no_replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 11 All queries proved. 713.064s (user 711.376s + system 1.688s), max rss 697488K END *) ') ',` (* WG.25519.psk_dyn.AB-BA.E_i_compr.S_r_compr.no_replay_prot EXPECTED FILENAME: examples/wireguard/WG.25519.psk_dyn.m4.cv TAG: 12 All queries proved. 1655.132s (user 1651.564s + system 3.568s), max rss 1598368K END *) ') ') ')