miTLS :: TLSFragment

F# Interface: TLSFragment.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 TLSFragment

open Bytes
open TLSInfo
open TLSConstants
open Range

type history

type fragment
type plain = fragment

val emptyHistory: epoch -> history
val extendHistory: epoch -> ContentType -> history -> range -> fragment -> history

val handshakeHistory: epoch -> history -> HSFragment.stream
val ccsHistory: epoch -> history -> HSFragment.stream
val alertHistory: epoch -> history -> HSFragment.stream

val plain: epoch -> ContentType -> history -> range -> bytes -> plain
val reprFragment: epoch -> ContentType -> range -> fragment -> bytes
val repr:  epoch -> ContentType -> history -> range -> plain -> bytes

val HSPlainToRecordPlain     : epoch -> history -> range -> HSFragment.plain -> plain
val CCSPlainToRecordPlain    : epoch -> history -> range -> HSFragment.plain -> plain
val AlertPlainToRecordPlain  : epoch -> history -> range -> HSFragment.plain -> plain
val AppPlainToRecordPlain    : epoch -> history -> range -> AppFragment.plain -> plain
val RecordPlainToHSPlain     : epoch -> history -> range -> plain -> HSFragment.plain
val RecordPlainToCCSPlain    : epoch -> history -> range -> plain -> HSFragment.plain
val RecordPlainToAlertPlain  : epoch -> history -> range -> plain -> HSFragment.plain
val RecordPlainToAppPlain    : epoch -> history -> range -> plain -> AppFragment.plain

#if ideal
val widen: epoch -> ContentType -> range -> fragment -> fragment
#endif

F# Implementation: TLSFragment.fs

module TLSFragment

open Error
open Bytes
open TLSInfo
open TLSConstants
open Range

type fragment =
    | FHandshake of HSFragment.fragment //Cf Handshake.fragment
    | FCCS of HSFragment.fragment
    | FAlert of HSFragment.fragment
    | FAppData of AppFragment.fragment
type plain = fragment

type history = {
  handshake: HSFragment.stream
  ccs:       HSFragment.stream
  alert:     HSFragment.stream
  appdata:   DataStream.stream
}

let emptyHistory ki =
    let es = HSFragment.init ki in
    let ehApp = DataStream.init ki in
    { handshake = es;
      ccs = es;
      alert = es;
      appdata = ehApp} in

let handshakeHistory (e:epoch) h = h.handshake
let ccsHistory (e:epoch) h = h.ccs
let alertHistory (e:epoch) h = h.alert

let plain ki (ct:ContentType) (h:history) (rg:range) b =
    match ct with
    | Handshake          -> FHandshake(HSFragment.fragmentPlain ki rg b)
    | Change_cipher_spec -> FCCS(HSFragment.fragmentPlain ki rg b)
    | Alert              -> FAlert(HSFragment.fragmentPlain ki rg b)
    | Application_data   -> FAppData(AppFragment.plain ki rg b)

let reprFragment ki (ct:ContentType) (rg:range) frag =
    match frag with
    | FHandshake(f) -> HSFragment.fragmentRepr ki rg f
    | FCCS(f)       -> HSFragment.fragmentRepr ki rg f
    | FAlert(f)     -> HSFragment.fragmentRepr ki rg f
    | FAppData(f)   -> AppFragment.repr ki rg f

let repr ki ct (h:history) rg frag = reprFragment ki ct rg frag

let HSPlainToRecordPlain    (e:epoch) (h:history) (r:range) (f:HSFragment.plain) = FHandshake(f)
let CCSPlainToRecordPlain   (e:epoch) (h:history) (r:range) (f:HSFragment.plain) = FCCS(f)
let AlertPlainToRecordPlain (e:epoch) (h:history) (r:range) (f:HSFragment.plain) = FAlert(f)
let AppPlainToRecordPlain   (e:epoch) (h:history) (r:range) (f:AppFragment.plain)= FAppData(f)

let RecordPlainToHSPlain    (e:epoch) (h:history) (r:range) ff =
    match ff with
    | FHandshake(f) -> f
    | FCCS(_)
    | FAlert(_)
    | FAppData(_)   -> unreachable "[RecordPlainToHSPlain] invoked on an invalid fragment"
