anchor.diff:   
   let recv conn =
       let net = conn.net_conn in
  +//Cedric: we need refinements to keep track of lengths, starting from TCP.read etc
       match Tcp.read net 5 with
       | Error (x,y) -> Error (x,y)
       | Correct header ->
       let (ct,pv,len) = parse_header header in
  -    if (conn.protocol_version <> ProtocolVersionType.UnknownPV && pv <> conn.protocol_version) || pv = ProtocolVersionType.UnknownPV then
  -        Error (RecordVersion,CheckFailed)
  +    if   (  conn.protocol_version <> ProtocolVersionType.UnknownPV 
  +         && pv <> conn.protocol_version)
  +      || pv = ProtocolVersionType.UnknownPV 
  +    then Error (RecordVersion,CheckFailed)
       else
           (* We commit to the received protocol version.
              In fact, this only changes the protcol version when receiving the first fragment *)
           let conn = {conn with protocol_version = pv} in
           (* No need to check len, since it's on 2 bytes and the max allowed value
              is 2^16. So, here len is always safe *)
  -        match Tcp.read net len with
  -        | Error (x,y) -> Error (x,y)
  +        match Tcp.read net len with 
  +        | Error (x,y) -> Error (x,y) 
           | Correct payload ->
           match decrypt conn payload with
           | Error (x,y) -> Error (x,y)
  
positive.code:       cipher_type = CT_stream;
        mac_algorithm = MA_null;
      }
    }
  
  let create ns info minpv =
  
negative.code:         min_padlen + rand
      | _ -> unexpectedError "Protocol version should be known (or not SSL2) when computing padding"
  
  //Cedric: rename? why +1? why not do this within encrypt? 
  let prepare_enc conn_state data =
      let sp = conn_state.sparams in
      match sp.cipher_type with
  