val isAnonCipherSuite : cs: MiTLS.CipherSuite.cipherSuite' -> Prims.bool
let isAnonCipherSuite cs =
  match cs with
  | CipherSuite Kex_DHE None _ -> true
  | _ -> false
module MiTLS.CipherSuite
open MiTLS

open FStar.Seq
open FStar.UInt32
open FStar.Bytes
open FStar.Error
open MiTLS.TLSError

open MiTLS.Mem
module Parse = MiTLS.Parse
//include Parse


/// CIPHERSUITES, with new structure for TLS 1.3
/// 18-02-22 QD fodder, will require a manual translation as we
/// primarily use this structured ADT --- see also cipherSuiteName
/// below, closer to the RFC.

include MiTLS.Parsers.CipherSuite // for TLS_DH_DSS_WITH_3DES_EDE_CBC_SHA

/// Various elements used in ciphersuites

(** Signature algorithms *)
type sigAlg =
 | RSASIG
 | DSA
 | ECDSA
 | RSAPSS

(** Key exchange algorithms **)
type kexAlg =
  | Kex_RSA
  | Kex_DH
  | Kex_PSK
  | Kex_PSK_DHE
  | Kex_PSK_ECDHE
  | Kex_DHE
  | Kex_ECDHE

(** Crypto algorithm names are defined in EverCrypt **)
type blockCipher = EverCrypt.block_cipher_alg
type streamCipher = EverCrypt.stream_cipher_alg
type aeadAlg = EverCrypt.aead_alg

(** Modes for the initialization vectors *)
type ivMode =
  | Fresh
  | Stale

(** Encryption types *)
type encAlg =
  | Block of blockCipher
  | Stream of streamCipher

(** TLS-specific hash and MAC algorithms *)

//18-09-08 eliminate once EverCrypt/Hashing are stable.

type hash_alg = Hashing.Spec.alg
type hashAlg = Hashing.Spec.tls_alg
type macAlg = Hashing.Spec.alg

let hashSize = Hashing.Spec.tls_tagLen
let macKeySize = Hacl.Hash.Definitions.hash_len
let macSize = Hacl.Hash.Definitions.hash_len

(** Authenticated Encryption modes *)
type aeAlg =
  | MACOnly: hash_alg -> aeAlg
  | MtE: encAlg -> hash_alg -> aeAlg
  | AEAD: aeadAlg -> hash_alg -> aeAlg // the hash algorithm is for the ciphersuite; it is not used by the record layer.

(** Ciphersuite definition *)
type cipherSuite' =
  | NullCipherSuite
  | CipherSuite    : kexAlg -> option sigAlg -> aeAlg -> cipherSuite'
  | CipherSuite13  : aeadAlg -> hash_alg -> cipherSuite'
  | SCSV // useless, because not a validCipherSuite (see below), but apparently needed in TLSInfo
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Parsers.CipherSuite.fsti.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.LowParseWrappers.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.EverCrypt.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.CipherSuite.fsti
cs: MiTLS.CipherSuite.cipherSuite' -> Prims.bool
MiTLS.CipherSuite.cipherSuite' MiTLS.CipherSuite.aeAlg Prims.bool
let isAnonCipherSuite cs =
  
match cs with
| CipherSuite Kex_DHE None _ -> true
| _ -> false