keyschedule.auth.prf.proof

Initial state
Game 2 is
     Ostart() :=
     cr_key_3 <-R cr_key_t;
     return(cr_key_3);
     ((
       foreach ikey_1 <= Nkey do
       Ok() :=
       return();
       foreach i_1 <= Nperkey do
       Oprf(info_4: bitstring) :=
       find [unique?] j_1 = j <= Nperkey suchthat defined(info_4[j], r[j]) && (info_4[j] = info_4) then
         return(r[j_1])
       else
         r <-R keys_t;
         return(r)
     ) | (
       OH() :=
       return(cr_key_3)
     ))


Applying expand get, insert and prove unique annotations
  - Proved that [unique] annotations are correct
yields

Game 3 is
     Ostart() :=
     cr_key_3 <-R cr_key_t;
     return(cr_key_3);
     ((
       foreach ikey_1 <= Nkey do
       Ok() :=
       return();
       foreach i_1 <= Nperkey do
       Oprf(info_4: bitstring) :=
       find [unique] j_1 = j <= Nperkey suchthat defined(info_4[j], r[j]) && (info_4[j] = info_4) then
         return(r[j_1])
       else
         r <-R keys_t;
         return(r)
     ) | (
       OH() :=
       return(cr_key_3)
     ))

Initial state
Game 1 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       return((mode: mode_t <- mode_auth; psk: bitstring <- default_psk; psk_id: bitstring <- default_psk_id; psk_id_hash: cr_output_t <- (salt_3: cr_salt_t <- empty; label_5: label_extract_t <- label_psk_id_hash; labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, psk_id); Extract_CR(cr_key_2, salt_3, labeled_input)); info_hash: cr_output_t <- (salt_4: cr_salt_t <- empty; label_6: label_extract_t <- label_info_hash; labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3); Extract_CR(cr_key_2, salt_4, labeled_input_1)); key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash); secrett: extract_t <- (label_7: label_extract_t <- label_secret; IKM: bitstring <- psk; labeled_IKM: bitstring <- concat_PRF(RFCXXXX, suite_id, label_7, IKM); Extract_PRF(k, labeled_IKM)); key: key_t <- (label_8: label_expand_t <- label_key; L_2: length_t <- Nk; truncate_to_Nk((labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context); Expand_PRF(secrett, labeledInfo)))); base_nonce: nonce_t <- (label_9: label_expand_t <- label_base_nonce; L_3: length_t <- Nn; truncate_to_Nn((labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context); Expand_PRF(secrett, labeledInfo_1)))); concat(key, base_nonce)))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying expand
  - Expand if/find/let
yields

Game 4 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       mode: mode_t <- mode_auth;
       psk: bitstring <- default_psk;
       psk_id: bitstring <- default_psk_id;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       label_7: label_extract_t <- label_secret;
       IKM: bitstring <- psk;
       labeled_IKM: bitstring <- concat_PRF(RFCXXXX, suite_id, label_7, IKM);
       secrett: extract_t <- Extract_PRF(k, labeled_IKM);
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on IKM (definition removed, all usages removed)
yields

Game 5 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       mode: mode_t <- mode_auth;
       psk: bitstring <- default_psk;
       psk_id: bitstring <- default_psk_id;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       label_7: label_extract_t <- label_secret;
       labeled_IKM: bitstring <- concat_PRF(RFCXXXX, suite_id, label_7, psk);
       secrett: extract_t <- Extract_PRF(k, labeled_IKM);
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of binder psk
  - Remove assignments on psk (definition removed, all usages removed)
yields

Game 6 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       mode: mode_t <- mode_auth;
       psk_id: bitstring <- default_psk_id;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       label_7: label_extract_t <- label_secret;
       labeled_IKM: bitstring <- concat_PRF(RFCXXXX, suite_id, label_7, default_psk);
       secrett: extract_t <- Extract_PRF(k, labeled_IKM);
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of binder psk_id
  - Remove assignments on psk_id (definition removed, all usages removed)
yields

Game 7 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       mode: mode_t <- mode_auth;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       label_7: label_extract_t <- label_secret;
       labeled_IKM: bitstring <- concat_PRF(RFCXXXX, suite_id, label_7, default_psk);
       secrett: extract_t <- Extract_PRF(k, labeled_IKM);
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of binder labeled_IKM
  - Remove assignments on labeled_IKM (definition removed, all usages removed)
