miTLS :: Sig

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

open Bytes
open TLSConstants

(* ------------------------------------------------------------------------ *)
type alg   = sigHashAlg

type text = bytes
type sigv = bytes

(* ------------------------------------------------------------------------ *)
type skey
type pkey

val create_skey: hashAlg -> CoreSig.sigskey -> skey
val create_pkey: hashAlg -> CoreSig.sigpkey -> pkey

val repr_of_skey: skey -> CoreSig.sigskey * hashAlg
val repr_of_pkey: pkey -> CoreSig.sigpkey * hashAlg

val sigalg_of_skeyparams : CoreSig.sigskey -> sigAlg
val sigalg_of_pkeyparams : CoreSig.sigpkey -> sigAlg

(* ------------------------------------------------------------------------ *)
val gen    : alg -> pkey * skey
val sign   : alg -> skey -> text -> sigv
val verify : alg -> pkey -> text -> sigv -> bool

F# Implementation: Sig.fs

module Sig

open Bytes
open TLSConstants

(* ------------------------------------------------------------------------ *)

type alg = sigHashAlg

type text = bytes
type sigv = bytes

(* ------------------------------------------------------------------------ *)
type skey = { skey : CoreSig.sigskey * hashAlg }
type pkey = { pkey : CoreSig.sigpkey * hashAlg }

let create_skey (h : hashAlg) (p : CoreSig.sigskey) = { skey = (p, h) }
let create_pkey (h : hashAlg) (p : CoreSig.sigpkey) = { pkey = (p, h) }

let repr_of_skey { skey = skey } = skey
let repr_of_pkey { pkey = pkey } = pkey

let sigalg_of_skeyparams = function
    | CoreSig.SK_RSA _ -> SA_RSA
    | CoreSig.SK_DSA _ -> SA_DSA

let sigalg_of_pkeyparams = function
    | CoreSig.PK_RSA _ -> SA_RSA
    | CoreSig.PK_DSA _ -> SA_DSA

#if ideal
// We maintain two logs:
// - a log of honest public keys (a,pk), not necessarily with strong crypto
// - a log of (a,pk,t) entries for all honestly signed texts

type entry = alg * pkey * text
// type entry = a:alg * pk:(;a) pk * t:text * s:(;a) sigv { Msg(a,pk,t) }

let honest_log = ref ([]: (alg * skey * pkey) list)
let log        = ref ([]: entry list)

let rec assoc hll pk =
    match hll with
      | (pk',sk')::_ when pk=pk' -> Some ()
      | _::hll                   -> assoc hll pk
      | []                       -> None

let rec pk_of_log sk hll =
    match hll with
        (pk',sk')::hll_tail when sk=sk' -> Some (pk')
      | _::hll_tail -> pk_of_log sk hll_tail
      | [] -> None

