val b_IK : Prims.bool
let b_IK = check_ac_levels pattern_IK pattern_IK_auth_conf_ref
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]
let pattern_X1N_auth_conf_ref : auth_conf = mk_auth_conf [0;0;0;0;2] [0;1;1;3;1]
let pattern_X1K_auth_conf_ref : auth_conf = mk_auth_conf [0;2;0;2;2;2] [2;1;5;3;5;5]
let pattern_XK1_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;1;5;5]
let pattern_X1K1_auth_conf_ref : auth_conf = mk_auth_conf [0;2;0;2;2;2] [0;1;5;3;5;5]
let pattern_X1X_auth_conf_ref : auth_conf = mk_auth_conf [0;2;0;2;2;2] [0;1;5;3;5;5]
let pattern_XX1_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;2;2] [0;1;3;5;5]
let pattern_X1X1_auth_conf_ref : auth_conf = mk_auth_conf [0;0;0;2;2;2] [0;1;3;3;5;5]
let pattern_K1N_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;0] [0;1;1;5]
let pattern_K1K_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [2;1;5;5]
let pattern_KK1_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;3;5;5]
let pattern_K1K1_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;1;5;5]
let pattern_K1X_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;1;5;5]
let pattern_KX1_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;2;2] [0;3;3;5;5]
let pattern_K1X1_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;2;2] [0;1;3;5;5]
let pattern_I1N_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;0] [0;1;1;5]
let pattern_I1K_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [2;1;5;5]
let pattern_IK1_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;3;5;5]
let pattern_I1K1_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;1;5;5]
let pattern_I1X_auth_conf_ref : auth_conf = mk_auth_conf [0;2;2;2] [0;1;5;5]
let pattern_IX1_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;2;2] [0;3;3;5;5]
let pattern_I1X1_auth_conf_ref : auth_conf = mk_auth_conf [0;0;2;2;2] [0;1;3;5;5]

let pattern_N_id_hide : id_hide = (None, Some 3)
let pattern_K_id_hide : id_hide = (Some 5, Some 5)
let pattern_X_id_hide : id_hide = (Some 4, Some 3)
let pattern_NN_id_hide : id_hide = (None, None)
let pattern_NK_id_hide : id_hide = (None, Some 3)
let pattern_NK1_id_hide : id_hide = (None, Some 9)
let pattern_NX_id_hide : id_hide = (None, Some 1)
let pattern_XN_id_hide : id_hide = (Some 2, None)
let pattern_XK_id_hide : id_hide = (Some 8, Some 3)
let pattern_XK1_id_hide : id_hide = (Some 8, Some 9)
let pattern_XX_id_hide : id_hide = (Some 8, Some 1)
let pattern_KN_id_hide : id_hide = (Some 7, None)
let pattern_KK_id_hide : id_hide = (Some 5, Some 5)
let pattern_KX_id_hide : id_hide = (Some 7, Some 6)
let pattern_IN_id_hide : id_hide = (Some 0, None)
let pattern_IK_id_hide : id_hide = (Some 4, Some 3)
let pattern_IK1_id_hide : id_hide = (Some 0, Some 9)
let pattern_IX_id_hide : id_hide = (Some 0, Some 6)

/// [Spec.Noise.AuthConf] defines functions to compute those security levels.
/// Below, we check that we get the same levels as listed above.
/// This is a bit redundant with what is already done in [Spec.Noise.AuthConf],
/// but we check very thoroughly below.
let check_ac_levels (hsk : handshake_pattern) (ac : auth_conf) : Tot bool =
  let messages = hsk.messages in
  // Append 2 empty messages only if the pattern is two ways
  let messages = if length messages > 1 then append messages [[]; []] else messages in
  // But the Noise spec doesn't always append two messages...
  let messages = fst (splitAt (length (fst ac)) messages) in
  let opt_ac' = ac_levels messages in
  let ac = zip (fst ac) (snd ac) in
  let ac = map (fun (z : auth_level & conf_level) -> let x, y = z in (x, y)) ac in // typing problem due to the refinements
  if Some? opt_ac' then Some?.v opt_ac' = ac else false

let b_N = check_ac_levels pattern_N pattern_N_auth_conf_ref
let b_K = check_ac_levels pattern_K pattern_K_auth_conf_ref
let b_X = check_ac_levels pattern_X pattern_X_auth_conf_ref
let b_NN = check_ac_levels pattern_NN pattern_NN_auth_conf_ref
let b_NK = check_ac_levels pattern_NK pattern_NK_auth_conf_ref
let b_NX = check_ac_levels pattern_NX pattern_NX_auth_conf_ref
let b_XN = check_ac_levels pattern_XN pattern_XN_auth_conf_ref
let b_XK = check_ac_levels pattern_XK pattern_XK_auth_conf_ref
let b_XX = check_ac_levels pattern_XX pattern_XX_auth_conf_ref
let b_KN = check_ac_levels pattern_KN pattern_KN_auth_conf_ref
let b_KK = check_ac_levels pattern_KK pattern_KK_auth_conf_ref
let b_KX = check_ac_levels pattern_KX pattern_KX_auth_conf_ref
/
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
Prims.bool
Spec.Noise.PatternsSecurity.check_ac_levels Spec.Noise.Patterns.pattern_IK Spec.Noise.PatternsSecurity.pattern_IK_auth_conf_ref
let b_IK =
  
check_ac_levels pattern_IK pattern_IK_auth_conf_ref