miTLS :: ENC

F# Interface: ENC.fsi

F# Implementation: ENC.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 ENC

open Bytes
open Error
open TLSConstants
open TLSInfo
open Range

(* We do not open Encode so that we can syntactically check its usage restrictions *)

type cipher = bytes

(* Early TLS chains IVs but this is not secure against adaptive CPA *)
let lastblock cipher alg =
    let ivl = blockSize alg in
    let (_,b) = split cipher (length cipher - ivl) in b

type key = {k:bytes}

type iv = bytes
type iv3 =
    | SomeIV of iv
    | NoIV

type blockState =
    {key: key;
     iv: iv3}
type streamState =
    {skey: key; // Ghost: Only stored so that we can LEAK it
     sstate: CoreCiphers.rc4engine}

type state =
    | BlockCipher of blockState
    | StreamCipher of streamState
type encryptor = state
type decryptor = state

let GENOne ki =
    let si = epochSI(ki) in
    let alg = encAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match alg with
    | Stream_RC4_128 ->
        let k = random (encKeySize alg) in
        let key = {k = k} in
        StreamCipher({skey = key; sstate = CoreCiphers.rc4create k})
    | CBC_Stale(cbc) ->
        let key = {k = random (encKeySize alg)}
        let iv = SomeIV(random (blockSize cbc))
        BlockCipher ({key = key; iv = iv})
    | CBC_Fresh(_) ->
        let key = {k = random (encKeySize alg)}
        let iv = NoIV
        BlockCipher ({key = key; iv = iv})

let GEN (ki) = let k = GENOne ki in (k,k)

let COERCE (ki:epoch) k iv =
    let si = epochSI(ki) in
    let alg = encAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match alg with
    | Stream_RC4_128 ->
        let key = {k = k} in
        StreamCipher({skey = key; sstate = CoreCiphers.rc4create k})
    | CBC_Stale(_) ->
        BlockCipher ({key = {k=k}; iv = SomeIV(iv)})
    | CBC_Fresh(_) ->
        BlockCipher ({key = {k=k}; iv = NoIV})

let LEAK (ki:epoch) s =
    match s with
    | BlockCipher (bs) ->
        let iv =
            match bs.iv with
            | NoIV -> [||]
            | SomeIV(iv) -> iv
        (bs.key.k,iv)
    | StreamCipher (ss) ->
        ss.skey.k,[||]

let cbcenc alg k iv d =
    match alg with
    | TDES_EDE -> CoreCiphers.des3_cbc_encrypt k iv d
    | AES_128 | AES_256  -> CoreCiphers.aes_cbc_encrypt  k iv d

(* Parametric ENC/DEC functions *)
let ENC_int ki s tlen d =
    let si = epochSI(ki) in
    let encAlg = encAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match s,encAlg with
    //#begin-ivStaleEnc
    | BlockCipher(s), CBC_Stale(alg) ->
        match s.iv with
        | NoIV -> unexpectedError "[ENC] Wrong combination of cipher algorithm and state"
        | SomeIV(iv) ->
            let cipher = cbcenc alg s.key.k iv d
            if length cipher <> tlen || tlen > max_TLSCipher_fragment_length then
                // unexpected, because it is enforced statically by the
                // CompatibleLength predicate
                unexpectedError "[ENC] Length of encrypted data do not match expected length"
            else
                let s = {s with iv = SomeIV(lastblock cipher alg) } in
                (BlockCipher(s), cipher)
    //#end-ivStaleEnc
    | BlockCipher(s), CBC_Fresh(alg) ->
        match s.iv with
        | SomeIV(b) -> unexpectedError "[ENC] Wrong combination of cipher algorithm and state"
        | NoIV   ->
            let ivl = blockSize alg in
            let iv = random ivl in
            let cipher = cbcenc alg s.key.k iv d
            let res = iv @| cipher in
            if length res <> tlen || tlen > max_TLSCipher_fragment_length then
                // unexpected, because it is enforced statically by the
                // CompatibleLength predicate
                unexpectedError "[ENC] Length of encrypted data do not match expected length"
            else
                let s = {s with iv = NoIV} in
                (BlockCipher(s), res)
    | StreamCipher(s), Stream_RC4_128 ->
        let cipher = CoreCiphers.rc4process s.sstate d in
        if length cipher <> tlen || tlen > max_TLSCipher_fragment_length then
                // unexpected, because it is enforced statically by the
                // CompatibleLength predicate
                unexpectedError "[ENC] Length of encrypted data do not match expected length"
        else
            (StreamCipher(s),cipher)
    | _, _ -> unexpectedError "[ENC] Wrong combination of cipher algorithm and state"

