miTLS

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

module TLSInfo

open Bytes
open TLSConstants

type sessionID = bytes
type preRole =
    | Client
    | Server
type Role = preRole

// Client/Server randomness
type random = bytes
type crand = random
type srand = random

type pmsData =
    | PMSUnset
    | RSAPMS of RSAKey.pk * ProtocolVersion * bytes
    | DHPMS  of DHGroup.p * DHGroup.g * DHGroup.elt * DHGroup.elt

type SessionInfo = {
    init_crand: crand;
    init_srand: srand;
    protocol_version: ProtocolVersion;
    cipher_suite: cipherSuite;
    compression: Compression;
    pmsData: pmsData;
    client_auth: bool;
    clientID: Cert.cert list;
    serverID: Cert.cert list;
    sessionID: sessionID;
    // Extensions:
    extended_record_padding: bool;
    }

type preEpoch
type epoch = preEpoch

val isInitEpoch: epoch -> bool
val epochSI: epoch -> SessionInfo
val epochSRand: epoch -> srand
val epochCRand: epoch -> crand

// Role is of the writer
type ConnectionInfo =
    { role: Role;
      id_rand: random;
      id_in:  epoch;
      id_out: epoch}
val connectionRole: ConnectionInfo -> Role

val initConnection: Role -> bytes -> ConnectionInfo
val nextEpoch: epoch -> crand -> srand -> SessionInfo -> epoch
//val dual_KeyInfo: epoch -> epoch

(* Application configuration options *)

type helloReqPolicy =
    | HRPIgnore
    | HRPFull
    | HRPResume

type config = {
    minVer: ProtocolVersion
    maxVer: ProtocolVersion
    ciphersuites: cipherSuites
    compressions: Compression list

(* Handshake specific options *)

(* Client side *)
    honourHelloReq: helloReqPolicy
    allowAnonCipherSuite: bool

(* Server side *)
    request_client_certificate: bool
    check_client_version_in_pms_for_old_tls: bool

(* Common *)
    safe_renegotiation: bool
    server_name: Cert.hint
    client_name: Cert.hint

(* Sessions database *)
    sessionDBFileName: string
    sessionDBExpiry: TimeSpan
    }

val defaultConfig: config

val max_TLSCipher_fragment_length: nat
val fragmentLength: nat

#if ideal
val safe: epoch -> bool
val safeHS: epoch -> bool
val auth: epoch -> bool
val safeMAC: epoch -> bool
val safeENC: epoch -> bool
#endif

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

module TLSInfo

open Bytes
open TLSConstants

type sessionID = bytes
type preRole =
    | Client
    | Server
type Role = preRole

// Client/Server randomness
type random = bytes
type crand = random
type srand = random

type pmsData =
    | PMSUnset
    | RSAPMS of RSAKey.pk * ProtocolVersion * bytes
    | DHPMS  of DHGroup.p * DHGroup.g * DHGroup.elt * DHGroup.elt

type SessionInfo = {
    init_crand: crand;
    init_srand: srand;
    protocol_version: ProtocolVersion;
    cipher_suite: cipherSuite;
    compression: Compression;
    pmsData: pmsData;
    client_auth: bool;
    clientID: Cert.cert list;
    serverID: Cert.cert list;
    sessionID: sessionID;
    // Extensions:
    extended_record_padding: bool;
    }

type preEpoch =
    | InitEpoch of Role
    | SuccEpoch of crand * srand * SessionInfo * preEpoch
type epoch = preEpoch
type succEpoch = preEpoch

let isInitEpoch e =
    match e with
    | InitEpoch (_) -> true
    | SuccEpoch (_,_,_,_) -> false

let epochSI e =
    match e with
    | InitEpoch (d) -> Error.unexpectedError "[epochSI] invoked on initial epoch."
    | SuccEpoch (cr,sr,si,pe) -> si

let epochSRand e =
    match e with
    | InitEpoch (d) -> Error.unexpectedError "[epochSRand] invoked on initial epoch."
    | SuccEpoch (cr,sr,si,pe) -> sr

let epochCRand e =
    match e with
    | InitEpoch (d) -> Error.unexpectedError "[epochCRand] invoked on initial epoch."
    | SuccEpoch (cr,sr,si,pe) -> cr

