miTLS :: TLSConstants

F# Interface: TLSConstants.fsi

(*
 * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved.
 * 
 * This code is distributed under the terms for the CeCILL-B (version 1)
 * license.
 * 
 * You should have received a copy of the CeCILL-B (version 1) license
 * along with this program.  If not, see:
 * 
 *   http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt
 *)

module TLSConstants

open Bytes
open Error

(* Not abstract, but meant to be used only by crypto modules and CipherSuites *)

type PreProtocolVersion =
    | SSL_3p0
    | TLS_1p0
    | TLS_1p1
    | TLS_1p2
type ProtocolVersion = PreProtocolVersion

type blockCipher =
    | TDES_EDE
    | AES_128
    | AES_256

type encAlg =
    | CBC_Stale of blockCipher
    | CBC_Fresh of blockCipher
    | Stream_RC4_128

type hashAlg =
    | NULL
    | MD5SHA1
    | MD5
    | SHA
    | SHA256
    | SHA384

type macAlg =
    | MA_HMAC of hashAlg
    | MA_SSLKHASH of hashAlg

type sigAlg =
  | SA_RSA
  | SA_DSA
  | SA_ECDSA

type sigHashAlg = sigAlg * hashAlg

type aeadAlg =
    | AES_128_GCM
    | AES_256_GCM

type authencAlg =
    | MACOnly of macAlg
    | MtE of encAlg * macAlg
    | AEAD of aeadAlg * macAlg

val sigAlgBytes: sigAlg -> bytes
val parseSigAlg: bytes -> sigAlg Result
val hashAlgBytes: hashAlg -> bytes
val parseHashAlg: bytes -> hashAlg Result

val encKeySize: encAlg -> nat
val blockSize: blockCipher -> nat
val aeadKeySize: aeadAlg -> nat
val aeadIVSize: aeadAlg -> nat
val macKeySize: macAlg -> nat
val macSize: macAlg -> nat

(* SSL/TLS Constants *)
val ssl_pad1_md5: bytes
val ssl_pad2_md5: bytes
val ssl_pad1_sha1: bytes
val ssl_pad2_sha1: bytes
val ssl_sender_client: bytes
val ssl_sender_server: bytes
val tls_sender_client: string
val tls_sender_server: string
val tls_master_secret: string
val tls_key_expansion: string

type cipherSuite

type cipherSuites = cipherSuite list

type Compression =
    | NullCompression

val versionBytes: ProtocolVersion -> bytes
val parseVersion: bytes -> ProtocolVersion Result
val minPV: ProtocolVersion -> ProtocolVersion -> ProtocolVersion
val geqPV: ProtocolVersion -> ProtocolVersion -> bool
val somePV: ProtocolVersion -> ProtocolVersion option

val nullCipherSuite: cipherSuite
val isNullCipherSuite: cipherSuite -> bool

val isAnonCipherSuite: cipherSuite -> bool
val isDHCipherSuite: cipherSuite -> bool
val isDHECipherSuite: cipherSuite -> bool
val isRSACipherSuite: cipherSuite -> bool
val contains_TLS_EMPTY_RENEGOTIATION_INFO_SCSV: cipherSuites -> bool
val verifyDataLen_of_ciphersuite: cipherSuite -> nat
val prfMacAlg_of_ciphersuite: cipherSuite -> macAlg
val verifyDataHashAlg_of_ciphersuite: cipherSuite -> hashAlg

val authencAlg_of_ciphersuite: cipherSuite -> ProtocolVersion -> authencAlg
val macAlg_of_ciphersuite: cipherSuite -> ProtocolVersion -> macAlg
val encAlg_of_ciphersuite: cipherSuite -> ProtocolVersion -> encAlg
val sigAlg_of_ciphersuite: cipherSuite -> sigAlg

val compressionBytes: Compression -> bytes
val compressionMethodsBytes: Compression list -> bytes
val parseCompression: bytes -> Compression Result
val parseCompressions: bytes -> Compression list

val cipherSuiteBytes: cipherSuite -> bytes
val parseCipherSuite: bytes -> cipherSuite Result
val parseCipherSuites: bytes -> cipherSuites Result
val cipherSuitesBytes: cipherSuites -> bytes

val getKeyExtensionLength: ProtocolVersion -> cipherSuite -> nat

(* Not for verification, just to run the implementation *)

type cipherSuiteName =
    | TLS_NULL_WITH_NULL_NULL

val cipherSuites_of_nameList: cipherSuiteName list -> cipherSuites
val name_of_cipherSuite: cipherSuite -> cipherSuiteName Result

(* val split_at_most: bytes -> nat -> (bytes * bytes) *)

type preContentType =
    | Change_cipher_spec
    | Alert
    | Handshake
    | Application_data

type ContentType = preContentType
val bytes_of_seq: nat -> bytes
val seq_of_bytes: bytes -> nat

val ctBytes: ContentType -> bytes
val parseCT: bytes -> ContentType Result
val CTtoString: ContentType -> string

val vlbytes: nat -> bytes -> bytes
val vlsplit: nat -> bytes -> (bytes * bytes) Result
val vlparse: nat -> bytes -> bytes Result

//val splitList: bytes -> nat list -> bytes list

type certType =
    | RSA_sign
    | DSA_sign
    | RSA_fixed_dh
    | DSA_fixed_dh

val certTypeBytes: certType -> bytes
val parseCertType: bytes -> certType Result
val certificateTypeListBytes: certType list -> bytes
val parseCertificateTypeList: bytes -> certType list Result
val defaultCertTypes: bool -> cipherSuite -> certType list
val distinguishedNameListBytes: string list -> bytes
val parseDistinguishedNameList: bytes -> string list -> string list Result

F# Implementation: TLSConstants.fs

module TLSConstants

open Bytes
open Error

type blockCipher =
    | TDES_EDE
    | AES_128
    | AES_256

type encAlg =
    | CBC_Stale of blockCipher
    | CBC_Fresh of blockCipher
    | Stream_RC4_128

type hashAlg =
    | NULL
    | MD5SHA1
    | MD5
    | SHA
    | SHA256
    | SHA384

type macAlg =
    | MA_HMAC of hashAlg
    | MA_SSLKHASH of hashAlg

type sigAlg =
  | SA_RSA
  | SA_DSA
  | SA_ECDSA

type sigHashAlg   = sigAlg * hashAlg

let sigAlgBytes sa =
    match sa with
    | SA_RSA   -> [|1uy|]
    | SA_DSA   -> [|2uy|]
    | SA_ECDSA -> [|3uy|]

let parseSigAlg b =
    match b with
    | [|1uy|] -> correct SA_RSA
    | [|2uy|] -> correct SA_DSA
    | [|3uy|] -> correct SA_ECDSA
    | _ -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let hashAlgBytes ha =
    match ha with
    | MD5     -> [|1uy|]
    | SHA     -> [|2uy|]
    | SHA256  -> [|4uy|]
    | SHA384  -> [|5uy|]
    | NULL    -> unexpectedError "[macAlgBytes] Cannot enode NULL hash alg."
    | MD5SHA1 -> unexpectedError "[macAlgBytes] Cannot enode MD5SHA1 hash alg."

