val ipkg : Type
let ipkg = Pkg.ipkg
(* 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?)
/
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
Type
MiTLS.Pkg.ipkg
let ipkg =
  
Pkg.ipkg