type ConnectionInfo = {
    role: Role; // cached, could be retrieved from id_out
    id_rand: random; // our random
    id_in: epoch;
    id_out: epoch}

let connectionRole ci = ci.role

let initConnection role rand =
    let ctos = InitEpoch Client in
    let stoc = InitEpoch Server in
    match role with
    | Client -> {role = Client; id_rand = rand; id_in = stoc; id_out = ctos}
    | Server -> {role = Server; id_rand = rand; id_in = ctos; id_out = stoc}

let nextEpoch epoch crand srand si =
    SuccEpoch (crand, srand, si, epoch )

// Application configuration
type helloReqPolicy =
    | HRPIgnore
    | HRPFull
    | HRPResume

type config = {
    minVer: ProtocolVersion
    maxVer: ProtocolVersion
    ciphersuites: cipherSuites
    compressions: Compression list

(* Handshake specific options *)

(* Client side *)
    honourHelloReq: helloReqPolicy
    allowAnonCipherSuite: bool

(* Server side *)
    request_client_certificate: bool
    check_client_version_in_pms_for_old_tls: bool

(* Common *)
    safe_renegotiation: bool
    server_name: Cert.hint
    client_name: Cert.hint

(* Sessions database *)
    sessionDBFileName: string
    sessionDBExpiry: TimeSpan
    }

let defaultConfig ={
    minVer = SSL_3p0
    maxVer = TLS_1p2
    ciphersuites = cipherSuites_of_nameList
                    [ TLS_RSA_WITH_AES_128_CBC_SHA;
                      TLS_RSA_WITH_3DES_EDE_CBC_SHA ]
    compressions = [ NullCompression ]

honourHelloReq = HRPResume
    allowAnonCipherSuite = false
    request_client_certificate = false
    check_client_version_in_pms_for_old_tls = true

safe_renegotiation = true
    server_name = "mitls.example.org"
    client_name = "client.example.org"

sessionDBFileName = "sessionDBFile.bin"
    sessionDBExpiry = newTimeSpan 1 0 0 0 (*@ one day, as suggested by the RFC *)
    }

let max_TLSPlaintext_fragment_length = 16384 (*@ 2^14 *)
let max_TLSCompressed_fragment_length = max_TLSPlaintext_fragment_length + 1024
let max_TLSCipher_fragment_length = max_TLSCompressed_fragment_length + 1024
let fragmentLength = max_TLSPlaintext_fragment_length

#if ideal
// These functions are used only for specifying ideal implementations
let safe (e:epoch) = failwith "spec only" : bool
let safeHS (e:epoch) = failwith "spec only": bool
let auth (e:epoch) = failwith "spec only": bool
let safeMAC (e:epoch) = failwith "spec only":bool
let safeENC (e:epoch) = failwith "spec only":bool
#endif

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

module TLSInfo

(* This module gathers the definitions of
   public datatypes, parameters, and predicates for our TLS API.

Its interface is used by most TLS modules; its implementation is typechecked. *)

open Bytes
open TLSConstants

type sessionID = b:bytes {Length(b) <= 32}
// "An arbitrary byte sequence chosen by the server
// to identify an active or resumable session state."
// We treat [||] as the absence of identifier.

type preRole =
	| Client
	| Server
type Role = r:preRole{r = Client \/ r = Server}
function val DualRole: Role -> Role
assume DualRole(Client) = Server
assume DualRole(Server) = Client

// Client/Server randomness (implemented in Nonce)
// their first 4 bytes give the local time,
// so that they are locally pairwise-distinct
type random = (;32) lbytes
type crand = random
type srand = random

// SessionInfo and epoch: Session and Connection level public immutable data.
// Used for indexing

type pmsData =
    | PMSUnset
    | RSAPMS of pk:RSAKey.pk * ProtocolVersion * encpms:bytes
    | DHPMS  of p:DHGroup.p * g:(;p)DHGroup.g *
		  	      gx:(;p)DHGroup.elt (* Client *) *
			      gy:(;p)DHGroup.elt (* Server *)

type SessionInfo = {
    init_crand: crand;
    init_srand: srand;
    protocol_version: ProtocolVersion;
    cipher_suite: cipherSuite;
    compression: Compression;
    pmsData: pmsData;
    client_auth: bool;
    clientID: Cert.cert list;
    serverID: Cert.cert list;
    sessionID: sessionID;
    // Extensions:
    extended_record_padding: bool;
    }
