DHGroup.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 DHGroup

open Bytes
open DHDB
open CoreKeys
open TLSError

// Marks "Strong" parameter generation used by compliant servers,
// formally a precondition for signing them with an honest key.
predicate PP of bytes * bytes

// For public parameters and exchanged values.
// We use an abstract predicate to ensure that elements
// are bytes that have been correctly generated or checked,
// e.g. Elt(p,g,b) => Num(b) in [2..p-1) /\ order(b) = order(g)

predicate Elt of bytes * bytes * bytes

type (;p:bytes,g:bytes) elt = b:bytes{ Elt(p,g,b) }

theorem !p,g. PP(p,g) => Elt(p,g,g)

private val goodPP_log: (dhparams list) ref
private val pp: dhp:dhparams ->
	dhp':dhparams {dhp = dhp' /\ PP(dhp.dhp,dhp.dhg)}
val goodPP: dhp:dhparams -> b:bool{b = true <=> PP(dhp.dhp,dhp.dhg)}

val genElement: dhp:dhparams -> (;dhp.dhp,dhp.dhg) elt
val checkParams: dhdb -> nat * nat -> p:bytes -> g:bytes ->
	((dhdb * dhp:dhparams){PP(p,g) /\ dhp.dhp = p /\ dhp.dhg = g}) Result

val checkElement: dhp:dhparams{PP(dhp.dhp,dhp.dhg)} -> b:bytes -> (b':(;dhp.dhp,dhp.dhg) elt {b = b'}) option

val defaultDHparams: string -> dhdb -> nat * nat -> ((dhdb * dhp:dhparams){PP(dhp.dhp,dhp.dhg)})