miTLS :: Range

F# Interface: Range.fsi

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

open Bytes
open TLSInfo
open TLSConstants

type range = nat * nat
type rbytes = bytes

let rangeSum (l0,h0) (l1,h1) =
  let l = l0 + l1
  let h = h0 + h1
  (l,h)

let ivSize e =
    let si = epochSI(e) in
    let authEnc = authencAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match authEnc with
    | MACOnly _ -> 0
    | MtE (encAlg,_) ->
        match encAlg with
        | Stream_RC4_128 -> 0
        | CBC_Stale(_) -> 0
        | CBC_Fresh(alg) -> blockSize alg
    | AEAD (_,_) -> Error.unexpectedError "[ivSize] invoked on unsupported ciphersuite"

let fixedPadSize (si:SessionInfo) = 1

let maxPadSize si =
    let authEnc = authencAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match authEnc with
    | MACOnly _ -> 0
    | MtE(enc,_) ->

let blockAlignPadding e len =
    let si = epochSI(e) in
    let authEnc = authencAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match authEnc with
    | MACOnly _ -> 0
    | MtE(enc,_) ->
        match enc with
        | Stream_RC4_128 -> 0
        | CBC_Stale(alg) | CBC_Fresh(alg) ->
            let bs = blockSize alg in
            let fp = fixedPadSize si in
            let overflow = (len + fp) % bs //@ at least fp bytes of fixed padding
            if overflow = 0 then fp else fp + bs - overflow
    | _ -> Error.unexpectedError "[maxPadSize] invoked on unsupported ciphersuite"

//@ From plaintext range to ciphertext length
let targetLength e (rg:range) =
    let (_,h) = rg in
    let si = epochSI(e) in
    let macLen = macSize (macAlg_of_ciphersuite si.cipher_suite si.protocol_version) in
    let ivL = ivSize e in
    let prePad = h + macLen in
    let padLen = blockAlignPadding e prePad in
    let res = ivL + prePad + padLen in
    if res > max_TLSCipher_fragment_length then
        Error.unexpectedError "[targetLength] given an invalid input range."
    else
        res

let minMaxPad si =
    let maxPad = maxPadSize si in
    if maxPad = 0 then
        (0,0)
    else
        let fp = fixedPadSize si in
        (fp,maxPad)

//@ From ciphertext length to (maximal) plaintext range
let cipherRangeClass (e:epoch) tlen =
    let si = epochSI(e) in
    let macSize = macSize (macAlg_of_ciphersuite si.cipher_suite si.protocol_version) in
    let ivL = ivSize e in
    let (minPad,maxPad) = minMaxPad si in
    let max = tlen - ivL - macSize - minPad in
    if max < 0 then
        Error.unexpectedError "[cipherRangeClass] the given tlen should be of a valid ciphertext"
    else
        let min = max - maxPad in
        if min < 0 then
            let rg = (0,max) in
            rg
        else
            let rg = (min,max) in
            rg

let rangeClass (e:epoch) (r:range) =
    let tlen = targetLength e r in
    cipherRangeClass e tlen

F7 Interface: Range.fs7

module Range

(* This modules defines the range computations for length-hiding *)

open Bytes
open TLSInfo
open TLSConstants

type range = low:nat * high:nat { low <= high }
type (;r:range) rbytes = b:bytes { ?l,h. r = (l,h) /\ l <= Length(b) /\ Length(b) <= h }
function val Sum: range * range -> range
definition !l0,h0,l1,h1. Sum((l0,h0),(l1,h1)) = (l0+l1,h0+h1)
val rangeSum: r0:range -> r1:range -> r:range{r = Sum(r0,r1)}

predicate SubRange of range * range
definition !l0,l1,h0,h1. SubRange((l0,h0),(l1,h1)) <=> l1 <= l0 && h0 <= h1

function val RangeClass: epoch * range -> range
function val TargetLength: epoch * range -> nat
function val CipherRangeClass: epoch * nat -> range

definition !e,r. RangeClass(e,r) = CipherRangeClass(e,TargetLength(e,r))
theorem !e,t,rg.  rg = CipherRangeClass(e,t) => t = TargetLength(e,rg)
theorem !e,r. SubRange(r,RangeClass(e,r))

function val IVSize: epoch -> nat
definition !e,mac,alg.
	((CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MACOnly(mac) \/
	  CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(Stream_RC4_128,mac) \/
	  CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Stale(alg),mac))
	 => IVSize(e) = 0 ) /\
	( CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Fresh(alg),mac)
	 => IVSize(e)= BlockSize(alg) )

