val shared_footprint:rset
val shared_footprint:rset
let shared_footprint: rset = Set.empty
(* Idealizing derived authentication tokens; independent of TLS, used for TLS 1.2 Finished message payloads. *)
module MiTLS.Token.UF1CMA
open MiTLS

//TODO use this file instead of TLSPRF

open FStar.Bytes
open MiTLS.Mem

// this file is adapted from HMAC.UFCMA but simpler, and yield
// probabilistic security: the advantage of an adversary guessing the
// random token is just 1/#tokens. (Do we need to enforce a single
// verification attempt?)

let ipkg = Pkg.ipkg
let model = Flags.model
let ideal = Flags.ideal_HMAC
// secret idealization flag for the UF1CMA assumption
//TODO use a separate flag

type safe (#ip:ipkg) (i:ip.Pkg.t) = b2t ideal /\ ip.Pkg.honest i

private let is_safe (#ip:ipkg) (i:ip.Pkg.t{ip.Pkg.registered i}): ST bool
  (requires fun h0 -> True)
  (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i))
  =
  let b = ip.Pkg.get_honesty i in
  ideal && b

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

// formally agile in the KDF algorithm, which controls the token length.
type ha = Hashing.Spec.alg

// initial parameters
noeq type info = {
  parent: r:rgn {~ (is_tls_rgn r)};
  alg: Hashing.Spec.alg; //too loose? Pkg.kdfa;
  good: bool //TODO: should be Type0 instead of bool, and erased, but hard to propagate
}

type tag (u:info) = lbytes32 (Hacl.Hash.Definitions.hash_len u.alg)

let keylen (u:info): Pkg.keylen = Hacl.Hash.Definitions.hash_len u.alg
type keyrepr (u:info) = lbytes (Hashing.Spec.hash_length u.alg)

let goodish (#ip:ipkg) (i:ip.Pkg.t) (u:info) = _: unit{~(safe i) \/ u.good}

private type log_t (#ip:ipkg) (i:ip.Pkg.t) (u:info) (r:rgn) =
  m_rref r (option (goodish #ip i u)) ssa

// runtime (concrete) type of MAC instances
val concrete_key : Type0

val concrete_key_info (k:concrete_key) : info
val concrete_key_repr (k:concrete_key) : keyrepr (concrete_key_info k)

// The model type of instances - either ideal, or real
// The real and concrete version are related by the functional correctness of HMAC
noeq (* abstract *) type ir_key (ip:ipkg) (i:ip.Pkg.t) =
  | IdealKey:
    ck: concrete_key ->
    region: Mem.subrgn (concrete_key_info ck).parent {~(is_tls_rgn region)} ->  // intuitively, the writer's region
    log: log_t i (concrete_key_info ck) region ->
    ir_key ip i
  | RealKey: ck:concrete_key -> ir_key ip i

type key (ip:ipkg) (i:ip.Pkg.t{ip.Pkg.registered i}) =
  (if model
  then k:ir_key ip i{IdealKey? k <==> safe i}
  else concrete_key)

let usage (#ip:ipkg) (#i:ip.Pkg.t{ip.Pkg.registered i}) (k:key ip i): GTot info =
  if model then
    let k' : ir_key ip i = k in
    match k' with
    | IdealKey ck _ _ -> concrete_key_info ck
    | RealKey ck -> concrete_key_info ck
  else (concrete_key_info k)

let keyval (#ip:ipkg) (#i:ip.Pkg.t{ip.Pkg.registered i}) (k:key ip i): GTot (keyrepr (usage k)) =
  if model then
    let k' : ir_key ip i = k in
    match k' with
    | IdealKey ck _ _ -> concrete_key_repr ck
    | RealKey ck -> concrete_key_repr ck
  else concrete_key_repr k

let region (#ip:ipkg) (#i:ip.Pkg.t{ip.Pkg.registered i}) (k:key ip i):
  Ghost (subrgn (usage k).parent)
  (requires safe i)
  (ensures fun _ -> True)
  = let IdealKey _ r _ = k <: ir_key ip i in r
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked MiTLS.Flags.fst.checked Hacl.Hash.Definitions.fst.checked FStar.Tactics.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Token.UF1CMA.fsti
MiTLS.Mem.rset
FStar.Set.empty FStar.Monotonic.HyperHeap.rid
let shared_footprint:rset =
  
Set.empty