miTLS :: LHAE

F# Interface: LHAE.fsi

F# Implementation: LHAE.fs

(*
 * 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 LHAE

open Bytes

open TLSConstants
open TLSInfo
open Error
open Range

type cipher = bytes

(***** keying *****)

type LHAEKey =
    | MtEK of MAC.key * ENC.state
    | MACOnlyK of MAC.key
(*  | GCM of AENC.state  *)

let GEN e =
    let si = epochSI(e) in
    let authEnc = authencAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match authEnc with
    | MACOnly _ ->
        let mk = MAC.GEN e
        (MACOnlyK(mk), MACOnlyK(mk))
    | MtE(_,_) ->
        let mk = MAC.GEN e in
        let (ek,dk) = ENC.GEN e in
        (MtEK(mk,ek),MtEK(mk,dk))
    | AEAD (_,_) -> unexpectedError "[GEN] invoked on unsupported ciphersuite"

let COERCE e b =
    // precondition: b is of the right length, so no need for a runtime checks here.
    let si = epochSI(e) in
    let cs = si.cipher_suite in
    let pv = si.protocol_version in
    let authEnc = authencAlg_of_ciphersuite cs pv in
    match authEnc with
    | MACOnly _ ->
      let mk = MAC.COERCE e b in
      MACOnlyK(mk)
    | MtE(encalg,macalg) ->
      let macKeySize = macKeySize macalg in
      let encKeySize = encKeySize encalg in
      let (mkb,rest) = split b macKeySize in
      let (ekb,ivb) = split rest encKeySize in
      let mk = MAC.COERCE e mkb in
      let ek = ENC.COERCE e ekb ivb in
      MtEK(mk,ek)
    | AEAD (_,_) ->
      unexpectedError "[COERCE] invoked on wrong ciphersuite"

let LEAK e k =
    match k with
    | MACOnlyK(mk) -> MAC.LEAK e mk
    | MtEK(mk,ek) ->
        let (k,iv) = ENC.LEAK e ek in
        MAC.LEAK e mk @| k @| iv

(***** authenticated encryption *****)

let encrypt' e key data rg plain =
    let si = epochSI(e) in
    let cs = si.cipher_suite in
    let pv = si.protocol_version in
    let authEnc = authencAlg_of_ciphersuite cs pv in
    match (authEnc,key) with
    | (MtE(encAlg,_), MtEK (ka,ke)) ->
        match encAlg with
        | Stream_RC4_128 -> // stream cipher
            let plain   = Encode.mac e ka data rg plain in
            let (l,h) = rg in
            if l <> h then
                unexpectedError "[encrypt'] given an invalid input range"
            else
                let (ke,res) = ENC.ENC e ke data rg plain
                (MtEK(ka,ke),res)
        | CBC_Stale(_) | CBC_Fresh(_) -> // block cipher
            let plain  = Encode.mac e ka data rg plain in
            let (ke,res) = ENC.ENC e ke data rg plain
            (MtEK(ka,ke),res)
    | (MACOnly _, MACOnlyK (ka)) ->
        let plain = Encode.mac e ka data rg plain in
        let (l,h) = rg in
        if l <> h then
            unexpectedError "[encrypt'] given an invalid input range"
        else
            let r = Encode.repr e data rg plain in
            (key,r)
//  | GCM (k) -> ...
    | (_,_) -> unexpectedError "[encrypt'] incompatible ciphersuite-key given."

let mteKey (e:epoch) ka ke = MtEK(ka,ke)

let decrypt' e key data cipher =
    let cl = length cipher in
    // by typing, we know that cl <= max_TLSCipher_fragment_length
    let si = epochSI(e) in
    let cs = si.cipher_suite in
    let pv = si.protocol_version in
    let authEnc = authencAlg_of_ciphersuite cs pv in
    match (authEnc,key) with
    | (MtE(encAlg,macAlg), MtEK (ka,ke)) ->
        let macSize = macSize macAlg in
        match encAlg with
        | Stream_RC4_128 -> // stream cipher
            if cl < macSize then
                (*@ It is safe to return early, because we are branching
                    on public data known to the attacker *)
                let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_bad_record_mac, reason)
            else
                let rg = cipherRangeClass e cl in
                let (ke,plain) = ENC.DEC e ke data cipher in
                let nk = mteKey e ka ke in
                match Encode.verify e ka data rg plain with
                | Error(x,y) -> Error(x,y)
                | Correct(aeplain) -> correct(nk,rg,aeplain)
        | CBC_Stale(alg) | CBC_Fresh(alg) -> // block cipher
            let ivL = ivSize e in
            let blockSize = blockSize alg in
            if (cl - ivL < macSize + 1) || (cl % blockSize <> 0) then
                (*@ It is safe to return early, because we are branching
                    on public data known to the attacker *)
                let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_bad_record_mac, reason)
            else
                let rg = cipherRangeClass e cl in
                let (ke,plain) = ENC.DEC e ke data cipher in
                let nk = mteKey e ka ke in
                match Encode.verify e ka data rg plain with
                | Error(x,y) -> Error(x,y)
                | Correct(aeplain) -> correct (nk,rg,aeplain)
    | (MACOnly macAlg ,MACOnlyK (ka)) ->
        let macSize = macSize macAlg in
        if cl < macSize then
            let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_bad_record_mac, reason)
        else
            let rg = cipherRangeClass e cl in
            let plain = Encode.plain e data cl cipher in
            match Encode.verify e ka data rg plain with
            | Error(x,y) -> Error(x,y)
            | Correct(aeplain) -> correct (key,rg,aeplain)