let parseHashAlg b =
    match b with
    | [|1uy|] -> correct MD5
    | [|2uy|] -> correct SHA
    | [|4uy|] -> correct SHA256
    | [|5uy|] -> correct SHA384
    | _ -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

type aeadAlg =
    | AES_128_GCM
    | AES_256_GCM

type authencAlg = //for specification
    | MACOnly of macAlg
    | MtE of encAlg * macAlg
    | AEAD of aeadAlg * macAlg // for the PRF

let blockSize ciph =
    match ciph with
    | TDES_EDE      -> 8
    | AES_128       -> 16
    | AES_256       -> 16

let aeadKeySize ciph =
    match ciph with
    | AES_128_GCM -> 16
    | AES_256_GCM -> 16

let aeadIVSize ciph =
    match ciph with
    | AES_128_GCM -> 16
    | AES_256_GCM -> 16

let hashSize alg =
    match alg with
    | MD5     -> 16
    | SHA     -> 20
    | SHA256  -> 32
    | SHA384  -> 48
    | MD5SHA1 -> 16 + 20
    | NULL    -> Error.unexpectedError "[hashSize] Unknown hash size for NULL algorithm"

let macKeySize mac =
    match mac with
    | MA_HMAC(alg) | MA_SSLKHASH(alg) ->
        hashSize alg

let macSize mac =
    match mac with
    | MA_HMAC(alg) | MA_SSLKHASH(alg) ->
        hashSize alg
(* SSL/TLS constants *)

let ssl_pad1_md5  = createBytes 48 0x36
let ssl_pad2_md5  = createBytes 48 0x5c
let ssl_pad1_sha1 = createBytes 40 0x36
let ssl_pad2_sha1 = createBytes 40 0x5c
let ssl_sender_client = [|0x43uy; 0x4Cuy; 0x4Euy; 0x54uy|]
let ssl_sender_server = [|0x53uy; 0x52uy; 0x56uy; 0x52uy|]
let tls_sender_client = "client finished"
let tls_sender_server = "server finished"
let tls_master_secret = "master secret"
let tls_key_expansion = "key expansion"

(* ------------------------------------------------------------------------ *)
(* Key parameters *)
type dsaparams = { p : bytes; q : bytes; g : bytes; }

type skeyparams =
| SK_RSA of bytes * bytes (* modulus x exponent *)
| SK_DSA of bytes * dsaparams

type pkeyparams =
| PK_RSA of bytes * bytes
| PK_DSA of bytes * dsaparams

let sigalg_of_skeyparams = function
| SK_RSA _ -> SA_RSA
| SK_DSA _ -> SA_DSA

let sigalg_of_pkeyparams = function
| PK_RSA _ -> SA_RSA
| PK_DSA _ -> SA_DSA

(* Cipher Suites *)

// For now we only support one SCSV, but there exist others.
type SCSVsuite =
    | TLS_EMPTY_RENEGOTIATION_INFO_SCSV

type cipherAlg = // used only in ciphersuite definition
    | RC4_128
    | TDES_EDE_CBC
    | AES_128_CBC
    | AES_256_CBC

type csAuthEncAlg =
    | CS_MtE of cipherAlg * hashAlg
    | CS_AEAD of aeadAlg * hashAlg

type cipherSuite =
    | NullCipherSuite
    | CipherSuite of kexAlg * csAuthEncAlg
    | OnlyMACCipherSuite of kexAlg * hashAlg
    | SCSV of SCSVsuite

type cipherSuites = cipherSuite list

type Compression =
    | NullCompression

let parseCompression b =
    match b with
    | [|0uy|] -> correct(NullCompression)
    | _       -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

// Ignore compression methods we don't understand. This is a departure
// from usual parsing, where we fail on unknown values, but that's how TLS
// handles compression method lists.
let rec parseCompressions b =
    let l = length b
    if l > 0
    then
        let (cmB,b) = split b 1 in
        match parseCompression cmB with
        | Error(x,y) -> // skip this one
            parseCompressions b
        | Correct(cm) -> cm :: parseCompressions b
    else []

let compressionBytes (comp:Compression) =
    match comp with
    | NullCompression -> [|0uy|]

let rec compressionMethodsBytes cs =
   match cs with
   | c::cs -> compressionBytes c @| compressionMethodsBytes cs
   | []    -> [||]

type PreProtocolVersion =
    | SSL_3p0
    | TLS_1p0
    | TLS_1p1
    | TLS_1p2
type ProtocolVersion = PreProtocolVersion

let somePV (a:ProtocolVersion) = Some a

let nullCipherSuite = NullCipherSuite

let isNullCipherSuite cs =
    cs = NullCipherSuite

let cipherSuiteBytes cs =
    match cs with
    | NullCipherSuite                                     -> [| 0x00uy; 0x00uy |]

| SCSV (TLS_EMPTY_RENEGOTIATION_INFO_SCSV)            -> [| 0x00uy; 0xFFuy |]

| _ -> unexpectedError "[cipherSuiteBytes] invoked on an unknown ciphersuite"

let parseCipherSuite b =
    match b with
    | [| 0x00uy; 0x00uy |] -> correct(NullCipherSuite)

| [| 0x00uy; 0xFFuy |] -> correct(SCSV (TLS_EMPTY_RENEGOTIATION_INFO_SCSV))

| _ -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let consCipherSuites (cs:cipherSuite) (css:cipherSuites) = cs::css

// called by the server handshake;
// ciphersuites that we do not understand are parsed,
// but not added to the list, and thus will be ignored by the server
let rec parseCipherSuites b:cipherSuites Result =
    if length b > 1 then
        let (b0,b1) = split b 2
        match parseCipherSuites b1 with
        | Correct(css) ->
            match parseCipherSuite b0 with
            | Error(x,y) -> // ignore this cs
                correct(css)
            | Correct(cs) -> let ncss = consCipherSuites cs css  in correct(ncss)
        | Error(x,y) -> Error(x,y)
    else if length b = 0 then Correct([])
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let rec cipherSuitesBytes css =
    match css with
    | [] -> [||]
    | cs::css -> cipherSuiteBytes cs @|
                 cipherSuitesBytes css

let isAnonCipherSuite cs =
    match cs with
    | CipherSuite ( DH_anon, _ )   -> true
 (* | ( ECDH_anon, _ ) -> true *)
    | _ -> false

let isDHCipherSuite cs =
    match cs with
    | CipherSuite (DH_DSS, _ ) -> true
    | CipherSuite (DH_RSA, _ ) -> true
    | _ -> false

let isRSACipherSuite cs =
    match cs with
    | CipherSuite ( RSA, _ )     -> true
    | OnlyMACCipherSuite ( RSA, _ ) -> true
    | _ -> false

let contains_TLS_EMPTY_RENEGOTIATION_INFO_SCSV (css: cipherSuite list) =

List.exists (fun cs -> cs = SCSV (TLS_EMPTY_RENEGOTIATION_INFO_SCSV) ) css