val ivSize: e:succEpoch -> l:nat{l=IVSize(e)}

val fixedPadSize: si:SessionInfo -> l:nat{l=1}

function val MaxPadSize: si:SessionInfo * unit -> nat
private definition !si,alg'.
	((?mac,alg. CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MACOnly(mac) \/
	  CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(Stream_RC4_128,mac))
	 <=> MaxPadSize(si,()) = 0 ) /\
	((?mac,alg. CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(CBC_Fresh(alg),mac) \/
	  CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(CBC_Stale(alg),mac)) /\
	 (si.protocol_version = TLS_1p0 \/ si.protocol_version = TLS_1p1 \/ si.protocol_version = TLS_1p2)
	 <=>   MaxPadSize(si,()) = 255 )  /\
	((?mac. CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(CBC_Fresh(alg'),mac) \/
	  CipherSuiteAuthEncAlg(si.cipher_suite,si.protocol_version) = MtE(CBC_Stale(alg'),mac)) /\
	 (si.protocol_version = SSL_3p0)
	 <=>   MaxPadSize(si,()) = BlockSize(alg') )
val maxPadSize: si:SessionInfo -> l:nat{l = MaxPadSize(si,())}

val minMaxPad: si:SessionInfo -> l:nat * h:nat{
	(MaxPadSize(si,()) = 0 /\ l = 0 /\ h = 0 ) \/
	 MaxPadSize(si,()) > 0 /\ l = 1 /\ h = MaxPadSize(si,())}

// Padding computations
function val BlockAligned: epoch * nat -> nat
definition !e,mac,alg,l.
	((CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MACOnly(mac) \/
	  CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(Stream_RC4_128,mac))
	 => BlockAligned(e,l) = 0 ) /\
	((CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Fresh(alg),mac) \/
	  CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Stale(alg),mac))
	 =>  ( BlockAligned(e,l) >= 1 /\ BlockAligned(e,l) < (BlockSize(alg) + 1) ) )

// We are not precise enough to prove this
private assume !e,mac,alg,l,l'.
	((CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Fresh(alg),mac) \/
	  CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Stale(alg),mac)) /\
	  (l' >= 1) /\ (l' <= (BlockSize(alg) + 1)) )
	 => (l' = BlockAligned(e,l))
private val blockAlignPadding: e:succEpoch -> l:nat -> l':nat{l' = BlockAligned(e,l)}

definition !e,l,h.
	TargetLength(e,(l,h)) =
		IVSize(e) + h + MacSize(CipherSuiteMACAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version)) +
		BlockAligned(e,h + MacSize(CipherSuiteMACAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version)))

val targetLength: e:succEpoch -> r:range ->
  tlen:nat {tlen = TargetLength(e,r) /\ tlen <= max_TLSCipher_fragment_length}

definition !h,tlen,e,l. (?alg,mac. (l,h) = CipherRangeClass(e,tlen) /\
	((CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Fresh(alg),mac) \/
	  CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(CBC_Stale(alg),mac))) ) <=>
	( h >= 0 /\
	  (h = tlen - IVSize(e) -
		   MacSize(CipherSuiteMACAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version)) - 1) /\
	  ( (h >= 255 /\ l = h - 255) \/
	    (h < 255 /\ l = 0 )
	  )
	)

definition !e,l,h,tlen. (?alg,mac. (l,h) = CipherRangeClass(e,tlen) /\
	((CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MACOnly(mac) \/
	  CipherSuiteAuthEncAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) = MtE(Stream_RC4_128,mac))) ) <=>
	( h >= 0 /\
	  (h = tlen - IVSize(e) -
		   MacSize(CipherSuiteMACAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version)) ) /\
	  ( l = h
	  )
	)

val cipherRangeClass: e:succEpoch ->
  tlen:nat{tlen <= max_TLSCipher_fragment_length} ->
  r:range {r = CipherRangeClass(e,tlen)}

val rangeClass: e:succEpoch -> r0:range -> r1:range{r1 = RangeClass(e,r0)}

Verification status

This module is trusted: its F# code is assumed to meet its F7 interface.

Verification depends on the F7 interfaces of the following modules: Error Bytes TLSConstants RSAKey DHGroup HASH Sig Cert TLSInfo

miTLS

A verified reference TLS implementation

miTLS :: Range

F# Interface: Range.fsi

F# Implementation: Range.fs

F7 Interface: Range.fs7

Verification status

Module list

Trusted

Idealized

Verified