// for certificates, the empty list represents the absence of identity
// (possibly refusing to present requested certs)
//
// for sessionID, the empty bytes [||] represents the absence of ID,
// that is, the session is not resumable.

private type preEpoch =
  | InitEpoch of writer:Role
  | SuccEpoch of crand * srand  (* the latest randoms     *)
               * si:SessionInfo
               * pred:preEpoch

predicate val IsInitEpoch: preEpoch -> bool
predicate val IsSuccEpoch: preEpoch -> bool
private definition !e. IsInitEpoch(e) <=> ?r. e = InitEpoch(r)
private definition !e. IsSuccEpoch(e) <=> ?c,s,si,pe. e = SuccEpoch(c,s,si,pe)

type epoch = e:preEpoch {IsInitEpoch(e) \/ IsSuccEpoch(e)}
type succEpoch = e:preEpoch {IsSuccEpoch(e)}

function val Pred: succEpoch -> epoch
private definition !cr,sr,si,pred. Pred(SuccEpoch(cr,sr,si,pred)) = pred

function val EpochSI: succEpoch -> SessionInfo
private definition !c,s,si,p. EpochSI(SuccEpoch(c,s,si,p)) = si

function val EpochSRand: succEpoch -> bytes
function val EpochCRand: succEpoch -> bytes
private definition !b1,b2,si,pe. EpochSRand(SuccEpoch(b1,b2,si,pe)) = b2
private definition !b1,b2,si,pe. EpochCRand(SuccEpoch(b1,b2,si,pe)) = b1

val isInitEpoch: e:epoch -> b:bool{(b = true /\ IsInitEpoch(e)) \/ (b = false /\ IsSuccEpoch(e))}
val epochSI: e:succEpoch -> si:SessionInfo{si = EpochSI(e)}

val epochSRand: e:succEpoch -> b:crand{b = EpochSRand(e)}
val epochCRand: e:succEpoch -> b:srand{b = EpochCRand(e)}

type ConnectionInfo =
	{ role: Role;
	  id_rand: random;
	  id_in:  epoch;
      id_out: epoch}

val connectionRole: ci:ConnectionInfo -> r:Role{r = ci.role}

val initConnection: r:Role -> ra:random -> ci:ConnectionInfo{ci.role = r /\ ci.id_rand = ra /\ IsInitEpoch(ci.id_in) /\ IsInitEpoch(ci.id_out)}
val nextEpoch: e:epoch -> c:crand -> s:srand -> si:SessionInfo ->
	e':succEpoch{Pred(e') = e /\ EpochSI(e') = si /\
			     EpochCRand(e') = c /\ EpochSRand(e') = s}

// Predicates specifying the honesty of keys and key material

predicate HonestSig of a:sigHashAlg * (;a) Sig.pkey
definition !a,k. HonestSig(a,k) <=> Sig.Honest(a,k)

predicate HonestRSAKey of RSAKey.pk
definition !pk. HonestRSAKey(pk) <=> RSAKey.Honest(pk)

// To be defined
predicate HonestRSAPMS of pk:RSAKey.pk * pv:ProtocolVersion * encpms:bytes
predicate HonestDHPMS of p:DHGroup.p * g:(;p)DHGroup.g *
		  	      gx:(;p)DHGroup.elt (* Client *) *
			      gy:(;p)DHGroup.elt (* Server *)

predicate HonestPMS of pmsData
assume !pd. HonestPMS(pd) <=>
      ((?pk,pv,e. pd = RSAPMS(pk,pv,e) /\ HonestRSAPMS(pk,pv,e)) \/
       (?p,g,gx,gy. pd = DHPMS(p,g,gx,gy) /\ HonestDHPMS(p,g,gx,gy)))

// Predicates specifying cryptographic assumptions on algorithms
predicate StrongAESI of SessionInfo
predicate StrongAuthSI of SessionInfo
predicate StrongAE of epoch
predicate StrongAuth of epoch

definition !e. StrongAE(e)   <=> StrongAESI(EpochSI(e))
definition !e. StrongAuth(e) <=> StrongAuthSI(EpochSI(e))

definition !si. StrongAESI(si)   <=> (?e,m. CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(e,m) /\ IND_CPA(e) /\ INT_CMA_M(m) /\ INT_CTXT(CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version),si.protocol_version))
definition !si. StrongAuthSI(si) <=> (?e,m. CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(e,m) /\ INT_CMA_M(m))

