miTLS :: Handshake

F# Interface: Handshake.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
 *)

(* Handshake protocol *)
module Handshake

open Error
open TLSInfo
open TLSConstants
open Range

// protocol state
type hs_state
type nextState = hs_state

(* Control Interface *)
// Create instance for a fresh connection (without resumption)
val init: Role -> config -> (ConnectionInfo * hs_state)

// Create instance for a fresh connection (Client-only, resuming some other sessions)
val resume: sessionID -> config -> (ConnectionInfo * hs_state)

// Idle client starts a full handshake on the current connection
val rehandshake: ConnectionInfo -> hs_state -> config -> bool * hs_state

// Idle client starts an abbreviated handshake resuming the current session
val rekey:       ConnectionInfo -> hs_state -> config -> bool * hs_state

// (Idle) Server requests an handshake
val request:  ConnectionInfo -> hs_state -> config -> bool * hs_state

val invalidateSession: ConnectionInfo -> hs_state -> hs_state

(* Network Interface *)

[<NoEquality;NoComparison>]
type outgoing =
  | OutIdle of hs_state
  | OutSome of range * HSFragment.fragment * hs_state
  | OutCCS of  range * HSFragment.fragment (* the unique one-byte CCS *) *
               ConnectionInfo * StatefulLHAE.state * hs_state
  | OutFinished of range * HSFragment.fragment * hs_state
  | OutComplete of range * HSFragment.fragment * hs_state
val next_fragment: ConnectionInfo  -> hs_state -> outgoing

(* Receiving Handshake and CCS fragments *)

[<NoEquality;NoComparison>]
type incoming = (* the fragment is accepted, and... *)
  | InAck of hs_state
  | InVersionAgreed of hs_state * ProtocolVersion
  | InQuery of Cert.chain * bool * hs_state
  | InFinished of hs_state
  | InComplete of hs_state
  | InError of alertDescription * string * hs_state
val recv_fragment: ConnectionInfo -> hs_state -> range -> HSFragment.fragment -> incoming
val authorize: ConnectionInfo -> hs_state -> Cert.chain -> incoming

[<NoEquality;NoComparison>]
type incomingCCS =
  | InCCSAck of ConnectionInfo * StatefulLHAE.state * hs_state
  | InCCSError of alertDescription * string * hs_state
val recv_ccs     : ConnectionInfo -> hs_state -> range -> HSFragment.fragment -> incomingCCS

val getMinVersion: ConnectionInfo -> hs_state -> ProtocolVersion

F# Implementation: Handshake.fs

(* Handshake protocol *)
module Handshake

open Bytes
open Error
open TLSConstants
open TLSExtensions
open TLSInfo
open Range

// BEGIN HS_msg

// This section is from the legacy HS_msg module, now merged with Handshake.
// Still, there are some redundancies that should be eliminated,
// by semantically merge the two.

(*** Following RFC5246 A.4 *)

let htBytes t =
    match t with
    | HT_hello_request       -> [|  0uy |]
    | HT_client_hello        -> [|  1uy |]
    | HT_server_hello        -> [|  2uy |]
    | HT_certificate         -> [| 11uy |]
    | HT_server_key_exchange -> [| 12uy |]
    | HT_certificate_request -> [| 13uy |]
    | HT_server_hello_done   -> [| 14uy |]
    | HT_certificate_verify  -> [| 15uy |]
    | HT_client_key_exchange -> [| 16uy |]
    | HT_finished            -> [| 20uy |]

let parseHt (b:bytes) =
    match b with
    | [|  0uy |] -> correct(HT_hello_request      )
    | [|  1uy |] -> correct(HT_client_hello       )
    | [|  2uy |] -> correct(HT_server_hello       )
    | [| 11uy |] -> correct(HT_certificate        )
    | [| 12uy |] -> correct(HT_server_key_exchange)
    | [| 13uy |] -> correct(HT_certificate_request)
    | [| 14uy |] -> correct(HT_server_hello_done  )
    | [| 15uy |] -> correct(HT_certificate_verify )
    | [| 16uy |] -> correct(HT_client_key_exchange)
    | [| 20uy |] -> correct(HT_finished           )
    | _   -> let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_decode_error, reason)

/// Handshake message format

let messageBytes ht data =
    let htb = htBytes ht in
    let vldata = vlbytes 3 data in
    htb @| vldata

let parseMessage buf =
    (* Somewhat inefficient implementation:
       we repeatedly parse the first 4 bytes of the incoming buffer until we have a complete message;
       we then remove that message from the incoming buffer. *)
    if length buf < 4 then Correct(None) (* not enough data to start parsing *)
    else
        let (hstypeb,rem) = Bytes.split buf 1 in
        match parseHt hstypeb with
        | Error(x,y) -> Error(x,y)
        | Correct(hstype) ->
            match vlsplit 3 rem with
            | Error(x,y) -> Correct(None) // not enough payload, try next time
            | Correct(res) ->
                let (payload,rem) = res in
                let to_log = messageBytes hstype payload in
                let res = (rem,hstype,payload,to_log) in
                let res = Some(res) in
                correct(res)

// We implement locally fragmentation, not hiding any length
let makeFragment ki b =
    let (b0,rem) = if length b < fragmentLength then (b,[||])
                   else Bytes.split b fragmentLength
    let r0 = (length b0, length b0) in
    let f = HSFragment.fragmentPlain ki r0 b0 in
    (r0,f,rem)

// we could use something more general for parsing lists, e.g.
// let rec parseList parseOne b =
//     if length b = 0 then correct([])
//     else
//     match parseOne b with
//     | Correct(x,b) ->
//         match parseList parseOne b with
//         | Correct(xs) -> correct(x::xs)
//         | Error(x,y)  -> Error(x,y)
//     | Error(x,y)      -> Error(x,y)

(** A.4.1 Hello Messages *)

let parseClientHello data =
    if length data >= 34 then
        let (clVerBytes,cr,data) = split2 data 2 32 in
        match parseVersion clVerBytes with
        | Error(x,y) -> Error(x,y)
        | Correct(cv) ->
        if length data >= 1 then
            match vlsplit 1 data with
            | Error(x,y) -> Error(x,y)
            | Correct (res) ->
            let (sid,data) = res in
            if length sid <= 32 then
                if length data >= 2 then
                    match vlsplit 2 data with
                    | Error(x,y) -> Error(x,y)
                    | Correct (res) ->
                    let (clCiphsuitesBytes,data) = res in
                    match parseCipherSuites clCiphsuitesBytes with
                    | Error(x,y) -> Error(x,y)
                    | Correct (clientCipherSuites) ->
                    if length data >= 1 then
                        match vlsplit 1 data with
                        | Error(x,y) -> Error(x,y)
                        | Correct (res) ->
                        let (cmBytes,extensions) = res in
                        let cm = parseCompressions cmBytes
                        correct(cv,cr,sid,clientCipherSuites,cm,extensions)
                    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
                else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
            else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
        else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let clientHelloBytes poptions crand session ext =
    let mv = poptions.maxVer in
    let cVerB      = versionBytes mv in
    let random     = crand in
    let csessB     = vlbytes 1 session in
    let cs = poptions.ciphersuites in
    let csb = cipherSuitesBytes cs in
    let ccsuitesB  = vlbytes 2 csb in
    let cm = poptions.compressions in
    let cmb = (compressionMethodsBytes cm) in
    let ccompmethB = vlbytes 1 cmb in
    let data = cVerB @| random @| csessB @| ccsuitesB @| ccompmethB @| ext in
    messageBytes HT_client_hello data

let serverHelloBytes sinfo srand ext =
    let verB = versionBytes sinfo.protocol_version in
    let sidB = vlbytes 1 sinfo.sessionID
    let csB = cipherSuiteBytes sinfo.cipher_suite in
    let cmB = compressionBytes sinfo.compression in
    let data = verB @| srand @| sidB @| csB @| cmB @| ext in
    messageBytes HT_server_hello data

let parseServerHello data =
    if length data >= 34 then
        let (serverVerBytes,serverRandomBytes,data) = split2 data 2 32
        match parseVersion serverVerBytes with
        | Error(x,y) -> Error(x,y)
        | Correct(serverVer) ->
        if length data >= 1 then
            match vlsplit 1 data with
            | Error(x,y) -> Error (x,y)
            | Correct (res) ->
            let (sid,data) = res in
            if length sid <= 32 then
                if length data >= 3 then
                    let (csBytes,cmBytes,data) = split2 data 2 1
                    match parseCipherSuite csBytes with
                    | Error(x,y) -> Error(x,y)
                    | Correct(cs) ->
                    match parseCompression cmBytes with
                    | Error(x,y) -> Error(x,y)
                    | Correct(cm) ->
                    correct(serverVer,serverRandomBytes,sid,cs,cm,data)
                else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
            else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
        else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let helloRequestBytes = messageBytes HT_hello_request [||]

let CCSBytes = [| 1uy |]

(** A.4.2 Server Authentication and Key Exchange Messages *)

let serverHelloDoneBytes = messageBytes HT_server_hello_done [||]

let serverCertificateBytes cl = messageBytes HT_certificate (Cert.certificateListBytes cl)

let clientCertificateBytes (cs:(Cert.chain * Sig.alg * Sig.skey) option) =

match cs with
    | None -> messageBytes HT_certificate (Cert.certificateListBytes [])
    | Some(v) ->
        let (certList,_,_) = v in
        messageBytes HT_certificate (Cert.certificateListBytes certList)

let parseClientOrServerCertificate data =
    if length data >= 3 then
        match vlparse 3 data with
        | Error(x,y) -> Error(AD_bad_certificate_fatal, perror __SOURCE_FILE__ __LINE__ y)
        | Correct (certList) -> Cert.parseCertificateList certList []
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let sigHashAlgBytesVersion version cs =
     match version with
        | TLS_1p2 ->
            let defaults = default_sigHashAlg version cs in
            let res = sigHashAlgListBytes defaults in
            vlbytes 2 res
        | TLS_1p1 | TLS_1p0 | SSL_3p0 -> [||]

let parseSigHashAlgVersion version data =
    match version with
    | TLS_1p2 ->
        if length data >= 2 then
            match vlsplit 2 data with
            | Error(x,y) -> Error(x,y)
            | Correct (res) ->
            let (sigAlgsBytes,data) = res in
            match parseSigHashAlgList sigAlgsBytes with
            | Error(x,y) -> Error(x,y)
            | Correct (sigAlgsList) -> correct (sigAlgsList,data)
        else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    | TLS_1p1 | TLS_1p0 | SSL_3p0 ->
        correct ([],data)

let certificateRequestBytes sign cs version =
    let certTypes = defaultCertTypes sign cs in
    let ctb = certificateTypeListBytes certTypes in
    let ctb = vlbytes 1 ctb in
    let sigAndAlg = sigHashAlgBytesVersion version cs in
    (* We specify no cert auth *)
    let distNames = distinguishedNameListBytes [] in
    let distNames = vlbytes 2 distNames in
    let data = ctb
            @| sigAndAlg
            @| distNames in
    messageBytes HT_certificate_request data

let parseCertificateRequest version data: (certType list * Sig.alg list * string list) Result =
    if length data >= 1 then
        match vlsplit 1 data with
        | Error(x,y) -> Error(x,y)
        | Correct (res) ->
        let (certTypeListBytes,data) = res in
        match parseCertificateTypeList certTypeListBytes with
        | Error(x,y) -> Error(x,y)
        | Correct(certTypeList) ->
        match parseSigHashAlgVersion version data with
        | Error(x,y) -> Error(x,y)
        | Correct (res) ->
        let (sigAlgs,data) = res in
        if length data >= 2 then
            match vlparse 2 data with
            | Error(x,y) -> Error(x,y)
            | Correct  (distNamesBytes) ->
            let el = [] in
            match parseDistinguishedNameList distNamesBytes el with
            | Error(x,y) -> Error(x,y)
            | Correct (distNamesList) ->
            correct (certTypeList,sigAlgs,distNamesList)

else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

(** A.4.3 Client Authentication and Key Exchange Messages *)

let encpmsBytesVersion version encpms =
    match version with
    | SSL_3p0 -> encpms
    | TLS_1p0 | TLS_1p1 | TLS_1p2 -> vlbytes 2 encpms

let parseEncpmsVersion version data =
    match version with
    | SSL_3p0 -> correct (data)
    | TLS_1p0 | TLS_1p1| TLS_1p2 ->
        if length data >= 2 then
            match vlparse 2 data with
            | Correct (encPMS) -> correct(encPMS)
            | Error(x,y) -> Error(x,y)
        else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let clientKEXBytes_RSA si config =
    if listLength si.serverID = 0 then
        unexpectedError "[clientKEXBytes_RSA] Server certificate should always be present with a RSA signing cipher suite."
    else
        match Cert.get_chain_public_encryption_key si.serverID with
        | Error(x,y) -> Error(x,y)
        | Correct(pubKey) ->
            let pms = CRE.genRSA pubKey config.maxVer in
            let encpms = RSA.encrypt pubKey config.maxVer pms in
            let nencpms = encpmsBytesVersion si.protocol_version encpms in
            let mex = messageBytes HT_client_key_exchange nencpms in
            let pmsdata = RSAPMS(pubKey,config.maxVer,encpms) in
            correct(mex,pmsdata,pms)

let parseClientKEX_RSA si skey cv config data =
    if listLength si.serverID = 0 then
        unexpectedError "[parseClientKEX_RSA] when the ciphersuite can encrypt the PMS, the server certificate should always be set"
    else
        match parseEncpmsVersion si.protocol_version data with
        | Correct(encPMS) ->
            let res = RSA.decrypt skey si cv config.check_client_version_in_pms_for_old_tls encPMS in
            let (Correct(pk)) = Cert.get_chain_public_encryption_key si.serverID in
            correct(RSAPMS(pk,cv,encPMS),res)
        | Error(x,y) -> Error(x,y)

let clientKEXExplicitBytes_DH y =
    let yb = vlbytes 2 y in
    messageBytes HT_client_key_exchange yb