#if ideal
type entry = epoch * LHAEPlain.adata * cipher * Encode.plain
let log:entry list ref = ref []
let rec cfind (e:epoch) (c:cipher) (xs: entry list) =
  match xs with
      [] -> failwith "not found"
    | (e',ad,c',text)::res when e = e' && c = c' -> (ad,cipherRangeClass e (length c),text)
    | _::res -> cfind e c res
#endif

let ENC ki s ad rg data =
    let tlen = targetLength ki rg in
  #if ideal
    if safeENC(ki) then
      let d = createBytes tlen 0 in
      let (s,c) = ENC_int ki s tlen d in
      log := (ki, ad, c, data)::!log;
      (s,c)
    else
  #endif
      let d = Encode.repr ki ad rg data in
      ENC_int ki s tlen d

let cbcdec alg k iv e =
    match alg with
    | TDES_EDE -> CoreCiphers.des3_cbc_decrypt k iv e
    | AES_128 | AES_256  -> CoreCiphers.aes_cbc_decrypt k iv e

let DEC_int ki s cipher =
    let si = epochSI(ki) in
    let encAlg = encAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match s, encAlg with
    //#begin-ivStaleDec
    | BlockCipher(s), CBC_Stale(alg) ->
        match s.iv with
        | NoIV -> unexpectedError "[DEC] Wrong combination of cipher algorithm and state"
        | SomeIV(iv) ->
            let data = cbcdec alg s.key.k iv cipher
            let s = {s with iv = SomeIV(lastblock cipher alg)} in
            (BlockCipher(s), data)
    //#end-ivStaleDec
    | BlockCipher(s), CBC_Fresh(alg) ->
        match s.iv with
        | SomeIV(_) -> unexpectedError "[DEC] Wrong combination of cipher algorithm and state"
        | NoIV ->
            let ivL = blockSize alg in
            let (iv,encrypted) = split cipher ivL in
            let data = cbcdec alg s.key.k iv encrypted in
            let s = {s with iv = NoIV} in
            (BlockCipher(s), data)
    | StreamCipher(s), Stream_RC4_128 ->
        let data = CoreCiphers.rc4process s.sstate cipher
        (StreamCipher(s),data)
    | _,_ -> unexpectedError "[DEC] Wrong combination of cipher algorithm and state"