let verifyDataLen_of_ciphersuite (cs:cipherSuite) =
    (* Only to be invoked with TLS 1.2 (hardcoded in previous versions *)
    match cs with
    | _ -> 12

let prfMacAlg_of_ciphersuite (cs:cipherSuite) =
    (* Only to be invoked with TLS 1.2 (hardcoded in previous versions *)
    match cs with
   // | CipherSuite ( ECDH*, MtE (_,SHA384)) -> SHA384
    | CipherSuite ( _ , CS_MtE ( _ , _ )) -> MA_HMAC(SHA256)
    | CipherSuite ( _ , CS_AEAD ( _ , hAlg ))   -> MA_HMAC(hAlg)
    | OnlyMACCipherSuite (_, hAlg) -> MA_HMAC(SHA256)
    | NullCipherSuite         -> unexpectedError "[prfHashAlg_of_ciphersuite] invoked on an invalid ciphersuite"
    | SCSV (_)                -> unexpectedError "[prfHashAlg_of_ciphersuite] invoked on an invalid ciphersuite"

// PRF and verifyData hash algorithms are potentially independent in TLS 1.2,
// so we use two distinct functions. However, all currently defined ciphersuites
// use the same hash algorithm, so the current implementation of the two functions
// is the same.
let verifyDataHashAlg_of_ciphersuite (cs:cipherSuite) =
    (* Only to be invoked with TLS 1.2 (hardcoded in previous versions *)
    match cs with
   // | CipherSuite ( ECDH*, MtE (_,SHA384)) -> SHA384
    | CipherSuite ( _ , CS_MtE ( _ , _ ))     -> SHA256
    | CipherSuite ( _ , CS_AEAD ( _ , hAlg )) -> hAlg
    | OnlyMACCipherSuite (_, hAlg)         -> SHA256
    | NullCipherSuite -> unexpectedError "[verifyDataHashAlg_of_ciphersuite] invoked on an invalid ciphersuite"
    | SCSV (_)        -> unexpectedError "[verifyDataHashAlg_of_ciphersuite] invoked on an invalid ciphersuite"

let authencAlg_of_ciphersuite cs pv =
    match cs with
    | OnlyMACCipherSuite (_,alg) ->
        let mac = macAlg_of_ciphersuite cs pv in
        MACOnly mac
    | CipherSuite(_, CS_MtE(e,a)) ->
        let enc = encAlg_of_ciphersuite cs pv in
        let mac = macAlg_of_ciphersuite cs pv in
        MtE (enc,mac)
    | _ -> unexpectedError "[authencAlg_of_ciphersuite] invoked on an invalid ciphersuite"

let mkIntTriple x:(int*int*int) = x

let getKeyExtensionLength pv cs =
    let (keySize, IVSize, hashSize ) =
        match cs with
        | CipherSuite (_, CS_MtE(cAlg, hAlg)) ->
            let encAlg = encAlg_of_ciphersuite cs pv in
            let macAlg = macAlg_of_ciphersuite cs pv in
            match encAlg with
            | Stream_RC4_128 | CBC_Fresh(_) -> mkIntTriple ((encKeySize encAlg), 0, (macKeySize macAlg))
            | CBC_Stale(blockEnc) -> mkIntTriple ((encKeySize encAlg),(blockSize blockEnc),(macKeySize macAlg))
        | CipherSuite (_, CS_AEAD(cAlg, hAlg)) -> ((aeadKeySize cAlg), (aeadIVSize cAlg), (macKeySize (MA_HMAC(hAlg))))
        | OnlyMACCipherSuite (_,hAlg) ->
            let macAlg = macAlg_of_ciphersuite cs pv in
            (0,0,macKeySize macAlg)
        | _ -> unexpectedError "[getKeyExtensionLength] invoked on an invalid ciphersuite"
    2 * (keySize + IVSize + hashSize)

(* Not for verification, just to run the implementation. See TLSInfo.fs *)
type cipherSuiteName =
    | TLS_NULL_WITH_NULL_NULL

let cipherSuites_of_nameList (nameList: cipherSuiteName list) =

List.map (
    fun name ->
        match name with
        | TLS_NULL_WITH_NULL_NULL                -> NullCipherSuite

| TLS_RSA_WITH_NULL_MD5                  -> OnlyMACCipherSuite (RSA, MD5)
        | TLS_RSA_WITH_NULL_SHA                  -> OnlyMACCipherSuite (RSA, SHA)
        | TLS_RSA_WITH_NULL_SHA256               -> OnlyMACCipherSuite (RSA, SHA256)
        | TLS_RSA_WITH_RC4_128_MD5               -> CipherSuite (RSA, CS_MtE (RC4_128, MD5))
        | TLS_RSA_WITH_RC4_128_SHA               -> CipherSuite (RSA, CS_MtE (RC4_128, SHA))
        | TLS_RSA_WITH_3DES_EDE_CBC_SHA          -> CipherSuite (RSA, CS_MtE (TDES_EDE_CBC, SHA))
        | TLS_RSA_WITH_AES_128_CBC_SHA           -> CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA))
        | TLS_RSA_WITH_AES_256_CBC_SHA           -> CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA))
        | TLS_RSA_WITH_AES_128_CBC_SHA256        -> CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA256))
        | TLS_RSA_WITH_AES_256_CBC_SHA256        -> CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA256))

| TLS_DHE_DSS_WITH_3DES_EDE_CBC_SHA      -> CipherSuite (DHE_DSS, CS_MtE (TDES_EDE_CBC, SHA))
        | TLS_DHE_RSA_WITH_3DES_EDE_CBC_SHA      -> CipherSuite (DHE_RSA, CS_MtE (TDES_EDE_CBC, SHA))
        | TLS_DHE_DSS_WITH_AES_128_CBC_SHA       -> CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA))
        | TLS_DHE_RSA_WITH_AES_128_CBC_SHA       -> CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA))
        | TLS_DHE_DSS_WITH_AES_256_CBC_SHA       -> CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA))
        | TLS_DHE_RSA_WITH_AES_256_CBC_SHA       -> CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA))
        | TLS_DHE_DSS_WITH_AES_128_CBC_SHA256    -> CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA256))
        | TLS_DHE_RSA_WITH_AES_128_CBC_SHA256    -> CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA256))
        | TLS_DHE_DSS_WITH_AES_256_CBC_SHA256    -> CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA256))
        | TLS_DHE_RSA_WITH_AES_256_CBC_SHA256    -> CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA256))

| TLS_DH_anon_WITH_RC4_128_MD5           -> CipherSuite (DH_anon, CS_MtE (RC4_128, MD5))
        | TLS_DH_anon_WITH_3DES_EDE_CBC_SHA      -> CipherSuite (DH_anon, CS_MtE (TDES_EDE_CBC, SHA))
        | TLS_DH_anon_WITH_AES_128_CBC_SHA       -> CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA))
        | TLS_DH_anon_WITH_AES_256_CBC_SHA       -> CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA))
        | TLS_DH_anon_WITH_AES_128_CBC_SHA256    -> CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA256))
        | TLS_DH_anon_WITH_AES_256_CBC_SHA256    -> CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA256))
   ) nameList