let RecordPlainToCCSPlain    (e:epoch) (h:history) (r:range) ff =
    match ff with
    | FCCS(f)       -> f
    | FHandshake(_)
    | FAlert(_)
    | FAppData(_)   -> unreachable "[RecordPlainToCCSPlain] invoked on an invalid fragment"
let RecordPlainToAlertPlain    (e:epoch) (h:history) (r:range) ff =
    match ff with
    | FAlert(f)     -> f
    | FHandshake(_)
    | FCCS(_)
    | FAppData(_)   -> unreachable "[RecordPlainToAlertPlain] invoked on an invalid fragment"
let RecordPlainToAppPlain    (e:epoch) (h:history) (r:range) ff =
    match ff with
    | FAppData(f)   -> f
    | FHandshake(_)
    | FCCS(_)
    | FAlert(_)     -> unreachable "[RecordPlainToAppPlain] invoked on an invalid fragment"

let extendHistory (e:epoch) ct ss r frag =
  match ct,frag with
    | Handshake,FHandshake(f)      -> let s' = HSFragment.extend e ss.handshake r f in {ss with handshake = s'}
    | Alert,FAlert(f)              -> let s' = HSFragment.extend e ss.alert r f in {ss with alert = s'}
    | Change_cipher_spec,FCCS(f)   -> let s' = HSFragment.extend e ss.ccs r f in {ss  with ccs = s'}
    | Application_data,FAppData(f) -> let d,s' = AppFragment.delta e ss.appdata r f in {ss with appdata = s'}
    | _,_                          -> unexpectedError "[extendHistory] invoked on an invalid contenttype/fragment"

#if ideal
let widen e ct r0 f0 =
    let r1 = rangeClass e r0 in
    match ct,f0 with
    | Handshake,FHandshake(f)      -> let f1 = HSFragment.widen e r0 r1 f in FHandshake(f1)
    | Alert,FAlert(f)              -> let f1 = HSFragment.widen e r0 r1 f in FAlert(f1)
    | Change_cipher_spec,FCCS(f)   -> let f1 = HSFragment.widen e r0 r1 f in FCCS(f1)
    | Application_data,FAppData(f) -> let f1 = AppFragment.widen e r0 f in FAppData(f1)
    | _,_                          -> unexpectedError "[widen] invoked on an invalid contenttype/fragment"

#endif

F7 Interface: TLSFragment.fs7

module TLSFragment

(* Multiplexing the 4 content types used by TLS (a bit tedious) *)

open Bytes
open TLSInfo
open TLSConstants
open Range

private type (;e:epoch,ct:ContentType,rg:range) fragment =
    | FHandshake of f:(;e,rg)HSFragment.fragment {ct=Handshake}
    | FCCS       of f:(;e,rg)HSFragment.fragment {ct=Change_cipher_spec}
    | FAlert     of f:(;e,rg)HSFragment.fragment {ct=Alert}
    | FAppData   of f:(;e,rg)AppFragment.fragment{ct=Application_data}

function val Payload: e:epoch * ct:ContentType * r:range * (;e,ct,r)fragment -> 'a // (;r)rbytes
private definition !e,r,f. Payload(e,Handshake,         r,FHandshake(f)) = HSFragment.Payload(e,r,f)
private definition !e,r,f. Payload(e,Change_cipher_spec,r,FCCS(f))       = HSFragment.Payload(e,r,f)
private definition !e,r,f. Payload(e,Alert,             r,FAlert(f))     = HSFragment.Payload(e,r,f)
private definition !e,r,f. Payload(e,Application_data,  r,FAppData(f))   = AppFragment.Payload(e,r,f)

private type (;e:epoch) history = {
  handshake: (;e) HSFragment.stream;
  ccs:       (;e) HSFragment.stream;
  alert:     (;e) HSFragment.stream;
  appdata:   (;e) DataStream.stream }

