val genRSA (pk: RSAKey.pk) (vc: protocolVersion) : St rsapms
val genRSA (pk: RSAKey.pk) (vc: protocolVersion) : St rsapms
let genRSA (pk:RSAKey.pk) (vc:protocolVersion): St rsapms =
  let verBytes = versionBytes vc in
  let rnd = Random.sample32 46ul in
  let pms = verBytes @| rnd in
  if ideal && RSAKey.honest pk && RSAKey.strong vc then
     IdealRSAPMS({seed=pms})
  else
    ConcreteRSAPMS(pms)
﻿module MiTLS.PMS

(* Split from KEF *)

open MiTLS.Mem
open FStar.Bytes
open MiTLS.TLSConstants

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

let ideal = Flags.ideal_PMS // controls idealization of PMS.

type rsarepr = bytes
(*private*)
type rsaseed = {seed: rsarepr}

// To ideally avoid collisions concerns between Honest and Coerced pms we use a sum type.
type rsapms =
//#if ideal
  | IdealRSAPMS of rsaseed
//#endif
  | ConcreteRSAPMS of rsarepr

//#if ideal
//this function is used to determine whether idealization should be performed
let honestRSAPMS (pk:RSAKey.pk) (cv:TLSConstants.protocolVersion) pms =
  match pms with
  | IdealRSAPMS(s)    -> true
  | ConcreteRSAPMS(s) -> false
//#endif
/
prims.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.RSAKey.fst.checked MiTLS.Random.fst.checked MiTLS.Mem.fst.checked MiTLS.Flags.fst.checked MiTLS.CommonDH.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.PMS.fst
pk: MiTLS.RSAKey.pk -> vc: MiTLS.TLSConstants.protocolVersion
  -> FStar.HyperStack.ST.St MiTLS.PMS.rsapms
MiTLS.RSAKey.pk MiTLS.TLSConstants.protocolVersion Prims.op_AmpAmp MiTLS.PMS.ideal MiTLS.RSAKey.honest MiTLS.RSAKey.strong MiTLS.PMS.IdealRSAPMS MiTLS.PMS.Mkrsaseed Prims.bool MiTLS.PMS.ConcreteRSAPMS MiTLS.PMS.rsapms FStar.Bytes.bytes FStar.Bytes.op_At_Bar FStar.Bytes.lbytes FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t MiTLS.Random.sample32 FStar.UInt32.__uint_to_t MiTLS.TLSConstants.versionBytes
let genRSA (pk: RSAKey.pk) (vc: protocolVersion) : St rsapms =
  
let verBytes = versionBytes vc in
let rnd = Random.sample32 46ul in
let pms = verBytes @| rnd in
if ideal && RSAKey.honest pk && RSAKey.strong vc
then IdealRSAPMS ({ seed = pms })
else ConcreteRSAPMS (pms)