yields

Game 8 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       mode: mode_t <- mode_auth;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       label_7: label_extract_t <- label_secret;
       secrett: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_7, default_psk));
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of binder label_7
  - Remove assignments on label_7 (definition removed, all usages removed)
yields

Game 9 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
 {11}  return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       mode: mode_t <- mode_auth;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       secrett: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying insert instruction sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk)) at occurrence 11
yields

Game 10 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       mode: mode_t <- mode_auth;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       secrett: extract_t <- {84}Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying use variable(s) sec
  - Use variable sec
    - Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk)) replaced with sec at 84
yields

Game 11 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
 {26}  mode: mode_t <- mode_auth;
       salt_3: cr_salt_t <- empty;
       label_5: label_extract_t <- label_psk_id_hash;
       labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
       psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
       salt_4: cr_salt_t <- empty;
       label_6: label_extract_t <- label_info_hash;
       labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
       info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
       key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
       secrett: extract_t <- sec;
       label_8: label_expand_t <- label_key;
       L_2: length_t <- Nk;
       labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
       key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
       label_9: label_expand_t <- label_base_nonce;
       L_3: length_t <- Nn;
       labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
       base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
       return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying insert instruction find [unique] l_1 = l <= Nperkey suchthat
      defined(else_br[l], info_3[l])
      && (info_3[l] = info_3)
      then else else_br <- true at occurrence 26
yields

