miTLS

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

// implemented using LHAE with a sequence number

open Bytes
open Error
open TLSInfo
open StatefulPlain
open Range

type rw =
    | ReaderState
    | WriterState

type state = {
  key: LHAE.LHAEKey;
  history: history
}

type reader = state
type writer = state

let GEN ki =
  let w,r = LHAE.GEN ki in
  let h = emptyHistory ki in
  ( { key = w; history = h},
    { key = r; history = h})
let COERCE ki (rw:rw) b =
  let k  = LHAE.COERCE ki b in
  let h = emptyHistory ki in
  { key = k; history = h}
let LEAK ki (rw:rw) s = LHAE.LEAK ki s.key

let history (ki:epoch) (rw:rw) s = s.history

type cipher = LHAE.cipher

let encrypt (ki:epoch) (w:writer) (ad0:adata) (r:range) (f:plain) =
  let h = w.history in
  let ad = LHAEPlain.makeAD ki h ad0 in
  let p = LHAEPlain.StatefulPlainToLHAEPlain ki h ad0 r f in
  let k,c = LHAE.encrypt ki w.key ad r p in
  let h = extendHistory ki ad0 h r f in
  let w = {key = k; history = h} in
  (w,c)

let decrypt (ki:epoch) (r:reader) (ad0:adata) (e:cipher) =
  let h = r.history in
  let ad = LHAEPlain.makeAD ki h ad0 in
  let res = LHAE.decrypt ki r.key ad e in
  match res with
    | Correct x ->
          let (k,rg,p) = x
          let f = LHAEPlain.LHAEPlainToStatefulPlain ki h ad0 rg p
          let h = extendHistory ki ad0 h rg f
          let r' = {history = h; key = k}
          correct ((r',rg,f))
    | Error (x,y) -> Error (x,y)

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

open Error
open Bytes
open TLSInfo
open Range

type rw =
	| ReaderState
	| WriterState

private type (;ki:epoch,rw:rw) state = {
  key    : (;ki) LHAE.LHAEKey;         // possibly stateful
  history: (;ki) StatefulPlain.history // ghost state, except for the sequence number
}

function val History: e:epoch * rw:rw * (;e,rw)state -> 'a //(;e)StatefulPlain.history
private definition !e,rw,s. History(e,rw,s) = s.history

type (;ki:epoch) reader = r:(;ki,ReaderState) state
type (;ki:epoch) writer = w:(;ki,WriterState) state

val GEN:    ki:succEpoch{Safe(ki)}     -> (;ki)reader * (;ki)writer
val COERCE: ki:succEpoch{not Auth(ki)} -> rw:rw -> b:bytes{Length(b)=LHAE.LHAESize(ki)} -> (;ki,rw)state
val LEAK:   ki:succEpoch{not Auth(ki)} -> rw:rw -> (;ki,rw)state -> b:bytes

val history: ki:epoch -> rw:rw -> s:(;ki,rw) state -> h:(;ki)StatefulPlain.history{h=History(ki,rw,s)}

// Ideally,
// the writer maintains a table (ki, h, ad, range, fragment, cipher) {...} [details?]
// when Safe(ki), the writer uses 0s instead of the actual fragment
// when Auth(ki), the reader decrypts by table lookup
// turning forgeries into errors; retrieving the "right" history index; returning the concrete decrypted range

type cipher = LHAE.cipher

predicate ENCrypted of e:epoch * h:(;e)StatefulPlain.history * ad:(;e)StatefulPlain.adata * cipher
private definition !e,h,ad,c.
  ENCrypted(e,h,ad,c) <=> LHAE.ENCrypted(e,LHAEPlain.MakeAD(e,h,ad),c)

val encrypt: ki:succEpoch ->
  wr:(;ki) writer ->
  ad:(;ki) StatefulPlain.adata ->
  rg:range ->
  f: (;ki,ad,History(ki,WriterState,wr),rg) StatefulPlain.plain ->
  (wr':(;ki) writer * c:cipher){
    History(ki,WriterState,wr') =
      StatefulPlain.ExtendHistory(ki,ad,History(ki,WriterState,wr),rg,f)
/\    (Safe(ki) => ENCrypted(ki,History(ki,WriterState,wr),ad,c))}

val decrypt: ki:succEpoch ->
  rd:(;ki) reader ->
  ad:(;ki) StatefulPlain.adata ->
  c:cipher ->
  res:((;ki) reader * rg:range * (;ki,ad,History(ki,ReaderState,rd),rg) StatefulPlain.plain) Result
  { !nrd,rg,f. res = Correct((nrd,rg,f)) =>
               (   History(ki,ReaderState,nrd) =
                   StatefulPlain.ExtendHistory(ki,ad,History(ki,ReaderState,rd),rg,f) /\
                   rg = CipherRangeClass(ki,Length(c)) /\
 	         (Safe(ki) =>
				( (!nrd,rg,f. res = Correct((nrd,rg,f)) => ENCrypted(ki,History(ki,ReaderState,rd),ad,c)) // /\
				//  (!rg,p. ENCrypted(ki,rd,ad,rg,StatefulPlain.Payload(ki,ad,rg,p),c) => (?nrd,rg. res = Correct((nrd,rg,p))))
				)
			 ) ) }

A verified reference TLS implementation

miTLS :: StatefulLHAE

F# Interface: StatefulLHAE.fsi

F# Implementation: StatefulLHAE.fs

F7 Interface: StatefulLHAE.fs7

Verification status

Module list

Trusted

Idealized

Verified