val vdAlg : si: MiTLS.TLSInfo.sessionInfo -> MiTLS.TLSConstants.protocolVersion * MiTLS.CipherSuite.cipherSuite
let vdAlg si = si.protocol_version, si.cipher_suite
module MiTLS.TLSInfo
open MiTLS

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

#set-options "--max_fuel 3 --initial_fuel 3 --max_ifuel 1 --initial_ifuel 1"

(* This module gathers the definitions of
   public datatypes, parameters, and predicates for our TLS API.

   Its interface is used by most TLS modules;
   its implementation is typechecked.
*)

open FStar.Bytes
open MiTLS.Mem
open MiTLS.TLSConstants

module DM = FStar.DependentMap
module MDM = FStar.Monotonic.DependentMap
module HST = FStar.HyperStack.ST

let default_cipherSuites = [
  TLS_AES_128_GCM_SHA256;
  TLS_AES_256_GCM_SHA384;
  TLS_CHACHA20_POLY1305_SHA256;
  TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256;
  TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256;
  TLS_DHE_RSA_WITH_AES_128_GCM_SHA256;
  TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384;
  TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384;
  TLS_DHE_RSA_WITH_AES_256_GCM_SHA384;
  TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256;
  TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256;
  TLS_DHE_RSA_WITH_CHACHA20_POLY1305_SHA256;
  ]

let default_signature_schemes =
  let schemes = [
    Ecdsa_secp256r1_sha256; Ecdsa_secp384r1_sha384; Ecdsa_secp521r1_sha512;
    Rsa_pss_rsae_sha256; Rsa_pss_rsae_sha384; Rsa_pss_rsae_sha512;
    Rsa_pkcs1_sha256; Rsa_pkcs1_sha384; Rsa_pkcs1_sha512;
    Ecdsa_sha1; Rsa_pkcs1_sha1
  ] in
  assert_norm (List.Tot.length schemes <= Parsers.SignatureSchemeList.max_count);
  assert_norm (List.Tot.for_all is_supported_signatureScheme schemes);
  schemes

let default_groups : CommonDH.supportedNamedGroups =
  let open MiTLS.CommonDH in
  let groups = [
    Secp521r1;
    Secp384r1;
    X25519;
    Secp256r1;
    Ffdhe4096;
    Ffdhe3072;
    Ffdhe2048;
  ] in
  assert_norm (List.Tot.length groups <= Parsers.NamedGroupList.max_count);
  assert_norm (List.Tot.for_all is_supported_group groups);
  groups

// By default we use an in-memory ticket table
// and the in-memory internal PSK database
val defaultTicketCBFun: ticket_cb_fun
let defaultTicketCBFun _ sni ticket info psk =
  let h0 = get() in
  begin
  match info with
  | TicketInfo_12 (pv, cs, ems) ->
    // 2018.03.10 SZ: The ticket must be fresh
    assume False;
    PSK.s12_extend ticket (pv, cs, ems, psk) // modifies PSK.tregion
  | TicketInfo_13 pskInfo ->
    // 2018.03.10 SZ: Missing refinement in ticket_cb_fun
    assume (exists i.{:pattern index psk i} index psk i <> 0z);
    // 2018.03.10 SZ: The ticket must be fresh
    assume False;
    PSK.coerce_psk ticket pskInfo psk;      // modifies psk_region
    PSK.extend sni ticket                   // modifies PSK.tregion
  end;
  let h1 = HST.get() in
  // 2018.03.10 SZ: [ticket_cb_fun] ensures [modifies_none]
  assume (modifies_none h0 h1)

val defaultTicketCB: ticket_cb
let defaultTicketCB = {
  ticket_context = (FStar.Dyn.mkdyn ());
  new_ticket = defaultTicketCBFun;
}

val defaultServerNegoCBFun: nego_cb_fun
let defaultServerNegoCBFun _ pv cext ocookie =
  Nego_accept []

let defaultServerNegoCB : nego_cb = {
  nego_context = FStar.Dyn.mkdyn ();
  negotiate = defaultServerNegoCBFun;
}

let none6 = fun _ _ _ _ _ _ -> None
let empty3 = fun _ _ _ -> []
let none5 = fun _ _ _ _ _ -> None
let false6 = fun _ _ _ _ _ _ -> false

let defaultCertCB : cert_cb =
  TLSConstants.mk_cert_cb
     (FStar.Dyn.mkdyn ())
     (FStar.Dyn.mkdyn ())
     none6
     (FStar.Dyn.mkdyn ())
     empty3
     (FStar.Dyn.mkdyn ())
     none5
     (FStar.Dyn.mkdyn ())
     false6