//  | GCM (GCMKey) -> ...
    | (_,_) -> unexpectedError "[decrypt'] incompatible ciphersuite-key given."

#if ideal

type preds = | ENCrypted of epoch * LHAEPlain.adata * range * LHAEPlain.plain * cipher

type entry = epoch * LHAEPlain.adata * range * LHAEPlain.plain * ENC.cipher
let log = ref ([]: entry list) // for defining the ideal functionality for CTXT

let rec cmem (e:epoch) (ad:LHAEPlain.adata) (c:ENC.cipher) (xs: entry list) =
  match xs with
  | (e',ad',r,p,c')::_ when e=e' && ad=ad' && c=c' -> let x = (r,p) in Some x
  | _::xs                  -> cmem e ad c xs
  | []                     -> None

#endif

let encrypt e key data rg plain =
  let (key,cipher) = encrypt' e key data rg plain in
  #if ideal

if safe e then
    log := (e,data,rg,plain,cipher)::!log
  else ()
  #endif
  (key,cipher)

let decrypt e (key: LHAEKey) data (cipher: bytes) =
  #if ideal
  if safe e then
    match cmem e data cipher !log with
    | Some x ->
       let (r,p) = x in
       let p' = LHAEPlain.widen e data r p in
       let tlen = length cipher in
       let rg' = cipherRangeClass e tlen in
       correct (key,rg',p')
    | None   -> Error(AD_bad_record_mac, "")
  else
  #endif
      decrypt' e key data cipher

F7 Interface: LHAE.fs7

module LHAE

open Bytes
open Error
open TLSInfo
open Range

open TLSConstants

type cipher = b:bytes{Length(b) <= max_TLSCipher_fragment_length}
(* no need to be more precise on the length *)

private type (;ki:epoch) LHAEKey =
    | MtEK of ka:(;ki)MAC.key * ke:(;ki)ENC.state // {MtEKey(ki,(ka,ke))}
    | MACOnlyK of (;ki) MAC.key
(*  | GCM of ke:(;ki:AENC.state)  *)

function val LHAESize: ki:epoch -> nat
private definition !ki,si,enc,mac. si = EpochSI(ki) =>
	(( CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MACOnly(mac) =>
	  LHAESize(ki) = MacSize(mac) ) /\
	 ( CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(enc,mac) =>
	  LHAESize(ki) = MacSize(mac) +
					    EncKeySize(enc) +
					    Range.IVSize(ki) ))

val GEN:    ki:succEpoch     -> encryptor:(;ki)LHAEKey * decryptor:(;ki)LHAEKey
val COERCE: ki:succEpoch{not Auth(ki)} -> b:bytes{Length(b) = LHAESize(ki)} -> (;ki)LHAEKey
val LEAK:   ki:succEpoch{not Auth(ki)} -> (;ki)LHAEKey -> b:bytes

private val mteKey: ki:epoch -> (;ki) MAC.key -> (;ki) ENC.state -> (;ki) LHAEKey

private assume !e,si. si = EpochSI(e) =>
	( (si.protocol_version = SSL_3p0 \/ si.protocol_version = TLS_1p0) => IVSize(e) = 0 ) /\
	( (si.protocol_version = TLS_1p1 \/ si.protocol_version = TLS_1p2) =>
	   IVSize(e) = EncAlgBlockSize(CipherSuiteENCAlg(si.cipher_suite,si.protocol_version)) )

// We have two variants for encryption and decryption:
// the first (primed) is concrete; the second is idealized at safe indexes,
// using either #ideal_F (filtering out non-cipher) or #ideal (decrypting just by lookup)

predicate ENCrypted of e:epoch * ad:(;e)LHAEPlain.adata * cipher

private definition !e,ad,c.
  ENCrypted(e,ad,c) <=> ?p'. ENC.ENCrypted(e,ad,c,p')

