val zeroRTT: mode -> bool
val zeroRTT: mode -> bool
let zeroRTT mode =
  zeroRTToffer mode.n_offer &&
  Some? mode.n_pski &&
  Some? mode.n_server_extensions &&
  List.Tot.existsb E_early_data? (Some?.v mode.n_server_extensions)
module MiTLS.Negotiation
open MiTLS

open FStar.Error
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSInfo
open MiTLS.TLSConstants
open MiTLS.HandshakeMessages

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

//16-05-31 these opens are implementation-only; overall we should open less
open MiTLS.Extensions

(**
  Debugging flag.
  F* normalizer will erase debug prints at extraction when set to false.
*)
val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string ("NGO| "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_NGO then print else (fun _ -> ())


//17-05-01 relocate these printing functions?!
//18-09-09
let string_of_option_extensions (o: option extensions) = match o with
  | None -> "None"
  | Some es -> "[ "^Extensions.string_of_extensions es^"]"

let string_of_ciphersuite (cs:cipherSuite) =
  string_of_cipherSuite (name_of_cipherSuite cs)

private
let accum_string_of_signatureSchemes s sa =
    s^(string_of_signatureScheme sa)^" "
let string_of_signatureSchemes sal =
  List.Tot.fold_left accum_string_of_signatureSchemes "" sal

private
let accum_string_of_ciphersuite s cs =
    s ^ "; " ^ string_of_ciphersuite cs
let string_of_ciphersuites csl =
  List.Tot.fold_left accum_string_of_ciphersuite "" csl

private
let accum_string_of_namedGroups s ng =
    s ^ "; " ^ (Parsers.NamedGroup.string_of_namedGroup ng)
let string_of_namedGroups ngl =
  List.Tot.fold_left accum_string_of_namedGroups "" ngl

private
let accum_string_of_ciphersuitename s cs =
    s ^ "; " ^ string_of_cipherSuite cs
let string_of_ciphersuitenames csl =
  List.Tot.fold_left accum_string_of_ciphersuitename "" csl

(* Negotiation: HELLO sub-module *)
type ri = cVerifyData * sVerifyData

type resumption_offer_12 = // part of resumeInfo
  | OfferNothing
  | OfferTicket of b:bytes{ length b <> 0 }
  | OfferSid of b:bytes { length b <> 0 }
// type resumption_mode_12 (o: resumption_offer_12) = b:bool { OfferNothing? o ==> b = false }

let valid_offer ch =
  True
// There is a pure function computing a ClientHello from an offer (minus the PSK binders)
type offer = ch:HandshakeMessages.ch { valid_offer ch }


// boilerplate code for accessing individual extensions
// 18-09-09 TODO use lowparse readers (simpler datatypes)

let find_client_extension (filter:Extensions.extension -> bool) o
  : option (e:Extensions.extension{filter e}) =
  match o.ch_extensions with
  | None -> None
  | Some es -> List.Tot.find filter es

let find_client_extension_aux env filter o =
  match o.ch_extensions with
  | None -> None
  | Some es -> List.Helpers.find_aux env filter es

let find_supported_versions o =
  match find_client_extension Extensions.E_supported_versions? o with
  | None -> None
  | Some (Extensions.E_supported_versions vs) -> Some vs

let find_signature_algorithms o : option signatureSchemeList =
  match find_client_extension Extensions.E_signature_algorithms? o with
  | None -> None
  | Some (Extensions.E_signature_algorithms algs) -> Some algs

let find_signature_algorithms_cert o : option signatureSchemeList =
  match find_client_extension Extensions.E_signature_algorithms_cert? o with
  | None -> None
  | Some (Extensions.E_signature_algorithms_cert algs) -> Some algs

let find_cookie o =
  match find_client_extension Extensions.E_cookie? o with
  | None -> None
  | Some (Extensions.E_cookie c) -> Some c

// finding the pre-shared keys in ClientHello
let find_pske o =
  match find_client_extension Extensions.E_pre_shared_key? o with
  | Some (Extensions.E_pre_shared_key (Extensions.ClientPSK psks _)) -> Some psks
  | _ -> None

let find_psk_key_exchange_modes o =
  match find_client_extension Extensions.E_psk_key_exchange_modes? o with
  | Some (Extensions.E_psk_key_exchange_modes l) -> l
  | _ -> []

let find_sessionTicket o =
  match find_client_extension Extensions.E_session_ticket? o with
  | None -> None
  | Some (Extensions.E_session_ticket b) -> Some b

let find_clientPske o =
  match find_client_extension Extensions.E_pre_shared_key? o with
  | Some (Extensions.E_pre_shared_key psk) ->
    (match psk with
    | ServerPSK _ -> None
    | ClientPSK ids tlen -> Some (ids,tlen))
  | _ -> None

let find_serverPske sh =
  match sh.sh_extensions with
  | None -> None
  | Some exts ->
    match List.Tot.find E_pre_shared_key? exts with
    | Some (E_pre_shared_key (ServerPSK idx)) -> Some (UInt16.v idx)
    | _ -> None

let find_serverKeyShare sh =
  match sh.sh_extensions with
  | None -> None
  | Some exts ->
    match List.Tot.find E_key_share? exts with
    | Some (E_key_share (CommonDH.ServerKeyShare ks)) -> Some ks
    | _ -> None

// index in the list of PSKs offered by the client
type pski (o:offer) = n:nat {
  o.ch_protocol_version = TLS_1p3 /\
  (match find_clientPske o with
  | Some (ids,_) -> n < List.length ids
  | _ -> False) }

let find_supported_groups o =
  match find_client_extension Extensions.E_supported_groups? o with
  | None -> None
  | Some (Extensions.E_supported_groups gns) -> Some gns

type share = g:CommonDH.group & CommonDH.share g
type pre_share = g:CommonDH.group & CommonDH.pre_share g

let find_key_shares (o:offer)
  : Tot (option (CommonDH.clientKeyShare))
  =
  match find_client_extension Extensions.E_key_share? o with
  | Some (Extensions.E_key_share (CommonDH.ClientKeyShare ks)) -> Some ks
  | _ -> None

private let rec list_of_ClientKeyShare (ks:list CommonDH.keyShareEntry)
  : Tot (list pre_share) =
  match ks with
  | [] -> []
  | (CommonDH.UnknownShare _ _) :: tl -> list_of_ClientKeyShare tl
  | (CommonDH.Share g s) :: tl -> (|g, s|) :: list_of_ClientKeyShare tl

let gs_of (o:offer) : Tot (list pre_share) =
  match find_key_shares o with
  | Some ksl -> list_of_ClientKeyShare ksl
  | _ -> []

let find_early_data o =
  match find_client_extension Extensions.E_early_data? o with
  | None -> None
  | Some (Extensions.E_early_data maxl) -> Some maxl

(**
  We keep both the server's HelloRetryRequest
  and the overwritten parts of the initial offer
*)
type retryInfo (offer:offer) =
  hrr *
  list pre_share (* we should actually keep the raw client extension content *) *
  list Extensions.pskIdentity

(**
  The final negotiated outcome, including key shares and long-term identities.
  mode is the name used in the resilience paper;
  session_info is the one from TLSInfo
*)
noeq type mode =
  | Mode:
    n_offer: offer -> // negotiated client offer
    n_hrr: option (retryInfo n_offer) ->  // optional HRR roundtrip

    // more from SH (both TLS 1.2 and TLS 1.3)
    n_protocol_version: protocolVersion ->
    n_server_random: TLSInfo.random ->
    n_sessionID: sessionID ->
    n_cipher_suite: cipherSuite ->

    // redundant with the server extension response?
    n_pski: option (pski n_offer) -> // only for TLS 1.3, result of a tricky stateful computation

    // concatenating SH and EE extensions for 1.3, in wire order
    // 18-09-09 recheck we exclude ambiguity
    n_server_extensions: option (se:list extension{List.Tot.length se < 256}) ->

    // more from SKE in ...ServerHelloDone (1.2) or SH (1.3)
    n_server_share: option share ->

    // more from either ...ServerHelloDone (1.2) or ServerFinished (1.3)
    n_client_cert_request: option HandshakeMessages.cr ->
    n_server_cert: option (Cert.chain13 * signatureScheme) ->

    // more from either CH+SH (1.3) or CKE (1.2)
    n_client_share: option share ->
    // { both shares are in the same negotiated group }
    mode

let find_server_extension filter m =
  match m.n_server_extensions with
  | None -> None
  | Some es -> List.Tot.find filter es

let is_resumption12 m =
  not (is_pv_13 m.n_protocol_version)  &&
  m.n_sessionID = m.n_offer.ch_sessionID

let is_cacheable12 m =
  not (is_pv_13 m.n_protocol_version)  &&
  ( let sid = m.n_sessionID in
    sid <> m.n_offer.ch_sessionID &&
    sid <> empty_bytes)

type certNego = option (cert_type * signatureScheme)

noeq type negotiationState (r:role) (cfg:config) : Type0 =
  // Have C_Offer_13 and C_Offer? Shares aren't available in C_Offer yet
  | C_Init:     n_client_random: TLSInfo.random ->
                negotiationState r cfg

  | C_Offer:    n_offer: offer ->
                negotiationState r cfg

  | C_HRR:      n_offer: offer ->
                n_hrr: retryInfo n_offer ->
                negotiationState r cfg

  | C_WaitFinished1:
                n_partialmode: mode ->
                negotiationState r cfg

  | C_Mode:     n_mode: mode -> // In 1.2, used for resumption and full handshakes
                negotiationState r cfg

  | C_WaitFinished2: // Only 1.2
                n_mode: mode ->
                n_client_certificate: option Cert.chain13 ->
                negotiationState r cfg

  | C_Complete: n_mode: mode ->
                n_client_certificate: option Cert.chain13 ->
                negotiationState r cfg

  | S_Init:     n_server_random: TLSInfo.random ->
                negotiationState r cfg

  // Waiting for ClientHello2
  | S_HRR:      n_offer: offer ->
                n_hrr: hrr ->
                negotiationState r cfg

  | S_ClientHello: // Transitional state to allow Handshake to call KS and generate a share
                n_mode: mode -> // n_server_share and n_server_extensions are None
                // We ask for a certificate from the PKI library - this is just a handle
                // If a certificate is actually used, it appears in network format in mode.n_server_cert
                n_selected_cert: certNego ->
                negotiationState r cfg

  // This state is used to wait for both Finished1 and Finished2
  | S_Mode:     n_mode: mode -> // If 1.2, then client_share is None
                n_selected_cert: certNego ->
                negotiationState r cfg

  | S_Complete: n_mode: mode ->
                n_client_certificate: option Cert.chain13 ->
                negotiationState r cfg

let ns_step (#r:role) (#cfg:config)
  (ns:negotiationState r cfg) (ns':negotiationState r cfg) =
  match ns, ns' with
  | C_Init nonce, C_Offer offer -> nonce == offer.ch_client_random
  | C_Offer offer, C_Mode mode -> mode.n_offer == offer
  | C_Offer _, C_Complete _ _ -> True
  | C_Mode _, C_WaitFinished2 _ _ -> True
  | C_Mode _, C_Complete _ _ -> True
  | S_Init _, S_ClientHello _ _ -> True
  | S_ClientHello _ _, S_Mode _ _ -> True
  | _, _ -> ns == ns'

let ns_rel (#r:role) (#cfg:config)
  (ns:negotiationState r cfg) (ns':negotiationState r cfg) =
  ns_step ns ns' \/
  (exists ns0. ns_step ns ns0 /\ ns_step ns0 ns')

assume val ns_rel_monotonic: #r:role -> #cfg:config ->
  Lemma (Preorder.preorder_rel (ns_rel #r #cfg))

type resumeInfo =
  option (psk_identifier * t:Ticket.ticket{Ticket.Ticket12? t}) *
  list (psk_identifier * t:Ticket.ticket{Ticket.Ticket13? t})

#reset-options "--admit_smt_queries true"
noeq type t (region:rgn) (role:TLSConstants.role) : Type0 =
  | NS:
    cfg: config -> // local configuration
    resume: resumeInfo ->
    nonce: TLSInfo.random ->
    state: HST.m_rref region (negotiationState role cfg) ns_rel ->
    t region role

private
let rec find_ticket12 (#a:Type0) (acc:option (a * Ticket.ticket))
    : list (a * Ticket.ticket) -> option (a * Ticket.ticket) =
    function
    | [] -> acc
    | (tid, t) :: r ->
      find_ticket12 (if Ticket.Ticket12? t then Some (tid, t) else acc) r

private
let rec filter_ticket13 (#a:Type0) (acc:list (a * Ticket.ticket))
    : list (a * Ticket.ticket) -> list (a * Ticket.ticket) =
    function
    | [] -> List.Tot.rev acc
    | (tid, t) :: r ->
      filter_ticket13 (if Ticket.Ticket13? t then (tid, t)::acc else acc) r

private
let rec ticket13_pskinfo (#a:Type0) (acc:list (a * pskInfo))
    : list (a * Ticket.ticket) -> list (a * pskInfo) =
    function
    | [] -> List.Tot.rev acc
    | (tid, t) :: r -> ticket13_pskinfo ((tid, Some?.v (Ticket.ticket_pskinfo t))::acc) r

#set-options "--admit_smt_queries true"
val computeOffer: r:role -> cfg:config -> nonce:TLSInfo.random
  -> ks:option CommonDH.keyShare -> resumeInfo -> now:UInt32.t
  -> Tot offer
let computeOffer r cfg nonce ks resume now =
  let ticket12, sid =
    match fst resume, cfg.enable_tickets, cfg.min_version with
    | _, _, TLS_1p3 -> None, empty_bytes // Don't bother sending session_ticket
    // Similar to what OpenSSL does, when we offer a 1.2 ticket
    // we send the hash of the ticket as SID to disambiguate the state machine
    | Some (tid, _), true, _ ->
      // FIXME Cannot compute hash in Tot
      //let sid = Hashing.compute Hashing.Spec.SHA2_256 t
      let sid = if length tid <= 32 then tid else fst (split tid 32ul) in
      Some tid, sid
    | None, true, _ -> Some (empty_bytes), empty_bytes
    | _ -> None, empty_bytes in
  let pskinfo = ticket13_pskinfo [] (snd resume) in
  // Don't offer EDI if there is no PSK or first PSK doesn't have ED enabled
  let compatible_psk =
    match pskinfo with
    | (_, i) :: _ -> i.allow_early_data // Must be the first PSK
    | _ -> false in
  let extensions =
    Extensions.prepareExtensions
      cfg.min_version
      cfg.max_version
      cfg.cipher_suites
      cfg.peer_name
      cfg.alpn
      cfg.custom_extensions
      // qp
      cfg.extended_master_secret
      cfg.safe_renegotiation
      (compatible_psk && Some? cfg.max_early_data)
      ticket12
      cfg.signature_algorithms
      cfg.named_groups
      None // : option (cVerifyData * sVerifyData)
      ks
      pskinfo
      now
  in
  {
    ch_protocol_version = minPV TLS_1p2 cfg.max_version; // legacy for 1.3
    ch_client_random = nonce;
    ch_sessionID = sid;
    ch_cipher_suites = nameList_of_cipherSuites cfg.cipher_suites;
    // This file is reconstructed from ch_cipher_suites in HandshakeMessages.clientHelloBytes;
    ch_compressions = [NullCompression];
    ch_extensions = Some extensions
  }

let rec unseal_tickets (acc:list (psk_identifier * Ticket.ticket))
                       (l:list (psk_identifier * b:bytes{length b <= 65551}))
    : St (list (psk_identifier * Ticket.ticket))
  = match l with
  | [] -> List.Tot.rev acc
  | (tid, seal) :: r ->
    let acc =
      match Ticket.check_ticket true seal with
      | Some t -> (tid, t) :: acc
      | None -> trace ("WARNING: failed to unseal the session data for ticket "^(print_bytes tid)^" (check sealing key)"); acc in
    unseal_tickets acc r

val create:
  region:rgn -> r:role -> cfg:config -> TLSInfo.random ->
  St (t region r)
let create region r cfg nonce =
  let resume = unseal_tickets [] cfg.use_tickets in
  let resume = (find_ticket12 None resume, filter_ticket13 [] resume) in
  match r with
  | Client ->
    let state = Mem.ralloc region (C_Init nonce) in
    NS cfg resume nonce state
  | Server ->
    let state = Mem.ralloc region (S_Init nonce) in
    NS cfg resume nonce state

// For QUIC: we need a different signal when returning HRR (special packet type)
let is_server_hrr (#region:rgn) (#role:TLSConstants.role) (ns:t region role) =
  match HST.op_Bang ns.state with
  | S_HRR _ _ -> true
  | _ -> false

// a bit too restrictive: use a single Hash in any given offer
val hashAlg: mode -> Hashing.Spec.alg
let hashAlg m =
  verifyDataHashAlg_of_ciphersuite m.n_cipher_suite

val kexAlg: mode -> TLSConstants.kexAlg
let kexAlg m =
  if is_pv_13 m.n_protocol_version then
    (match m.n_pski with
    | None -> Kex_ECDHE
    | Some _ ->
      if Some? m.n_server_share then Kex_PSK_ECDHE
      else Kex_PSK)
  else
    let CipherSuite kex _ _ = m.n_cipher_suite in
    kex

val aeAlg:
  m:mode{CipherSuite? m.n_cipher_suite \/ CipherSuite13? m.n_cipher_suite} ->
  TLSConstants.aeAlg
let aeAlg m =
  TLSConstants.get_aeAlg m.n_cipher_suite

val emsFlag: mode -> bool
let emsFlag mode =
  if is_pv_13 mode.n_protocol_version then
    true
  else
    match mode.n_offer.ch_extensions with
    | None -> false
    | Some cexts ->
      List.Tot.mem Extensions.E_extended_ms cexts &&
      (match mode.n_server_extensions with
       // called from server_ClientHello
       | None -> true
       // called from client_ServerHelloDone
       | Some sexts -> List.Tot.mem Extensions.E_extended_ms sexts)

// used only for TLS 1.2. FIXME: properly negotiate
val chosenGroup: mode -> option CommonDH.group
let chosenGroup mode =
  match kexAlg mode with
  | Kex_PSK_DHE
  | Kex_DHE -> CommonDH.group_of_namedGroup CommonDH.Ffdhe2048
  | Kex_PSK_ECDHE
  | Kex_ECDHE -> CommonDH.group_of_namedGroup CommonDH.Secp256r1

val zeroRTToffer: offer -> bool
let zeroRTToffer o = Some? (find_early_data o)
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.Random.fst.checked MiTLS.PSK.fst.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Mem.fst.checked MiTLS.List.Helpers.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.HandshakeLog.fsti.checked MiTLS.Extensions.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Date.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Negotiation.fst
mode: MiTLS.Negotiation.mode -> Prims.bool
MiTLS.Negotiation.mode Prims.op_AmpAmp MiTLS.Negotiation.zeroRTToffer MiTLS.Negotiation.__proj__Mode__item__n_offer FStar.Pervasives.Native.uu___is_Some MiTLS.Negotiation.pski MiTLS.Negotiation.__proj__Mode__item__n_pski Prims.list MiTLS.Extensions.extension Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length MiTLS.Negotiation.__proj__Mode__item__n_server_extensions FStar.List.Tot.Base.existsb MiTLS.Extensions.uu___is_E_early_data MiTLS.Extensions.unknown FStar.Pervasives.Native.__proj__Some__item__v Prims.bool
let zeroRTT mode =
  
zeroRTToffer mode.n_offer && Some? mode.n_pski && Some? mode.n_server_extensions &&
List.Tot.existsb E_early_data? (Some?.v mode.n_server_extensions)