val keylen (u: info) : Pkg.keylen
val keylen (u: info) : Pkg.keylen
let keylen (u:info): Pkg.keylen = Hacl.Hash.Definitions.hash_len u.alg
(* 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)
/
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
u27: MiTLS.Token.UF1CMA.info -> MiTLS.Pkg.keylen
MiTLS.Token.UF1CMA.info Hacl.Hash.Definitions.hash_len MiTLS.Token.UF1CMA.__proj__Mkinfo__item__alg MiTLS.Pkg.keylen
let keylen (u: info) : Pkg.keylen =
  
Hacl.Hash.Definitions.hash_len u.alg