ask !e,ad,c. ( Safe(e) => ENCrypted(e,ad,c) ) => (Safe(e) => ?p. ENC.ENCrypted(e,ad,c,p))

val encrypt': ki:succEpoch -> (;ki) LHAEKey -> ad:(;ki)LHAEPlain.adata ->
  rg:range -> p:(;ki,ad,rg) LHAEPlain.plain ->
  ((;ki) LHAEKey * c:cipher){Length(c) = TargetLength(ki,rg) /\
                             (Safe(ki) => ENCrypted(ki,ad,c))}

val encrypt : ki:succEpoch -> (;ki) LHAEKey -> ad:(;ki)LHAEPlain.adata ->
  rg:range -> p:(;ki,ad,rg) LHAEPlain.plain ->
  ((;ki) LHAEKey * c:cipher){Length(c) = TargetLength(ki,rg) /\
                             (Safe(ki) => ENCrypted(ki,ad,c))}

type entry =
  ki:succEpoch * ad:(;ki) LHAEPlain.adata * rg:range *
  p:(;ki,ad,rg) LHAEPlain.plain * c:ENC.cipher {ENCrypted(ki,ad,c)}
private val log: entry list ref
private val cmem: ki:succEpoch -> ad:(;ki)LHAEPlain.adata -> c:cipher ->
  entry list -> res:(r:range * (;ki,ad,r)LHAEPlain.plain) option {
    ( !rg,p. res = Some ((rg,p)) => (ENCrypted(ki,ad,c) /\ rg = CipherRangeClass(ki,Length(c))) ) /\
	( res = None => not ENCrypted(ki,ad,c) )}

val decrypt': ki:succEpoch -> k:(;ki) LHAEKey -> ad:(;ki)LHAEPlain.adata ->
  c:cipher{Safe(ki) => ENCrypted(ki,ad,c)} -> res:
  ( (
    (;ki) LHAEKey *
    rg:range *
    p:(;ki,ad,rg) LHAEPlain.plain) {rg = CipherRangeClass(ki,Length(c))} ) Result

// { (* partial functional correctness when decrypting what we encrypted *)
//   !pl,p,tag,rg.
//	(    Length(c) = EncryptedLength(ki,rg)
//	  /\ MACed(e,ad,pl,tag) // nb Encode.MACed has extra args.
//     /\ Encoded(e,ad,pl,tag,p)
//     /\ ENCrypted(e,Length(c),StateID(e,Encryptor(k)),p,c)
//   => ?k',r'. res = Correct((k',r',pl)) }

val decrypt: ki:succEpoch -> (;ki) LHAEKey -> ad:(;ki)LHAEPlain.adata ->
  c:cipher -> res:
  ( ((;ki) LHAEKey *  rg:range * (;ki,ad,rg) LHAEPlain.plain)
     {rg = CipherRangeClass(ki,Length(c))}
  ) Result
   {
    (Safe(ki) =>
        (   (!k,r,p. res = Correct((k,r,p)) => ENCrypted(ki,ad,c))
	 /\ (ENCrypted(ki,ad,c) => (?p,k,r'. res = Correct((k,r',p))))
		))}
// The last two lines are equivalent to (but easier to verify than)
// !p. CTXT(ki,ad,p,c) <=> (?k,r. res = Correct((k,r,p)))

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 Sig Cert TLSInfo Range DataStream AppFragment HSFragment TLSFragment StatefulPlain LHAEPlain MAC_SHA256 MAC_SHA1 MAC Encode ENC

miTLS

A verified reference TLS implementation

miTLS :: LHAE

F# Interface: LHAE.fsi

F# Implementation: LHAE.fs

F7 Interface: LHAE.fs7

Verification status

Module list

Trusted

Idealized

Verified