anchor.diff:  
       (* the post of this call is !sx,cy. PP((p,g) /\ DHE.Exp((p,g),x,cy)) /\ DHE.Exp((p,g),sx,sy) -> DHE.Secret((p,g),cy,sy) *)
       (* thus we have Honest(verifyKey(si.server_id)) /\ StrongHS(si) -> DHE.Secret((p,g),cy,sy) *) 
  -    let ms =
  -        if hasExtendedMS si.extensions then
  -            CRE.extract_extended si pms log
  -        else
  -            CRE.extract si pms
  +    let ms = extract si pms log in
       (* the post of this call is !p,g,gx,gy. StrongHS(si) /\ DHE.Secret((p,g),gx,gy) -> PRFs.Secret(ms) *)  
       (* thus we have Honest(verifyKey(si.server_id)) /\ StrongHS(si) -> PRFs.Secret(ms) *) 
   
  
positive.code:     let pmsid = pmsId pms
      let si = {si with pmsId = pmsid; pmsData = pmsdata} in
      let log = log @| clientKEXBytes in
      let ms =
          if hasExtendedMS si.extensions then
              CRE.extract_extended si pms log
          else
              CRE.extract si pms
      (* FIXME: here we should shred pms *)
      let certificateVerifyBytes = getCertificateVerifyBytes si ms cert_req log in
  
  
negative.code:         (* No client certificate ==> no certificateVerify message *)
          empty_bytes
    
  let extract si pms log =
      if hasExtendedMS si.extensions then
          CRE.extract_extended si pms log
      else
          CRE.extract si pms
  
  let prepare_client_output_full_RSA (ci:ConnectionInfo) (state:hs_state) (si:SessionInfo) (cert_req:Cert.sign_cert) (log:log) : (hs_state * SessionInfo * PRF.masterSecret * log) Result =
      let clientCertBytes,certList = getCertificateBytes si cert_req in
  