Game 12 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(else_br[l], info_3[l]) && (info_3[l] = info_3) then
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
         return(concat(key, base_nonce))
       else
         else_br: bool <- true;
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
{293}    return(concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying insert instruction r_1 <- concat(key, base_nonce) at occurrence 293
yields

Game 13 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(else_br[l], info_3[l]) && (info_3[l] = info_3) then
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
         return(concat(key, base_nonce))
       else
         else_br: bool <- true;
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return({303}concat(key, base_nonce))
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying use variable(s) r_1
  - Use variable r_1
    - concat(key, base_nonce) replaced with r_1 at 303
yields

Game 14 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(else_br[l], info_3[l]) && (info_3[l] = info_3) then
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
         return({152}concat(key, base_nonce))
       else
         else_br: bool <- true;
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying replace term at occurrence 152 with r_1[l_1]
yields

Game 15 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
         return(r_1[l_1])
       else
         else_br: bool <- true;
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         secrett: extract_t <- sec;
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(secrett, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(secrett, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on else_br (definition removed, all usages removed)
  - Remove assignments on secrett (definition removed, all usages removed)
  - Remove assignments on secrett (definition removed, all usages removed)
  - Remove assignments on key (definition removed, all usages removed)
  - Remove assignments on base_nonce (definition removed, all usages removed)
  - Remove assignments on labeledInfo (definition removed, all usages removed)
  - Remove assignments on labeledInfo_1 (definition removed, all usages removed)
  - Remove assignments on key_schedule_context (definition removed, all usages removed)
  - Remove assignments on label_8 (definition removed, all usages removed)
  - Remove assignments on L_2 (definition removed, all usages removed)
  - Remove assignments on label_9 (definition removed, all usages removed)
  - Remove assignments on L_3 (definition removed, all usages removed)
  - Remove assignments on mode (definition removed, all usages removed)
  - Remove assignments on psk_id_hash (definition removed, all usages removed)
  - Remove assignments on info_hash (definition removed, all usages removed)
  - Remove assignments on salt_3 (definition removed, all usages removed)
  - Remove assignments on labeled_input (definition removed, all usages removed)
  - Remove assignments on salt_4 (definition removed, all usages removed)
  - Remove assignments on labeled_input_1 (definition removed, all usages removed)
  - Remove assignments on label_5 (definition removed, all usages removed)
  - Remove assignments on label_6 (definition removed, all usages removed)
yields

Game 16 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       k <-R kemkey_t;
       sec: extract_t <- Extract_PRF(k, concat_PRF(RFCXXXX, suite_id, label_secret, default_psk));
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(sec, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(sec, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying equivalence prf(Extract_PRF) [probability P_PRF_Extract(time_1, Nkey, Nkey)]
  - Equivalence prf(Extract_PRF) with variables: k -> k_2
yields

Game 17 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       sec: extract_t <- (x: bitstring <- concat_PRF(RFCXXXX, suite_id, label_secret, default_psk); {17}find [unique]  else r_2 <-R extract_t; r_2);
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(sec, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(sec, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying simplify (non-expanded game)
  - Simplification pass
    - Find at 17 removed (else branch kept if any)
yields

Game 18 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       sec: extract_t <- (x: bitstring <- concat_PRF(RFCXXXX, suite_id, label_secret, default_psk); r_2 <-R extract_t; r_2);
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(sec, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(sec, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying expand
  - Expand if/find/let
yields

Game 19 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       x: bitstring <- concat_PRF(RFCXXXX, suite_id, label_secret, default_psk);
       r_2 <-R extract_t;
       sec: extract_t <- r_2;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(sec, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(sec, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on x (definition removed, all usages removed)
  - Remove assignments on sec (definition removed, all usages removed)
yields

Game 20 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       r_2 <-R extract_t;
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk(Expand_PRF(r_2, labeledInfo));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn(Expand_PRF(r_2, labeledInfo_1));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying equivalence prf(Expand_PRF) [probability P_PRF_Expand(time_2, Nkey, 2 * #Oprf)]
  - Equivalence prf(Expand_PRF) with variables: r_2 -> k_2
yields

Game 21 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk((x_1: bitstring <- labeledInfo; {116}find [unique] u_3 = ri_7 <= Nperkey suchthat defined(x_1[ri_7], r_3[ri_7]) && (x_1 = x_1[ri_7]) then r_3[u_3] orfind u_2 = ri_5 <= Nperkey suchthat defined(x_2[ri_5], r_4[ri_5]) && {137}(x_1 = x_2[ri_5]) then r_4[u_2] else r_3 <-R expand_t; r_3));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn((x_2: bitstring <- labeledInfo_1; {176}find [unique] u_1 = ri_3 <= Nperkey suchthat defined(x_1[ri_3], r_3[ri_3]) && {181}(x_2 = x_1[ri_3]) then r_3[u_1] orfind u = ri_1 <= Nperkey suchthat defined(x_2[ri_1], r_4[ri_1]) && (x_2 = x_2[ri_1]) then r_4[u] else r_4 <-R expand_t; r_4));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying simplify (non-expanded game)
  - Simplification pass
    - Replaced (x_1 = x_2[ri_5]) with false at 137
    - Remove branch 2 in find at 116
    - Replaced (x_2 = x_1[ri_3]) with false at 181
    - Remove branch 1 in find at 176
yields

Game 22 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         key: key_t <- truncate_to_Nk((x_1: bitstring <- labeledInfo; find [unique] u_3 = ri_7 <= Nperkey suchthat defined(x_1[ri_7], r_3[ri_7]) && (x_1 = x_1[ri_7]) then r_3[u_3] else r_3 <-R expand_t; r_3));
         label_9: label_expand_t <- label_base_nonce;
         L_3: length_t <- Nn;
         labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
         base_nonce: nonce_t <- truncate_to_Nn((x_2: bitstring <- labeledInfo_1; find [unique] u = ri_1 <= Nperkey suchthat defined(x_2[ri_1], r_4[ri_1]) && (x_2 = x_2[ri_1]) then r_4[u] else r_4 <-R expand_t; r_4));
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying expand
  - Expand if/find/let
yields

Game 23 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         x_1: bitstring <- labeledInfo;
         find [unique] u_3 = ri_7 <= Nperkey suchthat defined(x_1[ri_7], r_3[ri_7]) && (x_1 = x_1[ri_7]) then
           key: key_t <- truncate_to_Nk(r_3[u_3]);
           label_9: label_expand_t <- label_base_nonce;
           L_3: length_t <- Nn;
           labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
           x_2: bitstring <- labeledInfo_1;
           find [unique] u = ri_1 <= Nperkey suchthat defined(x_2[ri_1], r_4[ri_1]) && (x_2 = x_2[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
         else
           r_3 <-R expand_t;
           key: key_t <- truncate_to_Nk(r_3);
           label_9: label_expand_t <- label_base_nonce;
           L_3: length_t <- Nn;
           labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
           x_2: bitstring <- labeledInfo_1;
           find [unique] u = ri_1 <= Nperkey suchthat defined(x_2[ri_1], r_4[ri_1]) && (x_2 = x_2[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on x_1 (definition removed, all usages removed)
  - Remove assignments on x_2 (definition kept, array references kept)
  - Remove assignments on x_2 (definition kept, array references kept)
yields

Game 24 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
{110}    find [unique] u_3 = ri_7 <= Nperkey suchthat defined(labeledInfo[ri_7], r_3[ri_7]) && {115}(labeledInfo = labeledInfo[ri_7]) then
           key: key_t <- truncate_to_Nk(r_3[u_3]);
           label_9: label_expand_t <- label_base_nonce;
           L_3: length_t <- Nn;
           labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
           x_2: bitstring <- labeledInfo_1;
{150}      find [unique] u = ri_1 <= Nperkey suchthat defined(x_2[ri_1], r_4[ri_1]) && {155}(labeledInfo_1 = x_2[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
         else
           r_3 <-R expand_t;
           key: key_t <- truncate_to_Nk(r_3);
           label_9: label_expand_t <- label_base_nonce;
           L_3: length_t <- Nn;
           labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
           x_2: bitstring <- labeledInfo_1;
{239}      find [unique] u = ri_1 <= Nperkey suchthat defined(x_2[ri_1], r_4[ri_1]) && {244}(labeledInfo_1 = x_2[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying simplify
  - Simplification pass
    - Replaced (labeledInfo_1 = x_2[ri_1]) with (info_hash = info_hash[ri_1]) at 244
    - Replaced defined condition x_2[ri_1], r_4[ri_1] with r_4[ri_1], info_hash[ri_1] in find at 239
    - Replaced (labeledInfo = labeledInfo[ri_7]) with (info_hash = info_hash[ri_7]) at 115
    - Replaced (labeledInfo_1 = x_2[ri_1]) with (info_hash = info_hash[ri_1]) at 155
    - Replaced defined condition x_2[ri_1], r_4[ri_1] with r_4[ri_1], info_hash[ri_1] in find at 150
    - Replaced defined condition labeledInfo[ri_7], r_3[ri_7] with r_3[ri_7], info_hash[ri_7] in find at 110
yields

Game 25 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         mode: mode_t <- mode_auth;
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         key_schedule_context: bitstring <- concat_KeySched(mode, psk_id_hash, info_hash);
         label_8: label_expand_t <- label_key;
         L_2: length_t <- Nk;
         labeledInfo: bitstring <- concat_Expand(L_2, RFCXXXX, suite_id, label_8, key_schedule_context);
         find [unique] u_3 = ri_7 <= Nperkey suchthat defined(r_3[ri_7], info_hash[ri_7]) && (info_hash = info_hash[ri_7]) then
           key: key_t <- truncate_to_Nk(r_3[u_3]);
           label_9: label_expand_t <- label_base_nonce;
           L_3: length_t <- Nn;
           labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
           x_2: bitstring <- labeledInfo_1;
           find [unique] u = ri_1 <= Nperkey suchthat defined(r_4[ri_1], info_hash[ri_1]) && (info_hash = info_hash[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
         else
           r_3 <-R expand_t;
           key: key_t <- truncate_to_Nk(r_3);
           label_9: label_expand_t <- label_base_nonce;
           L_3: length_t <- Nn;
           labeledInfo_1: bitstring <- concat_Expand(L_3, RFCXXXX, suite_id, label_9, key_schedule_context);
           x_2: bitstring <- labeledInfo_1;
           find [unique] u = ri_1 <= Nperkey suchthat defined(r_4[ri_1], info_hash[ri_1]) && (info_hash = info_hash[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying move all binders
  - Move assignment to x_2
  - Move assignment to labeledInfo_1
  - Move assignment to L_3
  - Move assignment to label_9
  - Move assignment to x_2
  - Move assignment to labeledInfo_1
  - Move assignment to L_3
  - Move assignment to label_9
  - Move assignment to labeledInfo
  - Move assignment to L_2
  - Move assignment to label_8
  - Move assignment to key_schedule_context
  - Move assignment to mode
yields

Game 26 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         salt_3: cr_salt_t <- empty;
         label_5: label_extract_t <- label_psk_id_hash;
         labeled_input: bitstring <- concat_CR(RFCXXXX, suite_id, label_5, default_psk_id);
         psk_id_hash: cr_output_t <- Extract_CR(cr_key_2, salt_3, labeled_input);
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         find [unique] u_3 = ri_7 <= Nperkey suchthat defined(r_3[ri_7], info_hash[ri_7]) && (info_hash = info_hash[ri_7]) then
           key: key_t <- truncate_to_Nk(r_3[u_3]);
           find [unique] u = ri_1 <= Nperkey suchthat defined(r_4[ri_1], info_hash[ri_1]) && (info_hash = info_hash[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
         else
           r_3 <-R expand_t;
           key: key_t <- truncate_to_Nk(r_3);
           find [unique] u = ri_1 <= Nperkey suchthat defined(r_4[ri_1], info_hash[ri_1]) && (info_hash = info_hash[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on psk_id_hash (definition removed, all usages removed)
  - Remove assignments on salt_3 (definition removed, all usages removed)
  - Remove assignments on labeled_input (definition removed, all usages removed)
  - Remove assignments on label_5 (definition removed, all usages removed)
yields

Game 27 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
 {59}    find [unique] u_3 = ri_7 <= Nperkey suchthat defined(r_3[ri_7], info_hash[ri_7]) && {64}(info_hash = info_hash[ri_7]) then
           key: key_t <- truncate_to_Nk(r_3[u_3]);
           find [unique] u = ri_1 <= Nperkey suchthat defined(r_4[ri_1], info_hash[ri_1]) && (info_hash = info_hash[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
         else
           r_3 <-R expand_t;
           key: key_t <- truncate_to_Nk(r_3);
{142}      find [unique] u = ri_1 <= Nperkey suchthat defined(r_4[ri_1], info_hash[ri_1]) && {147}(info_hash = info_hash[ri_1]) then
             base_nonce: nonce_t <- truncate_to_Nn(r_4[u]);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
           else
             r_4 <-R expand_t;
             base_nonce: nonce_t <- truncate_to_Nn(r_4);
             r_1: keys_t <- concat(key, base_nonce);
             return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying simplify [probability P_hashcoll(time_3)]
  - Simplification pass
    - Replaced (info_hash = info_hash[ri_1]) with (info_3 = info_3[ri_1]) at 147
    - Remove branch 1 in find at 142
    - Find at 142 removed (else branch kept if any)
    - Replaced (info_hash = info_hash[ri_7]) with (info_3 = info_3[ri_7]) at 64
    - Remove branch 1 in find at 59
    - Find at 59 removed (else branch kept if any)
yields

Game 28 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         r_3 <-R expand_t;
         key: key_t <- truncate_to_Nk(r_3);
         r_4 <-R expand_t;
         base_nonce: nonce_t <- truncate_to_Nn(r_4);
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying equivalence truncate(truncate_to_Nk)
  - Equivalence truncate(truncate_to_Nk) with variables: r_3 -> h
yields

Game 29 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         salt_4: cr_salt_t <- empty;
         label_6: label_extract_t <- label_info_hash;
         labeled_input_1: bitstring <- concat_CR(RFCXXXX, suite_id, label_6, info_3);
         info_hash: cr_output_t <- Extract_CR(cr_key_2, salt_4, labeled_input_1);
         k_1 <-R key_t;
         key: key_t <- k_1;
         r_4 <-R expand_t;
         base_nonce: nonce_t <- truncate_to_Nn(r_4);
         r_1: keys_t <- concat(key, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on info_hash (definition removed, all usages removed)
  - Remove assignments on key (definition removed, all usages removed)
  - Remove assignments on salt_4 (definition removed, all usages removed)
  - Remove assignments on labeled_input_1 (definition removed, all usages removed)
  - Remove assignments on label_6 (definition removed, all usages removed)
yields

Game 30 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         k_1 <-R key_t;
         r_4 <-R expand_t;
         base_nonce: nonce_t <- truncate_to_Nn(r_4);
         r_1: keys_t <- concat(k_1, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying equivalence truncate(truncate_to_Nn)
  - Equivalence truncate(truncate_to_Nn) with variables: r_4 -> h
yields

Game 31 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         k_1 <-R key_t;
         k_2 <-R nonce_t;
         base_nonce: nonce_t <- k_2;
         r_1: keys_t <- concat(k_1, base_nonce);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on base_nonce (definition removed, all usages removed)
yields

Game 32 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         k_1 <-R key_t;
         k_2 <-R nonce_t;
         r_1: keys_t <- concat(k_1, k_2);
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying equivalence concat_random
  - Equivalence concat_random with variables: k_2 -> k2, k_1 -> k1
yields

Game 33 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(r_1[l], info_3[l]) && (info_3[l] = info_3) then
         return(r_1[l_1])
       else
         k_3 <-R keys_t;
         r_1: keys_t <- k_3;
         return(r_1)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Applying remove assignments of findcond
  - Remove assignments on r_1 (definition removed, all usages removed)
yields

Game 34 is
     Ostart() :=
     cr_key_2 <-R cr_key_t;
     return(cr_key_2);
     ((
       foreach ikey <= Nkey do
       Ok() :=
       return();
       foreach i <= Nperkey do
       Oprf(info_3: bitstring) :=
       find [unique] l_1 = l <= Nperkey suchthat defined(k_3[l], info_3[l]) && (info_3[l] = info_3) then
         return(k_3[l_1])
       else
         k_3 <-R keys_t;
         return(k_3)
     ) | (
       OH() :=
       return(cr_key_2)
     ))


Proved indistinguishability between game 34 and game 2
Game 34 is the same as game 3.
Adv[Game 2: indistinguishability from game 3] <= 0 + Adv[Game 3: indistinguishability from game 3]
Adv[Game 1: indistinguishability from game 34] <= P_hashcoll(time_3) + P_PRF_Expand(time_2, Nkey, 2 * #Oprf) + P_PRF_Extract(time_1, Nkey, Nkey) + Adv[Game 34: indistinguishability from game 34]
RESULT Proved indistinguishability between game 1 and game 2 up to probability P_hashcoll(time_3) + P_PRF_Expand(time_2, Nkey, 2 * #Oprf) + P_PRF_Extract(time_1, Nkey, Nkey)
RESULT time_1 = time + time(context for game 16) = Nkey * time(concat_PRF, length(default_psk)) + #Oprf * Nperkey * time(= bitstring, maxlength(game 16: info_3), maxlength(game 16: info_3)) + #Oprf * time(concat_CR, length(default_psk_id)) + #Oprf * time(Extract_CR, maxlength(game 16: labeled_input)) + #Oprf * time(concat_CR, maxlength(game 16: info_3)) + #Oprf * time(Extract_CR, maxlength(game 16: labeled_input_1)) + #Oprf * time(concat_KeySched) + #Oprf * time(truncate_to_Nk) + #Oprf * time(Expand_PRF, maxlength(game 16: labeledInfo)) + 2 * #Oprf * time(concat_Expand, maxlength(game 16: key_schedule_context)) + #Oprf * time(truncate_to_Nn) + #Oprf * time(Expand_PRF, maxlength(game 16: labeledInfo_1)) + #Oprf * time(concat) + time
RESULT time_2 = time + time(context for game 20) = #Oprf * Nperkey * time(= bitstring, maxlength(game 20: info_3), maxlength(game 20: info_3)) + #Oprf * time(concat_CR, length(default_psk_id)) + #Oprf * time(Extract_CR, maxlength(game 20: labeled_input)) + #Oprf * time(concat_CR, maxlength(game 20: info_3)) + #Oprf * time(Extract_CR, maxlength(game 20: labeled_input_1)) + #Oprf * time(concat_KeySched) + #Oprf * time(truncate_to_Nk) + 2 * #Oprf * time(concat_Expand, maxlength(game 20: key_schedule_context)) + #Oprf * time(truncate_to_Nn) + #Oprf * time(concat) + time
RESULT time_3 = time + time(game 27) = time + #Oprf * Nperkey * time(= bitstring, maxlength(game 27: info_3), maxlength(game 27: info_3)) + #Oprf * time(concat_CR, maxlength(game 27: info_3)) + #Oprf * time(Extract_CR, maxlength(game 27: labeled_input_1)) + #Oprf * time(truncate_to_Nk) + #Oprf * time(truncate_to_Nn) + #Oprf * time(concat)
All queries proved.