let name_of_cipherSuite cs =
    match cs with
    | NullCipherSuite                                      ->  correct TLS_NULL_WITH_NULL_NULL

| OnlyMACCipherSuite (RSA, MD5)                        ->  correct TLS_RSA_WITH_NULL_MD5
    | OnlyMACCipherSuite (RSA, SHA)                        ->  correct TLS_RSA_WITH_NULL_SHA
    | OnlyMACCipherSuite (RSA, SHA256)                     ->  correct TLS_RSA_WITH_NULL_SHA256
    | CipherSuite (RSA, CS_MtE (RC4_128, MD5))             ->  correct TLS_RSA_WITH_RC4_128_MD5
    | CipherSuite (RSA, CS_MtE (RC4_128, SHA))             ->  correct TLS_RSA_WITH_RC4_128_SHA
    | CipherSuite (RSA, CS_MtE (TDES_EDE_CBC, SHA))        ->  correct TLS_RSA_WITH_3DES_EDE_CBC_SHA
    | CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA))         ->  correct TLS_RSA_WITH_AES_128_CBC_SHA
    | CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA))         ->  correct TLS_RSA_WITH_AES_256_CBC_SHA
    | CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA256))      ->  correct TLS_RSA_WITH_AES_128_CBC_SHA256
    | CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA256))      ->  correct TLS_RSA_WITH_AES_256_CBC_SHA256

| CipherSuite (DHE_DSS, CS_MtE (TDES_EDE_CBC, SHA))    ->  correct TLS_DHE_DSS_WITH_3DES_EDE_CBC_SHA
    | CipherSuite (DHE_RSA, CS_MtE (TDES_EDE_CBC, SHA))    ->  correct TLS_DHE_RSA_WITH_3DES_EDE_CBC_SHA
    | CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA))     ->  correct TLS_DHE_DSS_WITH_AES_128_CBC_SHA
    | CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA))     ->  correct TLS_DHE_RSA_WITH_AES_128_CBC_SHA
    | CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA))     ->  correct TLS_DHE_DSS_WITH_AES_256_CBC_SHA
    | CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA))     ->  correct TLS_DHE_RSA_WITH_AES_256_CBC_SHA
    | CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA256))  ->  correct TLS_DHE_DSS_WITH_AES_128_CBC_SHA256
    | CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA256))  ->  correct TLS_DHE_RSA_WITH_AES_128_CBC_SHA256
    | CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA256))  ->  correct TLS_DHE_DSS_WITH_AES_256_CBC_SHA256
    | CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA256))  ->  correct TLS_DHE_RSA_WITH_AES_256_CBC_SHA256

| CipherSuite (DH_anon, CS_MtE (RC4_128, MD5))         ->  correct TLS_DH_anon_WITH_RC4_128_MD5
    | CipherSuite (DH_anon, CS_MtE (TDES_EDE_CBC, SHA))    ->  correct TLS_DH_anon_WITH_3DES_EDE_CBC_SHA
    | CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA))     ->  correct TLS_DH_anon_WITH_AES_128_CBC_SHA
    | CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA))     ->  correct TLS_DH_anon_WITH_AES_256_CBC_SHA
    | CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA256))  ->  correct TLS_DH_anon_WITH_AES_128_CBC_SHA256
    | CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA256))  ->  correct TLS_DH_anon_WITH_AES_256_CBC_SHA256