let parseClientKEXExplicit_DH p data =
    if length data >= 2 then
        match vlparse 2 data with
        | Error(x,y) -> Error(x,y)
        | Correct(y) ->
            match DHGroup.checkElement p y with
            | None -> Error(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Invalid DH key received")
            | Some(y) -> correct y
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

// Unused until we don't support DH ciphersuites.
let clientKEXImplicitBytes_DH = messageBytes HT_client_key_exchange [||]
// Unused until we don't support DH ciphersuites.
let parseClientKEXImplicit_DH data =
    if length data = 0 then
        correct ( () )
    else
        Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

(* Digitally signed struct *)

let parseDigitallySigned expectedAlgs payload pv =
    match pv with
    | TLS_1p2 ->
        if length payload >= 2 then
            let (recvAlgsB,sign) = Bytes.split payload 2 in
            match parseSigHashAlg recvAlgsB with
            | Error(x,y) -> Error(x,y)
            | Correct(recvAlgs) ->
                if sigHashAlg_contains expectedAlgs recvAlgs then
                    if length sign >= 2 then
                        match vlparse 2 sign with
                        | Error(x,y) -> Error(x,y)
                        | Correct(sign) -> correct(recvAlgs,sign)
                    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
                else Error(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "")
        else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    | SSL_3p0 | TLS_1p0 | TLS_1p1 ->
        if listLength expectedAlgs = 1 then
            if length payload >= 2 then
                match vlparse 2 payload with
                | Error(x,y) -> Error(x,y)
                | Correct(sign) ->
                correct(listHead expectedAlgs,sign)
            else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
        else unexpectedError "[parseDigitallySigned] invoked with invalid SignatureAndHash algorithms"

(* Server Key exchange *)

let dheParamBytes p g y = (vlbytes 2 p) @| (vlbytes 2 g) @| (vlbytes 2 y)
let parseDHEParams payload =
    if length payload >= 2 then
        match vlsplit 2 payload with
        | Error(x,y) -> Error(x,y)
        | Correct(res) ->
        let (p,payload) = res in
        if length payload >= 2 then
            match vlsplit 2 payload with
            | Error(x,y) -> Error(x,y)
            | Correct(res) ->
            let (g,payload) = res in
            if length payload >= 2 then
                match vlsplit 2 payload with
                | Error(x,y) -> Error(x,y)
                | Correct(res) ->
                let (y,payload) = res in
                // Check g and y are valid elements
                match DHGroup.checkElement p g with
                | None -> Error(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Invalid DH parameter received")
                | Some(g) ->
                    match DHGroup.checkElement p y with
                    | None -> Error(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Invalid DH parameter received")
                    | Some(y) -> correct(p,g,y,payload)
            else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
        else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
    else Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

let serverKeyExchangeBytes_DHE dheb alg sign pv =
    let sign = digitallySignedBytes alg sign pv in
    let payload = dheb @| sign in
    messageBytes HT_server_key_exchange payload

let parseServerKeyExchange_DHE pv cs payload =
    match parseDHEParams payload with
    | Error(x,y) -> Error(x,y)
    | Correct(res) ->
        let (p,g,y,payload) = res
        let allowedAlgs = default_sigHashAlg pv cs in
        match parseDigitallySigned allowedAlgs payload pv with
        | Error(x,y) -> Error(x,y)
        | Correct(res) ->
            let (alg,signature) = res
            correct(p,g,y,alg,signature)

let serverKeyExchangeBytes_DH_anon p g y =
    let dehb = dheParamBytes p g y in
    messageBytes HT_server_key_exchange dehb

let parseServerKeyExchange_DH_anon payload =
    match parseDHEParams payload with
    | Error(x,y) -> Error(x,y)
    | Correct(p,g,y,rem) ->
        if equalBytes rem [||] then
            correct(p,g,y)
        else
            Error(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")

(* Certificate Verify *)

let makeCertificateVerifyBytes si (ms:PRF.masterSecret) alg skey data =
    // The returned "tag" variable is ghost, only used to avoid
    // existentials in formal verification.
    match si.protocol_version with
    | TLS_1p2 | TLS_1p1 | TLS_1p0 ->
        let tag = Sig.sign alg skey data in
        let payload = digitallySignedBytes alg tag si.protocol_version in
        let mex = messageBytes HT_certificate_verify payload in
        (mex,tag)
    | SSL_3p0 ->
        let (sigAlg,_) = alg in
        let alg = (sigAlg,NULL) in
        let toSign = PRF.ssl_certificate_verify si ms sigAlg data in
        let tag = Sig.sign alg skey toSign in
        let payload = digitallySignedBytes alg tag si.protocol_version in
        let mex = messageBytes HT_certificate_verify payload in
        (mex,tag)

let certificateVerifyCheck si ms algs log payload =
    // The returned byte array is ghost, only used to avoid
    // existentials in formal verification.
    match parseDigitallySigned algs payload si.protocol_version with
    | Correct(res) ->
        let (alg,signature) = res in
        //let (alg,expected) =
        match si.protocol_version with
        | TLS_1p2 | TLS_1p1 | TLS_1p0 ->
            match Cert.get_chain_public_signing_key si.clientID alg with
            | Error(x,y) -> (false,[||])
            | Correct(vkey) ->
                let res = Sig.verify alg vkey log signature in
                (res,signature)
        | SSL_3p0 ->
            let (sigAlg,_) = alg in
            let alg = (sigAlg,NULL) in
            let expected = PRF.ssl_certificate_verify si ms sigAlg log in
            match Cert.get_chain_public_signing_key si.clientID alg with
            | Error(x,y) -> (false,[||])
            | Correct(vkey) ->
                let res = Sig.verify alg vkey expected signature in
                (res,signature)
    | Error(x,y) -> (false,[||])

// State machine begins

type events =
    Authorize of Role * SessionInfo
  | Configure of Role * epoch * config
  | EvSentFinishedFirst of ConnectionInfo * bool
  | SentCCS of Role * epoch
  | Negotiated of Role * SessionInfo * config * config

(* verify data authenticated by the Finished messages *)
type log = bytes         (* message payloads so far, to be eventually authenticated *)
type cVerifyData = bytes (* ClientFinished payload *)
type sVerifyData = bytes (* ServerFinished payload *)

// The constructor indicates either what we are doing locally or which peer message we are expecting,

type serverState =  (* note that the CertRequest bits are determined by the config *)
                    (* we may omit some ProtocolVersion, mostly a ghost variable *)
   | ClientHello                  of cVerifyData * sVerifyData

| ClientCertificateRSA         of SessionInfo * ProtocolVersion * RSAKey.sk * log
   | ServerCheckingCertificateRSA of SessionInfo * ProtocolVersion * RSAKey.sk * log * Cert.chain * bytes
   | ClientKeyExchangeRSA         of SessionInfo * ProtocolVersion * RSAKey.sk * log

| ClientCertificateDH          of SessionInfo * log
   | ServerCheckingCertificateDH  of SessionInfo * log * bytes
   | ClientKeyExchangeDH          of SessionInfo * log

| ClientCertificateDHE         of SessionInfo * DHGroup.p * DHGroup.g * DHGroup.elt * DH.secret * log
   | ServerCheckingCertificateDHE of SessionInfo * DHGroup.p * DHGroup.g * DHGroup.elt * DH.secret * log * Cert.chain * bytes
   | ClientKeyExchangeDHE         of SessionInfo * DHGroup.p * DHGroup.g * DHGroup.elt * DH.secret * log

| ClientKeyExchangeDH_anon     of SessionInfo * DHGroup.p * DHGroup.g * DHGroup.elt * DH.secret * log

| CertificateVerify            of SessionInfo * PRF.masterSecret * log
   | ClientCCS                    of SessionInfo * PRF.masterSecret * log
   | ClientFinished               of SessionInfo * PRF.masterSecret * epoch * StatefulLHAE.writer * log
   (* by convention, the parameters are named si, cv, cr', sr', ms, log *)
   | ServerWritingCCS             of SessionInfo * PRF.masterSecret * epoch * StatefulLHAE.writer * cVerifyData * log
   | ServerWritingFinished        of SessionInfo * PRF.masterSecret * epoch * cVerifyData * sVerifyData

| ServerWritingCCSResume       of epoch * StatefulLHAE.writer * epoch * StatefulLHAE.reader * PRF.masterSecret * log
   | ClientCCSResume              of epoch * StatefulLHAE.reader * sVerifyData * PRF.masterSecret * log
   | ClientFinishedResume         of SessionInfo * PRF.masterSecret * epoch * sVerifyData * log

| ServerIdle                   of cVerifyData * sVerifyData
   (* the ProtocolVersion is the highest TLS version proposed by the client *)

type clientState =
   | ServerHello                  of crand * sessionID (* * bytes for extensions? *) * cVerifyData * sVerifyData * log

| ServerCertificateRSA         of SessionInfo * log
   | ClientCheckingCertificateRSA of SessionInfo * log * Cert.cert list * ProtocolVersion option * bytes
   | CertificateRequestRSA        of SessionInfo * log (* In fact, CertReq or SHelloDone will be accepted *)
   | ServerHelloDoneRSA           of SessionInfo * Cert.sign_cert * log

| ServerCertificateDH          of SessionInfo * log
   | ClientCheckingCertificateDH  of SessionInfo * log * ProtocolVersion option * bytes
   | CertificateRequestDH         of SessionInfo * log (* We pick our cert and store it in sessionInfo as soon as the server requests it.
                                                         We put None if we don't have such a certificate, and we know whether to send
                                                         the Certificate message or not based on the state when we receive the Finished message *)
   | ServerHelloDoneDH            of SessionInfo * log

| ServerCertificateDHE         of SessionInfo * log
   | ClientCheckingCertificateDHE of SessionInfo * log * ProtocolVersion option * bytes
   | ServerKeyExchangeDHE         of SessionInfo * log
   | CertificateRequestDHE        of SessionInfo * DHGroup.p * DHGroup.g * DHGroup.elt * log
   | ServerHelloDoneDHE           of SessionInfo * Cert.sign_cert * DHGroup.p * DHGroup.g * DHGroup.elt * log

| ServerKeyExchangeDH_anon of SessionInfo * log (* Not supported yet *)
   | ServerHelloDoneDH_anon of SessionInfo * DHGroup.p * DHGroup.g * DHGroup.elt * log

| ClientWritingCCS       of SessionInfo * PRF.masterSecret * log
   | ServerCCS              of SessionInfo * PRF.masterSecret * epoch * StatefulLHAE.reader * cVerifyData * log
   | ServerFinished         of SessionInfo * PRF.masterSecret * epoch * cVerifyData * log

| ServerCCSResume        of epoch * StatefulLHAE.writer * epoch * StatefulLHAE.reader * PRF.masterSecret * log
   | ServerFinishedResume   of epoch * StatefulLHAE.writer * PRF.masterSecret * log
   | ClientWritingCCSResume of epoch * StatefulLHAE.writer * PRF.masterSecret * sVerifyData * log
   | ClientWritingFinishedResume of cVerifyData * sVerifyData

| ClientIdle             of cVerifyData * sVerifyData

type protoState = // Cannot use Client and Server, otherwise clashes with Role
  | PSClient of clientState
  | PSServer of serverState

let clientState (ci:ConnectionInfo) (p:clientState) = PSClient(p)
let serverState (ci:ConnectionInfo) (p:serverState) = PSServer(p)

type hs_state = {
  (* I/O buffers *)
  hs_outgoing    : bytes;                  (* outgoing data *)
  hs_incoming    : bytes;                  (* partial incoming HS message *)
  (* local configuration *)
  poptions: config;
  sDB: SessionDB.SessionDB;
  (* current handshake & session we are establishing *)
  pstate: protoState;
}

type nextState = hs_state

/// Initiating Handshakes, mostly on the client side.

let init (role:Role) poptions =
    (* Start a new session without resumption, as the first epoch on this connection. *)
    let sid = [||] in
    let rand = Nonce.mkHelloRandom() in
    match role with
    | Client ->
        let ci = initConnection role rand in
        Pi.assume (Configure(Client,ci.id_in,poptions));
        let ext = extensionsBytes poptions.safe_renegotiation [||] in
        let cHelloBytes = clientHelloBytes poptions rand sid ext in
        let sdb = SessionDB.create poptions in
        (ci,{hs_outgoing = cHelloBytes;
                     hs_incoming = [||];
                     poptions = poptions;
                     sDB = sdb;
                     pstate = PSClient (ServerHello (rand, sid, [||], [||], cHelloBytes))
            })
    | Server ->
        let ci = initConnection role rand in
        Pi.assume (Configure(Client,ci.id_in,poptions));
        let sdb = SessionDB.create poptions in
        (ci,{hs_outgoing = [||]
             hs_incoming = [||]
             poptions = poptions
             sDB = sdb
             pstate = PSServer (ClientHello([||],[||]))
            })

let resume next_sid poptions =
    (* Resume a session, as the first epoch on this connection.
       Set up our state as a client. Servers cannot resume *)

(* Search a client sid in the DB *)
    let sDB = SessionDB.create poptions in
    match SessionDB.select sDB (next_sid,Client,poptions.server_name) with
    | None -> init Client poptions
    | Some (retrieved) ->
    let (retrievedSinfo,retrievedMS) = retrieved in
    match retrievedSinfo.sessionID with
    | [||] -> unexpectedError "[resume] a resumed session should always have a valid sessionID"
    | sid ->
    let rand = Nonce.mkHelloRandom () in
    let ci = initConnection Client rand in
    Pi.assume (Configure(Server,ci.id_in,poptions));
    let ext = extensionsBytes poptions.safe_renegotiation [||]
    let cHelloBytes = clientHelloBytes poptions rand sid ext in
    let sdb = SessionDB.create poptions
    (ci,{hs_outgoing = cHelloBytes
         hs_incoming = [||]
         poptions = poptions
         sDB = sdb
         pstate = PSClient (ServerHello (rand, sid, [||], [||], cHelloBytes))
        })

let rehandshake (ci:ConnectionInfo) (state:hs_state) (ops:config) =
    (* Start a non-resuming handshake, over an existing epoch.
       Only client side, since a server can only issue a HelloRequest *)
    match state.pstate with
    | PSClient (cstate) ->
        match cstate with
        | ClientIdle(cvd,svd) ->
            let rand = Nonce.mkHelloRandom () in
            let sid = [||] in
            let ext = extensionsBytes ops.safe_renegotiation cvd in
            let cHelloBytes = clientHelloBytes ops rand sid ext in
            Pi.assume (Configure(Client,ci.id_in,ops));
            let sdb = SessionDB.create ops
            (true,{hs_outgoing = cHelloBytes
                   hs_incoming = [||]
                   poptions = ops
                   sDB = sdb
                   pstate = PSClient (ServerHello (rand, sid, cvd,svd, cHelloBytes))
                   })
        | _ -> (* handshake already happening, ignore this request *)
            (false,state)
    | PSServer (_) -> unexpectedError "[rehandshake] should only be invoked on client side connections."

let rekey (ci:ConnectionInfo) (state:hs_state) (ops:config) =
    if isInitEpoch(ci.id_out) then
        unexpectedError "[rekey] should only be invoked on established connections."
    else
    (* Start a (possibly) resuming handshake over an existing epoch *)
    let si = epochSI(ci.id_out) in // or equivalently ci.id_in
    let sidOp = si.sessionID in
    match sidOp with
    | [||] -> (* Non resumable session, let's do a full handshake *)
        rehandshake ci state ops
    | sid ->
        let sDB = SessionDB.create ops in
        (* Ensure the sid is in the SessionDB *)
        match SessionDB.select sDB (sid,Client,ops.server_name) with
        | None -> (* Maybe session expired, or was never stored. Let's not resume *)
            rehandshake ci state ops
        | Some s ->
            let (retrievedSinfo,retrievedMS) = s
            match state.pstate with
            | PSClient (cstate) ->
                match cstate with
                | ClientIdle(cvd,svd) ->
                    let rand = Nonce.mkHelloRandom () in
                    let ext = extensionsBytes ops.safe_renegotiation cvd in
                    Pi.assume (Configure(Client,ci.id_in,ops));
                    let cHelloBytes = clientHelloBytes ops rand sid ext in
                    (true,{hs_outgoing = cHelloBytes
                           hs_incoming = [||]
                           poptions = ops
                           sDB = sDB
                           pstate = PSClient (ServerHello (rand, sid, cvd, svd, cHelloBytes))
                           })
                | _ -> (* Handshake already ongoing, ignore this request *)
                    (false,state)
            | PSServer (_) -> unexpectedError "[rekey] should only be invoked on client side connections."

let request (ci:ConnectionInfo) (state:hs_state) (ops:config) =
    match state.pstate with
    | PSClient _ -> unexpectedError "[request] should only be invoked on server side connections."
    | PSServer (sstate) ->
        match sstate with
        | ServerIdle(cvd,svd) ->
            let sdb = SessionDB.create ops
            (* Put HelloRequest in outgoing buffer (and do not log it), and move to the ClientHello state (so that we don't send HelloRequest again) *)
            (true, { hs_outgoing = helloRequestBytes
                     hs_incoming = [||]
                     poptions = ops
                     sDB = sdb
                     pstate = PSServer(ClientHello(cvd,svd))
                    })
        | _ -> (* Handshake already ongoing, ignore this request *)
            (false,state)

let getPrincipal ci state =
  match ci.role with
    | Client -> state.poptions.server_name
    | Server -> state.poptions.client_name

let invalidateSession ci state =
    if isInitEpoch(ci.id_in) then
        state
    else
        let si = epochSI(ci.id_in)
        match si.sessionID with
        | [||] -> state
        | sid ->
            let hint = getPrincipal ci state
            let sdb = SessionDB.remove state.sDB (sid,ci.role,hint) in
            {state with sDB=sdb}

let getNextEpochs ci si crand srand =
    let id_in  = nextEpoch ci.id_in  crand srand si in
    let id_out = nextEpoch ci.id_out crand srand si in
    {ci with id_in = id_in; id_out = id_out}

type outgoing =
  | OutIdle of nextState
  | OutSome of range * HSFragment.plain * nextState
  | OutCCS of  range * HSFragment.plain (* the unique one-byte CCS *) *
               ConnectionInfo * StatefulLHAE.state * nextState
  | OutFinished of range * HSFragment.plain * nextState
  | OutComplete of range * HSFragment.plain * nextState

let check_negotiation (r:Role) (si:SessionInfo) (c:config) =
  Pi.assume (Negotiated(r,si,c,c))

let next_fragment ci state =
    match state.hs_outgoing with
    | [||] ->
        match state.pstate with
        | PSClient(cstate) ->
            match cstate with
            | ClientWritingCCS (si,ms,log) ->
                let next_ci = getNextEpochs ci si si.init_crand si.init_srand in
                let (writer,reader) = PRF.keyGen next_ci ms in
                Pi.assume (SentCCS(Client,next_ci.id_out));
                let cvd = PRF.makeVerifyData next_ci.id_out Client ms log in
                let cFinished = messageBytes HT_finished cvd in
                let log = log @| cFinished in
                let (rg,f,_) = makeFragment ci.id_out CCSBytes in
                let ci = {ci with id_out = next_ci.id_out} in

OutCCS(rg,f,ci,writer,
                       {state with hs_outgoing = cFinished
                                   pstate = PSClient(ServerCCS(si,ms,next_ci.id_in,reader,cvd,log))})

| ClientWritingCCSResume(e,w,ms,svd,log) ->
                Pi.assume (SentCCS(Client,e));
                let cvd = PRF.makeVerifyData e Client ms log in
                let cFinished = messageBytes HT_finished cvd in
                let (rg,f,_) = makeFragment ci.id_out CCSBytes in
                let ci = {ci with id_out = e} in

OutCCS(rg,f,ci,w,
                       {state with hs_outgoing = cFinished
                                   pstate = PSClient(ClientWritingFinishedResume(cvd,svd))})

| _ -> OutIdle(state)
        | PSServer(sstate) ->
            match sstate with
            | ServerWritingCCS (si,ms,e,w,cvd,log) ->
                Pi.assume (SentCCS(Server,e));
                let svd = PRF.makeVerifyData e Server ms log in
                let sFinished = messageBytes HT_finished svd in
                let (rg,f,_) = makeFragment ci.id_out CCSBytes in
                let ci = {ci with id_out = e} in

OutCCS(rg,f,ci,w,
                       {state with hs_outgoing = sFinished
                                   pstate = PSServer(ServerWritingFinished(si,ms,e,cvd,svd))})

| ServerWritingCCSResume(we,w,re,r,ms,log) ->
                Pi.assume (SentCCS(Server,we));
                let svd = PRF.makeVerifyData we Server ms log in
                let sFinished = messageBytes HT_finished svd in
                let log = log @| sFinished in
                let (rg,f,_) = makeFragment ci.id_out CCSBytes in
                let ci = {ci with id_out = we} in

OutCCS(rg,f,ci,w,
                       {state with hs_outgoing = sFinished
                                   pstate = PSServer(ClientCCSResume(re,r,svd,ms,log))})

| _ -> OutIdle(state)
    | outBuf ->
        let (rg,f,remBuf) = makeFragment ci.id_out outBuf in
        match remBuf with
        | [||] ->
            match state.pstate with
            | PSClient(cstate) ->
                match cstate with
                | ServerCCS (_,_,_,_,_,_) ->
                    OutFinished(rg,f,{state with hs_outgoing = remBuf})
                | ClientWritingFinishedResume(cvd,svd) ->
                    check_negotiation Client (epochSI ci.id_out) state.poptions;
                    OutComplete(rg,f,
                                {state with hs_outgoing = remBuf
                                            pstate = PSClient(ClientIdle(cvd,svd))})

| _ -> OutSome(rg,f,{state with hs_outgoing = remBuf})
            | PSServer(sstate) ->
                match sstate with
                | ServerWritingFinished(si,ms,e,cvd,svd) ->
                    if equalBytes si.sessionID [||] then
                      check_negotiation Server si state.poptions;
                      OutComplete(rg,f,
                                  {state with hs_outgoing = remBuf
                                              pstate = PSServer(ServerIdle(cvd,svd))})

else
                      let sdb = SessionDB.insert state.sDB (si.sessionID,Server,state.poptions.client_name) (si,ms)
                      check_negotiation Server si state.poptions;
                      OutComplete(rg,f,
                                  {state with hs_outgoing = remBuf
                                              pstate = PSServer(ServerIdle(cvd,svd))
                                              sDB = sdb})

| ClientCCSResume(_,_,_,_,_) ->
                    OutFinished(rg,f,{state with hs_outgoing = remBuf})
                | _ -> OutSome(rg,f,{state with hs_outgoing = remBuf})
        | _ -> OutSome(rg,f,{state with hs_outgoing = remBuf})

type incomingCCS =
  | InCCSAck of ConnectionInfo * StatefulLHAE.state * hs_state
  | InCCSError of alertDescription * string * hs_state

/// ClientKeyExchange
let find_client_cert_sign certType certAlg (distName:string list) pv hint =
    match pv with
    | TLS_1p2 ->
        let keyAlg = sigHashAlg_bySigList certAlg (cert_type_list_to_SigAlg certType) in
        Cert.for_signing certAlg hint keyAlg
    | TLS_1p1 | TLS_1p0 | SSL_3p0 ->
        let certAlg = cert_type_list_to_SigHashAlg certType pv
        let keyAlg = sigHashAlg_bySigList certAlg (cert_type_list_to_SigAlg certType) in
        Cert.for_signing certAlg hint keyAlg

let getCertificateBytes (si:SessionInfo) (cert_req:(Cert.chain * Sig.alg * Sig.skey) option) =
  let clientCertBytes = clientCertificateBytes cert_req in
  match cert_req with
    | None when si.client_auth = true -> clientCertBytes,[]
    | Some x when si.client_auth = true ->
        let (certList,_,_) = x in clientCertBytes,certList
    | _ when si.client_auth = false -> [||],[]

let getCertificateVerifyBytes (si:SessionInfo) (ms:PRF.masterSecret) (cert_req:(Cert.chain * Sig.alg * Sig.skey) option) (l:log) =
  match cert_req with
    | None when si.client_auth = true ->
        (* We sent an empty Certificate message, so no certificate verify message at all *)
        [||]
    | Some(x) when si.client_auth = true ->
        let (certList,algs,skey) = x in
          let (mex,_) = makeCertificateVerifyBytes si ms algs skey l in
          mex
    | _ when si.client_auth = false ->
        (* No client certificate ==> no certificateVerify message *)
        [||]

let prepare_client_output_full_RSA (ci:ConnectionInfo) (state:hs_state) (si:SessionInfo) (cert_req:Cert.sign_cert) (log:log) : (hs_state * SessionInfo * PRF.masterSecret * log) Result =
    let clientCertBytes,certList = getCertificateBytes si cert_req in
    let si = {si with clientID = certList}
    let log = log @| clientCertBytes in

match clientKEXBytes_RSA si state.poptions with
    | Error(x,y) -> Error(x,y)
    | Correct(v) ->
    let (clientKEXBytes,pmsdata,pms)  = v in

let si = {si with pmsData = pmsdata} in

let log = log @| clientKEXBytes in
    let pop = state.poptions in
    let ms = CRE.prfSmoothRSA si pop.maxVer pms in

let certificateVerifyBytes = getCertificateVerifyBytes si ms cert_req log in

let log = log @| certificateVerifyBytes in

(* Enqueue current messages in output buffer *)
    let to_send = clientCertBytes @| clientKEXBytes @| certificateVerifyBytes in
    let new_outgoing = state.hs_outgoing @| to_send in
    correct ({state with hs_outgoing = new_outgoing},si,ms,log)

let sessionInfoCertBytesAuth (si:SessionInfo) (cert_req:Cert.sign_cert)=
  if si.client_auth then
    let cb = clientCertificateBytes cert_req in
    match cert_req with
     | None -> (si,cb)
     | Some(x) ->
         let (certList,_,_) = x in
         ({si with clientID = certList},cb)
  else (si,[||])

let certificateVerifyBytesAuth (si:SessionInfo) (ms:PRF.masterSecret) (cert_req:Cert.sign_cert) (log:bytes) =
        if si.client_auth then
            match cert_req with
            | None ->
                (* We sent an empty Certificate message, so no certificate verify message at all *)
                [||]
            | Some(x) ->
                let (certList,algs,skey) = x in
                let (mex,_) = makeCertificateVerifyBytes si ms algs skey log in
                mex
        else
            (* No client certificate ==> no certificateVerify message *)
            [||]

let prepare_client_output_full_DHE (ci:ConnectionInfo) (state:hs_state) (si:SessionInfo) (cert_req:Cert.sign_cert) (p:DHGroup.p) (g:DHGroup.g) (sy:DHGroup.elt) (log:log) : (hs_state * SessionInfo * PRF.masterSecret * log) Result =

(* pre: Honest(verifyKey(si.server_id)) /\ StrongHS(si) -> DHE.PP((p,g)) /\ ServerDHE((p,g),sy,si.init_crand @| si.init_srand) *)
    (* moreover, by definition ServerDHE((p,g),sy,si.init_crand @| si.init_srand) implies ?sx.DHE.Exp((p,g),sx,sy) *)

let (si,clientCertBytes) = sessionInfoCertBytesAuth si cert_req in

let log = log @| clientCertBytes

let (cy,x) = DH.genKey p g in
    (* post: DHE.Exp((p,g),x,cy) *)

let si = {si with pmsData = DHPMS(p,g,cy,sy)} in
    (* si is now constant *)

let clientKEXBytes = clientKEXExplicitBytes_DH cy in
    let log = log @| clientKEXBytes in

let pms = DH.exp p g cy sy x in
    (* the post of this call is !sx,cy. PP((p,g) /\ DHE.Exp((p,g),x,cy)) /\ DHE.Exp((p,g),sx,sy) -> DHE.Secret((p,g),cy,sy) *)
    (* thus we have Honest(verifyKey(si.server_id)) /\ StrongHS(si) -> DHE.Secret((p,g),cy,sy) *)
    let ms = CRE.prfSmoothDHE si p g cy sy pms in
    (* the post of this call is !p,g,gx,gy. StrongHS(si) /\ DHE.Secret((p,g),gx,gy) -> PRFs.Secret(ms) *)
    (* thus we have Honest(verifyKey(si.server_id)) /\ StrongHS(si) -> PRFs.Secret(ms) *)

let certificateVerifyBytes = certificateVerifyBytesAuth si ms cert_req log in

let log = log @| certificateVerifyBytes in

let to_send = clientCertBytes @| clientKEXBytes @| certificateVerifyBytes in
    let new_outgoing = state.hs_outgoing @| to_send in
    correct ({state with hs_outgoing = new_outgoing},si,ms,log)
(* #endif *)

let on_serverHello_full (ci:ConnectionInfo) crand log to_log (shello:ProtocolVersion * srand * sessionID * cipherSuite * Compression * bytes) =
    let log = log @| to_log in
    let (sh_server_version,sh_random,sh_session_id,sh_cipher_suite,sh_compression_method,sh_neg_extensions) = shello
    let si = { clientID = []
               client_auth = false
               serverID = []
               sessionID = sh_session_id
               protocol_version = sh_server_version
               cipher_suite = sh_cipher_suite
               compression = sh_compression_method
               init_crand = crand
               init_srand = sh_random
               pmsData = PMSUnset
               extended_record_padding = false
               } in
    (* If DH_ANON, go into the ServerKeyExchange state, else go to the Certificate state *)
    if isAnonCipherSuite sh_cipher_suite then
        PSClient(ServerKeyExchangeDH_anon(si,log))
    elif isDHCipherSuite sh_cipher_suite then
        PSClient(ServerCertificateDH(si,log))
    elif isDHECipherSuite sh_cipher_suite then
        PSClient(ServerCertificateDHE(si,log))
    elif isRSACipherSuite sh_cipher_suite then
        PSClient(ServerCertificateRSA(si,log))
    else
        unexpectedError "[on_serverHello_full] Unknown ciphersuite"

let parseMessageState (ci:ConnectionInfo) state =
    match parseMessage state.hs_incoming with
    | Error(x,y) -> Error(x,y)
    | Correct(res) ->
        match res with
        | None -> correct(None)
        | Some(x) ->
             let (rem,hstype,payload,to_log) = x in
             let state = { state with hs_incoming = rem } in
             let nx = (state,hstype,payload,to_log) in
             let res = Some(nx) in
             correct(res)

let rec recv_fragment_client (ci:ConnectionInfo) (state:hs_state) (agreedVersion:ProtocolVersion option) =
    match parseMessageState ci state with
    | Error(x,y) -> InError(x,y,state)
    | Correct(res) ->
      match res with
      | None ->
          match agreedVersion with
          | None      -> InAck(state)
          | Some (pv) -> InVersionAgreed(state,pv)
      | Some (res) ->
      let (state,hstype,payload,to_log) = res in
      match state.pstate with
      | PSClient(cState) ->
        match hstype with
        | HT_hello_request ->
            match cState with
            | ClientIdle(_,_) ->
                (* This is a legitimate hello request.
                   Handle it, but according to the spec do not log this message *)
                match state.poptions.honourHelloReq with
                | HRPIgnore -> recv_fragment_client ci state agreedVersion
                | HRPResume -> let (_,state) = rekey ci state state.poptions in InAck(state)       (* Terminating case, we're not idle anymore *)
                | HRPFull   -> let (_,state) = rehandshake ci state state.poptions in InAck(state) (* Terminating case, we're not idle anymore *)
            | _ ->
                (* RFC 7.4.1.1: ignore this message *)
                recv_fragment_client ci state agreedVersion

| HT_server_hello ->
            match cState with
            | ServerHello (crand,sid,cvd,svd,log) ->
                match parseServerHello payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct (shello) ->
                  let (sh_server_version,sh_random,sh_session_id,sh_cipher_suite,sh_compression_method,sh_neg_extensions) = shello
                  let pop = state.poptions
                  // Sanity checks on the received message; they are security relevant.
                  // Check that the server agreed version is between maxVer and minVer.
                  if  (geqPV sh_server_version pop.minVer
                       && geqPV pop.maxVer sh_server_version) = false
                  then

InError(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Protocol version negotiation",state)

else
                  // Check that the negotiated ciphersuite is in the proposed list.
                  // Note: if resuming a session, we still have to check that this ciphersuite is the expected one!
                  if  (Bytes.memr state.poptions.ciphersuites sh_cipher_suite) = false
                  then

InError(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Ciphersuite negotiation",state)

else
                  // Check that the compression method is in the proposed list.
                  if (Bytes.memr state.poptions.compressions sh_compression_method) = false
                  then

InError(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Compression method negotiation",state)

else
                  // Parse extensions
                  match parseExtensions sh_neg_extensions with
                  | Error(x,y) ->

InError(x,y,state)

| Correct(extList) ->
                  // Handling of safe renegotiation //#begin-safe_renego
                  let safe_reneg_result =
                    if state.poptions.safe_renegotiation then
                        let expected = cvd @| svd in
                        inspect_ServerHello_extensions extList expected
                        //#end-safe_renego
                    else
                        // RFC Sec 7.4.1.4: with no safe renegotiation, we never send extensions; if the server sent any extension
                        // we MUST abort the handshake with unsupported_extension fatal alter (handled by the dispatcher)
                        if (equalBytes sh_neg_extensions [||]) = false
                        then Error(AD_unsupported_extension, perror __SOURCE_FILE__ __LINE__ "The server gave an unknown extension")
                        else let unitVal = () in correct (unitVal)
                  match safe_reneg_result with
                    | Error (x,y) ->

InError (x,y,state)

| Correct _ ->
                        // Log the received message.
                        (* Check whether we asked for resumption *)
                        if equalBytes sid [||] then
                            (* we did not request resumption, do a full handshake *)
                            (* define the sinfo we're going to establish *)
                            let next_pstate = on_serverHello_full ci crand log to_log shello in

recv_fragment_client ci {state with pstate = next_pstate}  (Some sh_server_version)

else
                            if equalBytes sid sh_session_id then (* use resumption *)
                                (* Search for the session in our DB *)
                                match SessionDB.select state.sDB (sid,Client,state.poptions.server_name) with
                                | None ->
                                    (* This can happen, although we checked for the session before starting the HS.
                                       For example, the session may have expired between us sending client hello, and now. *)

InError(AD_internal_error, perror __SOURCE_FILE__ __LINE__ "A session expried while it was being resumed",state)

| Some(storable) ->
                                let (si,ms) = storable in
                                let log = log @| to_log in
                                (* Check that protocol version, ciphersuite and compression method are indeed the correct ones *)
                                if si.protocol_version = sh_server_version then
                                    if si.cipher_suite = sh_cipher_suite then
                                        if si.compression = sh_compression_method then
                                            let next_ci = getNextEpochs ci si crand sh_random in
                                            let (writer,reader) = PRF.keyGen next_ci ms in
                                            let nout = next_ci.id_out in
                                            let nin = next_ci.id_in in
                                            recv_fragment_client ci
                                              {state with pstate = PSClient(ServerCCSResume(nout,writer,
                                                                                            nin,reader,
                                                                                            ms,log))}
                                              (Some(sh_server_version))
                                        else

InError(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Compression method negotiation",state)

else

InError(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Ciphersuite negotiation",state)

else

InError(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "Protocol version negotiation",state)

else (* server did not agree on resumption, do a full handshake *)
                                (* define the sinfo we're going to establish *)
                                let next_pstate = on_serverHello_full ci crand log to_log shello in
                                recv_fragment_client ci {state with pstate = next_pstate} (Some(sh_server_version))
            | _ ->

InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "ServerHello arrived in the wrong state",state)

| HT_certificate ->
            match cState with
            // Most of the code in the branches is duplicated, but it helps for verification
            | ServerCertificateRSA (si,log) ->
                match parseClientOrServerCertificate payload with
                | Error(x,y) ->

InError(x,y,state)

| Correct(certs) ->
                    let allowedAlgs = default_sigHashAlg si.protocol_version si.cipher_suite in // In TLS 1.2, this is the same as we sent in our extension
                    if Cert.is_chain_for_key_encryption certs then
                        let advice = Cert.validate_cert_chain allowedAlgs certs in
                        let advice =
                            match Cert.get_hint certs with
                            | None -> false
                            | Some(name) -> advice && (name = state.poptions.server_name)
                        InQuery(certs,advice,{state with pstate = PSClient(ClientCheckingCertificateRSA(si,log,certs,agreedVersion,to_log))})
                    else

InError(AD_bad_certificate_fatal, perror __SOURCE_FILE__ __LINE__ "Server sent wrong certificate type",state)

| ServerCertificateDHE (si,log) ->
                match parseClientOrServerCertificate payload with
                | Error(x,y) ->

InError(x,y,state)

| Correct(certs) ->
                    let allowedAlgs = default_sigHashAlg si.protocol_version si.cipher_suite in // In TLS 1.2, this is the same as we sent in our extension
                    if Cert.is_chain_for_signing certs then
                        let advice = Cert.validate_cert_chain allowedAlgs certs in
                        let advice =
                            match Cert.get_hint certs with
                            | None -> false
                            | Some(name) -> advice && (name = state.poptions.server_name)
                        InQuery(certs,advice,{state with pstate = PSClient(ClientCheckingCertificateDHE(si,log,agreedVersion,to_log))})
                    else

InError(AD_bad_certificate_fatal, perror __SOURCE_FILE__ __LINE__ "Server sent wrong certificate type",state)

| ServerCertificateDH (si,log) ->

InError(AD_internal_error, perror __SOURCE_FILE__ __LINE__ "Unimplemented",state)

| _ ->

InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "Certificate arrived in the wrong state",state)

| HT_server_key_exchange ->
            match cState with
            | ServerKeyExchangeDHE(si,log) ->
                match parseServerKeyExchange_DHE si.protocol_version si.cipher_suite payload with
                | Error(x,y) ->

InError(x,y,state)

| Correct(v) ->
                    let (p,g,y,alg,signature) = v in
                    match Cert.get_chain_public_signing_key si.serverID alg with
                    | Error(x,y) ->

InError(x,y,state)

| Correct(vkey) ->
                    let dheb = dheParamBytes p g y in
                    let expected = si.init_crand @| si.init_srand @| dheb in
                    if Sig.verify alg vkey expected signature then
                        let log = log @| to_log in
                        recv_fragment_client ci
                          {state with pstate = PSClient(CertificateRequestDHE(si,p,g,y,log))}
                          agreedVersion
                    else
                        InError(AD_decrypt_error, perror __SOURCE_FILE__ __LINE__ "",state)

| ServerKeyExchangeDH_anon(si,log) ->
                match parseServerKeyExchange_DH_anon payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(v) ->
                    let (p,g,y) = v in
                    let log = log @| to_log in
                    recv_fragment_client ci
                      {state with pstate = PSClient(ServerHelloDoneDH_anon(si,p,g,y,log))}
                      agreedVersion
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "ServerKeyExchange arrived in the wrong state",state)

| HT_certificate_request ->
            match cState with
            | CertificateRequestRSA(si,log) ->
                (* Log the received packet *)
                let log = log @| to_log in

(* Note: in next statement, use si, because the handshake runs according to the session we want to
                   establish, not the current one *)
                match parseCertificateRequest si.protocol_version payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(v) ->
                let (certType,alg,distNames) = v in
                let client_cert = find_client_cert_sign certType alg distNames si.protocol_version state.poptions.client_name in
                let si = {si with client_auth = true} in
                recv_fragment_client ci
                  {state with pstate = PSClient(ServerHelloDoneRSA(si,client_cert,log))}
                  agreedVersion
            | CertificateRequestDHE(si,p,g,y,log) ->
                // Duplicated code
                (* Log the received packet *)
                let log = log @| to_log in

(* Note: in next statement, use si, because the handshake runs according to the session we want to
                   establish, not the current one *)
                match parseCertificateRequest si.protocol_version payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(v) ->
                let (certType,alg,distNames) = v in
                let client_cert = find_client_cert_sign certType alg distNames si.protocol_version state.poptions.client_name in
                let si = {si with client_auth = true} in
                recv_fragment_client ci
                  {state with pstate = PSClient(ServerHelloDoneDHE(si,client_cert,p,g,y,log))}
                  agreedVersion
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "CertificateRequest arrived in the wrong state",state)

| HT_server_hello_done ->
            match cState with
            | CertificateRequestRSA(si,log) ->
                if equalBytes payload [||] then
                    (* Log the received packet *)
                    let log = log @| to_log in

match prepare_client_output_full_RSA ci state si None log with
                    | Error (x,y) -> InError (x,y, state)
                    | Correct z ->
                        let (state,si,ms,log) = z in
                        recv_fragment_client ci
                          {state with pstate = PSClient(ClientWritingCCS(si,ms,log))}
                          agreedVersion
                else
                    InError(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "",state)
            | ServerHelloDoneRSA(si,skey,log) ->
                if equalBytes payload [||] then
                    (* Log the received packet *)
                    let log = log @| to_log in

match prepare_client_output_full_RSA ci state si skey log with
                    | Error (x,y) -> InError (x,y, state)
                    | Correct z ->
                        let (state,si,ms,log) = z in
                        recv_fragment_client ci
                          {state with pstate = PSClient(ClientWritingCCS(si,ms,log))}
                          agreedVersion
                else
                    InError(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "",state)
            | CertificateRequestDHE(si,p,g,y,log) | ServerHelloDoneDH_anon(si,p,g,y,log) ->
                if equalBytes payload [||] then
                    (* Log the received packet *)
                    let log = log @| to_log in

match prepare_client_output_full_DHE ci state si None p g y log with
                    | Error (x,y) -> InError (x,y, state)
                    | Correct z ->
                        let (state,si,ms,log) = z in
                        recv_fragment_client ci
                          {state with pstate = PSClient(ClientWritingCCS(si,ms,log))}
                          agreedVersion
                else
                    InError(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "",state)
            | ServerHelloDoneDHE(si,skey,p,g,y,log) ->
                if equalBytes payload [||] then
                    (* Log the received packet *)
                    let log = log @| to_log in

match prepare_client_output_full_DHE ci state si skey p g y log with
                    | Error (x,y) -> InError (x,y, state)
                    | Correct z ->
                        let (state,si,ms,log) = z in
                        recv_fragment_client ci
                          {state with pstate = PSClient(ClientWritingCCS(si,ms,log))}
                          agreedVersion
                else
                    InError(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "",state)
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "ServerHelloDone arrived in the wrong state",state)

| HT_finished ->
            match cState with
            | ServerFinished(si,ms,e,cvd,log) ->
                if PRF.checkVerifyData ci.id_in Server ms log payload then
                    let sDB =
                        if equalBytes si.sessionID [||] then state.sDB
                        else SessionDB.insert state.sDB (si.sessionID,Client,state.poptions.server_name) (si,ms)
                    check_negotiation Client si state.poptions;
                    InComplete({state with pstate = PSClient(ClientIdle(cvd,payload)); sDB = sDB})
                else
                    InError(AD_decrypt_error, perror __SOURCE_FILE__ __LINE__ "Verify data did not match",state)
            | ServerFinishedResume(e,w,ms,log) ->
                if PRF.checkVerifyData ci.id_in Server ms log payload then
                    let log = log @| to_log in
                    InFinished({state with pstate = PSClient(ClientWritingCCSResume(e,w,ms,payload,log))})
                else
                    InError(AD_decrypt_error, perror __SOURCE_FILE__ __LINE__ "Verify data did not match",state)
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "Finished arrived in the wrong state",state)
        | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "Unrecognized message",state)

(* Should never happen *)
      | PSServer(_) -> unexpectedError "[recv_fragment_client] should only be invoked when in client role."

let prepare_server_output_full_RSA (ci:ConnectionInfo) state si cv calgs cvd svd log =
    let renInfo = cvd @| svd in
    let ext = extensionsBytes state.poptions.safe_renegotiation renInfo in
    let serverHelloB = serverHelloBytes si si.init_srand ext in
    match Cert.for_key_encryption calgs state.poptions.server_name with
    | None -> Error(AD_internal_error, perror __SOURCE_FILE__ __LINE__ "Could not find in the store a certificate for the negotiated ciphersuite")
    | Some(x) ->
        let (c,sk) = x in
        (* update server identity in the sinfo *)
        let si = {si with serverID = c} in
        let certificateB = serverCertificateBytes c in
        (* No ServerKEyExchange in RSA ciphersuites *)
        (* Compute the next state of the server *)
        if si.client_auth then
          let certificateRequestB = certificateRequestBytes true si.cipher_suite si.protocol_version in // true: Ask for sign-capable certificates
          let output = serverHelloB @| certificateB @| certificateRequestB @| serverHelloDoneBytes in
          (* Log the output and put it into the output buffer *)
          let log = log @| output in
          let ps = serverState ci (ClientCertificateRSA(si,cv,sk,log)) in
          correct ({state with hs_outgoing = output
                               pstate = ps},
                    si.protocol_version)
        else
          let output = serverHelloB @| certificateB @| serverHelloDoneBytes in
          (* Log the output and put it into the output buffer *)
          let log = log @| output in
          let ps = serverState ci (ClientKeyExchangeRSA(si,cv,sk,log)) in
          correct ({state with hs_outgoing = output
                               pstate = ps},
                    si.protocol_version)

let prepare_server_output_full_DH ci state si log =
    Error(AD_internal_error, perror __SOURCE_FILE__ __LINE__ "Unimplemented")

let prepare_server_output_full_DHE (ci:ConnectionInfo) state si certAlgs cvd svd log =
    let renInfo = cvd @| svd in
    let ext = extensionsBytes state.poptions.safe_renegotiation renInfo in
    let serverHelloB = serverHelloBytes si si.init_srand ext in
    let keyAlgs = sigHashAlg_bySigList certAlgs [sigAlg_of_ciphersuite si.cipher_suite] in
    if listLength keyAlgs = 0 then
        Error(AD_illegal_parameter, perror __SOURCE_FILE__ __LINE__ "The client provided inconsistent signature algorithms and ciphersuites")
    else
    match Cert.for_signing certAlgs state.poptions.server_name keyAlgs with
    | None -> Error(AD_internal_error, perror __SOURCE_FILE__ __LINE__ "Could not find in the store a certificate for the negotiated ciphersuite")
    | Some(x) ->
        let (c,alg,sk) = x in
        (* set server identity in the session info *)
        let si = {si with serverID = c} in
        let certificateB = serverCertificateBytes c in
        (* ServerKEyExchange *)
        let (p,g) = DH.default_pp () in
        let (y,x) = DH.genKey p g in
        let dheb = dheParamBytes p g y in
        let toSign = si.init_crand @| si.init_srand @| dheb in
        let sign = Sig.sign alg sk toSign in
        let serverKEXB = serverKeyExchangeBytes_DHE dheb alg sign si.protocol_version in
        (* CertificateRequest *)
        if si.client_auth then
          let certificateRequestB = certificateRequestBytes true si.cipher_suite si.protocol_version in // true: Ask for sign-capable certificates
          let output = serverHelloB @| certificateB @| serverKEXB @| certificateRequestB @| serverHelloDoneBytes in
          (* Log the output and put it into the output buffer *)
          let log = log @| output in
          let ps = serverState ci (ClientCertificateDHE(si,p,g,y,x,log)) in
        (* Compute the next state of the server *)
            correct (
              {state with hs_outgoing = output
                          pstate = ps},
               si.protocol_version)
        else
          let output = serverHelloB @| certificateB @| serverKEXB @| serverHelloDoneBytes in
          (* Log the output and put it into the output buffer *)
          let log = log @| output in
          let ps = serverState ci (ClientKeyExchangeDHE(si,p,g,y,x,log)) in
            correct (
              {state with hs_outgoing = output
                          pstate = ps},
               si.protocol_version)

(* ClientKeyExchangeDHE(si,p,g,x,log) should carry PP((p,g)) /\ ?gx. DHE.Exp((p,g),x,gx) *)

let prepare_server_output_full_DH_anon (ci:ConnectionInfo) state si cvd svd log =
    let renInfo = cvd @| svd in
    let ext = extensionsBytes state.poptions.safe_renegotiation renInfo in
    let serverHelloB = serverHelloBytes si si.init_srand ext in

(* ServerKEyExchange *)
    let (p,g) = DH.default_pp () in
    let (y,x) = DH.genKey p g in
    let serverKEXB = serverKeyExchangeBytes_DH_anon p g y in

let output = serverHelloB @|serverKEXB @| serverHelloDoneBytes in
    (* Log the output and put it into the output buffer *)
    let log = log @| output in
    (* Compute the next state of the server *)
    let ps = serverState ci (ClientKeyExchangeDH_anon(si,p,g,y,x,log)) in
    correct ({state with hs_outgoing = output
                         pstate = ps},
             si.protocol_version)

let prepare_server_output_full ci state si cv cvd svd log =
    if isAnonCipherSuite si.cipher_suite then
        prepare_server_output_full_DH_anon ci state si cvd svd log
    elif isDHCipherSuite si.cipher_suite then
        prepare_server_output_full_DH ci state si log
    elif isDHECipherSuite si.cipher_suite then
        // Get the client supported SignatureAndHash algorithms. In TLS 1.2, this should be extracted from a client extension
        let calgs = default_sigHashAlg si.protocol_version si.cipher_suite in
        prepare_server_output_full_DHE ci state si calgs cvd svd log
    elif isRSACipherSuite si.cipher_suite then
        // Get the client supported SignatureAndHash algorithms. In TLS 1.2, this should be extracted from a client extension
        let calgs = default_sigHashAlg si.protocol_version si.cipher_suite in
        prepare_server_output_full_RSA ci state si cv calgs cvd svd log
    else
        unexpectedError "[prepare_server_output_full] unexpected ciphersuite"

// The server "negotiates" its first proposal included in the client's proposal
let negotiate cList sList =
    Bytes.tryFind (fun s -> Bytes.exists (fun c -> c = s) cList) sList

let prepare_server_output_resumption ci state crand si ms cvd svd log =
    let srand = Nonce.mkHelloRandom () in
    let renInfo = cvd @| svd in
    let ext = extensionsBytes state.poptions.safe_renegotiation renInfo in
    let sHelloB = serverHelloBytes si srand ext in

let log = log @| sHelloB
    let next_ci = getNextEpochs ci si crand srand in
    let (writer,reader) = PRF.keyGen next_ci ms in
    {state with hs_outgoing = sHelloB
                pstate = PSServer(ServerWritingCCSResume(next_ci.id_out,writer,
                                                         next_ci.id_in,reader,
                                                         ms,log))}

let startServerFull (ci:ConnectionInfo) state (cHello:ProtocolVersion * crand * sessionID * cipherSuites * Compression list * bytes) cvd svd log =
    let (ch_client_version,ch_random,ch_session_id,ch_cipher_suites,ch_compression_methods,ch_extensions) = cHello in
    let cfg = state.poptions in
    // Negotiate the protocol parameters
    let version = minPV ch_client_version cfg.maxVer in
    if (geqPV version cfg.minVer) = false then
        Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Protocol version negotiation")
    else
        match negotiate ch_cipher_suites cfg.ciphersuites with
        | Some(cs) ->
            match negotiate ch_compression_methods cfg.compressions with
            | Some(cm) ->
                let sid = random 32 in
                let srand = Nonce.mkHelloRandom () in
                (* Fill in the session info we're establishing *)
                let si = { clientID         = []
                           client_auth      = cfg.request_client_certificate
                           serverID         = []
                           sessionID        = sid
                           protocol_version = version
                           cipher_suite     = cs
                           compression      = cm
                           init_crand       = ch_random
                           init_srand       = srand
                           pmsData          = PMSUnset
                           extended_record_padding = false }
                prepare_server_output_full ci state si ch_client_version cvd svd log
            | None -> Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Compression method negotiation")
        | None ->     Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Ciphersuite negotiation")

let rec recv_fragment_server (ci:ConnectionInfo) (state:hs_state) (agreedVersion:ProtocolVersion option) =
    match parseMessageState ci state with
    | Error(x,y) -> InError(x,y,state)
    | Correct(res) ->
      match res with
      | None ->
          match agreedVersion with
          | None      -> InAck(state)
          | Some (pv) -> InVersionAgreed(state,pv)
      | Some (res) ->
      let (state,hstype,payload,to_log) = res in
      match state.pstate with
      | PSServer(sState) ->
        match hstype with
        | HT_client_hello ->
            match sState with
            | ClientHello(cvd,svd) | ServerIdle(cvd,svd) ->
                match parseClientHello payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct (cHello) ->
                let (ch_client_version,ch_random,ch_session_id,ch_cipher_suites,ch_compression_methods,ch_extensions) = cHello
                (* Log the received message *)
                let log = to_log in
                (* handle extensions: for now only renegotiation_info *)
                match parseExtensions ch_extensions with
                | Error(x,y) -> InError(x,y,state)
                | Correct(extList) ->
                let extRes =
                    if state.poptions.safe_renegotiation then
                        if checkClientRenegotiationInfoExtension extList ch_cipher_suites cvd then
                            correct(state)
                        else
                            (* We don't accept an insecure client *)
                            Error(AD_handshake_failure, perror __SOURCE_FILE__ __LINE__ "Safe renegotiation not supported by the peer")
                    else
                        (* We can ignore the extension, if any *)
                        correct(state)
                match extRes with
                | Error(x,y) -> InError(x,y,state)
                | Correct(state) ->
                    if equalBytes ch_session_id [||]
                    then
                        (* Client asked for a full handshake *)
                        match startServerFull ci state cHello cvd svd log with
                        | Error(x,y) -> InError(x,y,state)
                        | Correct(v) ->
                            let (state,pv) = v in
                            let spv = somePV pv in
                              recv_fragment_server ci state spv
                    else
                        (* Client asked for resumption, let's see if we can satisfy the request *)
                        match SessionDB.select state.sDB (ch_session_id,Server,state.poptions.client_name) with
                        | Some sentry ->
                            let (storedSinfo,storedMS)  = sentry in
                            if geqPV ch_client_version storedSinfo.protocol_version
                              && Bytes.memr ch_cipher_suites storedSinfo.cipher_suite
                              && Bytes.memr ch_compression_methods storedSinfo.compression
                            then
                              (* Proceed with resumption *)
                              let state = prepare_server_output_resumption ci state ch_random storedSinfo storedMS cvd svd log in
                              recv_fragment_server ci state (somePV(storedSinfo.protocol_version))
                            else
                              match startServerFull ci state cHello cvd svd log with
                                | Correct(v) -> let (state,pv) = v in recv_fragment_server ci state (somePV (pv))
                                | Error(x,y) -> InError(x,y,state)
                        | None ->
                              match startServerFull ci state cHello cvd svd log with
                                | Correct(v) -> let (state,pv) = v in recv_fragment_server ci state (somePV (pv))
                                | Error(x,y) -> InError(x,y,state)
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "ClientHello arrived in the wrong state",state)

| HT_certificate ->
            match sState with
            | ClientCertificateRSA (si,cv,sk,log) ->
                match parseClientOrServerCertificate payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(certs) ->
                    if Cert.is_chain_for_signing certs then
                        let advice = Cert.validate_cert_chain (default_sigHashAlg si.protocol_version si.cipher_suite) certs in
                        match Cert.get_hint certs with
                            | None ->
                                InQuery(certs,false,
                                        {state with pstate = PSServer(ServerCheckingCertificateRSA(si,cv,sk,log,certs,to_log))})
                            | Some(name) when advice && (name = state.poptions.client_name) ->
                                InQuery(certs,true,
                                        {state with pstate = PSServer(ServerCheckingCertificateRSA(si,cv,sk,log,certs,to_log))})
                            | Some(name) ->
                                InQuery(certs,false,
                                        {state with pstate = PSServer(ServerCheckingCertificateRSA(si,cv,sk,log,certs,to_log))})
                    else
                        InError(AD_bad_certificate_fatal, perror __SOURCE_FILE__ __LINE__ "Client sent wrong certificate type",state)
            | ClientCertificateDHE (si,p,g,gx,x,log) ->
                // Duplicated code from above.
                match parseClientOrServerCertificate payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(certs) ->
                    if Cert.is_chain_for_signing certs then
                        let advice = Cert.validate_cert_chain (default_sigHashAlg si.protocol_version si.cipher_suite) certs in
                        match Cert.get_hint certs with
                            | None ->
                                InQuery(certs,false,{state with pstate = PSServer(ServerCheckingCertificateDHE(si,p,g,gx,x,log,certs,to_log))})
                            | Some(name) when advice && (name = state.poptions.client_name) ->
                                InQuery(certs,true,{state with pstate = PSServer(ServerCheckingCertificateDHE(si,p,g,gx,x,log,certs,to_log))})
                            | Some(name) ->
                                InQuery(certs,false,{state with pstate = PSServer(ServerCheckingCertificateDHE(si,p,g,gx,x,log,certs,to_log))})
                    else
                        InError(AD_bad_certificate_fatal, perror __SOURCE_FILE__ __LINE__ "Client sent wrong certificate type",state)
            | ClientCertificateDH  (si,log) ->  InError(AD_internal_error, perror __SOURCE_FILE__ __LINE__ "Unimplemented",state)
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "Certificate arrived in the wrong state",state)

| HT_client_key_exchange ->
            match sState with
            | ClientKeyExchangeRSA(si,cv,sk,log) ->
                match parseClientKEX_RSA si sk cv state.poptions payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(res) ->
                    let (pmsdata,pms) = res in
                    let si = {si with pmsData = pmsdata} in
                    let log = log @| to_log in
                    let ms = CRE.prfSmoothRSA si cv pms in

(* move to new state *)
                    if si.client_auth then
                        recv_fragment_server ci
                          {state with pstate = PSServer(CertificateVerify(si,ms,log))}
                          agreedVersion
                    else
                        recv_fragment_server ci
                          {state with pstate = PSServer(ClientCCS(si,ms,log))}
                          agreedVersion
            | ClientKeyExchangeDHE(si,p,g,gx,x,log) ->
                match parseClientKEXExplicit_DH p payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(y) ->
                    let log = log @| to_log in
                    let si = {si with pmsData = DHPMS(p,g,y,gx)} in
                    (* from the local state, we know: PP((p,g)) /\ ?gx. DHE.Exp((p,g),x,gx) ; tweak the ?gx for genPMS. *)
                    let pms = DH.exp p g gx y x in
                    (* StrongHS(si) /\ DHE.Exp((p,g),?cx,y) -> DHE.Secret(pms) *)
                    let ms = CRE.prfSmoothDHE si p g gx y pms in
                    (* StrongHS(si) /\ DHE.Exp((p,g),?cx,y) -> PRFs.Secret(ms) *)

(* we rely on scopes & type safety to get forward secrecy*)
                    (* move to new state *)
                    if si.client_auth then
                        recv_fragment_server ci
                          {state with pstate = PSServer(CertificateVerify(si,ms,log))}
                          agreedVersion
                    else
                        recv_fragment_server ci
                          {state with pstate = PSServer(ClientCCS(si,ms,log))}
                          agreedVersion
            | ClientKeyExchangeDH_anon(si,p,g,gx,x,log) ->
                match parseClientKEXExplicit_DH p payload with
                | Error(x,y) -> InError(x,y,state)
                | Correct(y) ->
                    let log = log @| to_log in
                    let pms = DH.exp p g gx y x in
                    let ms = CRE.prfSmoothDHE si p g gx y pms in

(* move to new state *)
                    recv_fragment_server ci
                      {state with pstate = PSServer(ClientCCS(si,ms,log))}
                      agreedVersion
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "ClientKeyExchange arrived in the wrong state",state)

| HT_certificate_verify ->
            match sState with
            | CertificateVerify(si,ms,log) ->
                let allowedAlgs = default_sigHashAlg si.protocol_version si.cipher_suite in // In TLS 1.2, these are the same as we sent in CertificateRequest
                let (verifyOK,_) = certificateVerifyCheck si ms allowedAlgs log payload in
                if verifyOK then// payload then
                    let log = log @| to_log in
                    recv_fragment_server ci
                      {state with pstate = PSServer(ClientCCS(si,ms,log))}
                      agreedVersion
                else
                    InError(AD_decrypt_error, perror __SOURCE_FILE__ __LINE__ "Certificate verify check failed",state)
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "CertificateVerify arrived in the wrong state",state)

| HT_finished ->
            match sState with
            | ClientFinished(si,ms,e,w,log) ->
                if PRF.checkVerifyData ci.id_in Client ms log payload then
                    let log = log @| to_log in
                    InFinished({state with pstate = PSServer(ServerWritingCCS(si,ms,e,w,payload,log))})
                else
                    InError(AD_decrypt_error, perror __SOURCE_FILE__ __LINE__ "Verify data did not match",state)
            | ClientFinishedResume(si,ms,e,svd,log) ->
                if PRF.checkVerifyData ci.id_in Client ms log payload then
                    check_negotiation Server si state.poptions;
                    InComplete({state with pstate = PSServer(ServerIdle(payload,svd))})
                else
                    InError(AD_decrypt_error, perror __SOURCE_FILE__ __LINE__ "Verify data did not match",state)
            | _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "Finished arrived in the wrong state",state)

| _ -> InError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "Unknown message received",state)
      (* Should never happen *)
      | PSClient(_) -> unexpectedError "[recv_fragment_server] should only be invoked when in server role."

let enqueue_fragment (ci:ConnectionInfo) state fragment =
    let new_inc = state.hs_incoming @| fragment in
    {state with hs_incoming = new_inc}

let recv_fragment ci (state:hs_state) (r:range) (fragment:HSFragment.fragment) =

let b = HSFragment.fragmentRepr ci.id_in r fragment in
    if length b = 0 then
        // Empty HS fragment are not allowed
        InError(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "Empty handshake fragment received",state)
    else
        let state = enqueue_fragment ci state b in
        match state.pstate with
        | PSClient (_) -> recv_fragment_client ci state None
        | PSServer (_) -> recv_fragment_server ci state None

let recv_ccs (ci:ConnectionInfo) (state: hs_state) (r:range) (fragment:HSFragment.fragment): incomingCCS =

let b = HSFragment.fragmentRepr ci.id_in r fragment in
    if equalBytes b CCSBytes then
        match state.pstate with
        | PSClient (cstate) -> // Check that we are in the right state (CCCS)
            match cstate with
            | ServerCCS(si,ms,e,r,cvd,log) ->
                let ci = {ci with id_in = e} in
                InCCSAck(ci,r,{state with pstate = PSClient(ServerFinished(si,ms,e,cvd,log))})
            | ServerCCSResume(ew,w,er,r,ms,log) ->
                let ci = {ci with id_in = er} in
                InCCSAck(ci,r,{state with pstate = PSClient(ServerFinishedResume(ew,w,ms,log))})
            | _ -> InCCSError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "CCS arrived in the wrong state",state)
        | PSServer (sState) ->
            match sState with
            | ClientCCS(si,ms,log) ->
                let next_ci = getNextEpochs ci si si.init_crand si.init_srand in
                let (writer,reader) = PRF.keyGen next_ci ms in
                let ci = {ci with id_in = next_ci.id_in} in
                InCCSAck(ci,reader,{state with pstate = PSServer(ClientFinished(si,ms,next_ci.id_out,writer,log))})
            | ClientCCSResume(e,r,svd,ms,log) ->
                let ci = {ci with id_in = e} in
                InCCSAck(ci,r,{state with pstate = PSServer(ClientFinishedResume(epochSI e,ms,e,svd,log))})
            | _ -> InCCSError(AD_unexpected_message, perror __SOURCE_FILE__ __LINE__ "CCS arrived in the wrong state",state)
    else           InCCSError(AD_decode_error, perror __SOURCE_FILE__ __LINE__ "",state)

let getMinVersion (ci:ConnectionInfo) state =
  let pop = state.poptions in
  pop.minVer

let authorize (ci:ConnectionInfo) (state:hs_state) (q:Cert.chain) =
    let pstate = state.pstate in
    match pstate with
    | PSClient(cstate) ->
        match cstate with
        | ClientCheckingCertificateRSA(si,log,certs,agreedVersion,to_log) ->
            if certs = q then
              let log = log @| to_log in
              let si = {si with serverID = q} in
              Pi.assume (Authorize(Client,si));
              recv_fragment_client ci
                {state with pstate = PSClient(CertificateRequestRSA(si,log))}
                agreedVersion
            else unexpectedError "[authorize] invoked with different cert"
        | ClientCheckingCertificateDHE(si,log,agreedVersion,to_log) ->
            let log = log @| to_log in
            let si = {si with serverID = q} in
            Pi.assume (Authorize(Client,si));
            recv_fragment_client ci
              {state with pstate = PSClient(ServerKeyExchangeDHE(si,log))}
              agreedVersion
        // | ClientCheckingCertificateDH -> TODO
        | _ -> unexpectedError "[authorize] invoked on the wrong state"
    | PSServer(sstate) ->
        match sstate with
        | ServerCheckingCertificateRSA(si,cv,sk,log,c,to_log) when c = q ->
            let log = log @| to_log in
            let si = {si with clientID = q} in
             Pi.assume (Authorize(Server,si));
            recv_fragment_server ci
              {state with pstate = PSServer(ClientKeyExchangeRSA(si,cv,sk,log))}
              None
        | ServerCheckingCertificateDHE(si,p,g,gx,x,log,c,to_log) when c = q ->
            let log = log @| to_log in
            let si = {si with clientID = q} in
            Pi.assume (Authorize(Server,si));
            recv_fragment_server ci
              {state with pstate = PSServer(ClientKeyExchangeDHE(si,p,g,gx,x,log))}
              None
        // | ServerCheckingCertificateDH -> TODO
        | _ -> unexpectedError "[authorize] invoked on the wrong state"

(* function used by an ideal handshake implementation to decide whether to idealize keys
let safe ki =
    match (CS(ki), Honest(LTKey(ki, Server)), Honest(LTKey(ki,Client))) with
    | (CipherSuite (RSA, MtE (AES_256_CBC, SHA256)), true, _) -> pmsGenerated ki
    | (CipherSuite (DHE_DSS, MtE (AES_256_CBC, SHA)), _, _) ->
        if (TcGenerated ki) && (TsGenerated ki) then
            true
        else
            false
    | _ -> false

F7 Interface: Handshake.fs7

module Handshake

open Bytes
open Error
open TLSInfo
open Range
open StatefulLHAE
open TLSConstants
open TLSExtensions

function val HTBytes: HandshakeType -> bytes

private definition
    HTBytes(HT_hello_request      ) = [|  0uy |] /\
    HTBytes(HT_client_hello       ) = [|  1uy |] /\
    HTBytes(HT_server_hello       ) = [|  2uy |] /\
    HTBytes(HT_certificate        ) = [| 11uy |] /\
    HTBytes(HT_server_key_exchange) = [| 12uy |] /\
    HTBytes(HT_certificate_request) = [| 13uy |] /\
    HTBytes(HT_server_hello_done  ) = [| 14uy |] /\
    HTBytes(HT_certificate_verify ) = [| 15uy |] /\
    HTBytes(HT_client_key_exchange) = [| 16uy |] /\
    HTBytes(HT_finished           ) = [| 20uy |]

val htBytes: ht:HandshakeType -> b:bytes{b=HTBytes(ht)}
val parseHt: b:bytes -> (ht:HandshakeType{b=HTBytes(ht)}) Result

function val MessageBytes: HandshakeType * bytes -> bytes
private definition !ht,b. MessageBytes(ht,b) = HTBytes(ht) @| VLBytes(3,b)
val messageBytes: ht:HandshakeType -> x:bytes -> m:bytes{m = MessageBytes(ht,x)}
val parseMessage: buf:bytes -> ((rem:bytes * ht:HandshakeType * x:bytes * to_log:bytes)
				{buf = to_log @| rem /\ to_log = MessageBytes(ht,x)}) option Result

// Next predicate to make sure we can make fragments
predicate type unsafe = Unsafe of epoch
private definition !ki. Unsafe(ki) <=> not Auth(ki)
val makeFragment: ki:epoch -> b:bytes -> (r:range * (;ki,HSFragment.EmptyStream(ki),r) HSFragment.plain * bytes)

// For each Handshake message x, we have:
// XMsg   : a logical specification of its wire format
// xBytes : a formatting function
// parseX : a parsing function (returning a Result, as parsing may fail)

function val ClientHelloMsg: (ProtocolVersion * random * sessionID * cipherSuites * Compression list * bytes) -> bytes
definition !cv,clRdm,sid,cls,cm,ext,b.
    ClientHelloMsg(cv,clRdm,sid,cls,cm,ext) =
		MessageBytes(HT_client_hello,
            (VersionBytes(cv) @|
             clRdm @|
             VLBytes(1,sid) @|
             VLBytes(2,CipherSuitesBytes(cls)) @|
             VLBytes(1,CompressionsBytes(cm)) @|
             ext)
		)

val clientHelloBytes: c:config -> cr:random -> sid:sessionID -> ext:bytes -> m:bytes{m = ClientHelloMsg(c.maxVer,cr,sid,c.ciphersuites,c.compressions,ext)}
val parseClientHello: m:bytes ->
	( pv:ProtocolVersion * cr:crand * sid:sessionID * cs:cipherSuites * cm:Compression list * ext:bytes
	  {?cs',cm'. MessageBytes(HT_client_hello,m) = ClientHelloMsg(pv,cr,sid,cs',cm',ext)
              /\ ContainsCipherSuites(cs',cs) /\ ContainsCompressions(cm',cm)}) Result

function val ServerHelloMsg: (ProtocolVersion * random * sessionID * cipherSuite * Compression * bytes) -> bytes
private definition !pv,sr,sid,cs,cm,ext.
	ServerHelloMsg(pv,sr,sid,cs,cm,ext) =
		MessageBytes(HT_server_hello,
			(VersionBytes(pv) @|
			 sr @|
			 VLBytes(1,sid) @|
			 CipherSuiteBytes(cs) @|
			 CompressionBytes(cm) @|
			 ext)
		)

function val  SessionHelloParams: SessionInfo * unit -> (ProtocolVersion * cipherSuite * Compression)
private definition !si.
 SessionHelloParams(si,()) = (si.protocol_version,si.cipher_suite,si.compression)

val serverHelloBytes: si:SessionInfo -> sr:random -> ext:bytes ->
	b:bytes{b = ServerHelloMsg(si.protocol_version,sr,si.sessionID,si.cipher_suite,
							   si.compression,ext)}
val parseServerHello: b:bytes ->
	((pv:ProtocolVersion * sr:random * sid:sessionID * cs:cipherSuite * cm:Compression * ext:bytes)
	 {MessageBytes(HT_server_hello,b) = ServerHelloMsg(pv,sr,sid,cs,cm,ext)})
	Result

val helloRequestBytes: b:bytes{b=MessageBytes(HT_hello_request,[||])}
val CCSBytes: b:bytes{b=[|1uy|]}

function val ServerHelloDoneMsg: bytes -> bytes
private definition !x. ServerHelloDoneMsg(x) = MessageBytes(HT_server_hello_done,[||])

val serverHelloDoneBytes: b:bytes{b=ServerHelloDoneMsg([||])}

function val CertificateMsg: Cert.chain -> bytes
private definition !cl. CertificateMsg(cl) = MessageBytes(HT_certificate,VLBytes(3,Cert.CertificateListBytes(cl)))

val serverCertificateBytes: cl:Cert.chain ->
	b:bytes{b = CertificateMsg(cl)}

val clientCertificateBytes: clo: (Cert.chain * a:Sig.alg * (;a)Sig.skey) option ->
	b:bytes{
		( clo = None /\ b = CertificateMsg([]) ) \/
		( ?cl,a',b'. clo = Some((cl,a',b')) /\ b = CertificateMsg(cl)
		)}

val parseClientOrServerCertificate: b:bytes ->
	(bl:Cert.chain{
	  MessageBytes(HT_certificate,b) = CertificateMsg(bl)
	}) Result

function val CertificateRequestTLS12: certType list * Sig.alg list * string list -> bytes
private definition !ct,sa,dn.
	CertificateRequestTLS12(ct,sa,dn) =
		MessageBytes(HT_certificate_request,
		  VLBytes(1,CertTypesBytes(ct)) @|
		  VLBytes(2,SigHashAlgsBytes(sa)) @|
		  VLBytes(2,DistinguishedNamesBytes(dn)))
function val CertificateRequestTLS: certType list * string list -> bytes
private definition !ct,dn.
	CertificateRequestTLS(ct,dn) =
		MessageBytes(HT_certificate_request,
		    VLBytes(1,CertTypesBytes(ct)) @| [||] @|
		    VLBytes(2,DistinguishedNamesBytes(dn)))
function val CertificateRequestMsg: ProtocolVersion * certType list * Sig.alg list * string list -> bytes
private definition !pv,ct,sa,dn.
	(pv = TLS_1p2 => CertificateRequestMsg(pv,ct,sa,dn) = CertificateRequestTLS12(ct,sa,dn)) /\
	((pv = TLS_1p1 \/ pv = TLS_1p0 \/ pv = SSL_3p0) => CertificateRequestMsg(pv,ct,sa,dn) = CertificateRequestTLS(ct,dn))

val sigHashAlgBytesVersion: pv:ProtocolVersion -> cs:cipherSuite ->
	b:bytes{(pv = TLS_1p2 => b=VLBytes(2,SigHashAlgsBytes(DefaultSigHashAlgs(pv,cs)))) /\
			((pv = TLS_1p1 \/ pv = TLS_1p0 \/ pv = SSL_3p0) =>
				b = [||])}

val parseSigHashAlgVersion: pv:ProtocolVersion -> b:bytes ->
	((a:(Sig.alg list) * r:bytes){
		(pv = TLS_1p2 =>
			(b = VLBytes(2,SigHashAlgsBytes(a)) @| r)
		) /\
		((pv = TLS_1p1 \/ pv = TLS_1p0 \/ pv = SSL_3p0) =>
			a = [] /\  r=b)
	}) Result

val certificateRequestBytes: sign:bool -> cs:cipherSuite -> pv:ProtocolVersion ->
	b:bytes{b = CertificateRequestMsg(pv,DefaultCertTypes(sign,cs),DefaultSigHashAlgs(pv,cs),[])}

val parseCertificateRequest: pv:ProtocolVersion -> b:bytes ->
	((ctl:certType list * al:(Sig.alg list) * sl:string list){
		MessageBytes(HT_certificate_request,b) = CertificateRequestMsg(pv,ctl,al,sl)})	 Result

function val ClientKeyExchangeMsg_RSA: pv:ProtocolVersion * bytes -> bytes
private definition !pv,encpms,b.
       ((pv = TLS_1p2 \/ pv = TLS_1p1 \/ pv = TLS_1p0) => ClientKeyExchangeMsg_RSA(pv,encpms) = MessageBytes(HT_client_key_exchange,VLBytes(2,encpms))) /\
	(pv = SSL_3p0 => ClientKeyExchangeMsg_RSA(pv,encpms) = MessageBytes(HT_client_key_exchange,encpms))

val encpmsBytesVersion: pv:ProtocolVersion -> encpms:bytes ->
	b:bytes{(pv = SSL_3p0 => b=encpms) /\
		((pv = TLS_1p0 \/ pv = TLS_1p1 \/ pv = TLS_1p2) => b=VLBytes(2,encpms))}

val parseEncpmsVersion: pv:ProtocolVersion -> b:bytes ->
	(encpms:bytes{
		(pv = SSL_3p0 => b=encpms) /\
		((pv = TLS_1p0 \/ pv = TLS_1p1 \/ pv = TLS_1p2) => b = VLBytes(2,encpms))
	}) Result

// For the next two functions, the returned encpms is a ghost variable used to
// avoid an existential.
val clientKEXBytes_RSA: si:SessionInfo -> c:config ->
	((b:bytes * pmsdata:TLSInfo.pmsData * pms:(;Cert.RSAPKCert(si.serverID),c.maxVer)CRE.rsapms){
           ?encpms. pmsdata = RSAPMS(Cert.RSAPKCert(si.serverID),c.maxVer,encpms) /\
		b=ClientKeyExchangeMsg_RSA(si.protocol_version,encpms)
		}) Result
val parseClientKEX_RSA: si:SessionInfo -> RSAKey.sk -> pv:ProtocolVersion -> config -> b:bytes ->
	((pmsdata:TLSInfo.pmsData *
         (;Cert.RSAPKCert(si.serverID),pv)CRE.rsapms){
           ?encpms. pmsdata = RSAPMS(Cert.RSAPKCert(si.serverID),pv,encpms) /\
     	            ClientKeyExchangeMsg_RSA(si.protocol_version,encpms) = MessageBytes(HT_client_key_exchange,b)
	}) Result

function val ClientKeyExchangeMsg_DHE: bytes -> bytes
private definition !b.
	ClientKeyExchangeMsg_DHE(b) =
		MessageBytes(HT_client_key_exchange,
			VLBytes(2,b))

val clientKEXExplicitBytes_DH: gx:bytes ->
	b:bytes{b = ClientKeyExchangeMsg_DHE(gx)}
val parseClientKEXExplicit_DH: p:DHGroup.p -> b:bytes ->
	(gx:(;p)DHGroup.elt{
		MessageBytes(HT_client_key_exchange,b) =
                ClientKeyExchangeMsg_DHE(gx)
	}) Result
val clientKEXImplicitBytes_DH: bytes
val parseClientKEXImplicit_DH: bytes -> unit Result

(* Digitally signed and DHE parameters *)
function val DigitallySignedBytes: Sig.alg * bytes * ProtocolVersion -> bytes
private definition !a,p,pv.
	(pv = TLS_1p2 => DigitallySignedBytes(a,p,pv) = SigHashAlgBytes(a) @| VLBytes(2,p)) /\
	( (pv = TLS_1p1 \/ pv = TLS_1p0 \/ pv = SSL_3p0) => DigitallySignedBytes(a,p,pv) = VLBytes(2,p))

val digitallySignedBytes: a:Sig.alg -> p:bytes -> pv:ProtocolVersion ->
	b:bytes{b = DigitallySignedBytes(a,p,pv)}
val parseDigitallySigned: al:Sig.alg list -> b:bytes -> pv:ProtocolVersion ->
	((a:Sig.alg * p:bytes){
		b = DigitallySignedBytes(a,p,pv)
		// /\ SigHashAlgContains(al,a)
	}) Result

function val DHEParamBytes: bytes * bytes * bytes -> bytes
private definition !p,g,y.
	DHEParamBytes(p,g,y) =
		VLBytes(2,p) @|
		VLBytes(2,g) @|
		VLBytes(2,y)
val dheParamBytes: p:bytes -> g:bytes -> y:bytes ->
	b:bytes{b = DHEParamBytes(p,g,y)}
val parseDHEParams: b:bytes ->
 (p:DHGroup.p * g:(;p)DHGroup.elt * y:(;p)DHGroup.elt * rem:bytes {
	b = (DHEParamBytes(p,g,y) @| rem)
 }) Result

function val ServerKeyExchangeMsg_DHE:  ProtocolVersion * p:bytes * g:bytes * y:bytes * Sig.alg * sign:bytes-> bytes
private definition !pv,p,g,y,a,sign.
	ServerKeyExchangeMsg_DHE(pv,p,g,y,a,sign) =
		MessageBytes(HT_server_key_exchange,
			DHEParamBytes(p,g,y) @| DigitallySignedBytes(a,sign,pv))

val serverKeyExchangeBytes_DHE: dheb:bytes{?p,g,y. dheb = DHEParamBytes(p,g,y)} ->
	a:Sig.alg -> sign:bytes -> pv:ProtocolVersion ->
	b:bytes{?p,g,y. dheb = DHEParamBytes(p,g,y) /\
		b = ServerKeyExchangeMsg_DHE(pv,p,g,y,a,sign)}
val parseServerKeyExchange_DHE: pv:ProtocolVersion -> cs:cipherSuite ->
	b:bytes ->
	((p:DHGroup.p * g:(;p)DHGroup.elt * y:(;p)DHGroup.elt * a:Sig.alg * sign:bytes){
	MessageBytes(HT_server_key_exchange,b) =
		ServerKeyExchangeMsg_DHE(pv,p,g,y,a,sign)
	}) Result

function val ServerKeyExchangeMsg_DH_anon: bytes * bytes * bytes -> bytes

val serverKeyExchangeBytes_DH_anon: bytes -> bytes -> bytes -> bytes
val parseServerKeyExchange_DH_anon: bytes -> (bytes * bytes * bytes) Result

//function val CertificateVerifyMsg: si:SessionInfo * (;si)PRF.masterSecret * a:Sig.alg * Cert.chain * (;a)Sig.pkey * log -> bytes
function val CertificateVerifyMsg: ProtocolVersion * Sig.alg * bytes -> bytes
private definition !pv,a,sign.
		 CertificateVerifyMsg(pv,a,sign) = MessageBytes(HT_certificate_verify,DigitallySignedBytes(a,sign,pv))

val makeCertificateVerifyBytes: si:SessionInfo -> (;si)PRF.masterSecret -> a:Sig.alg -> k:(;a)Sig.skey ->
  l:log{Sig.Msg(a,Sig.PK(k),l)} ->
	b:bytes * sign:bytes{
	  b = CertificateVerifyMsg(si.protocol_version,a,sign)
	}
val certificateVerifyCheck: si:SessionInfo -> (;si)PRF.masterSecret -> al:Sig.alg list -> l:log -> payload:bytes ->
	b:bool * sign:bytes{
	  b = true => (?a.
		   MessageBytes(HT_certificate_verify,payload) = CertificateVerifyMsg(si.protocol_version,a,sign)
		/\ ((si.protocol_version <> SSL_3p0 /\ Sig.Strong(a) /\ Sig.Honest(a,Cert.SigPKCert(si.clientID,a))) =>
                    Sig.Msg(a,Cert.SigPKCert(si.clientID,a),l)))}

//function val ServerFinishedMsg: si:SessionInfo * (;si)PRF.masterSecret * log -> bytes
function val ServerFinishedMsg: sVerifyData -> bytes

private definition !svd. ServerFinishedMsg(svd) = MessageBytes(HT_finished,svd)

//function val ClientFinishedMsg: si:SessionInfo * (;si)PRF.masterSecret * log -> bytes
function val ClientFinishedMsg: cVerifyData -> bytes

private definition !svd. ClientFinishedMsg(svd) = MessageBytes(HT_finished,svd)

predicate ServerLogBeforeClientCertificateRSA of SessionInfo * ProtocolVersion * log
predicate ServerLogBeforeClientCertificateRSA_Auth of SessionInfo * ProtocolVersion * log
predicate ServerLogBeforeClientCertificateRSA_NoAuth of SessionInfo * ProtocolVersion * log

private definition !si,pv,l.
  ServerLogBeforeClientCertificateRSA_Auth(si,pv,l) <=>
  ((si.client_auth = true /\  ServerLogBeforeClientCertificateRSA_Auth(si,pv,l)) \/
   (si.client_auth = false /\  ServerLogBeforeClientCertificateRSA_NoAuth(si,pv,l)))

private definition !si,pv,l.
  ServerLogBeforeClientCertificateRSA_Auth(si,pv,l) <=>
  (?crand,cpv,csl,cml,csess,ex1,ex2,ctl,sal,nl.
    l = (ClientHelloMsg(cpv,crand,csess,csl,cml,ex1)  @|
        (ServerHelloMsg(si.protocol_version,si.init_srand,si.sessionID,si.cipher_suite,si.compression,ex2) @|
         CertificateMsg(si.serverID) @|
         CertificateRequestMsg(si.protocol_version,ctl,sal,nl) @|
         ServerHelloDoneMsg([||]))))

private definition !si,pv,l.
  ServerLogBeforeClientCertificateRSA_NoAuth(si,pv,l) <=>
  (?cs,cm,sess,ex1,ex2.
     l = (ClientHelloMsg(pv,si.init_crand,sess,cs,cm,ex1) @|
          (ServerHelloMsg(si.protocol_version,si.init_srand,si.sessionID,si.cipher_suite,si.compression,ex2) @|
          CertificateMsg(si.serverID) @|
          ServerHelloDoneMsg([||]))))

predicate ServerLogBeforeClientCertificateDHE of SessionInfo * log
predicate ServerLogBeforeClientCertificateDHE_Auth of SessionInfo * log
predicate ServerLogBeforeClientCertificateDHE_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeClientCertificateDHE_Auth(si,l) <=>
  ((si.client_auth = true /\  ServerLogBeforeClientCertificateDHE_Auth(si,l)) \/
   (si.client_auth = false /\  ServerLogBeforeClientCertificateDHE_NoAuth(si,l)))

private definition !si,l.
  ServerLogBeforeClientCertificateDHE_Auth(si,l) <=>
  (?crand,cpv,csl,cml,csess,ex1,ex2,ctl,sal,nl,p,g,y,a,sign.
    l = (ClientHelloMsg(cpv,crand,csess,csl,cml,ex1)  @|
        (ServerHelloMsg(si.protocol_version,si.init_srand,si.sessionID,si.cipher_suite,si.compression,ex2) @|
         CertificateMsg(si.serverID) @|
         ServerKeyExchangeMsg_DHE(si.protocol_version,p,g,y,a,sign) @|
         CertificateRequestMsg(si.protocol_version,ctl,sal,nl) @|
         ServerHelloDoneMsg([||]))))

private definition !si,l.
  ServerLogBeforeClientCertificateDHE_NoAuth(si,l) <=>
  (?pv,cs,cm,sess,ex1,ex2,p,g,y,a,sign.
     l = (ClientHelloMsg(pv,si.init_crand,sess,cs,cm,ex1) @|
          (ServerHelloMsg(si.protocol_version,si.init_srand,si.sessionID,si.cipher_suite,si.compression,ex2) @|
           ServerKeyExchangeMsg_DHE(si.protocol_version,p,g,y,a,sign) @|
           CertificateMsg(si.serverID) @|
           ServerHelloDoneMsg([||]))))

predicate ServerLogBeforeClientKeyExchangeRSA of SessionInfo * ProtocolVersion * log
predicate ServerLogBeforeClientKeyExchangeRSA_Auth of SessionInfo * ProtocolVersion * log
predicate ServerLogBeforeClientKeyExchangeRSA_NoAuth of SessionInfo * ProtocolVersion * log

private definition !si,pv,l.
  ServerLogBeforeClientKeyExchangeRSA(si,pv,l) <=>
  ((si.client_auth = true /\  ServerLogBeforeClientKeyExchangeRSA_Auth(si,pv,l)) \/
   (si.client_auth = false /\  ServerLogBeforeClientKeyExchangeRSA_NoAuth(si,pv,l)))

private definition !si,pv,l.
  ServerLogBeforeClientKeyExchangeRSA_Auth(si,pv,l) <=>
  (?si',l'. ServerLogBeforeClientCertificateRSA_Auth(si',pv,l') /\
        SessionHelloParams(si,()) = SessionHelloParams(si',()) /\
        l = l' @| CertificateMsg(si.clientID))

private definition !si,pv,l.
  ServerLogBeforeClientKeyExchangeRSA_NoAuth(si,pv,l) <=>
  ServerLogBeforeClientCertificateRSA_NoAuth(si,pv,l)

predicate ServerLogBeforeClientKeyExchangeDHE of SessionInfo * log
predicate ServerLogBeforeClientKeyExchangeDHE_Auth of SessionInfo * log
predicate ServerLogBeforeClientKeyExchangeDHE_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeClientKeyExchangeDHE(si,l) <=>
  ((si.client_auth = true /\  ServerLogBeforeClientKeyExchangeDHE_Auth(si,l)) \/
   (si.client_auth = false /\  ServerLogBeforeClientKeyExchangeDHE_NoAuth(si,l)))

private definition !si,pv,l.
  ServerLogBeforeClientKeyExchangeDHE_Auth(si,l) <=>
  (?si',l'. ServerLogBeforeClientCertificateDHE_Auth(si',l') /\
        SessionHelloParams(si,()) = SessionHelloParams(si',()) /\
        l = l' @| CertificateMsg(si.clientID))

private definition !si,pv,l.
  ServerLogBeforeClientKeyExchangeDHE_NoAuth(si,l) <=>
  ServerLogBeforeClientCertificateDHE_NoAuth(si,l)

predicate ServerLogBeforeClientCertificateVerifyRSA of SessionInfo * log
predicate ServerLogBeforeClientCertificateVerifyRSA_Auth of SessionInfo * log
predicate ServerLogBeforeClientCertificateVerifyRSA_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeClientCertificateVerifyRSA(si,l) <=>
  (?si',pv,l',encpms,pk. ServerLogBeforeClientKeyExchangeRSA(si',pv,l') /\
      SessionHelloParams(si,()) = SessionHelloParams(si',()) /\
(*      si'.pmsData = RSAPMS(pk,pv,encpms) /\ *)
      l = l' @| ClientKeyExchangeMsg_RSA(si.protocol_version,encpms))

predicate ServerLogBeforeClientCertificateVerifyDHE of SessionInfo * log
predicate ServerLogBeforeClientCertificateVerifyDHE_Auth of SessionInfo * log
predicate ServerLogBeforeClientCertificateVerifyDHE_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeClientCertificateVerifyDHE(si,l) <=>
  (?si',d,l'. ServerLogBeforeClientKeyExchangeDHE(si',l') /\
        SessionHelloParams(si,()) = SessionHelloParams(si',()) /\
(*      si'.pmsData = DHPMS(d) /\ *)
          l = l' @| ClientKeyExchangeMsg_DHE(d))

predicate ServerLogBeforeClientCertificateVerify of SessionInfo * log

private definition
 !si,l. ServerLogBeforeClientCertificateVerify(si,l) =>
  (ServerLogBeforeClientCertificateVerifyRSA(si,l) \/
   ServerLogBeforeClientCertificateVerifyDHE(si,l) \/
   (!a. si.cipher_suite <> CipherSuite(RSA,a) /\
        si.cipher_suite <> CipherSuite(DHE_RSA,a)))

private assume  !si,l.
    ServerLogBeforeClientCertificateVerifyRSA(si,l) =>
    ServerLogBeforeClientCertificateVerify(si,l)

private assume  !si,l.
    ServerLogBeforeClientCertificateVerifyDHE(si,l) =>
    ServerLogBeforeClientCertificateVerify(si,l)

predicate ServerLogBeforeClientFinishedRSA of SessionInfo * log
predicate ServerLogBeforeClientFinishedRSA_Auth of SessionInfo * log
predicate ServerLogBeforeClientFinishedRSA_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeClientFinishedRSA(si,l) <=>
  ((si.client_auth = true  /\ ServerLogBeforeClientFinishedRSA_Auth(si,l)) \/
  ((si.client_auth = false ) /\ ServerLogBeforeClientFinishedRSA_NoAuth(si,l)))

private definition !si,l.
  ServerLogBeforeClientFinishedRSA_Auth(si,l) <=>
  (?l',a,sign. ServerLogBeforeClientCertificateVerifyRSA(si,l') /\
   (l = l' @| CertificateVerifyMsg(si.protocol_version,a,sign)))

private definition !si,l.
  ServerLogBeforeClientFinishedRSA_NoAuth(si,l) <=>
  ServerLogBeforeClientCertificateVerifyRSA(si,l)

predicate ServerLogBeforeClientFinishedDHE of SessionInfo * log
predicate ServerLogBeforeClientFinishedDHE_Auth of SessionInfo * log
predicate ServerLogBeforeClientFinishedDHE_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeClientFinishedDHE(si,l) <=>
  ((si.client_auth = true  /\ ServerLogBeforeClientFinishedDHE_Auth(si,l)) \/
   ((si.client_auth = false ) /\ ServerLogBeforeClientFinishedDHE_NoAuth(si,l)))

private definition !si,l.
  ServerLogBeforeClientFinishedDHE_Auth(si,l) <=>
  (?l',a,sign. ServerLogBeforeClientCertificateVerifyDHE(si,l') /\
   (l = l' @| CertificateVerifyMsg(si.protocol_version,a,sign)))

private definition !si,l.
  ServerLogBeforeClientFinishedDHE_NoAuth(si,l) <=>
  ServerLogBeforeClientCertificateVerifyDHE(si,l)

predicate ServerLogBeforeClientFinished of SessionInfo * log
predicate ServerLogBeforeClientFinished_Auth of SessionInfo * log
predicate ServerLogBeforeClientFinished_NoAuth of SessionInfo * log
private definition
 !si,l. ServerLogBeforeClientFinished(si,l) <=>
  ((si.client_auth = true  /\ ServerLogBeforeClientFinished_Auth(si,l)) \/
  ((si.client_auth = false  ) /\ ServerLogBeforeClientFinished_NoAuth(si,l)))

private definition !si,l.
  ServerLogBeforeClientFinished_Auth(si,l) <=>
  (?l',a,sign. ServerLogBeforeClientCertificateVerify(si,l') /\
   (l = l' @| CertificateVerifyMsg(si.protocol_version,a,sign)))

private definition !si,l.
  ServerLogBeforeClientFinished_NoAuth(si,l) <=>
  ServerLogBeforeClientCertificateVerify(si,l)

predicate ServerLogBeforeServerFinishedRSA of SessionInfo * log
predicate ServerLogBeforeServerFinishedRSA_Auth of SessionInfo * log
predicate ServerLogBeforeServerFinishedRSA_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeServerFinishedRSA(si,l) <=>
  ((si.client_auth = true /\ ServerLogBeforeServerFinishedRSA_Auth(si,l)) \/
   (si.client_auth = false /\ ServerLogBeforeServerFinishedRSA_NoAuth(si,l)))

private definition !si,l.
  ServerLogBeforeServerFinishedRSA_Auth(si,l) <=>
  (?l',cvd. ServerLogBeforeClientFinishedRSA_Auth(si,l') /\
   (l' = l @| ClientFinishedMsg(cvd)))

private definition !si,l.
  ServerLogBeforeServerFinishedRSA_NoAuth(si,l) <=>
  (?l',cvd. ServerLogBeforeClientFinishedRSA_NoAuth(si,l') /\
   (l' = l @| ClientFinishedMsg(cvd)))

predicate ServerLogBeforeServerFinishedDHE of SessionInfo * log
predicate ServerLogBeforeServerFinishedDHE_Auth of SessionInfo * log
predicate ServerLogBeforeServerFinishedDHE_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ServerLogBeforeServerFinishedDHE(si,l) <=>
  ((si.client_auth = true /\ ServerLogBeforeServerFinishedDHE_Auth(si,l)) \/
   (si.client_auth = false /\ ServerLogBeforeServerFinishedDHE_NoAuth(si,l)))

private definition !si,l.
  ServerLogBeforeServerFinishedDHE_Auth(si,l) <=>
  (?l',cvd. ServerLogBeforeClientFinishedDHE_Auth(si,l') /\
   (l' = l @| ClientFinishedMsg(cvd)))

private definition !si,l.
  ServerLogBeforeServerFinishedDHE_NoAuth(si,l) <=>
  (?l',cvd. ServerLogBeforeClientFinishedDHE_NoAuth(si,l') /\
   (l' = l @| ClientFinishedMsg(cvd)))

predicate ServerLogBeforeServerFinished of SessionInfo * log
private definition
 !si,l. ServerLogBeforeServerFinished(si,l) <=>
  ((?a. si.cipher_suite = CipherSuite(RSA,a) /\ ServerLogBeforeServerFinishedRSA(si,l)) \/
   (?a. si.cipher_suite = CipherSuite(DHE_RSA,a) /\
       ServerLogBeforeServerFinishedDHE(si,l)) \/
   (!a. si.cipher_suite <> CipherSuite(RSA,a) /\
        si.cipher_suite <> CipherSuite(DHE_RSA,a)))

predicate ClientLogBeforeServerHello of random * log
predicate ClientLogBeforeServerCertificate of SessionInfo * log

private definition !cr,sid,l.
  ClientLogBeforeServerHello(cr,l) <=>
  (?pv,csid,cs,cm,ex1. l = ClientHelloMsg(pv,cr,sid,cs,cm,ex1))

ask !pv,cs,cm,ex1,cr,sid. ClientLogBeforeServerHello(cr,ClientHelloMsg(pv,cr,sid,cs,cm,ex1))

private definition !si,l.
  ClientLogBeforeServerCertificate(si,l) <=>
  (?l',cr,ex2.
     ClientLogBeforeServerHello(cr,l') /\
     l = l' @|
     ServerHelloMsg(si.protocol_version,si.init_srand,si.sessionID,si.cipher_suite,si.compression,ex2))

predicate ClientLogBeforeCertificateRequestRSA of SessionInfo * log
private definition !si,pv,l.
  ClientLogBeforeCertificateRequestRSA(si,l) <=>
  (?l'. ClientLogBeforeServerCertificate(si,l') /\
     l = l @| CertificateMsg(si.serverID))

predicate ClientLogBeforeServerKeyExchangeDHE of SessionInfo * log
private definition !si,pv,l.
  ClientLogBeforeServerKeyExchangeDHE(si,l) <=>
  (?l'. ClientLogBeforeServerCertificate(si,l') /\
     l = l @| CertificateMsg(si.serverID))

predicate ClientLogBeforeCertificateRequestDHE of SessionInfo * log
private definition !si,pv,l.
  ClientLogBeforeCertificateRequestDHE(si,l) <=>
  (?l',p,g,y,a,sign. ClientLogBeforeServerKeyExchangeDHE(si,l') /\
     l = l @| ServerKeyExchangeMsg_DHE(pv,p,g,y,a,sign))

predicate ClientLogBeforeServerHelloDoneRSA of SessionInfo * log
predicate ClientLogBeforeServerHelloDoneRSA_Auth of SessionInfo * log
predicate ClientLogBeforeServerHelloDoneRSA_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ClientLogBeforeServerHelloDoneRSA(si,l) <=>
  ((si.client_auth = true /\ ClientLogBeforeServerHelloDoneRSA_Auth(si,l)) \/
   (si.client_auth = false /\ ClientLogBeforeServerHelloDoneRSA_NoAuth(si,l)))

private definition !si,pv,l.
  ClientLogBeforeServerHelloDoneRSA_Auth(si,l) <=>
  (?l',ctl,sal,nl. ClientLogBeforeCertificateRequestRSA(si,l) /\
     l = CertificateRequestMsg(si.protocol_version,ctl,sal,nl))

private definition !si,pv,l.
  ClientLogBeforeServerHelloDoneRSA_NoAuth(si,l) <=>
  ClientLogBeforeCertificateRequestRSA(si,l)

predicate ClientLogBeforeServerHelloDoneDHE of SessionInfo * log
predicate ClientLogBeforeServerHelloDoneDHE_Auth of SessionInfo * log
predicate ClientLogBeforeServerHelloDoneDHE_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ClientLogBeforeServerHelloDoneDHE(si,l) <=>
  ((si.client_auth = true /\ ClientLogBeforeServerHelloDoneDHE_Auth(si,l)) \/
   (si.client_auth = false /\ ClientLogBeforeServerHelloDoneDHE_NoAuth(si,l)))

private definition !si,pv,l.
  ClientLogBeforeServerHelloDoneDHE_Auth(si,l) <=>
  (?l',ctl,sal,nl. ClientLogBeforeCertificateRequestDHE(si,l) /\
     l = CertificateRequestMsg(si.protocol_version,ctl,sal,nl))

private definition !si,pv,l.
  ClientLogBeforeServerHelloDoneDHE_NoAuth(si,l) <=>
  ClientLogBeforeCertificateRequestDHE(si,l)

predicate ClientLogBeforeCertificateVerifyRSA_Auth of SessionInfo * log

private definition !si,pv,l.
  ClientLogBeforeCertificateVerifyRSA_Auth(si,l) <=>
  (?l',encpms. ClientLogBeforeServerHelloDoneRSA_Auth(si,l') /\
     l = l' @| ServerHelloDoneMsg([||])
         @| CertificateMsg(si.clientID)
         @| ClientKeyExchangeMsg_RSA(si.protocol_version,encpms))

predicate ClientLogBeforeCertificateVerifyDHE_Auth of SessionInfo * log

private definition !si,pv,l.
  ClientLogBeforeCertificateVerifyDHE_Auth(si,l) <=>
  (?l',b. ClientLogBeforeServerHelloDoneDHE_Auth(si,l') /\
     l = l' @| ServerHelloDoneMsg([||])
         @| CertificateMsg(si.clientID)
         @| ClientKeyExchangeMsg_DHE(b))

predicate ClientLogBeforeClientFinishedRSA of SessionInfo * log
predicate ClientLogBeforeClientFinishedRSA_Auth of SessionInfo * log
predicate ClientLogBeforeClientFinishedRSA_TryNoAuth of SessionInfo * log
predicate ClientLogBeforeClientFinishedRSA_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ClientLogBeforeClientFinishedRSA(si,l) <=>
  ((si.client_auth = true /\ si.clientID <> [] /\ ClientLogBeforeClientFinishedRSA_Auth(si,l)) \/
   (si.client_auth = true /\ si.clientID = [] /\ ClientLogBeforeClientFinishedRSA_TryNoAuth(si,l)) \/
   (si.client_auth = false /\ ClientLogBeforeClientFinishedRSA_NoAuth(si,l)))

private definition !si,pv,l.
  ClientLogBeforeClientFinishedRSA_Auth(si,l) <=>
  (?l',encpms,a,sign. ClientLogBeforeCertificateVerifyRSA_Auth(si,l') /\
     l = l'
         @| CertificateVerifyMsg(si.protocol_version,a,sign))

private definition !si,pv,l.
  ClientLogBeforeClientFinishedRSA_TryNoAuth(si,l) <=>
  (?l',l'',encpms. ClientLogBeforeServerHelloDoneRSA_Auth(si,l') /\
     l = l' @| ServerHelloDoneMsg([||])
         @| CertificateMsg(si.clientID)
         @| ClientKeyExchangeMsg_RSA(si.protocol_version,encpms))

private definition !si,pv,l.
  ClientLogBeforeClientFinishedRSA_NoAuth(si,l) <=>
  (?l',encpms. ClientLogBeforeServerHelloDoneRSA_NoAuth(si,l') /\
     l = l' @| ServerHelloDoneMsg([||])
         @| ClientKeyExchangeMsg_RSA(si.protocol_version,encpms))

predicate ClientLogBeforeClientFinishedDHE of SessionInfo * log
predicate ClientLogBeforeClientFinishedDHE_Auth of SessionInfo * log
predicate ClientLogBeforeClientFinishedDHE_TryNoAuth of SessionInfo * log
predicate ClientLogBeforeClientFinishedDHE_NoAuth of SessionInfo * log

private definition !si,pv,l.
  ClientLogBeforeClientFinishedDHE(si,l) <=>
  ((si.client_auth = true /\ si.clientID <> [] /\ ClientLogBeforeClientFinishedDHE_Auth(si,l)) \/
   (si.client_auth = true /\ si.clientID = [] /\ ClientLogBeforeClientFinishedDHE_TryNoAuth(si,l)) \/
   (si.client_auth = false /\ ClientLogBeforeClientFinishedDHE_NoAuth(si,l)))

private definition !si,pv,l.
  ClientLogBeforeClientFinishedDHE_Auth(si,l) <=>
  (?l',encpms,a,sign. ClientLogBeforeCertificateVerifyDHE_Auth(si,l') /\
     l = l'
         @| CertificateVerifyMsg(si.protocol_version,a,sign))

private definition !si,pv,l.
  ClientLogBeforeClientFinishedDHE_TryNoAuth(si,l) <=>
  (?l',l'',b. ClientLogBeforeServerHelloDoneDHE_Auth(si,l') /\
     l = l' @| ServerHelloDoneMsg([||])
         @| CertificateMsg(si.clientID)
         @| ClientKeyExchangeMsg_DHE(b))

private definition !si,pv,l.
  ClientLogBeforeClientFinishedDHE_NoAuth(si,l) <=>
  (?l',b. ClientLogBeforeServerHelloDoneDHE_NoAuth(si,l') /\
     l = l' @| ServerHelloDoneMsg([||])
         @| ClientKeyExchangeMsg_DHE(b))

predicate ClientLogBeforeClientFinished of SessionInfo * log
private definition
 !si,l. ClientLogBeforeClientFinished(si,l) <=>
  ((?a. si.cipher_suite = CipherSuite(RSA,a) /\ ClientLogBeforeClientFinishedRSA(si,l)) \/
   (?a. si.cipher_suite = CipherSuite(DHE_RSA,a) /\
   ClientLogBeforeClientFinishedDHE(si,l)) \/
   (!a. si.cipher_suite <> CipherSuite(RSA,a) /\
        si.cipher_suite <> CipherSuite(DHE_RSA,a)))

predicate ClientLogBeforeServerFinished of SessionInfo * log
private definition !si,l.
  ClientLogBeforeServerFinished(si,l) <=>
  (?l',cvd. ClientLogBeforeClientFinished(si,l') /\
     l = l' @| ClientFinishedMsg(cvd))

predicate ServerLogBeforeServerFinishedResume of SessionInfo * log
private definition !si,l.
  ServerLogBeforeServerFinishedResume(si,l) <=>
  (?crand,cpv,csl,cml,ex1,ex2,ctl,sal,nl.
    l = (ClientHelloMsg(cpv,crand,si.sessionID,csl,cml,ex1)  @|
        (ServerHelloMsg(si.protocol_version,si.init_srand,si.sessionID,si.cipher_suite,si.compression,ex2))))

predicate ServerLogBeforeClientFinishedResume of SessionInfo * log
private definition !si,l.
  ServerLogBeforeClientFinishedResume(si,l) <=>
  (?l',svd.   ServerLogBeforeServerFinishedResume(si,l') /\
    l = l' @| ServerFinishedMsg(svd))

predicate ClientLogBeforeServerFinishedResume of SessionInfo * log
private definition !si,l.
  ClientLogBeforeServerFinishedResume(si,l) <=>
  (?crand,cpv,csl,cml,ex1,ex2,ctl,sal,nl.
    l = (ClientHelloMsg(cpv,crand,si.sessionID,csl,cml,ex1)  @|
        (ServerHelloMsg(si.protocol_version,si.init_srand,si.sessionID,si.cipher_suite,si.compression,ex2))))

predicate ClientLogBeforeClientFinishedResume of SessionInfo * log
private definition !si,l.
  ClientLogBeforeClientFinishedResume(si,l) <=>
  (?l',svd.   ClientLogBeforeServerFinishedResume(si,l') /\
    l = l' @| ServerFinishedMsg(svd))

predicate Configure of Role * epoch * config
predicate Authorize of Role * SessionInfo
// If the user Authorize, we can put the session in the DB
private definition !r,si. Authorize(r,si) => SessionDB.Authorize(r,si)
// If we select a session from the DB, the user previously authorized it
private theorem !r,si. SessionDB.Authorize(r,si) => Authorize(r,si)

predicate SentCCS of Role * epoch (* CCS will be sent multiple times,
                                     one for each epoch *)
predicate EvSentFinishedFirst of ConnectionInfo * bool
predicate Negotiated of Role * SessionInfo * config * config
predicate CompleteEpoch of Role * epoch * config
predicate Complete of ConnectionInfo * config

val check_negotiation: r:Role -> si:SessionInfo -> cfg:config -> unit{?cfg'. Negotiated(r,si,cfg,cfg')}

(* Anonymous clients are authorized for client-unauthenticated sessions *)
private assume !si. (si.client_auth = false /\ si.clientID = []) => Authorize(Server,si)
private assume !r,si,si'. Authorize(Client,si) /\ SessionHelloParams(si,()) =
  SessionHelloParams(si',()) /\ si'.serverID = si.serverID => Authorize(Client,si')

private assume !r,si,si'. Authorize(Server,si) /\ SessionHelloParams(si,()) =
  SessionHelloParams(si',()) /\ si'.serverID = si.serverID /\ si'.clientID = si.clientID /\ si'.client_auth = si.client_auth => Authorize(Server,si')

private definition !a,k,t. Sig.Msg(a,k,t)
  <=> ((?si,pk,pv,e.
             ClientLogBeforeCertificateVerifyRSA_Auth(si,t) /\
             si.pmsData = RSAPMS(pk,pv,e) /\
             HonestRSAPMS(pk,pv,e) /\
             k = Cert.SigPKCert(si.clientID,a)) \/
        (?si,p,g,gx,gy.
           ClientLogBeforeCertificateVerifyDHE_Auth(si,t) /\
           si.pmsData = DHPMS(p,g,gx,gy) /\
           DH.HonestExponent(p,g,gy) => HonestDHPMS(p,g,gx,gy) /\
           k = Cert.SigPKCert(si.clientID,a)) \/
        (?si,p,g,gy. t = si.init_crand @| si.init_srand @|
           DHEParamBytes(p,g,gy) /\
           DH.HonestExponent(p,g,gy) /\
           k = Cert.SigPKCert(si.serverID,a)))

private definition !e,r,b. PRF.VerifyData(e,r,b)

<=> ((r = Client /\
        Authorize(Client,EpochSI(e)) /\
        SentCCS(Client,e) /\
        ClientLogBeforeClientFinished(EpochSI(e),b)) \/
       (r = Server /\
        Authorize(Server,EpochSI(e)) /\
        SentCCS(Server,e) /\
        ServerLogBeforeServerFinished(EpochSI(e),b)) \/
       (r = Client /\
        Authorize(Client,EpochSI(e)) /\
        SentCCS(Client,e) /\
        ClientLogBeforeClientFinishedResume(EpochSI(e),b)) \/
       (r = Server /\
        Authorize(Server,EpochSI(e)) /\
        SentCCS(Server,e) /\
        ServerLogBeforeServerFinishedResume(EpochSI(e),b)))

private definition !role,e,cfg.
  CompleteEpoch(role,e,cfg)

<=>
  ((StrongHS(EpochSI(e)) /\ HonestPMS(EpochSI(e).pmsData) =>
              (Authorize(Client,EpochSI(e)) /\
               Authorize(Server,EpochSI(e)) /\
               SentCCS(Client,e) /\
               SentCCS(Server,e) /\
               (?cfgPeer. Negotiated(role,EpochSI(e),cfg,cfgPeer))
              )) /\
   ((EpochSI(e).client_auth = true /\
     (?a. Sig.Honest(a,Cert.SigPKCert(EpochSI(e).clientID,a))) /\
     (?a. Sig.Honest(a,Cert.SigPKCert(EpochSI(e).serverID,a))) /\
     RSAKey.Honest(Cert.RSAPKCert(EpochSI(e).serverID)))
    => HonestPMS(EpochSI(e).pmsData)))

(* Negotiated remains to be defined but it can be a nice global spec of what HS is meant to achieve.
   Especially interesting would be proving that the result is the "best possible" *)

definition !ci,cfg. Complete(ci,cfg) <=>
        ( IsSuccEpoch(ci.id_in) /\ IsSuccEpoch(ci.id_out) /\
		  EpochSI(ci.id_in) = EpochSI(ci.id_out) /\
          CompleteEpoch(ci.role,ci.id_in,cfg))

type (;ci:ConnectionInfo) serverState =  (* note that the CertRequest bits are determined by the config *)
                    (* we may omit some ProtocolVersion, mostly a ghost variable *)
   | ClientHello                  of cVerifyData * sVerifyData

| ClientCertificateRSA         of (si:SessionInfo * pv:ProtocolVersion * sk:RSAKey.sk * l:log){ServerLogBeforeClientCertificateRSA(si,pv,l)}
   | ServerCheckingCertificateRSA of (si:SessionInfo * pv:ProtocolVersion * sk:RSAKey.sk * l:log * certs:Cert.chain * b:bytes){ServerLogBeforeClientCertificateRSA(si,pv,l) /\ b = CertificateMsg(certs)}
   | ClientKeyExchangeRSA         of (si:SessionInfo * pv:ProtocolVersion * sk:RSAKey.sk * l:log){ServerLogBeforeClientKeyExchangeRSA(si,pv,l) /\ Authorize(Server,si)}

| ClientCertificateDH          of si:SessionInfo * l:log
   | ServerCheckingCertificateDH  of si:SessionInfo * l:log * b:bytes
   | ClientKeyExchangeDH          of si:SessionInfo * l:log

| ClientCertificateDHE         of si:SessionInfo * p:DHGroup.p * g:(;p)DHGroup.g * gx:(;p)DHGroup.elt * (;p,g,gx)DH.secret * l:log{
       ServerLogBeforeClientCertificateDHE(si,l)}

| ServerCheckingCertificateDHE of si:SessionInfo * p:DHGroup.p * g:(;p)DHGroup.g * gx:(;p)DHGroup.elt * (;p,g,gx)DH.secret * l:log * c:Cert.chain * b:bytes{
       ServerLogBeforeClientCertificateDHE(si,l) /\
       b = CertificateMsg(c)}

| ClientKeyExchangeDHE         of si:SessionInfo * p:DHGroup.p * g:(;p)DHGroup.g * gx:(;p)DHGroup.elt * (;p,g,gx)DH.secret * l:log{
       ServerLogBeforeClientKeyExchangeDHE(si,l) /\ Authorize(Server,si)}

| ClientKeyExchangeDH_anon     of SessionInfo * p:DHGroup.p * g:(;p)DHGroup.g * gx:(;p)DHGroup.elt * (;p,g,gx)DH.secret * log

| CertificateVerify            of (si:SessionInfo * (;si)PRF.masterSecret * l:log){si.client_auth = true /\ ServerLogBeforeClientCertificateVerify(si,l) /\ Authorize(Server,si)}
   | ClientCCS                    of (si:SessionInfo * (;si)PRF.masterSecret * l:log){ServerLogBeforeClientFinished(si,l) /\ Authorize(Server,si)}
   | ClientFinished               of (si:SessionInfo * (;si)PRF.masterSecret * e:succEpoch * (;e)StatefulLHAE.writer * l:log){
       IsSuccEpoch(ci.id_in) /\ EpochSI(e)=si /\ ServerLogBeforeClientFinished(si,l) /\ Authorize(Server,si)}
   (* by convention, the parameters are named si, cv, cr', sr', ms, log *)
   | ServerWritingCCS             of (si:SessionInfo * (;si)PRF.masterSecret * e:succEpoch * (;e)StatefulLHAE.writer * cv:cVerifyData * l:log){
                                       EpochSI(e)=si /\ ServerLogBeforeServerFinished(si,l) /\
         (* PRF.VerifyData(e,Client,cv) /\ *)
         Authorize(Server,si)}
   | ServerWritingFinished        of si:SessionInfo * (;si)PRF.masterSecret * e:succEpoch * cv:cVerifyData * sv:sVerifyData{
       EpochSI(e)=si /\
         (* PRF.VerifyData(e,Client,cv) /\ PRF.VerifyData(e,Server,sv) /\ *)
         Authorize(Server,si)}

| ServerWritingCCSResume       of (ew:succEpoch * (;ew)StatefulLHAE.writer * er:succEpoch * (;er)StatefulLHAE.reader * (;epochSI(ew))PRF.masterSecret * l:log){EpochSI(ew)=EpochSI(er) /\ ServerLogBeforeServerFinishedResume(EpochSI(ew),l) /\ Authorize(Server,EpochSI(ew))}
   | ClientCCSResume              of e:succEpoch * (;e)StatefulLHAE.reader * sVerifyData * (;EpochSI(e))PRF.masterSecret * l:log{ServerLogBeforeClientFinishedResume(EpochSI(e),l) /\ ci.id_in = Pred(e) /\ Authorize(Server,EpochSI(e))}
   | ClientFinishedResume         of si:SessionInfo * (;si)PRF.masterSecret * e:succEpoch * sv:sVerifyData * log{
       EpochSI(e)=si /\
(* PRF.VerifyData(e,Server,sv) /\ *)
         Authorize(Server,EpochSI(e))}

| ServerIdle                   of cVerifyData * sVerifyData
   (* the ProtocolVersion is the highest TLS version proposed by the client *)

type (;ci:ConnectionInfo) clientState =
   | ServerHello                  of cr:crand * sid:sessionID (* * bytes for extensions? *) * cvd:cVerifyData * svd:sVerifyData * l:log{ClientLogBeforeServerHello(cr,l)}

| ServerCertificateRSA         of si:SessionInfo * l:log{ClientLogBeforeServerCertificate(si,l)}
   | ClientCheckingCertificateRSA of si:SessionInfo * l:log * ser:Cert.cert list * pv:ProtocolVersion option * b:bytes{ClientLogBeforeServerCertificate(si,l) /\ b = CertificateMsg(ser)}
   | CertificateRequestRSA        of si:SessionInfo * l:log{ClientLogBeforeCertificateRequestRSA(si,l) /\ Authorize(Client,si)} (* both certificate request and hellodone will be accepted *)
   | ServerHelloDoneRSA           of si:SessionInfo * c:Cert.sign_cert * l:log{ClientLogBeforeServerHelloDoneRSA(si,l) /\ Authorize(Client,si)}

| ServerCertificateDHE         of si:SessionInfo * l:log{ClientLogBeforeServerCertificate(si,l)}
   | ClientCheckingCertificateDHE of si:SessionInfo * l:log * ProtocolVersion option * b:bytes{ClientLogBeforeServerCertificate(si,l) (* /\ b = CertificateMsg(ser) *) }
   | ServerKeyExchangeDHE         of si:SessionInfo * l:log{ClientLogBeforeServerKeyExchangeDHE(si,l) /\ Authorize(Client,si)}
   | CertificateRequestDHE        of si:SessionInfo * p:DHGroup.p * g:(;p)DHGroup.g * gx:(;p)DHGroup.elt * l:log{ClientLogBeforeCertificateRequestDHE(si,l) /\ Authorize(Client,si)}
   | ServerHelloDoneDHE           of si:SessionInfo * Cert.sign_cert * p:DHGroup.p * g:(;p)DHGroup.g * gx:(;p)DHGroup.elt * l:log{ClientLogBeforeServerHelloDoneDHE(si,l) /\ Authorize(Client,si)}

| ServerKeyExchangeDH_anon of SessionInfo * log (* Not supported yet *)
   | ServerHelloDoneDH_anon of SessionInfo * p:DHGroup.p * g:(;p)DHGroup.g * gx:(;p)DHGroup.elt * log

| ClientWritingCCS       of si:SessionInfo * (;si)PRF.masterSecret * l:log{ClientLogBeforeClientFinished(si,l) /\ Authorize(Client,si)}
   | ServerCCS              of (si:SessionInfo * (;si)PRF.masterSecret * e:succEpoch * (;e)StatefulLHAE.reader * cv:cVerifyData * l:log){ EpochSI(e)=si  /\ ClientLogBeforeServerFinished(si,l) /\
         ci.id_in = Pred(e) /\
         (* PRF.VerifyData(e,Client,cv) /\ *)
         Authorize(Client,si)}
   | ServerFinished         of si:SessionInfo * (;si)PRF.masterSecret * e:succEpoch * cv:cVerifyData * l:log{ClientLogBeforeServerFinished(si,l) /\
                                                                                                               EpochSI(e)=si  /\
         (* ci.id_in = Pred(e) /\ *)
         (* PRF.VerifyData(e,Client,cv) /\ *)
         Authorize(Client,si)}

| ServerCCSResume        of (ew:succEpoch * (;ew)StatefulLHAE.writer * er:succEpoch * (;er)StatefulLHAE.reader * (;EpochSI(ew))PRF.masterSecret * l:log){EpochSI(ew)=EpochSI(er) /\ ci.id_in = Pred(er) /\ ClientLogBeforeServerFinishedResume(EpochSI(ew),l) /\ Authorize(Client,EpochSI(ew))}
   | ServerFinishedResume   of e:succEpoch * (;e)StatefulLHAE.writer * (;EpochSI(e))PRF.masterSecret * l:log{ClientLogBeforeServerFinishedResume(EpochSI(e),l) /\ Authorize(Client,EpochSI(e))}
   | ClientWritingCCSResume of e:succEpoch * w:(;e)StatefulLHAE.writer * (;EpochSI(e))PRF.masterSecret * sv:sVerifyData * l:log{ClientLogBeforeClientFinishedResume(EpochSI(e),l) /\ (* PRF.VerifyData(e,Server,sv) /\ *)
Authorize(Client,EpochSI(e)) /\
ci.id_out = Pred(e) /\
         StatefulLHAE.History(e,StatefulLHAE.WriterState,w) =
         StatefulPlain.EmptyHistory(e) }
   | ClientWritingFinishedResume of cVerifyData * sVerifyData

| ClientIdle             of cVerifyData * sVerifyData

type (;ci:ConnectionInfo) protoState = // Cannot use Client and Server, otherwise clashes with Role
  | PSClient of (;ci) clientState
  | PSServer of (;ci) serverState

val clientState: ci:ConnectionInfo -> c:(;ci) clientState -> p:(;ci) protoState{p = PSClient(c)}
val serverState: ci:ConnectionInfo -> c:(;ci) serverState -> p:(;ci) protoState{p = PSServer(c)}

private type (;ci:ConnectionInfo) hs_state = {
  (* I/O buffers *)
  hs_outgoing    : bytes;                  (* outgoing data *)
  hs_incoming    : bytes;                  (* partial incoming HS message *)
  (* local configuration *)
  poptions: config;
  sDB: SessionDB.SessionDB;
  (* current handshake & session we are establishing *)
  pstate: (;ci) protoState;
}

(*--- controlinterface *)
(* Control Interface *)

function val Config: ci:ConnectionInfo * s:(;ci)hs_state -> config
private definition !ci,s. Config(ci,s) = s.poptions

type (;ci:ConnectionInfo,c:config) nextState = s:(;ci)hs_state {Config(ci,s) = c}

val init:  rl:Role  -> c:config  ->
	(ci:ConnectionInfo * s:(;ci)hs_state){Config(ci,s) = c /\
                ci.role = rl /\
		IsInitEpoch(ci.id_in) /\
		IsInitEpoch(ci.id_out)}

val resume: nextSID:sessionID -> c:config  ->
	(ci:ConnectionInfo * s:(;ci)hs_state){ Config(ci,s) = c /\
                ci.role = Client /\
		IsInitEpoch(ci.id_in) /\
		IsInitEpoch(ci.id_out)}

val rehandshake: ci:ConnectionInfo -> s:(;ci)hs_state -> c:config  ->
	b:bool * s':(;ci)hs_state{
		((b = true /\ Config(ci,s') = c) \/
                 (b = false /\ Config(ci,s') = Config(ci,s)))}

val rekey: ci:ConnectionInfo -> s:(;ci)hs_state -> c:config  ->
	   b:bool * s':(;ci)hs_state{((b = true /\ Config(ci,s') = c) \/ (b = false /\ Config(ci,s') = Config(ci,s)))}

val request:     ci:ConnectionInfo -> s:(;ci)hs_state -> c:config  ->
                 b:bool * s':(;ci)hs_state{
		((b = true /\ Config(ci,s') = c) \/ (b = false /\ Config(ci,s') = Config(ci,s)))}

val getPrincipal:  ci:ConnectionInfo -> s:(;ci)hs_state -> string
val invalidateSession: ci:ConnectionInfo -> s:(;ci)hs_state -> s':(;ci,Config(ci,s))nextState
(*{SameStreams(ci,s,s')} *)

val getNextEpochs: ci:ConnectionInfo -> si:SessionInfo -> crand -> srand -> ci':ConnectionInfo{
    IsSuccEpoch(ci'.id_in) /\
    IsSuccEpoch(ci'.id_out) /\
    EpochSI(ci'.id_in) = si /\
    EpochSI(ci'.id_out) = si /\
    ci.id_out = Pred(ci'.id_out) /\
    ci.id_in = Pred(ci'.id_in) /\
    ci.role = ci'.role
}

(*--- networkinterface *)
(* Network Interface*)

type (;ci:ConnectionInfo, hs:(;ci) hs_state) outgoing =
  | OutIdle of s':(;ci,Config(ci,hs))nextState
  | OutSome of (rg:range * f:(;ci.id_out,HSFragment.EmptyStream(ci.id_out),rg)HSFragment.plain * s':(;ci,Config(ci,hs))nextState)
  | OutCCS of  (rg:range * f:(;ci.id_out,HSFragment.EmptyStream(ci.id_out),rg)HSFragment.plain *
               ci':ConnectionInfo * cs:(;ci'.id_out,StatefulLHAE.WriterState)StatefulLHAE.state * s':(;ci',Config(ci,hs))nextState)
               { StatefulLHAE.History(ci'.id_out,StatefulLHAE.WriterState,cs) = StatefulPlain.EmptyHistory(ci'.id_out) /\
                 ci.id_out = Pred(ci'.id_out) /\ IsSuccEpoch(ci'.id_out) /\
                 ci.id_in = ci'.id_in /\
                 ci.role = ci'.role /\
				 ci.id_rand = ci'.id_rand}
  | OutFinished of (rg:range * f:(;ci.id_out,HSFragment.EmptyStream(ci.id_out),rg)HSFragment.plain * s':(;ci,Config(ci,hs))nextState){
				EvSentFinishedFirst(ci,true)}
  | OutComplete of (rg:range * f:(;ci.id_out,HSFragment.EmptyStream(ci.id_out),rg)HSFragment.plain * s':(;ci,Config(ci,hs))nextState)
                   {Complete(ci,Config(ci,hs))}
val next_fragment: ci:ConnectionInfo -> s:(;ci)hs_state -> (;ci,s)outgoing

type (;ci:ConnectionInfo,c:config)incoming =
  | InAck of (;ci,c)nextState
  | InVersionAgreed  of (;ci,c)nextState * ProtocolVersion
  | InQuery of Cert.chain * advice:bool * (;ci,c)nextState
  | InFinished of (;ci,c)nextState {EvSentFinishedFirst(ci,false)}
  | InComplete of (;ci,c)nextState {Complete(ci,c)}
  | InError of alertDescription * string * (;ci,c)nextState
val recv_fragment: ci:ConnectionInfo -> s:(;ci)hs_state -> rg:range -> (;ci.id_in,rg)HSFragment.fragment ->
                   (;ci,Config(ci,s))incoming
val authorize:     ci:ConnectionInfo -> s:(;ci)hs_state ->
                   c:Cert.chain -> (;ci,Config(ci,s))incoming

type (;ci:ConnectionInfo,c:config)incomingCCS =
  | InCCSAck of ci':ConnectionInfo * (;ci'.id_in,StatefulLHAE.ReaderState)StatefulLHAE.state * (;ci',c)nextState
				{ci.id_out = ci'.id_out /\ ci.id_in = Pred(ci'.id_in)}
  | InCCSError of alertDescription * string * (;ci,c)nextState
val recv_ccs     : ci:ConnectionInfo -> s:(;ci)hs_state -> rg:range -> (;ci.id_in,rg)HSFragment.fragment ->
                   (;ci,Config(ci,s))incomingCCS

function val GetMinVersion: ci:ConnectionInfo * (;ci)hs_state -> ProtocolVersion
private definition !ci,s. GetMinVersion(ci,s) = s.poptions.minVer
val getMinVersion: ci:ConnectionInfo -> s:(;ci)hs_state ->
	pv:ProtocolVersion{pv = GetMinVersion(ci,s)}

(*--- end *)

(* INTERNAL HS VERIFICATION (ALL THESE DEFS ARE PRIVATE) *)

val find_client_cert_sign: certType list -> Sig.alg list -> string list ->
	ProtocolVersion -> Cert.hint -> Cert.sign_cert
val getCertificateBytes: si:SessionInfo ->
  cert_req:(Cert.chain * a:Sig.alg * (;a)Sig.skey) option ->
  (b:bytes * cl:Cert.chain){
    (si.client_auth = true /\  b = CertificateMsg(cl)) \/
    (si.client_auth = false /\ b = [||])}

val getCertificateVerifyBytes: si:SessionInfo -> (;si) PRF.masterSecret ->
  cert_req:(Cert.chain * a:Sig.alg * (;a)Sig.skey) option ->
  l:log{!cl,a,k. cert_req = Some((cl,a,k)) => Sig.Msg(a,Sig.PK(k),l)} ->
  b:bytes{(!cl,a,k. (cert_req = Some((cl,a,k)) /\ si.client_auth = true) =>
                    (?sign. b = CertificateVerifyMsg(si.protocol_version,a,sign))) /\
          ((cert_req = None \/ si.client_auth = false) => b = [||])}

val prepare_client_output_full_RSA: ci:ConnectionInfo -> (;ci)hs_state ->
	si:SessionInfo -> (Cert.chain * a:Sig.alg * (;a)Sig.skey) option -> l:log ->
	((;ci)hs_state * si':SessionInfo * (;si)PRF.masterSecret * log) Result
val prepare_client_output_full_DHE: ci:ConnectionInfo -> (;ci)hs_state ->
	si:SessionInfo -> (Cert.chain * a:Sig.alg * (;a)Sig.skey) option ->
	p:DHGroup.p -> (;p)DHGroup.g -> (;p)DHGroup.elt -> log ->
	((;ci)hs_state * si':SessionInfo * (;si)PRF.masterSecret * log) Result
val on_serverHello_full: ci:ConnectionInfo -> cr:crand -> l:log -> to_log:bytes ->
         (pv:ProtocolVersion * sr:random * sid:sessionID * cs:cipherSuite * cm:Compression * ext:bytes){
         ClientLogBeforeServerHello(cr,l) /\
         to_log = ServerHelloMsg(pv,sr,sid,cs,cm,ext)} ->
 	 (;ci) protoState
val parseMessageState: ci:ConnectionInfo -> hs:(;ci)hs_state ->
	(hs':(;ci)hs_state * ht:HandshakeType * pl:bytes * to_log:bytes{Config(ci,hs) = Config(ci,hs') /\
                                                                     to_log = MessageBytes(ht,pl)}) option Result
val recv_fragment_client: ci:ConnectionInfo -> s:(;ci)hs_state -> ProtocolVersion option ->
	(;ci,Config(ci,s))incoming

val prepare_server_output_full_RSA: ci:ConnectionInfo -> s:(;ci)hs_state -> si:SessionInfo ->
	pv:ProtocolVersion -> Sig.alg list -> cVerifyData -> sVerifyData -> l:log{
          ?csid,cs,cm,ex. l = ClientHelloMsg(pv,si.init_crand,csid,cs,cm,ex)
        }->
	((s':(;ci)hs_state{Config(ci,s) = Config(ci,s')}) * ProtocolVersion) Result
val prepare_server_output_full_DH: 'a -> 'b -> 'c -> 'd -> res:('e Result){?x,y. res = Error(x,y)}
val prepare_server_output_full_DHE: ci:ConnectionInfo -> s:(;ci)hs_state -> SessionInfo ->
	Sig.alg list -> cVerifyData -> sVerifyData -> log ->
	((s':(;ci)hs_state{Config(ci,s) = Config(ci,s')}) * ProtocolVersion) Result
val prepare_server_output_full_DH_anon: ci:ConnectionInfo -> s:(;ci)hs_state -> SessionInfo ->
	cVerifyData -> sVerifyData -> log ->
	((s':(;ci)hs_state{Config(ci,s) = Config(ci,s')}) * ProtocolVersion) Result
val prepare_server_output_full: ci:ConnectionInfo -> s:(;ci)hs_state -> si:SessionInfo ->
	pv:ProtocolVersion -> cVerifyData -> sVerifyData -> l:log{
          ?csid,cs,cm,ex. l = ClientHelloMsg(pv,si.init_crand,csid,cs,cm,ex)
        } ->
	((s':(;ci)hs_state{Config(ci,s) = Config(ci,s')}) * ProtocolVersion) Result
val negotiate: 'a list -> 'a list -> 'a option
val prepare_server_output_resumption: ci:ConnectionInfo -> s:(;ci)hs_state -> crand ->
	si:SessionInfo -> (;si)PRF.masterSecret -> cVerifyData -> sVerifyData -> log ->
	s':(;ci)hs_state{Config(ci,s) = Config(ci,s')}
val startServerFull: ci:ConnectionInfo -> s:(;ci)hs_state ->
  ch:(ProtocolVersion * crand * sessionID * cipherSuites * Compression list * bytes) ->// CHello
  cVerifyData -> sVerifyData ->
  l:log{!pv,cr,sid,cs,cms,ex. ch = (pv,cr,sid,cs,cms,ex) =>
         l = ClientHelloMsg(pv,cr,sid,cs,cms,ex)} ->
  ((s':(;ci)hs_state{Config(ci,s') = Config(ci,s)}) * ProtocolVersion) Result
val recv_fragment_server: ci:ConnectionInfo -> s:(;ci)hs_state -> pv:ProtocolVersion option ->
	(;ci,Config(ci,s))incoming
val enqueue_fragment: ci:ConnectionInfo -> s1:(;ci)hs_state -> bytes -> s2:(;ci)hs_state{Config(ci,s1) = Config(ci,s2)}

val sessionInfoCertBytesAuth: (si:SessionInfo) ->
  (clo: (Cert.chain * a:Sig.alg * (;a)Sig.skey) option) ->
  (si':SessionInfo * b:bytes){
    (si.client_auth = false /\ si' = si /\ b = [||]) \/
    (si.client_auth = true /\ clo = None /\ b = CertificateMsg([]) /\ si = si') \/
    (si.client_auth = true /\  (?cl,a',b'. clo = Some((cl,a',b')) /\ b = CertificateMsg(cl) /\ si'.clientID = cl))}

val certificateVerifyBytesAuth: si:SessionInfo ->
  (;si) PRF.masterSecret ->
  cert_req: (Cert.chain * a:Sig.alg * (;a)Sig.skey) option ->
  log:bytes{!cl,a,sk. cert_req = Some((cl,a,sk)) => Sig.Msg(a,Sig.PK(sk),log)} ->
  b:bytes{
    ((si.client_auth = false \/ cert_req = None) /\ b = [||]) \/
     (si.client_auth = true /\
         (?cl,a,sk,sign.
            cert_req = Some((cl,a,sk)) /\
            b = CertificateVerifyMsg(si.protocol_version,a,sign)))}

Verification status

The F# code of this module has been verified to meet its F7 interface.

Verification depends on the F7 interfaces of the following modules: Error Bytes Nonce TLSConstants RSAKey DHGroup HASH HMAC TLSPRF Sig Cert TLSInfo Range DataStream AppFragment HSFragment TLSFragment StatefulPlain LHAEPlain MAC_SHA256 MAC_SHA1 MAC Encode ENC LHAE StatefulLHAE PRF CRE DH RSA SessionDB TLSExtensions

miTLS

A verified reference TLS implementation

miTLS :: Handshake

F# Interface: Handshake.fsi

F# Implementation: Handshake.fs

F7 Interface: Handshake.fs7

Verification status

Module list

Trusted

Idealized

Verified