function val HandshakeHistory: e:epoch * (;e) history -> 'a //(;e)HSFragment.stream
function val   AppDataHistory: e:epoch * (;e) history -> 'a //(;e)DataStream.stream
function val     AlertHistory: e:epoch * (;e) history -> 'a //(;e)HSFragment.stream
function val       CCSHistory: e:epoch * (;e) history -> 'a //(;e)HSFragment.stream

private definition !e,h. HandshakeHistory(e,h) = h.handshake
private definition !e,h. AlertHistory(e,h)     = h.alert
private definition !e,h. CCSHistory(e,h)       = h.ccs
private definition !e,h. AppDataHistory(e,h)   = h.appdata

val handshakeHistory: e:epoch -> h:(;e)history -> s:(;e)HSFragment.stream{s = HandshakeHistory(e,h)}
val ccsHistory: e:epoch -> h:(;e)history -> s:(;e)HSFragment.stream{s = CCSHistory(e,h)}
val alertHistory: e:epoch -> h:(;e)history -> s:(;e)HSFragment.stream{s = AlertHistory(e,h)}

predicate RecordSent of e:epoch * ct:ContentType * h:(;e) history * rg:range * (;e,ct,rg)fragment
private definition !e,ct,h,rg,d.
  RecordSent(e,ct,h,rg,d) <=> (
    (?f. ct=Handshake          /\ d = FHandshake(f) /\ HSFragment.Sent(e,HandshakeHistory(e,h),rg,f) ) \/
    (?f. ct=Change_cipher_spec /\ d = FCCS(f)       /\ HSFragment.Sent(e,CCSHistory(e,h),rg,f) ) \/
    (?f. ct=Alert              /\ d = FAlert(f)     /\ HSFragment.Sent(e,AlertHistory(e,h),rg,f) ) \/
    (?f. ct=Application_data   /\ d = FAppData(f)   /\ AppFragment.Sent(e,AppDataHistory(e,h),rg,f)))

ask !e,h,rg,f. HSFragment.Sent(e,HandshakeHistory(e,h),rg,f) =>
      RecordSent(e,Handshake,h,rg,FHandshake(f))

type (;e:epoch,ct:ContentType,h:(;e)history,rg:range) plain =
  f:(;e,ct,rg)fragment { Auth(e) => RecordSent(e,ct,h,rg,f) }

function val ExtendHistory: e:epoch * ct:ContentType * ss:(;e)history * r:range * (;e,ct,ss,r)plain -> 'a //(;e)history

val extendHistory: e:epoch -> ct:ContentType -> ss:(;e)history -> r:range ->
  f:(;e,ct,ss,r)plain -> ss':(;e)history{ss' = ExtendHistory(e,ct,ss,r,f)}

val plain: e:epoch{not Auth(e)} -> ct:ContentType -> h: (;e) history -> rg:range ->
  b:(;rg)rbytes -> p:(;e,ct,h,rg)plain {b = Payload(e,ct,rg,p)}

val reprFragment: e:epoch{not Safe(e)} -> ct:ContentType -> rg:range ->
  f:(;e,ct,rg)fragment -> b:(;rg)rbytes{b = Payload(e,ct,rg,f)}

val repr: e:epoch{not Safe(e)} -> ct:ContentType -> h: (;e) history -> rg:range ->
  p:(;e,ct,h,rg)plain -> b:(;rg)rbytes{b = Payload(e,ct,rg,p)}

val widen: e:succEpoch -> ct:ContentType ->
  r0:range ->
  f0:(;e,ct,r0)fragment ->
  f1:(;e,ct,RangeClass(e,r0))fragment{
    Payload(e,ct,r0,f0) = Payload(e,ct,RangeClass(e,r0),f1) /\
    !h. RecordSent(e,ct,h,r0,f0) =>
        RecordSent(e,ct,h,RangeClass(e,r0),f1)}

function val EmptyHistory: e:epoch -> (;e)history
private definition !e. EmptyHistory(e) = {
	handshake = HSFragment.EmptyStream(e);
	ccs = HSFragment.EmptyStream(e);
	alert = HSFragment.EmptyStream(e);
	appdata = DataStream.EmptyStream(e)}