| _ -> Error(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Invoked on a unknown ciphersuite")

(* From Formats *)

type preContentType =
    | Change_cipher_spec
    | Alert
    | Handshake
    | Application_data

type ContentType = preContentType

let ctBytes ct =
    match ct with
    | Change_cipher_spec -> [|20uy|]
    | Alert              -> [|21uy|]
    | Handshake          -> [|22uy|]
    | Application_data   -> [|23uy|]

let parseCT b =
    match b with
    | [|20uy|] -> correct(Change_cipher_spec)
    | [|21uy|] -> correct(Alert)
    | [|22uy|] -> correct(Handshake)
    | [|23uy|] -> correct(Application_data)
    | _        -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let CTtoString = function
    | Change_cipher_spec -> "CCS"
    | Alert              -> "Alert"
    | Handshake          -> "Handshake"
    | Application_data   -> "Data"

let bytes_of_seq sn = bytes_of_int 8 sn
let seq_of_bytes b = int_of_bytes b

let vlbytes (lSize:int) b = bytes_of_int lSize (length b) @| b

let vlsplit lSize vlb : (bytes * bytes) Result =
    let (vl,b) = split vlb lSize
    let l = int_of_bytes vl
    if l <= length b
    then correct(split b l)
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let vlparse lSize vlb : bytes Result =
    let (vl,b) = split vlb lSize
    let l = int_of_bytes vl
    if l = length b
    then correct b
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

type certType =
    | RSA_sign
    | DSA_sign
    | RSA_fixed_dh
    | DSA_fixed_dh

let certTypeBytes ct =
    match ct with
    | RSA_sign     -> [|1uy|]
    | DSA_sign     -> [|2uy|]
    | RSA_fixed_dh -> [|3uy|]
    | DSA_fixed_dh -> [|4uy|]

let parseCertType b =
    match b with
    | [|1uy|] -> Correct(RSA_sign)
    | [|2uy|] -> Correct(DSA_sign)
    | [|3uy|] -> Correct(RSA_fixed_dh)
    | [|4uy|] -> Correct(DSA_fixed_dh)
    | _ -> Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let rec certificateTypeListBytes ctl =
    match ctl with
    | [] -> [||]
    | h::t ->
        let ct = certTypeBytes h in
        ct @| certificateTypeListBytes t

let rec parseCertificateTypeList data =
    if length data = 0 then let res = [] in correct(res)
    else
        let (thisByte,data) = Bytes.split data 1 in
        match parseCertType thisByte with
        | Correct(ct) ->
            match parseCertificateTypeList data with
            | Correct(ctList) -> Correct(ct :: ctList)
            | Error(x,y) -> Error(x,y)
        | Error(x,y) -> Error(x,y)

let defaultCertTypes sign cs =
    if sign then
        match sigAlg_of_ciphersuite cs with
        | SA_RSA -> [RSA_sign]
        | SA_DSA -> [DSA_sign]
        | _ -> unexpectedError "[defaultCertTypes] invoked on an invalid ciphersuite"
    else
        match sigAlg_of_ciphersuite cs with
        | SA_RSA -> [RSA_fixed_dh]
        | SA_DSA -> [DSA_fixed_dh]
        | _ -> unexpectedError "[defaultCertTypes] invoked on an invalid ciphersuite"

let rec distinguishedNameListBytes names =
    match names with
    | [] -> [||]
    | h::t ->
        let name = vlbytes 2 (utf8 h) in
        name @| distinguishedNameListBytes t

let rec parseDistinguishedNameList data res =
    if length data = 0 then
        correct (res)
    else
        if length data < 2 then (* Maybe at least 3 bytes, because we don't want empty names... *)
            Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
        else
            match vlsplit 2 data with
            | Error(x,y) -> Error(x,y)
            | Correct (nameBytes,data) ->
            let name = iutf8 nameBytes in
            let res = name :: res in
            parseDistinguishedNameList data res

F7 Interface: TLSConstants.fs7

module TLSConstants

(* Identifiers and sizes for the TLS crypto algorithms *)

open Bytes
open Error

type PreProtocolVersion =
    | SSL_3p0
    | TLS_1p0
    | TLS_1p1
    | TLS_1p2

type ProtocolVersion = p:PreProtocolVersion{p = SSL_3p0 \/ p = TLS_1p0 \/ p = TLS_1p1 \/ p = TLS_1p2}

(* Not abstract, but meant to be used only by crypto modules and CipherSuites *)

type blockCipher =
    | TDES_EDE
    | AES_128
    | AES_256

type encAlg =
	| CBC_Stale of blockCipher
	| CBC_Fresh of blockCipher
	| Stream_RC4_128

predicate IND_CPA of encAlg
//#begin-cipherAssert
// some reasonable cryptographic assumptions if you believe that you are sufficiently
// protected against timing attacks (see: http://www.isg.rhul.ac.uk/tls/Lucky13.html )
// assume(IND_CPA(CBC_Fresh(AES_128_CBC)))
// assume(IND_CPA(CBC_Fresh(AES_256_CBC)))
// examples for wrong cryptographic assumptions:
// assume(IND_CPA(Stream_RC4_128)) (see: http://vnhacker.blogspot.co.uk/2011/09/beast.html )
// assume(IND_CPA(CBC_Stale(AES_256_CBC))) (see: http://www.isg.rhul.ac.uk/tls/ )
//#end-cipherAssert

type hashAlg =
    | NULL
    | MD5SHA1
    | MD5
    | SHA
    | SHA256
    | SHA384

(** Algorithms for the MAC module *)

type macAlg =
	| MA_HMAC of hashAlg
	| MA_SSLKHASH of hashAlg

predicate INT_CMA_M of macAlg  (* Strong algorithms for the INT-CMA game *)
// some reasonable cryptogaphic assumptions:
// assume(INT_CMA_M(MA_HMAC(SHA)))
// assume(INT_CMA_M(MA_HMAC(SHA256)))
// assume(INT_CMA_M(MA_HMAC(SHA384)))

(** Signing algorithms for the Sig module *)

type sigAlg =
  | SA_RSA
  | SA_DSA
  | SA_ECDSA

type sigHashAlg   = sigAlg * hashAlg

predicate INT_CMA_S of sigAlg * hashAlg * hashAlg list
// INT_CMA_S(s,h,hs) indicates that signing hashes using s,h is INT-CMA,
// even if we also sign hashes using s,h' in hs
// (
//
// some reasonable cryptographic assumptions:
// assume(INT_CMA_S(SA_DSA,SHA,[SHA]))
// assume(INT_CMA_S(SA_ECDSA,SHA,[SHA]))

type aeadAlg =
    | AES_128_GCM
    | AES_256_GCM

type authencAlg = // for specification of INT_CTXT predicate
    | MACOnly of macAlg
    | MtE of encAlg * macAlg
    | AEAD of aeadAlg * macAlg // macAlg is for the PRF

predicate INT_CTXT of authencAlg * ProtocolVersion
// some reasonable assumptions:
// assume INT_CTXT(MtE(CBC_Fresh(AES_128_CBC),HMAC(SHA256)),TLS_1p2)
// This follows from Paterson et al.
// assume !e,m. PRF(m) /\ SPRP(e) => INT_CTXT(MtE(CBC_Fresh(e),m),TLS_1p2)

type kexAlg =  (* all these kex have server auth & optional client auth, *)
               (* except for anon which has nothing *)
    | RSA     // --> client-generated pms encrypted using server's public key
    | DH_DSS  // <-- Certificate(DSA containing g^y); --> g^x then pms = g^xy

| DH_RSA  // idem with an RSA cert
    | DHE_DSS // <-- Certificate(DSA); ServerKeyExchange({Cr,Sr,p,g,g^y}signed); --> g^x then pms = g^xy

| DHE_RSA
    | DH_anon // --> g^x ; <-- g^y then pms = g^xy ; secure only against passive adversaries

predicate PRF of ProtocolVersion * macAlg
predicate CRE_DH of ProtocolVersion * macAlg
predicate CRE_RSA of ProtocolVersion * macAlg
// In the paper, these are global assumptions. Here we get StrongHS even if one of them is false.

(* With F7, we need to declare both logical functions for lengths, constants, etc
   and their concrete F# implementations, typechecked against these logical functions. *)

function val SigAlgBytes: sigAlg -> bytes
private definition !s.
           (SigAlgBytes(SA_RSA) = [|1uy|]) /\
           (SigAlgBytes(SA_DSA) = [|2uy|]) /\
           (SigAlgBytes(SA_ECDSA) = [|3uy|])

val sigAlgBytes: s:sigAlg -> b:bytes{b=SigAlgBytes(s)}
val parseSigAlg: b:bytes -> (s:sigAlg{b=SigAlgBytes(s)}) Result
function val HashAlgBytes: hashAlg -> bytes
definition HashAlgBytes(MD5) = [|1uy|] /\
       HashAlgBytes(SHA) = [|2uy|] /\
       HashAlgBytes(SHA256) = [|4uy|] /\
       HashAlgBytes(SHA384) = [|5uy|]

val hashAlgBytes: h:hashAlg -> b:bytes{b=HashAlgBytes(h)}
val parseHashAlg: b:bytes -> (h:hashAlg{b=HashAlgBytes(h)}) Result

function val EncKeySize: encAlg -> nat
assume !x. EncKeySize(x) >= 0
private definition EncKeySize(Stream_RC4_128)      = 16
private definition EncKeySize(CBC_Stale(TDES_EDE)) = 24
private definition EncKeySize(CBC_Stale(AES_128))  = 16
private definition EncKeySize(CBC_Stale(AES_256))  = 32
private definition EncKeySize(CBC_Fresh(TDES_EDE)) = 24
private definition EncKeySize(CBC_Fresh(AES_128))  = 16
private definition EncKeySize(CBC_Fresh(AES_256))  = 32
val encKeySize: a:encAlg -> l:nat{l=EncKeySize(a)}

function val BlockSize: blockCipher -> nat
assume !x. BlockSize(x) >= 0
private definition BlockSize(TDES_EDE)	=  8
private definition BlockSize(AES_128)	= 16
private definition BlockSize(AES_256)	= 16
val blockSize: a:blockCipher -> l:nat {l=BlockSize(a)}

function val EncAlgBlockSize: encAlg -> nat
assume !x. EncAlgBlockSize(x) >= 0
private definition !b. EncAlgBlockSize(CBC_Stale(b)) = BlockSize(b)
private definition !b. EncAlgBlockSize(CBC_Fresh(b)) = BlockSize(b)
private definition EncAlgBlockSize(Stream_RC4_128) = 0

val aeadKeySize: aeadAlg -> nat
val aeadIVSize: aeadAlg -> nat

function val HashSize: hashAlg -> nat
private assume !x. HashSize(x) >= 0
private definition HashSize(MD5    )     = 16
private definition HashSize(SHA    )     = 20
private definition HashSize(SHA256 )     = 32
private definition HashSize(SHA384 )     = 48
private definition HashSize(MD5SHA1)     = 36

function val MacSize: macAlg -> nat
assume !x. MacSize(x) >= 0
private definition !a. MacSize(MA_HMAC(a)) = HashSize(a)
private definition !a. MacSize(MA_SSLKHASH(a)) = HashSize(a)

val macKeySize: a:macAlg -> l:nat{l=MacSize(a)}
val macSize:    a:macAlg -> l:nat{l=MacSize(a)}
private val hashSize:   a:hashAlg -> l:nat{l=HashSize(a)}

(* SSL/TLS Constants *)

val ssl_pad1_md5:  bytes
val ssl_pad2_md5:  bytes
val ssl_pad1_sha1: bytes
val ssl_pad2_sha1: bytes

val ssl_sender_client: bytes
val ssl_sender_server: bytes
val tls_sender_client: string
val tls_sender_server: string
val tls_master_secret: string
val tls_key_expansion: string

(* ------------------------------------------------------------------------ *)
(* Key parameters *)
type dsaparams = { p : bytes; q : bytes; g : bytes; }

type skeyparams =
| SK_RSA of bytes * bytes (* modulus x exponent *)
| SK_DSA of bytes * dsaparams

type pkeyparams =
| PK_RSA of bytes * bytes
| PK_DSA of bytes * dsaparams

val sigalg_of_skeyparams: skeyparams -> sigAlg
val sigalg_of_pkeyparams: pkeyparams -> sigAlg
(*** Following RFC5246 A.5 *)

private type SCSVsuite =
    | TLS_EMPTY_RENEGOTIATION_INFO_SCSV

type cipherAlg = // internal; used only in ciphersuite definition
    | RC4_128
    | TDES_EDE_CBC
    | AES_128_CBC
    | AES_256_CBC

type csAuthEncAlg = // internal; used only in ciphersuite definition
    | CS_MtE of cipherAlg * hashAlg
    | CS_AEAD of aeadAlg * hashAlg

private type cipherSuite = // internal; kept abstract in the .fsi
    | NullCipherSuite
    | CipherSuite of kexAlg * csAuthEncAlg
    | OnlyMACCipherSuite of kexAlg * hashAlg
    | SCSV of SCSVsuite

type cipherSuites = cipherSuite list

type Compression =
    | NullCompression

function val CompressionBytes: Compression -> bytes
private definition CompressionBytes(NullCompression) = [| 0uy |]

predicate ContainsCompressions of Compression list * Compression list
function val CompressionsBytes: Compression list -> bytes

private assume CompressionsBytes([]) = [||] /\
  (!h,t. CompressionsBytes(h::t) = CompressionBytes(h) @| CompressionsBytes(t))
private assume !cl. ContainsCompressions(cl,cl) /\
   (!cl. ContainsCompressions(cl,[])) /\
   (!h,t,cl. ContainsCompressions(t,cl) => ContainsCompressions(h::t,cl)) /\
   (!h,t,h',t'. ContainsCompressions(t,t') => ContainsCompressions(h::t,h'::t'))

val compressionBytes: c:Compression -> b:bytes{CompressionBytes(c) = b}
val compressionMethodsBytes: cl:Compression list -> b:bytes{b = CompressionsBytes(cl)}
val parseCompression: b:bytes -> (c:Compression{b=CompressionBytes(c)}) Result
val parseCompressions: b:bytes -> cl:Compression list{?cl'. b = CompressionsBytes(cl') /\ ContainsCompressions(cl',cl)}

val versionBytes: pv:ProtocolVersion -> b:bytes{Length(b) = 2 /\ b = VersionBytes(pv)}
val parseVersion: b:bytes{Length(b) = 2} -> (pv:ProtocolVersion{ b= VersionBytes(pv)}) Result
val minPV: a:ProtocolVersion -> b:ProtocolVersion -> c:ProtocolVersion

val geqPV: a:ProtocolVersion -> b:ProtocolVersion -> r:bool
val somePV: a: ProtocolVersion -> b:ProtocolVersion option {b = Some(a)}

predicate val IsNullCiphersuite: cipherSuite -> bool
definition !x. IsNullCiphersuite(x) <=> x = NullCipherSuite
val nullCipherSuite: c:cipherSuite{IsNullCiphersuite(c)}
val isNullCipherSuite: c:cipherSuite -> r:bool{r=true <=> IsNullCiphersuite(c)}

predicate val IsSCSVCiphersuite: cipherSuite -> bool
definition !x. IsSCSVCiphersuite(x) <=> ?z. x = SCSV(z)

val isAnonCipherSuite: cipherSuite -> bool
val isDHCipherSuite: cipherSuite -> bool
val isDHECipherSuite: cipherSuite -> bool
val isRSACipherSuite: cipherSuite -> bool
val contains_TLS_EMPTY_RENEGOTIATION_INFO_SCSV: cipherSuites -> bool
val verifyDataLen_of_ciphersuite: cipherSuite -> nat
val prfMacAlg_of_ciphersuite: cipherSuite  -> macAlg
val verifyDataHashAlg_of_ciphersuite: cs:cipherSuite -> hashAlg

function val TLSMACAlg: hashAlg   * ProtocolVersion -> macAlg
function val TLSENCAlg: cipherAlg * ProtocolVersion -> encAlg

private definition !mac. TLSMACAlg(mac,SSL_3p0) = MA_SSLKHASH(mac)
private definition !mac. TLSMACAlg(mac,TLS_1p0) = MA_HMAC(mac)
private definition !mac. TLSMACAlg(mac,TLS_1p1) = MA_HMAC(mac)
private definition !mac. TLSMACAlg(mac,TLS_1p1) = MA_HMAC(mac)

private definition !pv. TLSENCAlg(RC4_128,pv) = Stream_RC4_128
private definition TLSENCAlg(TDES_EDE_CBC,SSL_3p0) = CBC_Stale(TDES_EDE)
private definition TLSENCAlg(TDES_EDE_CBC,TLS_1p0) = CBC_Stale(TDES_EDE)
private definition TLSENCAlg(AES_128_CBC, SSL_3p0) = CBC_Stale(AES_128)
private definition TLSENCAlg(AES_128_CBC, TLS_1p0) = CBC_Stale(AES_128)
private definition TLSENCAlg(AES_256_CBC, SSL_3p0) = CBC_Stale(AES_256)
private definition TLSENCAlg(AES_256_CBC, TLS_1p0) = CBC_Stale(AES_256)
private definition TLSENCAlg(TDES_EDE_CBC,TLS_1p1) = CBC_Fresh(TDES_EDE)
private definition TLSENCAlg(TDES_EDE_CBC,TLS_1p2) = CBC_Fresh(TDES_EDE)
private definition TLSENCAlg(AES_128_CBC, TLS_1p1) = CBC_Fresh(AES_128)
private definition TLSENCAlg(AES_128_CBC, TLS_1p2) = CBC_Fresh(AES_128)
private definition TLSENCAlg(AES_256_CBC, TLS_1p1) = CBC_Fresh(AES_256)
private definition TLSENCAlg(AES_256_CBC, TLS_1p2) = CBC_Fresh(AES_256)

function val CipherSuiteSigAlg: cipherSuite -> sigAlg
function val CipherSuiteSigHashAlg: cipherSuite -> sigHashAlg
function val CipherSuiteMACAlg: cipherSuite * ProtocolVersion -> macAlg
function val CipherSuiteENCAlg: cipherSuite * ProtocolVersion -> encAlg
function val CipherSuiteAuthEncAlg: cipherSuite * ProtocolVersion -> authencAlg

private definition !kex,mac,pv.
	CipherSuiteAuthEncAlg(OnlyMACCipherSuite(kex,mac),pv) = MACOnly(TLSMACAlg(mac,pv))
private definition !kex,enc,mac,pv.
	CipherSuiteAuthEncAlg(CipherSuite(kex,CS_MtE(enc,mac)),pv) = MtE(TLSENCAlg(enc,pv),TLSMACAlg(mac,pv))

assume !cs,pv,mac.
        CipherSuiteAuthEncAlg(cs,pv) = MACOnly(mac) => CipherSuiteMACAlg(cs,pv) = mac
assume !cs,pv,mac,enc.
        CipherSuiteAuthEncAlg(cs,pv) = MtE(enc,mac) => CipherSuiteMACAlg(cs,pv) = mac
assume !cs,pv,mac,enc.
        CipherSuiteAuthEncAlg(cs,pv) = MtE(enc,mac) => CipherSuiteENCAlg(cs,pv) = enc

val authencAlg_of_ciphersuite: cs:cipherSuite -> pv:ProtocolVersion -> a:authencAlg{a = CipherSuiteAuthEncAlg(cs,pv)}
val macAlg_of_ciphersuite: cs:cipherSuite -> pv:ProtocolVersion -> h:macAlg{h = CipherSuiteMACAlg(cs,pv)}
val encAlg_of_ciphersuite: cs:cipherSuite -> pv:ProtocolVersion -> c:encAlg{c = CipherSuiteENCAlg(cs,pv)}
val sigAlg_of_ciphersuite: cs:cipherSuite -> s:sigAlg{s = CipherSuiteSigAlg(cs)}

predicate KnownCipherSuite of cipherSuite
function val CipherSuiteBytes: cipherSuite -> bytes

private assume !cs. KnownCipherSuite(cs) <=>
       (cs = NullCipherSuite)
    \/ (cs = OnlyMACCipherSuite (RSA, MD5))
    \/ (cs = OnlyMACCipherSuite (RSA, SHA))
    \/ (cs = OnlyMACCipherSuite (RSA, SHA256))
    \/ (cs = CipherSuite (RSA, CS_MtE (RC4_128, MD5)))
    \/ (cs = CipherSuite (RSA, CS_MtE (RC4_128, SHA)))
    \/ (cs = CipherSuite (RSA, CS_MtE (TDES_EDE_CBC, SHA)))
    \/ (cs = CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA)))
    \/ (cs = CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA)))
    \/ (cs = CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA256)))
    \/ (cs = CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA256)))

