DH.fs7

(*
 * Copyright 2015 INRIA and Microsoft Corporation
 * 
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 * 
 *     http://www.apache.org/licenses/LICENSE-2.0
 * 
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 *)

module DH

open Bytes
open DHGroup
open CoreKeys

//#begin-abstraction
private type (;p:bytes, g:bytes, gx:(;p,g)elt) secret = Key of bytes
//#end-abstraction

// We maintain 2 logs:
// - a log of honest gx and gy values
// - a log for looking up honest pms values using gx and gy values

// Any parameters returned by the Core modules are taken from the trusted DHDB,
// which only contains good parameters.

// 1: log of honest gx and gy values
type honest_entry = (dhp:dhparams * (;dhp.dhp,dhp.dhg) elt){PP(dhp.dhp,dhp.dhg)}
private val honest_log: (honest_entry list) ref

// marks "Honest" exponentials generated using genKey (or serverGen)
predicate type predHE = HonestExponential of p:bytes * g:bytes * gx:(;p,g) elt
private val honest: dhp:dhparams -> e:(;dhp.dhp,dhp.dhg) elt -> b:bool{b = true <=> HonestExponential(dhp.dhp,dhp.dhg,e)}

definition !p,g,gx,gy. PMS.SafeDH(p,g,gx,gy) <=> HonestExponential(p,g,gx) /\ HonestExponential(p,g,gy) /\ PP(p,g)

ask !p,g,gx,gy. not HonestExponential(p,g,gx) => not PMS.SafeDH(p,g,gx,gy)
ask !p,g,gx,gy. not HonestExponential(p,g,gy) => not PMS.SafeDH(p,g,gx,gy)
ask !p,g,gx,gy. not PP(p,g) => not PMS.SafeDH(p,g,gx,gy)
val safeDH: dhp:dhparams -> gx:(;dhp.dhp,dhp.dhg)elt -> gy:(;dhp.dhp,dhp.dhg)elt -> b:bool { b=true <=> PMS.SafeDH(dhp.dhp,dhp.dhg,gx,gy) }

// 2: log for looking up honest pms values using gx and gy values
type entry = dhp:dhparams * gx:(;dhp.dhp,dhp.dhg) elt * gy:(;dhp.dhp,dhp.dhg) elt * pms:(;dhp.dhp,dhp.dhg, gx, gy) PMS.dhpms{PMS.HonestDHPMS(dhp.dhp,dhp.dhg,gx,gy,pms)}
private val log: entry list ref
private val assoc: dhp:dhparams -> gx:(;dhp.dhp,dhp.dhg)elt -> gy:(;dhp.dhp,dhp.dhg)elt -> entry list -> pmsoption:(;dhp.dhp, dhp.dhg, gx, gy) PMS.dhpms option{!pms. pmsoption=Some(pms) => PMS.HonestDHPMS(dhp.dhp,dhp.dhg,gx,gy,pms)}

val leak  : dhp:dhparams -> gx:(;dhp.dhp,dhp.dhg)elt -> x:(;dhp.dhp,dhp.dhg,gx)secret{not HonestExponential(dhp.dhp,dhp.dhg,gx)} -> bytes
val coerce: dhp:dhparams -> gx:(;dhp.dhp,dhp.dhg)elt{not HonestExponential(dhp.dhp,dhp.dhg,gx)} -> b:bytes -> x:(;dhp.dhp,dhp.dhg,gx)secret

val genKey: dhp:dhparams -> gx:(;dhp.dhp,dhp.dhg)elt * (;dhp.dhp,dhp.dhg,gx) secret{HonestExponential(dhp.dhp,dhp.dhg,gx)}

val serverGen: string -> DHDB.dhdb -> nat * nat ->
	(DHDB.dhdb * dhp:dhparams * gs:(;dhp.dhp,dhp.dhg) elt * (;dhp.dhp,dhp.dhg,gs) secret
		{PP(dhp.dhp,dhp.dhg) /\ HonestExponential(dhp.dhp,dhp.dhg,gs)})

val clientGenExp: dhp:dhparams{PP(dhp.dhp,dhp.dhg)} -> gs:(;dhp.dhp,dhp.dhg) elt
				      -> (gc:(;dhp.dhp,dhp.dhg) elt * res:(;dhp.dhp,dhp.dhg,gs,gc) PMS.dhpms)
					     {HonestExponential(dhp.dhp,dhp.dhg,gc) /\
							(HonestExponential(dhp.dhp,dhp.dhg,gs) => PMS.HonestDHPMS(dhp.dhp,dhp.dhg,gs,gc,res))}

val serverExp: dhp:dhparams{PP(dhp.dhp,dhp.dhg)} -> gs:(;dhp.dhp,dhp.dhg) elt{HonestExponential(dhp.dhp,dhp.dhg,gs)} -> gc:(;dhp.dhp,dhp.dhg) elt -> s:(;dhp.dhp,dhp.dhg,gs) secret
				   -> res:(;dhp.dhp,dhp.dhg,gs,gc) PMS.dhpms{HonestExponential(dhp.dhp,dhp.dhg,gc) => PMS.HonestDHPMS(dhp.dhp,dhp.dhg,gs,gc,res)}