let pk_of (sk:skey) =
    let _,_,pk = (find (fun (_,sk',_) -> sk=sk') !honest_log )
    pk

let honest a pk = exists (fun (a',_,pk') -> a=a' && pk=pk') !honest_log
let strong a = if a=(SA_DSA ,SHA384) then true else false
#endif

(* ------------------------------------------------------------------------ *)
let sign (a: alg) (sk: skey) (t: text): sigv =
    let asig, ahash = a in
    let { skey = (kparams, khash) } = sk in

if ahash <> khash then
        Error.unexpectedError
            (sprintf "Sig.sign: requested sig-hash = %A, but key requires %A"
                ahash khash)
    if asig <> sigalg_of_skeyparams kparams then
        Error.unexpectedError
            (sprintf "Sig.sign: requested sig-algo = %A, but key requires %A"
                asig (sigalg_of_skeyparams kparams))

let signature =
        match khash with
        | NULL    -> CoreSig.sign None                     kparams t
        | MD5     -> CoreSig.sign (Some CoreSig.SH_MD5)    kparams t
        | SHA     -> CoreSig.sign (Some CoreSig.SH_SHA1  ) kparams t
        | SHA256  -> CoreSig.sign (Some CoreSig.SH_SHA256) kparams t
        | SHA384  -> CoreSig.sign (Some CoreSig.SH_SHA384) kparams t
        | MD5SHA1 ->
            let t = HASH.hash MD5SHA1 t in
            CoreSig.sign None kparams t
    #if ideal
    log := (a, pk_of sk, t)::!log
    #endif
    signature

(* ------------------------------------------------------------------------ *)
let verify (a : alg) (pk : pkey) (t : text) (s : sigv) =
    let asig, ahash = a in
    let { pkey = (kparams, khash) } = pk in

if ahash <> khash then
        Error.unexpectedError
            (sprintf "Sig.verify: requested sig-hash = %A, but key requires %A"
                ahash khash)
    if asig <> sigalg_of_pkeyparams kparams then
        Error.unexpectedError
            (sprintf "Sig.verify: requested sig-algo = %A, but key requires %A"
                asig (sigalg_of_pkeyparams kparams))

let result =
        match khash with
        | NULL    -> CoreSig.verify None                     kparams t s
        | MD5     -> CoreSig.verify (Some CoreSig.SH_MD5)    kparams t s
        | SHA     -> CoreSig.verify (Some CoreSig.SH_SHA1  ) kparams t s
        | SHA256  -> CoreSig.verify (Some CoreSig.SH_SHA256) kparams t s
        | SHA384  -> CoreSig.verify (Some CoreSig.SH_SHA384) kparams t s
        | MD5SHA1 ->
            let t = HASH.hash MD5SHA1 t in
            CoreSig.verify None kparams t s
    #if ideal //#begin-idealization
    let result = if strong a && honest a pk
                    then result && memr !log (a,pk,t)
                    else result
    #endif //#end-idealization
    result

(* ------------------------------------------------------------------------ *)
let gen (a:alg) : pkey * skey =
    let asig, ahash  = a in
    let (pkey, skey) =
        match asig with
        | SA_RSA -> CoreSig.gen CoreSig.SA_RSA
        | SA_DSA -> CoreSig.gen CoreSig.SA_DSA
        | _      -> Error.unexpectedError "[gen] invoked on unsupported algorithm"
    let p,s =  ({ pkey = (pkey, ahash) }, { skey = (skey, ahash) })
    #if ideal
    honest_log := (a,s,p)::!honest_log
    #endif
    (p,s)

let leak (a:alg) (s:skey) : CoreSig.sigskey =
    let (sk, ahash) = repr_of_skey s
    sk

let coerce (a:alg)  (p:pkey)  (csk:CoreSig.sigskey) : skey =
    let (_,ahash)=a in
    create_skey ahash csk

F7 Interface: Sig.fs7

module Sig

open Bytes
open TLSConstants

// TLS uses three signatures algorithms, together with hash algorithm.
// We verify TLS security relative to those *combinations* of algorithms
// that provide CMA-security, as specified in this interface.
// However, none of them are CMA-secure in the standard model under an
// assumption weaker than "This scheme is secure".

// This interface is adapted from the one described in CCS'11:
//
//      Cedric Fournet, Markulf Kohlweiss, Pierre-Yves Strub: Modular
//      code-based cryptographic verification. ACM Conference on Computer
//      and Communications Security 2011: 341-350
//
// Its implementation is trusted, not verified.

//*********************** Cryptographic agility ****************************

// note that the same key may be used with different hashes.
// so we require some joint security assumption for them

// TLS 1.2 provides explicit support for it:
// [1.2] - Substantial cleanup to the client's and server's ability to
//         specify which hash and signature algorithms they will accept.
//         Note that this also relaxes some of the constraints on signature
//         and hash algorithms from previous versions of TLS.

// implements SignatureAndHashAlgorithm, with fewer values for hashAlg

type alg   = sigHashAlg

type text = bytes
type (;a:alg) sigv = bytes

// with TLS 1.2, this explicitly contains a; see DigitallySigned struct

// Summary of the extension logic for the client:
// - specific to TLS 1.2
// - cs indicates sigAlg but not hashAlg, but "this is historical"
// - extension indicates supported algs (not necessarily following the cs)
// - no extension == client supports exactly the default alg

//********************** Ideal Functionality for Signing ***********************

//#begin-abstraction
type (;a:alg) skey
//#end-abstraction
type (;a:alg) pkey

function val PK: 'a -> 'b // a:alg * (;a)skey -> vkey
predicate Msg of a:alg * (;a)pkey * text
predicate Honest of a:alg * (;a) pkey
predicate Strong of alg

val gen:     a:alg -> pk:(;a) pkey * sk:(;a) skey { pk = PK(sk) }
val sign:    a:alg -> sk:(;a) skey -> t:text{Msg(a,PK(sk),t)} -> (;a) sigv
val verify:  a:alg -> pk:(;a) pkey -> t:text -> m:(;a) sigv ->
  b:bool {(b=true /\ Strong(a) /\ Honest(a,pk)) => Msg(a,pk,t)}

val coerce:  a:alg -> p:(;a) pkey{not Honest(a,p)} -> CoreSig.sigskey -> s:(;a)skey{p = PK(s)}
val leak:    a:alg -> s:(;a) skey{not Honest(a,PK(s))} -> CoreSig.sigskey

Verification status

This module is idealized: it contains both concrete F# code and an ideal implementation (when "ideal" flag set to true). The concrete code is not verified. Where applicable, we verify that the ideal implementation matches the F7 interface.

Verification depends on the F7 interfaces of the following modules: Error Bytes TLSConstants HASH

miTLS

A verified reference TLS implementation

miTLS :: Sig

F# Interface: Sig.fsi

F# Implementation: Sig.fs

F7 Interface: Sig.fs7

Verification status

Module list

Trusted

Idealized

Verified