\/ (cs = CipherSuite (DHE_DSS, CS_MtE (TDES_EDE_CBC, SHA)))
    \/ (cs = CipherSuite (DHE_RSA, CS_MtE (TDES_EDE_CBC, SHA)))
    \/ (cs = CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA)))
    \/ (cs = CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA)))
    \/ (cs = CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA)))
    \/ (cs = CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA)))
    \/ (cs = CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA256)))
    \/ (cs = CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA256)))
    \/ (cs = CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA256)))
    \/ (cs = CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA256)))

\/ (cs = CipherSuite (DH_anon, CS_MtE (RC4_128, MD5)))
    \/ (cs = CipherSuite (DH_anon, CS_MtE (TDES_EDE_CBC, SHA)))
    \/ (cs = CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA)))
    \/ (cs = CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA)))
    \/ (cs = CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA256)))
    \/ (cs = CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA256)))

\/ (cs = SCSV (TLS_EMPTY_RENEGOTIATION_INFO_SCSV))

private assume
       CipherSuiteBytes(NullCipherSuite)                                  = [| 0x00uy; 0x00uy |]
    /\ CipherSuiteBytes(OnlyMACCipherSuite (RSA, MD5))                    = [| 0x00uy; 0x01uy |]
    /\ CipherSuiteBytes(OnlyMACCipherSuite (RSA, SHA))                    = [| 0x00uy; 0x02uy |]
    /\ CipherSuiteBytes(OnlyMACCipherSuite (RSA, SHA256))                 = [| 0x00uy; 0x3Buy |]
    /\ CipherSuiteBytes(CipherSuite (RSA, CS_MtE (RC4_128, MD5)))            = [| 0x00uy; 0x04uy |]
    /\ CipherSuiteBytes(CipherSuite (RSA, CS_MtE (RC4_128, SHA)))            = [| 0x00uy; 0x05uy |]
    /\ CipherSuiteBytes(CipherSuite (RSA, CS_MtE (TDES_EDE_CBC, SHA)))       = [| 0x00uy; 0x0Auy |]
    /\ CipherSuiteBytes(CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA)))        = [| 0x00uy; 0x2Fuy |]
    /\ CipherSuiteBytes(CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA)))        = [| 0x00uy; 0x35uy |]
    /\ CipherSuiteBytes(CipherSuite (RSA, CS_MtE (AES_128_CBC, SHA256)))     = [| 0x00uy; 0x3Cuy |]
    /\ CipherSuiteBytes(CipherSuite (RSA, CS_MtE (AES_256_CBC, SHA256)))     = [| 0x00uy; 0x3Duy |]

