miTLS :: DH

F# Interface: DH.fsi

F# Implementation: DH.fs

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

open Bytes
open DHGroup

type secret = Key of bytes

#if ideal
// We maintain 4 logs:
// - a log DH parameters returned by pp
// - a log of honest gx and gy values
// - a log for looking up good pms values using gx and gy values
let goodPP_log = ref []
let honest_log = ref []
let log = ref []
let goodPP dhparams =  exists (fun el-> el = dhparams) !goodPP_log
let honest gx = exists (fun el-> el = gx) !honest_log
#endif

let private pp (pg:CoreKeys.dhparams) : p * g =
    let dhparams = pg.p, pg.g
    #if ideal
    goodPP_log := dhparams ::!goodPP_log
    #endif
    dhparams

let private dhparams p g: CoreKeys.dhparams = { p = p; g = g }

let gen_pp()     = pp (CoreDH.gen_params())

let default_pp() = pp (CoreDH.load_default_params())

let genKey p g: elt * secret =
    let ((x, _), (e, _)) = CoreDH.gen_key (dhparams p g)
    #if ideal
    honest_log := e::!honest_log
    #endif
    (e, Key x)

let exp p g (gx:elt) (gy:elt) (Key x) : CRE.dhpms =
    let pms = CoreDH.agreement (dhparams p g) x gy in
    //#begin-ideal
    #if ideal
    if honest gy && honest gx && goodPP (p,g)
    then

match tryFind (fun el -> fst el=(gx,gy)) !log with
      | Some(_,pms) -> pms
      | None ->
                 let pms=CRE.sampleDH p g gx gy
                 log := ((gx,gy),pms)::!log;
                 pms
    else CRE.coerceDH p g gx gy pms
    //#end-ideal
    #else
    CRE.coerceDH p g gx gy pms
    #endif

F7 Interface: DH.fs7

module DH

open Bytes
open DHGroup

// "Strong" parameter generation used by compliant servers,
// formally a precondition for signing them with an honest key.
predicate val PP: p:p * g:(;p) g -> bool

//#begin-abstraction
type (;p:p,g:(;p)g,gx:(;p)elt) secret
//#end-abstraction

// the RFCs are vague about best practices for ppgen
val gen_pp:     unit -> p:p * g:(;p) g {PP(p,g)}
val default_pp: unit -> p:p * g:(;p) g {PP(p,g)}

predicate HonestExponent of p:p * g:(;p)g * gx:(;p)elt
val genKey: p:p -> g: (;p) g -> gx:(;p) elt * (;p,g,gx) secret{
  HonestExponent(p,g,gx)}

val exp: p:p -> g:(;p)g -> gx:(;p) elt -> gy:(;p) elt -> x:(;p,g,gx) secret -> res:(;p,g,gx,gy) CRE.dhpms{
  HonestExponent(p,g,gx) /\ HonestExponent(p,g,gy) =>
    TLSInfo.HonestDHPMS(p,g,gx,gy)}

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 RSAKey DHGroup HASH HMAC TLSPRF Sig Cert TLSInfo Range DataStream AppFragment HSFragment TLSFragment StatefulPlain LHAEPlain MAC_SHA256 MAC_SHA1 MAC Encode ENC LHAE StatefulLHAE PRF CRE

miTLS

A verified reference TLS implementation

miTLS :: DH

F# Interface: DH.fsi

F# Implementation: DH.fs

F7 Interface: DH.fs7

Verification status

Module list

Trusted

Idealized

Verified