val emptyHistory: e:epoch -> h:(;e)history{h = EmptyHistory(e)}

private definition !e,h,r,f. ExtendHistory(e,TLSConstants.Handshake,h,r,FHandshake(f)) =
	 { handshake = HSFragment.Extend(e,HandshakeHistory(e,h),r,f);
	   alert = AlertHistory(e,h);
	   ccs = CCSHistory(e,h);
	   appdata = AppDataHistory(e,h)}
private definition !e,h,r,f. ExtendHistory(e,TLSConstants.Alert,h,r,FAlert(f)) =
	 { handshake = HandshakeHistory(e,h);
	   alert = HSFragment.Extend(e,AlertHistory(e,h),r,f);
	   ccs = CCSHistory(e,h);
	   appdata = AppDataHistory(e,h)}
private definition !e,h,r,f. ExtendHistory(e,TLSConstants.Change_cipher_spec,h,r,FCCS(f)) =
	 { handshake = HandshakeHistory(e,h);
	   alert = AlertHistory(e,h);
	   ccs = HSFragment.Extend(e,CCSHistory(e,h),r,f);
	   appdata = AppDataHistory(e,h)}
private definition !e,h,r,f. ExtendHistory(e,TLSConstants.Application_data,h,r,FAppData(f)) =
	 { handshake = HandshakeHistory(e,h);
	   alert = AlertHistory(e,h);
	   ccs = CCSHistory(e,h);
	   appdata = AppFragment.Extend(e,AppDataHistory(e,h),r,f)}

function val HandshakeRecordPlain: e:epoch * h:(;e)history * r:range * f:(;e,h,r)HSFragment.plain -> 'a //(;e,TLSConstants.Handshake,h,r)plain
private definition !e,h,r,f. HandshakeRecordPlain(e,h,r,f) = FHandshake(f)
function val CCSRecordPlain: e:epoch * h:(;e)history * r:range * f:(;e,h,r)HSFragment.plain -> 'a //(;e,TLSConstants.Change_cipher_spec,h,r)plain
private definition !e,h,r,f. CCSRecordPlain(e,h,r,f) = FCCS(f)
function val AlertRecordPlain: e:epoch * h:(;e)history * r:range * f:(;e,h,r)HSFragment.plain -> 'a //(;e,TLSConstants.Alert,h,r)plain
private definition !e,h,r,f. AlertRecordPlain(e,h,r,f) = FAlert(f)
function val AppDataRecordPlain: e:epoch * h:(;e)history * r:range * f:(;e,h,r)AppFragment.plain -> 'a //(;e,TLSConstants.Application_data,h,r)plain
private definition !e,h,r,f. AppDataRecordPlain(e,h,r,f) = FAppData(f)

ask !e,h,h',r,f. h' = ExtendHistory(e,TLSConstants.Handshake,h,r,HandshakeRecordPlain(e,h,r,f)) =>
	( HandshakeHistory(e,h') = HSFragment.Extend(e,HandshakeHistory(e,h),r,f) /\
	  AlertHistory(e,h') = AlertHistory(e,h) /\
	  CCSHistory(e,h') = CCSHistory(e,h) /\
	  AppDataHistory(e,h') = AppDataHistory(e,h))
ask !e,h,h',r,f. h' = ExtendHistory(e,TLSConstants.Alert,h,r,AlertRecordPlain(e,h,r,f)) =>
	( AlertHistory(e,h') = HSFragment.Extend(e,AlertHistory(e,h),r,f) /\
	  HandshakeHistory(e,h') = HandshakeHistory(e,h) /\
	  CCSHistory(e,h') = CCSHistory(e,h) /\
	  AppDataHistory(e,h') = AppDataHistory(e,h))
ask !e,h,h',r,f. h' = ExtendHistory(e,TLSConstants.Change_cipher_spec,h,r,CCSRecordPlain(e,h,r,f)) =>
	( CCSHistory(e,h') = HSFragment.Extend(e,CCSHistory(e,h),r,f) /\
	  AlertHistory(e,h') = AlertHistory(e,h) /\
	  HandshakeHistory(e,h') = HandshakeHistory(e,h) /\
	  AppDataHistory(e,h') = AppDataHistory(e,h))
