val pattern_X1K_auth_conf_ref:auth_conf
val pattern_X1K_auth_conf_ref:auth_conf
let pattern_X1K_auth_conf_ref : auth_conf = mk_auth_conf [0;2;0;2;2;2] [2;1;5;3;5;5]
module Spec.Noise.PatternsSecurity

open Spec.Noise.Base
open Spec.Noise.WellFormedness
open Meta.Noise
open Spec.Noise.AuthConf
open Spec.Noise.Patterns
module T = FStar.Tactics
open FStar.List.Tot

#set-options "--z3rlimit 15 --fuel 0 --ifuel 0"

(*** Reference levels *)
/// The following file defines the security (secrecy, authentication, identity hiding)
/// levels for the patterns listed in the Noise technical paper.
/// We just copied the levels listed in the paper.

//type secrecy_level = x:nat{x <= 5}
//type auth_level = x:nat{x <= 2}
type id_hide_level = nat // x:nat{x <= 9}

type pattern_levels = {
  confidentiality : list conf_level;
  authentication : (auth:list auth_level{List.Tot.length auth = List.Tot.length confidentiality});
  init_hide : option id_hide_level;
  resp_hide : option id_hide_level;
}

type auth_conf =
  ls:((list auth_level) & (list conf_level)) {
    let ls1, ls2 = ls in
    List.Tot.length ls1 = List.Tot.length ls2
  }

type id_hide = option id_hide_level & option id_hide_level // (initiator, responder)

let mk_auth_conf(auth : list auth_level) (conf : list conf_level) :
  Pure auth_conf
  (requires (normalize_term (List.Tot.length auth) = normalize_term (List.Tot.length conf)))
  (ensures (fun _ -> True)) =
  normalize_term_spec (List.Tot.length auth);
  normalize_term_spec (List.Tot.length conf);
  auth, conf

let pattern_N_auth_conf_ref : auth_conf = mk_auth_conf [0] [2]
let pattern_K_auth_conf_ref : auth_conf = mk_auth_conf [1] [2]
let pattern_X_auth_conf_ref : auth_conf = mk_auth_conf [1] [2]
let pattern_NN_auth_conf_ref : auth_conf = mk_auth_conf [0;0;0] [0;1;1]
let pattern_NK_auth_conf_ref : auth_conf = mk_auth_conf [0;2;0] [2;1;5]
let pattern_NX_auth_conf_ref : auth_conf = mk_auth_conf [0;2;0] [0;1;5]
let pattern_XN_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;0] [0;1;1;5]
let pattern_XK_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [2;1;5;5]
let pattern_XX_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;1;5;5]
let pattern_KN_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;0] [0;3;1;5]
let pattern_KK_auth_conf_ref : auth_conf = mk_auth_conf [1;2;2;2] [2;4;5;5]
let pattern_KX_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;3;5;5]
let pattern_IN_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;0] [0;3;1;5]
let pattern_IK_auth_conf_ref : auth_conf = mk_auth_conf [1;2;2;2] [2;4;5;5]
let pattern_IX_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;3;5;5]
let pattern_NK1_auth_conf_ref : auth_conf = mk_auth_conf [0;2;0] [0;1;5]
let pattern_NX1_auth_conf_ref : auth_conf = mk_auth_conf [0;0;0;2;0] [0;1;3;1;5]
/
Spec.Noise.WellFormedness.fsti.checked Spec.Noise.Patterns.fst.checked Spec.Noise.Base.fst.checked Spec.Noise.AuthConf.fst.checked prims.fst.checked Meta.Noise.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.PatternsSecurity.fst
Spec.Noise.PatternsSecurity.auth_conf
Spec.Noise.PatternsSecurity.mk_auth_conf Prims.Cons Spec.Noise.AuthConf.auth_level Prims.Nil Spec.Noise.AuthConf.conf_level
let pattern_X1K_auth_conf_ref:auth_conf =
  
mk_auth_conf [0; 2; 0; 2; 2; 2] [2; 1; 5; 3; 5; 5]