/\ CipherSuiteBytes(CipherSuite (DHE_DSS, CS_MtE (TDES_EDE_CBC, SHA)))   = [| 0x00uy; 0x13uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_RSA, CS_MtE (TDES_EDE_CBC, SHA)))   = [| 0x00uy; 0x16uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA)))    = [| 0x00uy; 0x32uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA)))    = [| 0x00uy; 0x33uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA)))    = [| 0x00uy; 0x38uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA)))    = [| 0x00uy; 0x39uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_DSS, CS_MtE (AES_128_CBC, SHA256))) = [| 0x00uy; 0x40uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_RSA, CS_MtE (AES_128_CBC, SHA256))) = [| 0x00uy; 0x67uy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_DSS, CS_MtE (AES_256_CBC, SHA256))) = [| 0x00uy; 0x6Auy |]
    /\ CipherSuiteBytes(CipherSuite (DHE_RSA, CS_MtE (AES_256_CBC, SHA256))) = [| 0x00uy; 0x6Buy |]

/\ CipherSuiteBytes(CipherSuite (DH_anon, CS_MtE (RC4_128, MD5)))        = [| 0x00uy; 0x18uy |]
    /\ CipherSuiteBytes(CipherSuite (DH_anon, CS_MtE (TDES_EDE_CBC, SHA)))   = [| 0x00uy; 0x1Buy |]
    /\ CipherSuiteBytes(CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA)))    = [| 0x00uy; 0x34uy |]
    /\ CipherSuiteBytes(CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA)))    = [| 0x00uy; 0x3Auy |]
    /\ CipherSuiteBytes(CipherSuite (DH_anon, CS_MtE (AES_128_CBC, SHA256))) = [| 0x00uy; 0x6Cuy |]
    /\ CipherSuiteBytes(CipherSuite (DH_anon, CS_MtE (AES_256_CBC, SHA256))) = [| 0x00uy; 0x6Duy |]