predicate StrongSig of SessionInfo
definition !si. StrongSig(si) <=> Sig.Strong(CipherSuiteSigHashAlg(si.cipher_suite))

predicate StrongPRF of SessionInfo

predicate StrongCRE of SessionInfo

predicate StrongHS  of SessionInfo

predicate SafeRSAPMS of RSAKey.pk * ProtocolVersion // The public key and protocol version yields a good rsapms
predicate SafeDHPMS of p:DHGroup.p * (;p)DHGroup.g * (;p)DHGroup.elt * (;p)DHGroup.elt // The DH parameters, generator, and gx and gy values yield a good dhpms

predicate StrongRSAPMS   of SessionInfo
predicate StrongDHPMS    of SessionInfo

definition !si. StrongHS(si) <=>

StrongSig(si)
		   /\ StrongPRF(si)
           /\ StrongCRE(si)
           /\ (StrongRSAPMS(si) \/
	   	       StrongDHPMS(si))

// Predicates specifying the security of TLS connections
predicate type cryptopreds =
| SafeSI  of SessionInfo // The session ciphersuite yields secrecy and integrity
| AuthSI  of SessionInfo // The session ciphersuite yields integrity (not necessarily secrecy)
| SafeHS_SI of SessionInfo // Good handshake for this sessioninfo
| SafeHS of epoch // Good handshake for this epoch
| Safe   of epoch // The epoch parameters yield privacy & integrity
| Auth   of epoch // The epoch parameters yield integrity (not necesarily privacy)

definition !si. SafeSI(si) <=>
           SafeHS_SI(si) /\
           StrongAESI(si)
definition !si. AuthSI(si) <=>
           SafeHS_SI(si) /\
           StrongAuthSI(si)

definition !id. SafeHS_SI(id) <=>
      StrongHS(id)
   /\ HonestPMS(id.pmsData)

definition !id. SafeHS(id) <=> SafeHS_SI(EpochSI(id))

definition !e. Safe(e) <=> SafeSI(EpochSI(e))
definition !e. Auth(e) <=> AuthSI(EpochSI(e))
// Safety for epochs relies only on SessionInfo, but this would change if we introduce a finer model of compromise
// E.g. if we allowed the attacker to compromise specific epochs

// In the code of ideal implementations only,
// we use F# functions that characterize the Safe and Auth predicates.
val safe: (e:epoch) -> b:bool { b = true <=> Safe(e) }
val safeHS: (e:epoch) -> b:bool {b = true <=> SafeHS(e)}
val auth :(e:epoch) -> b:bool {b = true <=> Auth(e)}
val safeMAC: (e:epoch) -> b:bool {b = true <=> Auth(e)}
val safeENC: (e:epoch) -> b:bool {b = true <=> Safe(e)}

ask !e. Safe(e) => Auth(e)

ask !e,mac. CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MACOnly(mac) => not Safe(e)

// so that TLS can exchange any traffic on the initial null connection
assume !e. IsInitEpoch(e) => not Auth(e)

(* Application configuration options *)

type helloReqPolicy =
    | HRPIgnore
    | HRPFull
    | HRPResume

type config = {
    minVer: ProtocolVersion;
    maxVer: ProtocolVersion;
    ciphersuites: cipherSuites;
    compressions: Compression list;

(* Handshake specific options *)

(* Client side *)
    honourHelloReq: helloReqPolicy;
    allowAnonCipherSuite: bool;

(* Server side *)
    request_client_certificate: bool;
    check_client_version_in_pms_for_old_tls: bool;

(* Common *)
    safe_renegotiation: bool;
	server_name: Cert.hint;
	client_name: Cert.hint;

(* Sessions database *)
    sessionDBFileName: string;
    sessionDBExpiry: TimeSpan
    }

val defaultConfig: config

private val max_TLSPlaintext_fragment_length: nat
private val max_TLSCompressed_fragment_length: nat
val max_TLSCipher_fragment_length: nat
val fragmentLength: nat

A verified reference TLS implementation

miTLS :: TLSInfo

F# Interface: TLSInfo.fsi

F# Implementation: TLSInfo.fs

F7 Interface: TLSInfo.fs7

Verification status

Module list

Trusted

Idealized

Verified