anchor.diff:              | ClientWritingCCS (si,ms,log) ->
                   let next_ci = getNextEpochs_full ci si ms log si.init_crand si.init_srand in
                   let (writer,reader) = PRFs.keyGen next_ci ms in
  -                let cFinished = makeMessage HT_finished (epochCVerifyData next_ci.id_out) in
  -                let state = {state with hs_outgoing = cFinished // Equivalently, next_ci.id_in
  +                let cFinished = makeMessage HT_finished (epochCVerifyData next_ci.id_out) in // Equivalently, next_ci.id_in
  +                let state = {state with hs_outgoing = cFinished 
                                           pstate = PSClient(ServerCCS(si,ms,next_ci.id_in,reader))} in
                   let (((rg,f),_),_) = makeCCSFragment ci.id_out CCSBytes in
                   let ci = {ci with id_out = next_ci.id_out} in 
  
positive.code:         | _ -> (* Handshake already ongoing, ignore this request *)
              (false,state)
  
  let storeSession sDB (sinfo, ms, role) =
      match sinfo.sessionID with
      | [||] -> (* Non-resumable session *)
          sDB
      | sid ->
          SessionDB.insert sDB sinfo.sessionID (sinfo, ms, role)
  
  // FIXME: Seems we can skip this function with the new state machine *)
  (*
  let goToIdle state =
      let init_sessionInfo = null_sessionInfo state.poptions.minVer in
      match state.pstate with
      | PSClient (_) ->
          let sDB = storeSession Client state in
          {hs_outgoing = [||];
           ccs_outgoing = None;
           hs_outgoing_after_ccs = [||];
           hs_incoming = [||];
           ccs_incoming = None
           poptions = state.poptions;
           sDB = sDB;
           pstate = PSClient(CIdle);
           hs_msg_log = [||]
           hs_next_info = init_sessionInfo
           next_ms = empty_masterSecret init_sessionInfo
           ki_crand = [||]
           ki_srand = [||]
           hs_renegotiation_info_cVerifyData = state.hs_renegotiation_info_cVerifyData
           hs_renegotiation_info_sVerifyData = state.hs_renegotiation_info_sVerifyData}
      | PSServer (_) ->
          let rand = makeRandom () in
          let init_sessionInfo = {init_sessionInfo with init_srand = rand} in
          let sDB = storeSession Server state in
          {hs_outgoing = [||];
           ccs_outgoing = None;
           hs_outgoing_after_ccs = [||];
           hs_incoming = [||];
           ccs_incoming = None
           poptions = state.poptions;
           sDB = sDB;
           pstate = PSServer(SIdle);
           hs_msg_log = [||]
           hs_next_info = init_sessionInfo
           next_ms = empty_masterSecret init_sessionInfo
           ki_crand = [||]
           ki_srand = rand
           hs_renegotiation_info_cVerifyData = state.hs_renegotiation_info_cVerifyData
           hs_renegotiation_info_sVerifyData = state.hs_renegotiation_info_sVerifyData}
  *)
  
  let invalidateSession ci state =
      let si = epochSI(ci.id_in) // FIXME: which epoch to choose? Here it matters since they could be mis-aligned
      match si.sessionID with
  
negative.code:       (* Should never happen *)
        | PSServer(_) -> unexpectedError "[recv_fragment_client] should only be invoked when in client role."
  
  let prepare_server_output_full state maxClVer =
      let ext = 
        if state.poptions.safe_renegotiation then
  