anchor.diff:          (* 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
  
positive.code: 
      (* 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
      (* 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) *) 
  
  
negative.code:                     let pmsid = pmsId pms
                      let si = {si with pmsId = pmsid; pmsData = pmsdata} in
                      let log = log @| to_log in
                      let ms = extract si pms log in
                      (* TODO: we should shred the pms *)
                      (* move to new state *)
                      if si.client_auth then
  