val defaultConfig: config
let defaultConfig =
  assert_norm (List.Tot.length (cipherSuites_of_nameList default_cipherSuites) < 256);
  assert_norm (List.Tot.length default_signature_schemes < 65536/2);
  {
  min_version = TLS_1p2;
  max_version = TLS_1p3;
  is_quic = false;
  
  cipher_suites = cipherSuites_of_nameList default_cipherSuites;
  named_groups = default_groups;
  signature_algorithms = default_signature_schemes;

  // Client
  hello_retry = true;
  offer_shares = CommonDH.as_supportedNamedGroups [Parsers.NamedGroup.X25519];
  custom_extensions = [];
  use_tickets = [];

  // Server
  check_client_version_in_pms_for_old_tls = true;
  request_client_certificate = false;
  send_ticket = Some empty_bytes;

  // Common
  non_blocking_read = false;
  max_early_data = None;
  max_ticket_age = 3600ul;
  safe_renegotiation = true;
  extended_master_secret = true;
  enable_tickets = true;

  ticket_callback = defaultTicketCB;
  nego_callback = defaultServerNegoCB;
  cert_callbacks = defaultCertCB;

  alpn = None;
  peer_name = None;
  }

// -------------------------------------------------------------------
// Client/Server randomness (implemented in Nonce)

// their first 4 bytes give the local time,
// so that they are locally pairwise-distinct
type random = Nonce.random
type crand = random
type srand = random
type csRands = lbytes 64

type sessionHash = bytes

//let noCsr:csRands = Nonce.noCsr

include MiTLS.TLSInfoFlags

// -------------------------------------------------------------------
// Session information (public immutable data)

type sessionID = b:bytes { length b <= 32 }
// ``An arbitrary byte sequence chosen by the server
// to identify an active or resumable session state.''

noeq type sessionInfo = {
    init_crand: crand;
    init_srand: srand;
    protocol_version: p:protocolVersion; // { p <> TLS_1p3 };
    cipher_suite: cipherSuite;
    compression: compression;
    extended_ms: bool;
    pmsId: pmsId;
    session_hash: sessionHash;
    client_auth: bool;
    clientID: Cert.chain;
    clientSigAlg: signatureScheme;
    serverID: Cert.chain;
    serverSigAlg: signatureScheme;
    sessionID: sessionID;
    }

type abbrInfo =
    {abbr_crand: crand;
     abbr_srand: srand;
     abbr_session_hash: sessionHash;
     abbr_vd: option (cVerifyData * sVerifyData) }

// for sessionID. we treat empty bytes as the absence of identifier,
// i.e. the session is not resumable.

// for certificates, the empty list represents the absence of identity
// (possibly refusing to present requested certs)

val csrands: sessionInfo -> Tot csRands
let csrands si = si.init_crand @| si.init_srand
//CF subsumes mk_csrands

// Getting algorithms from sessionInfo
//CF subsume mk_kefAlg, mk_kefAlgExtended, mk_kdfAlg
val kefAlg: pv:protocolVersion -> cs:cipherSuite{pv = TLS_1p2 ==> ~(NullCipherSuite? cs \/ SCSV? cs) /\ Some? (prfMacAlg_of_ciphersuite_aux cs)} -> bool -> Tot kefAlg_t
let kefAlg pv cs ems =
  let label = if ems then extended_extract_label else extract_label in
  match pv with
  | SSL_3p0           -> PRF_SSL3_nested
  | TLS_1p0 | TLS_1p1 -> PRF_TLS_1p01 label
  | TLS_1p2           -> PRF_TLS_1p2 label (prfMacAlg_of_ciphersuite cs)
  | TLS_1p3           -> PRF_TLS_1p3 //TBC

val kdfAlg: pv:protocolVersion -> cs:cipherSuite{pv = TLS_1p2 ==> ~(NullCipherSuite? cs \/ SCSV? cs) /\ Some? (prfMacAlg_of_ciphersuite_aux cs)} -> Tot kdfAlg_t
let kdfAlg pv cs =
  match pv with
  | SSL_3p0           -> PRF_SSL3_nested
  | TLS_1p0 | TLS_1p1 -> PRF_TLS_1p01 kdf_label
  | TLS_1p2           -> PRF_TLS_1p2 kdf_label (prfMacAlg_of_ciphersuite cs)
  | TLS_1p3           -> PRF_TLS_1p3 //TBC
/
prims.fst.checked MiTLS.TLSInfoFlags.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.PSK.fst.checked MiTLS.PMS.fst.checked MiTLS.Parsers.SignatureSchemeList.fsti.checked MiTLS.Parsers.NamedGroupList.fsti.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Nonce.fsti.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked MiTLS.Flags.fst.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Dyn.fsti.checked FStar.DependentMap.fsti.checked FStar.Bytes.fsti.checked
MiTLS.TLSInfo.fst
si: MiTLS.TLSInfo.sessionInfo -> MiTLS.TLSConstants.protocolVersion * MiTLS.CipherSuite.cipherSuite
MiTLS.TLSInfo.sessionInfo FStar.Pervasives.Native.Mktuple2 MiTLS.TLSConstants.protocolVersion MiTLS.CipherSuite.cipherSuite MiTLS.TLSInfo.__proj__MksessionInfo__item__protocol_version MiTLS.TLSInfo.__proj__MksessionInfo__item__cipher_suite FStar.Pervasives.Native.tuple2
let vdAlg si =
  
si.protocol_version, si.cipher_suite