ask !e,h,h',r,f. h' = ExtendHistory(e,TLSConstants.Application_data,h,r,AppDataRecordPlain(e,h,r,f)) =>
	( AppDataHistory(e,h') = AppFragment.Extend(e,AppDataHistory(e,h),r,f) /\
	  AlertHistory(e,h') = AlertHistory(e,h) /\
	  CCSHistory(e,h') = CCSHistory(e,h) /\
	  HandshakeHistory(e,h') = HandshakeHistory(e,h))

ask !e,h,r,p. AppDataHistory(e,h) = AppDataHistory(e,ExtendHistory(e,TLSConstants.Handshake,h,r,HandshakeRecordPlain(e,h,r,p)))
ask !e,h,r,p. AppDataHistory(e,h) = AppDataHistory(e,ExtendHistory(e,TLSConstants.Alert,h,r,AlertRecordPlain(e,h,r,p)))

ask !e. HandshakeHistory(e,EmptyHistory(e)) = HSFragment.EmptyStream(e)
ask !e. AlertHistory(e,EmptyHistory(e))     = HSFragment.EmptyStream(e)
ask !e. CCSHistory(e,EmptyHistory(e))       = HSFragment.EmptyStream(e)
ask !e. AppDataHistory(e,EmptyHistory(e))   = DataStream.EmptyStream(e)

val HSPlainToRecordPlain: e:epoch -> h:(;e)history -> r:range ->
  d:(;e,HandshakeHistory(e,h),r) HSFragment.plain ->
  f:(;e,TLSConstants.Handshake,h,r) plain{f = HandshakeRecordPlain(e,h,r,d)}

val RecordPlainToHSPlain: e:epoch -> h:(;e) history -> r:range ->
  f:(;e,TLSConstants.Handshake,h,r) plain ->
  d:(;e,HandshakeHistory(e,h),r) HSFragment.plain{f = HandshakeRecordPlain(e,h,r,d)}

val CCSPlainToRecordPlain: e:epoch -> h:(;e)history -> r:range ->
  d:(;e,CCSHistory(e,h),r) HSFragment.plain ->
  f:(;e,TLSConstants.Change_cipher_spec,h,r) plain{f = CCSRecordPlain(e,h,r,d)}

val RecordPlainToCCSPlain: e:epoch -> h:(;e) history -> r:range ->
  f:(;e,TLSConstants.Change_cipher_spec,h,r) plain ->
  d:(;e,CCSHistory(e,h),r) HSFragment.plain{f = CCSRecordPlain(e,h,r,d)}

val AlertPlainToRecordPlain: e:epoch -> h:(;e)history -> r:range ->
  d:(;e,AlertHistory(e,h),r) HSFragment.plain ->
  f:(;e,TLSConstants.Alert,h,r) plain{f = AlertRecordPlain(e,h,r,d)}

val RecordPlainToAlertPlain: e:epoch -> h:(;e) history -> r:range ->
  f:(;e,TLSConstants.Alert,h,r) plain ->
  d:(;e,AlertHistory(e,h),r) HSFragment.plain{f = AlertRecordPlain(e,h,r,d)}

val AppPlainToRecordPlain: e:epoch -> h:(;e)history -> r:range ->
  d:(;e,AppDataHistory(e,h),r) AppFragment.plain ->
  f:(;e,TLSConstants.Application_data,h,r) plain{f = AppDataRecordPlain(e,h,r,d)}

val RecordPlainToAppPlain: e:epoch -> h:(;e) history -> r:range ->
  f:(;e,TLSConstants.Application_data,h,r) plain ->
  d:(;e,AppDataHistory(e,h),r) AppFragment.plain{f = AppDataRecordPlain(e,h,r,d)}

Verification status

The F# code of this module has been verified to meet its F7 interface.

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

miTLS

A verified reference TLS implementation

miTLS :: TLSFragment

F# Interface: TLSFragment.fsi

F# Implementation: TLSFragment.fs

F7 Interface: TLSFragment.fs7

Verification status

Module list

Trusted

Idealized

Verified