miTLS :: PwToken

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

// ------------------------------------------------------------------------
open Bytes
open TLSInfo
open DataStream
open Range

// ------------------------------------------------------------------------
type token
type username = string

val create   : unit -> token
val register : username -> token -> unit
val verify   : username -> token -> bool
val guess    : bytes -> token

// ------------------------------------------------------------------------
type delta = DataStream.delta

val MaxTkReprLen : int

val tk_repr  : epoch -> stream -> username -> token -> delta
val tk_plain : epoch -> stream -> range -> delta -> (username * token) option

val rp_repr  : epoch -> stream -> bool -> delta
val rp_plain : epoch -> stream -> range -> delta -> bool

F# Implementation: PwToken.fs

module PwToken

// ------------------------------------------------------------------------
open Bytes
open DER
open Nonce
open TLSInfo
open DataStream
open Range

// ------------------------------------------------------------------------
type username = string

type token =
  | GToken of bytes
  | BToken  of bytes

type utk = UTK of username * token

// ------------------------------------------------------------------------
let MaxTkReprLen = 512

// ------------------------------------------------------------------------
let tokens = ref ([] : utk list)

// ------------------------------------------------------------------------
let create () =
    let token = GToken (random 256)
    token

// ------------------------------------------------------------------------
let register (username : username) (token : token) =
    match token with
    | BToken _  -> ()
    | GToken tk ->
        let utk = UTK (username, token)
        tokens := utk :: !tokens

// ------------------------------------------------------------------------
let rec verify_r (utk : utk) (tokens : utk list) =
    match tokens with
    | [] -> false
    | x :: tokens -> (utk = x) || verify_r utk tokens

let verify (username : username) (token : token) =
    let utk = UTK (username, token)
    verify_r utk !tokens

// ------------------------------------------------------------------------
let guess (bytes : bytes) =
    BToken bytes

// ------------------------------------------------------------------------
type delta = DataStream.delta

// ------------------------------------------------------------------------
let tk_good (token : token) =
    match token with GToken _ -> true | _ -> false

let tk_bytes (token : token) =
    match token with
    | GToken bytes -> bytes
    | BToken bytes -> bytes

// ------------------------------------------------------------------------
let tk_repr (e : epoch) (s : stream) (u : username) (tk : token) : delta =
    let tkgood  = tk_good  tk
    let tkbytes = tk_bytes tk

let der = DER.Sequence [DER.Utf8String u; DER.Bool tkgood; DER.Bytes tkbytes]
    let der = DER.encode der

if Bytes.length der > MaxTkReprLen then
        Error.unexpectedError "PwToken.tk_repr: token too large"
    else
        DataStream.createDelta e s (0, MaxTkReprLen) der

// ------------------------------------------------------------------------
let tk_plain (e : epoch) (s : stream) (r : range) (delta : delta) : (username * token) option =
    let data =
        DataStream.deltaRepr e s r delta
    in
        match DER.decode data with
        | Some (Sequence [Utf8String u; Bool tkgood; Bytes tkbytes]) ->
            let token = if tkgood then GToken tkbytes else BToken tkbytes in
                Some (u, token)
        | _ -> None

// ------------------------------------------------------------------------
let rp_repr (e : epoch) (s : stream) (b : bool) : delta =
    let bytes = DER.encode (DER.Bool b)

if Bytes.length bytes > MaxTkReprLen then
        Error.unexpectedError "PwToken.rp_repr: token too large"
    else
        DataStream.createDelta e s (0, MaxTkReprLen) bytes

// ------------------------------------------------------------------------
let rp_plain (e : epoch) (s : stream) (r : range) (d : delta) : bool =
    let data =
        DataStream.deltaRepr e s r d
    in
        match DER.decode data with
        | Some (DER.Bool b) -> b
        | _ -> false

F7 Interface: PwToken.fs7

module PwToken

// ------------------------------------------------------------------------
open Bytes
open TLSInfo
open DataStream
open Range

// ------------------------------------------------------------------------
type username = string

type token =
  | GToken of bytes
  | BToken of bytes

private type utk = UTK of username * token

predicate GoodClient      of unit
predicate GoodToken       of token
predicate RegisteredToken of utk

assume !bs.     GoodToken(GToken(bs))
assume !bs. not GoodToken(BToken(bs))

private val tokens : (utk:utk{RegisteredToken(utk)}) list ref

function val TokenBytes : token -> bytes

definition !bs. TokenBytes(GToken(bs)) = bs
definition !bs. TokenBytes(BToken(bs)) = bs

// ------------------------------------------------------------------------
private val verify_r :
     utk:utk
  -> tokens:(utk:utk{RegisteredToken(utk)}) list
  -> b:bool{b = true => RegisteredToken(utk)}

// ------------------------------------------------------------------------
val create   : unit{GoodClient()} -> tk:token{GoodToken(tk)}
val register : u:username -> tk:token{GoodToken(tk)} -> unit{RegisteredToken(UTK(u, tk))}
val verify   : u:username -> tk:token -> b:bool{b = true => RegisteredToken(UTK(u, tk))}
val guess    : bytes -> tk:token{not GoodToken(tk)}

// ------------------------------------------------------------------------
private val tk_good  : tk:token -> b:bool{b = true => GoodToken(tk)}
private val tk_bytes : tk:token -> bs:bytes{bs = TokenBytes(tk)}

// ------------------------------------------------------------------------
type (;ki : epoch, s : (;ki)stream, r : range) delta = (;ki, s, r) DataStream.delta

private val MaxTkReprLen : nat

// ------------------------------------------------------------------------
val tk_repr :
     ki : epoch
  -> s  : (;ki) stream{s=EmptyStream(ki)}
  -> u  : username
  -> tk : token

-> (;ki, s, (0, MaxTkReprLen)) delta

val tk_plain :
     ki : epoch
  -> s  : (;ki) stream
  -> r  : range
  -> d  : (;ki, s, r) delta

-> (username * token) option

// ------------------------------------------------------------------------
val rp_repr :
     ki : epoch
  -> s  : (;ki)stream
  -> b  : bool

-> (;ki, s, (0, MaxTkReprLen)) delta

val rp_plain :
     ki : epoch
  -> s  : (;ki) stream
  -> r  : range
  -> d  : (;ki, s, r) delta

-> bool

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 Nonce DER TLSConstants RSAKey DHGroup HASH Sig Cert TLSInfo Range DataStream

miTLS

A verified reference TLS implementation

miTLS :: PwToken

F# Interface: PwToken.fsi

F# Implementation: PwToken.fs

F7 Interface: PwToken.fs7

Verification status

Module list

Trusted

Idealized

Verified