(* Noise NK: see http://www.noiseprotocol.org/noise.html
  <- s
  ...
  -> e, es 
  <- e, ee
  ->   [prove strong forward secrecy for this payload, sent by the initiator]
*)

(* To speed up proofs of correspondences *)
set casesInCorresp = false.
(* To speed up the proof *)
set autoMergeBranches = false.
(* To save memory *)
set forgetOldGames = true.


proof {
  (* 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;
  (* This is in fact the default; mentioned here just as a reminder.
     We unset it later for speed. *)
  set elsefindFactsInSimplify = true;
  out_game "g1.cv";
  (* 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. *)

  (* Distinguish whether the ephemeral E_r_pub_rcvd_1 received by the
     initiator is equivalent to an ephemeral E_r_pub generated by
     the honest responder. *)
  SArename E_r_pub;
  out_game "g2.cv";
  insert after "in(c_resp2init_recv\\[" "find j <= n_S suchthat defined(E_r_pub_1[j]) && pow8(E_r_pub_rcvd_1) = pow8(E_r_pub_1[j]) then";
  simplify;
  (* We apply the ROM assumptions in the order rom2, rom1
     to reduce the number of case distinctions made by CryptoVerif.
     Since rom2 is called after rom1, if we applied 
     rom1 first, that would copy the calls to rom2 
     for each case distinguished by rom1, and thus creates many
     more calls and case distinctions to make in rom2.
     Appliying them in the reverse order avoids that.

     In the random oracle rom2 provided to the adversary,
     distinguish whether the argument of rom2 is a pair in which the
     components are elements of the subgroup of curve25519
     generated by the base point.
     In all calls to rom2 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_rom2" "let rom2_input(G8_to_G(x1_rom2), G8_to_G(x2_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 G8_to_G(x1_rom1) = x_rom1 in";
  (* Apply the ROM assumption to rom1 *)
  crypto rom(rom1);
  out_game "g3.cv";
  crypto gdh(exp_div8) [variables: S_r_priv_2 -> b, E_i_priv_2 -> a, E_r_priv_5 -> b, E_r_priv_4 -> b .];
  crypto splitter(concat_three_keys) **;
  (* Apply ciphertext integrity for the AEAD scheme *)
  crypto int_ctxt(enc) *;
  out_game "g4.cv";
  crypto int_ctxt_corrupt(enc) k_8;
  success; (* some nonce reuse *)
  crypto ind_cpa(enc) *;
  success
}

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'.) *)

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].

type nonce_t [large,fixed].        (* 12 byte counter nonce for AEAD. *)
const nonce_0: nonce_t.            (* const value for the zero nonce  *)

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

expand ROM_hash_refactored(
  (* types *)
  hashkey_t,   (* key of the hash function, models the choice of the
                  hash function *)
  G_t, (* input type *)
  key_t,       (* output type *)
  (* functions *)
  rom1,  (* name of the random oracle hash function:
                  rom1(hashkey_t, G_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 *)
).

(* This models the derivation of a second intermediate symmetric key. *)
type rom2_input_t.
fun rom2_input(G_t, G_t): rom2_input_t [data].
type three_keys_t [large,fixed].

expand ROM_hash_refactored(
  (* types *)
  hashkey_t,   (* key of the hash function, models the choice of the
                  hash function *)
  rom2_input_t, (* input type *)
  three_keys_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) =
   rom2_intermediate(hk, rom2_input(x1_rom2, x2_rom2)).


expand split_3(
  (* types *)
  three_keys_t,  (* intermediary output type of the actual random      *)
                (* oracle *)
  key_t,        (* All the 3 parts to extract have type key_t *)
  key_t,
  key_t,
  (* functions *)
  concat_three_keys, (* function that concatenates the three parts. *)
  (* variables *)
  k, (* Names of the variables used when applying the equivalence   *)
  T_i_send,   (* This makes the games in the proof much more readable.       *)
  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_r.

(* WireGuard specific types *)
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. *)


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

(* Convenience wrappers for enc and dec that take care
   of type conversions. *)
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_bitstring(plaintext: bitstring, current_hash: hashoutput_t, k: key_t, n: nonce_t) =
  enc(plaintext, hashoutput_to_bitstring(current_hash), k, n).

const empty_bitstring: bitstring. (* additional data for data messages *)

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


(* Authentication *)

event sent_msg_initiator(
  (* values sent in the first protocol message *)
  G_t,                (* initiator's ephemeral public key *)
  bitstring,          (* payload1 *)
  bitstring,          (* encrypted payload1 *)
  (* values sent in the second protocol message *)
  G_t,                (* responder's ephemeral public key *)
  bitstring,          (* payload2 *)
  bitstring,          (* encrypted payload2 *)
  (* data keys *)
  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, bitstring, bitstring, 
                      G_t, bitstring, bitstring, key_t, key_t,
                      counter_t, bitstring, bitstring).
event sent_msg_responder(G_t, bitstring, bitstring, 
                      G_t, bitstring, bitstring, key_t, key_t,
                      counter_t, bitstring, bitstring).
event rcvd_msg_initiator(G_t, bitstring, bitstring, 
                      G_t, bitstring, bitstring, key_t, key_t,
                      counter_t, bitstring, bitstring).


query
  (* values sent in the first protocol message *)
  E_i_pub: G_t,
  payload1: bitstring,
  payload1_enc: bitstring,
  (* values sent in the second protocol message *)
  E_r_pub: G_t,
  payload2: bitstring,
  payload2_enc: bitstring,
  (* data keys *)
  T_r_recv: key_t,
  T_r_send: key_t,
  (* 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 *)
  inj-event(rcvd_msg_responder(E_i_pub, payload1, payload1_enc, E_r_pub, payload2, payload2_enc, T_r_recv, T_r_send, counter, ciphertext, plaintext)) ==>
  inj-event(sent_msg_initiator(E_i_pub, payload1, payload1_enc, E_r_pub, payload2, payload2_enc, T_r_recv, T_r_send, counter, ciphertext, plaintext)).

query
  (* values sent in the first protocol message *)
  E_i_pub: G_t,
  payload1: bitstring,
  payload1_enc: bitstring,
  (* values sent in the second protocol message *)
  E_r_pub: G_t,
  payload2: bitstring,
  payload2_enc: bitstring,
  (* data keys *)
  T_r_recv: key_t,
  T_r_send: key_t,
  (* 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 *)
  inj-event(rcvd_msg_initiator(E_i_pub, payload1, payload1_enc, E_r_pub, payload2, payload2_enc, T_r_recv, T_r_send, counter, ciphertext, plaintext)) ==>
  inj-event(sent_msg_responder(E_i_pub, payload1, payload1_enc, E_r_pub, payload2, payload2_enc, T_r_recv, T_r_send, counter, ciphertext, plaintext)).

(* Secrecy *)
query secret secret_bit.


(* 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(Z_t, G_t, bitstring, G_t, hashoutput_t): prepare1res_t [data].
const prepare1fail: prepare1res_t.
equation forall x1: Z_t, x2: G_t, x3: bitstring, x4: G_t, x5: hashoutput_t;
   prepare1succ(x1,x2,x3,x4,x5) <> prepare1fail.

type process1res_t.
fun process1succ(G_t, hashoutput_t, bitstring):process1res_t [data].
const process1fail: process1res_t.
equation forall x1: G_t, x2: hashoutput_t, x3: bitstring;
   process1succ(x1,x2,x3) <> process1fail.

type prepare2res_t.
fun prepare2succ(Z_t, G_t, key_t, key_t, hashoutput_t, bitstring):prepare2res_t [data].
const prepare2fail: prepare2res_t.
equation forall x1: Z_t, x2: G_t, x3: key_t, x4: key_t, x5: hashoutput_t, x6: bitstring;
   prepare2succ(x1,x2,x3,x4,x5,x6) <> prepare2fail.
   
type process2res_t.
fun process2succ(key_t, key_t, hashoutput_t, bitstring):process2res_t [data].
const process2fail: process2res_t.
equation forall x1: key_t, x2: key_t, x3: hashoutput_t, x4: bitstring;
   process2succ(x1,x2,x3,x4) <> 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, {p1} *)

letfun prepare1(
          key_hash: hashkey_t,
          key_rom1: hashkey_t,
          S_X_pub_rcvd: G_t,
          payload1: bitstring) =

  new E_i_priv: Z_t;
  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

  let k_i2: key_t = rom1(key_rom1, es_i) in

  let payload1_enc: bitstring = enc_bitstring(payload1, H_i2, k_i2, nonce_0) in
  let H_i3: hashoutput_t = mix_hash_bitstring(key_hash, H_i2, payload1_enc) in

  prepare1succ(E_i_priv, E_i_pub, payload1_enc, es_i, H_i3).

(* Process a received first message *)

letfun process1(
          key_hash: hashkey_t,
          key_rom1: hashkey_t,
          S_r_priv: Z_t,
          S_r_pub: G_t,
          E_i_pub_rcvd: G_t,
          payload1_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

    let k_r2: key_t = rom1(key_rom1, es_r) in

    let injbot(payload1_rcvd) = dec_ad_hash(payload1_enc_rcvd, H_r2, k_r2, nonce_0) in
    (
        let H_r3: hashoutput_t = mix_hash_bitstring(key_hash, H_r2, payload1_enc_rcvd) in

        process1succ(es_r, H_r3, payload1_rcvd)
    ) else (
      (* payload1 did not decrypt *)
      process1fail
    ).

(* Prepare the second message e, ee, {p2} *)

letfun prepare2(
    key_hash: hashkey_t,
    key_rom2: hashkey_t,
    E_i_pub_rcvd: G_t,
    H_r3: hashoutput_t, es_r: G_t, payload2: bitstring) =

  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

  let H_r4: hashoutput_t = mix_hash_G(key_hash, H_r3, E_r_pub) in

  let concat_three_keys(k_r4: key_t, T_r_recv: key_t, T_r_send: key_t) = rom2(key_rom2, es_r, ee_r) in
  (
    let payload2_enc: bitstring = enc_bitstring(payload2, H_r4, k_r4, nonce_0) in
    let H_r5: hashoutput_t = mix_hash_bitstring(key_hash, H_r4, payload2_enc) in

    prepare2succ(E_r_priv, E_r_pub, T_r_recv, T_r_send, H_r5, payload2_enc)
  ) else (
    prepare2fail
  ).

(* Process a received second message *)

letfun process2(
          key_hash: hashkey_t,
          key_rom2: hashkey_t,
          E_i_priv: Z_t, E_i_pub: G_t, 
          E_r_pub_rcvd: G_t, payload2_enc_rcvd: bitstring, 
          H_i3: hashoutput_t,
          es_i: G_t) =
  let ee_i: G_t = DH(E_r_pub_rcvd, E_i_priv) in

  let H_i4: hashoutput_t = mix_hash_G(key_hash, H_i3, E_r_pub_rcvd) in

  let concat_three_keys(k_i4: key_t, T_i_send: key_t, T_i_recv: key_t) = rom2(key_rom2, es_i, ee_i) in
  (
    let injbot(payload2_rcvd) = dec_ad_hash(payload2_enc_rcvd, H_i4, k_i4, nonce_0) in
    (
      let H_i5: hashoutput_t = mix_hash_bitstring(key_hash, H_i4, payload2_enc_rcvd) in
      process2succ(T_i_send, T_i_recv, H_i5, payload2_rcvd)
    ) else (
      (* payload2_enc_rcvd did not decrypt *)
      process2fail
    )
  ) else (
    (* weird case where the rom2 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,
              S_r_pub: G_t,
              secret_bit_I: bool) =

  ! i_N_init_parties <= n_S
  (* Receive the payload the initiator should use. *)
  in(c_config_initiator, payload1: bitstring);

    let prepare1succ(
         E_i_priv: Z_t, E_i_pub_sent: G_t, payload1_enc: bitstring,
         es_i: G_t, H_i3: hashoutput_t) =
      prepare1(key_hash, key_rom1, S_r_pub, payload1) in

    out(c_init2resp_send, (E_i_pub_sent, payload1_enc));

    in(c_resp2init_recv, (E_r_pub_rcvd: G_t, payload2_enc_rcvd: bitstring));

    let honest_session_i = (if defined(S_r_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 true) in

    let process2succ(T_i_send: key_t, T_i_recv: key_t, H_i5: hashoutput_t, payload2_rcvd: bitstring) =
      process2(key_hash, key_rom2, E_i_priv, E_i_pub_sent, E_r_pub_rcvd, payload2_enc_rcvd, H_i3, es_i) in

    if not(honest_session_i) then
      out(c_wait_before_2nd_part, (T_i_send, T_i_recv))
      (* The adversary can run the rest of the session by himself *)
    else

    out(c_wait_before_2nd_part, ());

    ((
      ! 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(E_i_pub_sent, payload1, payload1_enc, E_r_pub_rcvd, payload2_rcvd, payload2_enc_rcvd, T_i_send, T_i_recv, counter, ciphertext_data_send, plaintext_data_send);
      out(c_N_init_send, (counter, ciphertext_data_send))
    )|(
      ! i_Nir<=n_M
      in(c_N_init_recv, (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(E_i_pub_sent, payload1, payload1_enc, E_r_pub_rcvd, payload2_rcvd, payload2_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, S_r_priv: Z_t, S_r_pub: G_t, secret_bit_R: bool) =

  ! i_N_resp_parties <= n_S

  in(c_init2resp_recv, (E_i_pub_rcvd: G_t, payload1_enc_rcvd: bitstring, payload2: bitstring));

      (* This means we have honest E_i and S_r. Thus, the attacker cannot get the secret key, because E_i_priv and S_r_priv are secret. *)
    let honest_session_r : bool = (find j <= n_S suchthat defined(E_i_pub_sent[j]) && pow8(E_i_pub_rcvd) = pow8(E_i_pub_sent[j]) then true else false) in

    let process1succ(es_r: G_t, H_r3: hashoutput_t, payload1_rcvd: bitstring) =
      process1(
        key_hash, key_rom1, S_r_priv, S_r_pub,
        E_i_pub_rcvd, payload1_enc_rcvd) in

    let prepare2succ(E_r_priv: Z_t, E_r_pub_sent: G_t, T_r_recv: key_t, T_r_send: key_t, H_r5: hashoutput_t, payload2_enc: bitstring) =
      prepare2(key_hash, key_rom2,
        E_i_pub_rcvd, H_r3, es_r, payload2) in

    if not(honest_session_r) then
        out(c_resp2init_send, (E_r_pub_sent, payload2_enc, T_r_recv, T_r_send))
        (* The adversary can run the rest of the session by himself *)

    else
    out(c_resp2init_send, (E_r_pub_sent, payload2_enc));

    ((
      ! 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(E_i_pub_rcvd, payload1_rcvd, payload1_enc_rcvd, E_r_pub_sent, payload2, payload2_enc, T_r_recv, T_r_send, counter, ciphertext_data_send, plaintext_data_send);
      out(c_N_resp_send, (counter, ciphertext_data_send))
    )|(
      ! i_Nrr<=n_M
      in(c_N_resp_recv, (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(E_i_pub_rcvd, payload1_rcvd, payload1_enc_rcvd, E_r_pub_sent, payload2, payload2_enc, T_r_recv, T_r_send, counter_rcvd, ciphertext_data_rcvd, plaintext_data_rcvd)
    )).


(* Corruption process: the adversary uses it to corrupt
   the long-term key dynamically *)

let corrupt_S_r(S_r_priv: Z_t) =
  in(c_corrupt_S_r, ());
  let S_r_is_corrupted: bool = true in
  out(c_corrupt_S_r, S_r_priv).


process
  in(c_start, ());

  new key_hash: hashkey_t;
  new key_rom1: hashkey_t;
  new key_rom2: hashkey_t;

  new S_r_priv: Z_t;
  let S_r_pub = exp(g, S_r_priv) in

  (* Secret bit for the indistinguishability game. *)
  new secret_bit : bool;

  (* hand over control to the attacker *)
  out(c_publickeys, S_r_pub);

  (initiator(key_hash, key_rom1, key_rom2, S_r_pub, secret_bit) |
   responder(key_hash, key_rom1, key_rom2, S_r_priv, S_r_pub, secret_bit) |
   rom1_oracle(key_rom1) | rom2_oracle(key_rom2) |
   hash_oracle(key_hash) |
   corrupt_S_r(S_r_priv)
  )


(* EXPECTED
All queries proved.
15.928s (user 15.848s + system 0.080s), max rss 58556K
END *)