miTLS :: CRE

F# Interface: CRE.fsi

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

module CRE

open Bytes
open TLSConstants
open TLSInfo
open Error

type rsarepr = bytes
type rsapms
type dhpms

#if ideal

type pms = RSA_pms of rsapms | DHE_pms of dhpms
val corrupt: pms -> bool
#endif

val genRSA: RSAKey.pk -> TLSConstants.ProtocolVersion -> rsapms

val coerceRSA: RSAKey.pk -> ProtocolVersion -> rsarepr -> rsapms
val leakRSA: RSAKey.pk -> ProtocolVersion -> rsapms -> rsarepr

val sampleDH: DHGroup.p -> DHGroup.g -> DHGroup.elt -> DHGroup.elt -> dhpms

val coerceDH: DHGroup.p -> DHGroup.g -> DHGroup.elt -> DHGroup.elt -> DHGroup.elt -> dhpms

val prfSmoothRSA: SessionInfo -> ProtocolVersion -> rsapms -> PRF.masterSecret
val prfSmoothDHE: SessionInfo -> DHGroup.p -> DHGroup.g -> DHGroup.elt -> DHGroup.elt -> dhpms -> PRF.masterSecret

(* Used when generating key material from the MS.
   The result must still be split into the various keys.
   Of course this method can do the splitting internally and return a record/pair *)

F# Implementation: CRE.fs

module CRE

open Bytes
open TLSConstants
open TLSInfo
open TLSPRF

type rsarepr = bytes
type rsapms = {rsapms: rsarepr}
type dhpms = {dhpms: DHGroup.elt}

#if ideal
type pms = RSA_pms of rsapms | DHE_pms of dhpms

type pred = GeneratedRSAPMS of RSAKey.pk * ProtocolVersion * rsapms

// We maintain two log:
// - a log of honest pms values
// - a log for looking up good ms values using their pms values values

let honest_log = ref []
let honest pms = exists (fun el -> el=pms) !honest_log

let corrupt pms = not(honest pms)

let log = ref []
#endif

let genRSA (pk:RSAKey.pk) (vc:TLSConstants.ProtocolVersion) : rsapms =
    let verBytes = TLSConstants.versionBytes vc in
    let rnd = random 46 in
    let pms = verBytes @| rnd in
    let pms = {rsapms = pms}
    #if ideal
    if RSAKey.honest pk then honest_log := RSA_pms(pms)::!honest_log
    // event keeping track of honestly-generated PMSs
    Pi.assume (GeneratedRSAPMS(pk,vc,pms));
    #endif
    pms

let coerceRSA (pk:RSAKey.pk) (pv:ProtocolVersion) b = {rsapms = b}
let leakRSA (pk:RSAKey.pk) (pv:ProtocolVersion) pms = pms.rsapms

let sampleDH p g (gx:DHGroup.elt) (gy:DHGroup.elt) =
    let gz = DHGroup.genElement p g in
    let pms = {dhpms = gz}
    #if ideal
    honest_log := DHE_pms(pms)::!honest_log
    #endif
    pms

let coerceDH (p:DHGroup.p) (g:DHGroup.g) (gx:DHGroup.elt) (gy:DHGroup.elt) b = {dhpms = b}

// internal
let prfMS sinfo pmsBytes: PRF.masterSecret =
    let pv = sinfo.protocol_version in
    let cs = sinfo.cipher_suite in
    let data = sinfo.init_crand @| sinfo.init_srand in
    let res = prf pv cs pmsBytes tls_master_secret data 48 in
    PRF.coerce sinfo res

let prfSmoothRSA si (pv:ProtocolVersion) pms =
    #if ideal

if not(corrupt (RSA_pms(pms)))
    then match tryFind (fun el -> fst el = RSA_pms(pms)) !log with
             Some(_,ms) -> ms
           | None ->
                 let ms=PRF.sample si
                 log := (RSA_pms(pms),ms)::!log
                 ms
    else prfMS si pms.rsapms
    #else
    prfMS si pms.rsapms
    #endif

let prfSmoothDHE si (p:DHGroup.p) (g:DHGroup.g) (gx:DHGroup.elt) (gy:DHGroup.elt) (pms:dhpms) =
    //#begin-ideal
    #if ideal

if not(corrupt (DHE_pms(pms)))
    then match tryFind (fun el -> fst el = DHE_pms(pms)) !log  with
             Some(_,ms) -> ms
           | None ->
                 let ms=PRF.sample si
                 log := (DHE_pms(pms),ms)::!log;
                 ms
    else prfMS si pms.dhpms
    //#end-ideal
    #else
    prfMS si pms.dhpms
    #endif

F7 Interface: CRE.fs7

module CRE

open Bytes
open TLSConstants
open TLSInfo
open DHGroup

type rsarepr = (;48)lbytes

//#begin-abstractionRSA
private type (;pk:RSAKey.pk,pv:ProtocolVersion) rsapms = {rsapms:rsarepr}
predicate GeneratedRSAPMS of pk:RSAKey.pk * pv:ProtocolVersion * (;pk,pv)rsapms

val genRSA: pk:RSAKey.pk -> pv:ProtocolVersion -> pms:(;pk,pv)rsapms{GeneratedRSAPMS(pk,pv,pms)}
val coerceRSA: pk:RSAKey.pk -> pv:ProtocolVersion {not SafeRSAPMS(pk,pv)}-> bytes -> (;pk,pv)rsapms
val leakRSA: pk:RSAKey.pk -> pv:ProtocolVersion {not SafeRSAPMS(pk,pv)}-> (;pk,pv)rsapms -> bytes
//#end-abstractionRSA

//#begin-abstractionDH
private type (;p:p, g:(;p) g, gx:(;p) elt, gy:(;p) elt) dhpms = {dhpms: (;p) elt} // strong secret when (p,g), gx, and gy have been honestly generated

val sampleDH:   p:p -> g:(;p)g -> gx:(;p)elt -> gy:(;p)elt ->            (;p,g,gx,gy) dhpms
val coerceDH:   p:p -> g:(;p)g -> gx:(;p)elt -> gy:(;p)elt {not SafeDHPMS(p,g,gx,gy)}-> (;p)elt -> (;p,g,gx,gy) dhpms
//#end-abstractionDH

val prfSmoothRSA:
    si:SessionInfo ->
    pv:ProtocolVersion ->
    pms: (;Cert.RSAPKCert(si.serverID),pv) rsapms ->
    (;si) PRF.masterSecret

val prfSmoothDHE:
    si:SessionInfo ->
    p:DHGroup.p -> g:(;p)DHGroup.g -> gx:(;p)DHGroup.elt -> gy:(;p)DHGroup.elt ->
    pms: (;p,g,gx,gy)dhpms ->
    (;si) PRF.masterSecret

Verification status

This module is idealized: it contains both concrete F# code and an ideal implementation (when "ideal" flag set to true). The concrete code is not verified. Where applicable, we verify that the ideal implementation matches the F7 interface.

Verification depends on the F7 interfaces of the following modules: Error Bytes 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

miTLS

A verified reference TLS implementation

miTLS :: CRE

F# Interface: CRE.fsi

F# Implementation: CRE.fs

F7 Interface: CRE.fs7

Verification status

Module list

Trusted

Idealized

Verified