/\ CipherSuiteBytes(SCSV (TLS_EMPTY_RENEGOTIATION_INFO_SCSV))         = [| 0x00uy; 0xFFuy |]

function val CipherSuitesBytes: cipherSuites -> bytes
private definition !cs,b. (b = CipherSuitesBytes(cs)) <=>
   ((cs = [] /\ b = [||]) \/
    (?h,t. cs = h::t /\ b = CipherSuiteBytes(h) @| CipherSuitesBytes(t)))

predicate ContainsCipherSuite of cipherSuites * cipherSuite
private definition !b,cs. ContainsCipherSuite(b,cs) <=>
                (?h,t. b = h::t /\ (h = cs \/ ContainsCipherSuite(t,cs)))

predicate ContainsCipherSuites of cipherSuites * cipherSuites
private definition !b,l. ContainsCipherSuites(b,l) <=>
  (l = [] \/
   (?h,t. l = h::t /\ ContainsCipherSuite(b,h) /\ ContainsCipherSuites(b,t)))

private val consCipherSuites: cs:cipherSuite -> css:cipherSuites -> css':cipherSuites{css' = cs::css}

val cipherSuiteBytes: c:cipherSuite -> b:bytes{Length(b)=2 /\ b = CipherSuiteBytes(c)}
val parseCipherSuite: b:bytes{Length(b)=2} -> (c:cipherSuite{b = CipherSuiteBytes(c)}) Result

// this parsing function may fail if b has the wrong length,
// or if we were strict on unknown ciphersuites
val parseCipherSuites: b:bytes -> (css:cipherSuites {?csl. b = CipherSuitesBytes(csl) /\ ContainsCipherSuites(csl,css)}) Result
val cipherSuitesBytes: css:cipherSuites -> b:bytes {b = CipherSuitesBytes(css)}

val mkIntTriple: (nat * nat * nat) -> (nat * nat * nat)
val getKeyExtensionLength: ProtocolVersion -> cipherSuite -> nat

type cipherSuiteName =
    | TLS_NULL_WITH_NULL_NULL

val cipherSuites_of_nameList: cipherSuiteName list -> cipherSuites
val name_of_cipherSuite: cipherSuite -> cipherSuiteName Result

type preContentType =
  | Change_cipher_spec
  | Alert
  | Handshake
  | Application_data

type ContentType = ct:preContentType
  {ct = Change_cipher_spec \/ ct = Alert \/
   ct = Handshake \/ ct = Application_data}

val bytes_of_seq: sn:nat -> b:bytes{Length(b) = 8 /\ b = IntBytes(8,sn)}
val seq_of_bytes: b:bytes{Length(b)=8} -> sn:nat{b = IntBytes(8,sn)}

function val CTBytes: ContentType -> bytes

assume !c. Length(CTBytes(c)) = 1

private definition CTBytes(Change_cipher_spec) = [|20uy|]
private definition CTBytes(Alert)              = [|21uy|]
private definition CTBytes(Handshake)          = [|22uy|]
private definition CTBytes(Application_data)   = [|23uy|]

val ctBytes: ct:ContentType -> b:bytes{b=CTBytes(ct)}
val parseCT: b:bytes {Length(b)=1} -> (ct:ContentType{b=CTBytes(ct)}) Result
val CTtoString: ContentType -> string

// binary format for length-prefixed bytes;
// the integer is the length of the prefix (1,2, 3 or 4 for TLS)

function val VLBytes: (nat * bytes) -> bytes
private definition !i,b. VLBytes(i,b) = IntBytes(i,Length(b)) @| b
val vlbytes: l:nat -> b:bytes -> r:bytes {r=VLBytes(l,b)}
val vlsplit:
  l:nat{l<=8} -> b:bytes{Length(b)>=l} ->
  ( b1:bytes * b2:bytes {b = VLBytes(l,b1) @| b2}) Result

val vlparse:
  l:nat{l<=8} -> b:bytes{Length(b)>=l} ->
  ( r:bytes { b = VLBytes(l,r) }) Result

// nice to have, not used so far.
ask !i,b. Length(VLBytes(i,b)) = i + Length(b)

// relies on associativity
ask !i,b1,b2,c1,c2.
  (VLBytes(i,b1) @| b2 = VLBytes(i,c1) @| c2) => (b1 = c1 /\ b2 = c2)

// cert-type parsing / formatting
type certType =
    | RSA_sign
    | DSA_sign
    | RSA_fixed_dh
    | DSA_fixed_dh

function val CertTypeBytes: certType -> bytes
private definition CertTypeBytes(RSA_sign)     = [|1uy|]
private definition CertTypeBytes(DSA_sign)     = [|2uy|]
private definition CertTypeBytes(RSA_fixed_dh) = [|3uy|]
private definition CertTypeBytes(DSA_fixed_dh) = [|4uy|]

val certTypeBytes: ct:certType -> b:bytes{b=CertTypeBytes(ct)}
val parseCertType: b:bytes -> (ct:certType {b=CertTypeBytes(ct)}) Result

function val CertTypesBytes: certType list -> bytes
private definition !h,t.
	CertTypesBytes([]) = [||] /\
	CertTypesBytes(h::t) = CertTypeBytes(h) @| CertTypesBytes(t)

val certificateTypeListBytes: ctl:certType list ->
	b:bytes{b=CertTypesBytes(ctl)}
val parseCertificateTypeList: b:bytes ->
	(ctl:certType list{b = CertTypesBytes(ctl)}) Result

function val DefaultCertTypes: bool * cipherSuite -> certType list
val defaultCertTypes: sign:bool -> cs:cipherSuite -> ctl:certType list{ctl=DefaultCertTypes(sign,cs)}

function val DistinguishedNameListBytes: string list -> bytes
private definition !h,t.
	DistinguishedNameListBytes([]) = [||] /\
	DistinguishedNameListBytes(h::t) = VLBytes(2,Utf8(h)) @| DistinguishedNameListBytes(t)
function val DistinguishedNamesBytes: string list -> bytes
private definition !l.
	DistinguishedNamesBytes(l) = VLBytes(2,DistinguishedNameListBytes(l))

val distinguishedNameListBytes: n:string list -> b:bytes{b=DistinguishedNamesBytes(n)}
val parseDistinguishedNameList: b:bytes -> s:string list ->
	(res:string list{
		(* ?l. res = l @ s /\ b = DistinguishedNameListBytes(l) *)
		s = [] => b = DistinguishedNameListBytes(res)
	}) Result

miTLS

A verified reference TLS implementation

miTLS :: TLSConstants

F# Interface: TLSConstants.fsi

F# Implementation: TLSConstants.fs

F7 Interface: TLSConstants.fs7

Verification status

Module list

Trusted

Idealized

Verified