let DEC ki s ad cipher =
  #if ideal
    if safeENC(ki) then
      let (s,p) = DEC_int ki s cipher in
      let (ad',rg',p') = cfind ki cipher !log in
      (s,p')
    else
  #endif
      let (s,p) = DEC_int ki s cipher in
      let tlen = length cipher in
      let p' = Encode.plain ki ad tlen p in
      (s,p')

(* the SPRP game in F#, without indexing so far.
   the adversary gets
   enc: block -> block
   dec: block -> block

// two copies of assoc
let rec findp pcs c =
  match pcs with
  | (p,c')::pcs -> if c = c' then Some(p) else findp pcs c
  | [] -> None
let rec findc pcs p =
  match pcs with
  | (p',c)::pcs -> if p = p' then Some(c) else findc pcs p
  | [] -> None

let k = mkRandom blocksize
let qe = ref 0
let qd = ref 0
#if ideal
let log = ref ([] : (block * block) list)
let F p =
  match findc !pcs p with
  | Some(c) -> c // non-parametric;
                 // after CBC-collision avoidance,
                 // we will always use the "None" case
  | None    -> let c = mkfreshc !log blocksize
               log := (p,c)::!log
               c
let G c =
  match findp !log c with
  | Some(p) -> p
  | None    -> let p = mkfreshp !log blocksize
               log := (p,c)::!log
               p
#else
let F = AES k
let G = AESminus k
#endif
let enc p = incr qe; F p
let dec c = incr qd; G c
*)

F7 Interface: ENC.fs7

module ENC

(* Bulk encryption for TLS record, agile & assumed conditionally CPA with "Encode" for plaintexts *)
(* This module is trusted *)

open Bytes
open Encode
open TLSInfo
open Error
open Range

// ciphers consist of one or more blocks of bytes.
type cipher = b:bytes{Length(b) <= max_TLSCipher_fragment_length}

private type (;ki:epoch) key = {k:bytes}

type iv = bytes
private type (;ki:epoch) iv3 =
	| SomeIV of iv // SSL_3p0 and TLS_1p0
	| NoIV         // TLS_1p0 and TLS_1p2

private type (;ki:epoch)state =	{key: (;ki)key; iv: (;ki)iv3}

type (;ki:epoch)encryptor = (;ki)state
type (;ki:epoch)decryptor = (;ki)state

// We do not use the state, but an abstract ID over it, so that we can link
// encryptor and decryptor states
private function val StateID: ki:epoch * (;ki)state -> int

val GEN:    ki:epoch -> (e:(;ki)encryptor{StateID(ki,e)=0}) * (d:(;ki)decryptor{StateID(ki,d)=0})
val LEAK:   ki:epoch{not Safe(ki)} -> (;ki)state -> key:bytes * iv:bytes
val COERCE: ki:epoch{not Safe(ki)} -> key:bytes -> iv:bytes -> (;ki)state

(* an abstract predicate recording all encryption results. *)
predicate val ENCrypted:
  (e:epoch * ad:(;e)LHAEPlain.adata * c:cipher * 'a) -> bool // p:(;e,ad,CipherRangeClass(e,Length(c))) plain

val ENC: ki:epoch -> s:(;ki) encryptor -> ad:(;ki)LHAEPlain.adata -> r:range ->
  p:(;ki,ad,r)plain ->
  ( (s': (;ki) encryptor{StateID(ki,s') = StateID(ki,s)+1}) *
    (c : cipher{(Safe(ki) => ENCrypted(ki,ad,c,p)) /\ Length(c)=TargetLength(ki,r)}) )

val DEC: ki:epoch -> s:(;ki) decryptor -> ad:(;ki)LHAEPlain.adata ->
  c:cipher
  { (Safe(ki) => ?p'. ENCrypted(ki,ad,c,p')) /\ Length(c) >= MinTlen(ki) } ->
  ( (s': (;ki) decryptor{StateID(ki,s') = StateID(ki,s)+1}) *
    (p : (;ki,ad,CipherRangeClass(ki,Length(c)))plain {!p'. ENCrypted(ki,ad,c,p') => p=p'}))

type entry =
  (ki:epoch * ad:(;ki)LHAEPlain.adata * c:cipher * p:(;ki,ad,CipherRangeClass(ki,Length(c)))plain)
  { ENCrypted(ki,ad,c,p) }

val log: entry list ref
val cfind: e:epoch -> c:cipher -> xs: entry list ->
	(ad:(;e)LHAEPlain.adata * rg:range * (;e,ad,rg) Encode.plain)

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

miTLS

A verified reference TLS implementation

miTLS :: ENC

F# Interface: ENC.fsi

F# Implementation: ENC.fs

F7 Interface: ENC.fs7

Verification status

Module list

Trusted

Idealized

Verified