miTLS :: HSFragment

F# Interface: HSFragment.fsi

F# Implementation: HSFragment.fs

F7 Interface: HSFragment.fs7

(*
 * 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 HSFragment
open Bytes
open TLSInfo
open Range

private type (;ki:epoch,r:range) fragment = {frag: (;r)rbytes}
private type (;ki:epoch) stream = {sb:bytes list}

predicate Sent of ki:epoch * (;ki) stream * r:range * (;ki,r)fragment
assume !ki,s,r,f. Sent(ki,s,r,f)

type (;e:epoch,s:(;e)stream,r:range)plain = f:(;e,r)fragment{Auth(e) => Sent(e,s,r,f)}

function val Payload: e:epoch * r:range * (;e,r)fragment -> 'a // (;r)rbytes
private definition !e,r,f. Payload(e,r,f) = f.frag

function val EmptyStream: e:epoch -> (;e)stream
private definition !e. EmptyStream(e) = {sb = []}
val init: e:epoch -> s:(;e)stream{s = EmptyStream(e)}

val fragmentPlain: ki:epoch -> r:range -> b:(;r) rbytes -> f:(;ki,EmptyStream(ki),r) plain{b = Payload(ki,r,f)}
val fragmentRepr:  ki:epoch -> r:range -> f:(;ki,r) fragment -> b:(;r) rbytes{b = Payload(ki,r,f)}

val reStream: e:epoch -> s:(;e)stream -> r:range -> p:(;e,s,r)plain -> s':(;e)stream ->
	p':(;e,s',r)plain{Payload(e,r,p) = Payload(e,r,p')}

val widen: e:epoch -> r0:range -> r1:range {r1 = RangeClass(e,r0)} ->
    f0:(;e,r0)fragment -> f1:(;e,r1)fragment{Payload(e,r0,f0) = Payload(e,r1,f1) /\ !s. Sent(e,s,r0,f0) => Sent(e,s,r1,f1)}

function val Extend: e:epoch * s:(;e)stream * r:range * (;e,r)fragment -> 'a // (;e)stream
private definition !ki,s,r,f. Extend(ki,s,r,f) = {sb = f.frag :: s.sb }
val extend: e:epoch -> s:(;e)stream -> r:range -> f:(;e,r)fragment -> s':(;e)stream{s'=Extend(e,s,r,f)}

Verification status

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

miTLS

A verified reference TLS implementation

miTLS :: HSFragment

F# Interface: HSFragment.fsi

F# Implementation: HSFragment.fs

F7 Interface: HSFragment.fs7

Verification status

Module list

Trusted

Idealized

Verified