open Global
open Base64
open Data
open Pi
open Crypto
open Prins

let debug_impl = debug "impl"

type principal = string

type mackey = bytes hkey
let get_mackey (a:principal) (b:principal) = Prins.get_mackey (cS a) (cS b)
let session = sha1 (utf8 (cS"(c_start,c_cpdqLogin),({c,p,d,q}Login{p,d,c,q}),(p_start,p_cpdqLogin))(p_cpdqLogin,p_Reject_cpdqLogin),({}Reject{p,d,c}),(d_start,d_Reject_cpdqLogin))(d_Reject_cpdqLogin,d_rBasicreply_Reject_cpdqLogin),({r}Basicreply{r}),(c_cpdqLogin,c_rBasicreply_Reject_cpdqLogin))(p_cpdqLogin,p_wRedirect_cpdqLogin),({w}Redirect{w}),(c_cpdqLogin,c_wRedirect_cpdqLogin))(c_wRedirect_cpdqLogin,c_qRequest_cpdwRedirect),({q}Request{c,p,w,q}),(w_start,w_qRequest_cpdwRedirect))(w_qRequest_cpdwRedirect,w_Fault_qRequest_cpdwRedirect),({}Fault{}),(c_qRequest_cpdwRedirect,c_Fault_qRequest_cpdwRedirect))(w_qRequest_cpdwRedirect,w_rReply_qRequest_cpdwRedirect),({r}Reply{r}),(c_qRequest_cpdwRedirect,c_rReply_qRequest_cpdwRedirect))(c_rReply_qRequest_cpdwRedirect,c_qExtra_rReply_cpdwRedirect),({q}Extra{q}),(w_rReply_qRequest_cpdwRedirect,w_qExtra_rReply_cpdwRedirect))(w_qExtra_rReply_cpdwRedirect,w_rReply_qExtra_cpdwRedirect),({r}Reply{r}),(c_qExtra_rReply_cpdwRedirect,c_rReply_qExtra_cpdwRedirect))(c_rReply_qExtra_cpdwRedirect,c_qExtra_rReply_cpdwRedirect),({q}Extra{q}),(w_rReply_qExtra_cpdwRedirect,w_qExtra_rReply_cpdwRedirect))(w_qExtra_rReply_cpdwRedirect,w_Fault_rqExtra_cpdwRedirect),({}Fault{}),(c_qExtra_rReply_cpdwRedirect,c_Fault_rqExtra_cpdwRedirect))"))


type vars = {
  c : principal ;
  w : principal ;
  p : principal ;
  d : principal ;
  q : string ;
  r : int }
type hashes = {
  hc : bytes ;
  hw : bytes ;
  hp : bytes ;
  hd : bytes ;
  hq : bytes ;
  hr : bytes }
type macs = {
  pLogincpdq : bytes ;
  dLogincpdq : bytes ;
  dReject : bytes ;
  cReject : bytes ;
  cBasicreplyr : bytes ;
  cRedirectw : bytes ;
  wRedirectcpdw : bytes ;
  wRequestq : bytes ;
  cReplyr : bytes ;
  wExtraq : bytes ;
  cFault : bytes }
type keys = {
  key_cw : bytes ;
  key_cp : bytes ;
  key_cd : bytes ;
  key_wc : bytes ;
  key_wp : bytes ;
  key_wd : bytes ;
  key_pc : bytes ;
  key_pw : bytes ;
  key_pd : bytes ;
  key_dc : bytes ;
  key_dw : bytes ;
  key_dp : bytes }
type header = {
  ts : int ;
  sid : bytes }
type store = 
  { vars : vars ; hashes : hashes ; macs : macs ; keys : keys ; header :  header}

let empty_store_c role starting = 
  {vars = { c = role ; w = "" ; p = "" ; d = "" ; q = "" ; r = 0 };
   hashes = { hc = utf8 (cS "") ; hw = utf8 (cS "") ; hp = utf8 (cS "") ; hd = utf8 (cS "") ; hq = utf8 (cS "") ; hr = utf8 (cS "") };
   macs = { pLogincpdq = utf8 (cS "") ; dLogincpdq = utf8 (cS "") ; dReject = utf8 (cS "") ; cReject = utf8 (cS "") ; cBasicreplyr = utf8 (cS "") ; cRedirectw = utf8 (cS "") ; wRedirectcpdw = utf8 (cS "") ; wRequestq = utf8 (cS "") ; cReplyr = utf8 (cS "") ; wExtraq = utf8 (cS "") ; cFault = utf8 (cS "") };
   keys = { key_cw = utf8 (cS "") ;
  key_cp = utf8 (cS "") ;
  key_cd = utf8 (cS "") ;
  key_wc = utf8 (cS "") ;
  key_wp = utf8 (cS "") ;
  key_wd = utf8 (cS "") ;
  key_pc = utf8 (cS "") ;
  key_pw = utf8 (cS "") ;
  key_pd = utf8 (cS "") ;
  key_dc = utf8 (cS "") ;
  key_dw = utf8 (cS "") ;
  key_dp = utf8 (cS "") };
   header = { sid = if starting then sha1 (concat (mkNonce()) session) else utf8 (cS ""); ts = 0 } }

let empty_store_w role starting = 
  {vars = { c = "" ; w = role ; p = "" ; d = "" ; q = "" ; r = 0 };
   hashes = { hc = utf8 (cS "") ; hw = utf8 (cS "") ; hp = utf8 (cS "") ; hd = utf8 (cS "") ; hq = utf8 (cS "") ; hr = utf8 (cS "") };
   macs = { pLogincpdq = utf8 (cS "") ; dLogincpdq = utf8 (cS "") ; dReject = utf8 (cS "") ; cReject = utf8 (cS "") ; cBasicreplyr = utf8 (cS "") ; cRedirectw = utf8 (cS "") ; wRedirectcpdw = utf8 (cS "") ; wRequestq = utf8 (cS "") ; cReplyr = utf8 (cS "") ; wExtraq = utf8 (cS "") ; cFault = utf8 (cS "") };
   keys = { key_cw = utf8 (cS "") ;
  key_cp = utf8 (cS "") ;
  key_cd = utf8 (cS "") ;
  key_wc = utf8 (cS "") ;
  key_wp = utf8 (cS "") ;
  key_wd = utf8 (cS "") ;
  key_pc = utf8 (cS "") ;
  key_pw = utf8 (cS "") ;
  key_pd = utf8 (cS "") ;
  key_dc = utf8 (cS "") ;
  key_dw = utf8 (cS "") ;
  key_dp = utf8 (cS "") };
   header = { sid = if starting then sha1 (concat (mkNonce()) session) else utf8 (cS ""); ts = 0 } }

let empty_store_p role starting = 
  {vars = { c = "" ; w = "" ; p = role ; d = "" ; q = "" ; r = 0 };
   hashes = { hc = utf8 (cS "") ; hw = utf8 (cS "") ; hp = utf8 (cS "") ; hd = utf8 (cS "") ; hq = utf8 (cS "") ; hr = utf8 (cS "") };
   macs = { pLogincpdq = utf8 (cS "") ; dLogincpdq = utf8 (cS "") ; dReject = utf8 (cS "") ; cReject = utf8 (cS "") ; cBasicreplyr = utf8 (cS "") ; cRedirectw = utf8 (cS "") ; wRedirectcpdw = utf8 (cS "") ; wRequestq = utf8 (cS "") ; cReplyr = utf8 (cS "") ; wExtraq = utf8 (cS "") ; cFault = utf8 (cS "") };
   keys = { key_cw = utf8 (cS "") ;
  key_cp = utf8 (cS "") ;
  key_cd = utf8 (cS "") ;
  key_wc = utf8 (cS "") ;
  key_wp = utf8 (cS "") ;
  key_wd = utf8 (cS "") ;
  key_pc = utf8 (cS "") ;
  key_pw = utf8 (cS "") ;
  key_pd = utf8 (cS "") ;
  key_dc = utf8 (cS "") ;
  key_dw = utf8 (cS "") ;
  key_dp = utf8 (cS "") };
   header = { sid = if starting then sha1 (concat (mkNonce()) session) else utf8 (cS ""); ts = 0 } }

let empty_store_d role starting = 
  {vars = { c = "" ; w = "" ; p = "" ; d = role ; q = "" ; r = 0 };
   hashes = { hc = utf8 (cS "") ; hw = utf8 (cS "") ; hp = utf8 (cS "") ; hd = utf8 (cS "") ; hq = utf8 (cS "") ; hr = utf8 (cS "") };
   macs = { pLogincpdq = utf8 (cS "") ; dLogincpdq = utf8 (cS "") ; dReject = utf8 (cS "") ; cReject = utf8 (cS "") ; cBasicreplyr = utf8 (cS "") ; cRedirectw = utf8 (cS "") ; wRedirectcpdw = utf8 (cS "") ; wRequestq = utf8 (cS "") ; cReplyr = utf8 (cS "") ; wExtraq = utf8 (cS "") ; cFault = utf8 (cS "") };
   keys = { key_cw = utf8 (cS "") ;
  key_cp = utf8 (cS "") ;
  key_cd = utf8 (cS "") ;
  key_wc = utf8 (cS "") ;
  key_wp = utf8 (cS "") ;
  key_wd = utf8 (cS "") ;
  key_pc = utf8 (cS "") ;
  key_pw = utf8 (cS "") ;
  key_pd = utf8 (cS "") ;
  key_dc = utf8 (cS "") ;
  key_dw = utf8 (cS "") ;
  key_dp = utf8 (cS "") };
   header = { sid = if starting then sha1 (concat (mkNonce()) session) else utf8 (cS ""); ts = 0 } }

type preds = 
| Send_Login of (principal * bytes * int* principal * principal * principal * string)
| Send_Redirect of (principal * bytes * int* principal)
| Send_Request of (principal * bytes * int* string)
| Send_Reply of (principal * bytes * int* int)
| Send_Extra of (principal * bytes * int* string)
| Send_Fault of (principal * bytes * int)
| Send_Reject of (principal * bytes * int)
| Send_Basicreply of (principal * bytes * int* int)
| Recv_Login of (principal * bytes * int * principal * principal * principal * string)
| Recv_Redirect of (principal * bytes * int * principal)
| Recv_Request of (principal * bytes * int * principal * principal * principal * string)
| Recv_Reply of (principal * bytes * int * int)
| Recv_Extra of (principal * bytes * int * string)
| Recv_Fault of (principal * bytes * int)
| Recv_Reject of (principal * bytes * int * principal * principal * principal)
| Recv_Basicreply of (principal * bytes * int * int)



(*******************************************)
(* Wired types, send and receive functions *)
(*******************************************)

let content_c_cpdqLogin_cpdq = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hq hashes in
  let hashes = concat store.hashes.hd hashes in
  let hashes = concat store.hashes.hp hashes in
  let hashes = concat store.hashes.hc hashes in
  let nextstate = cS "c_cpdqLogin" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_d_rBasicreply_Reject_cpdqLogin_r = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hr hashes in
  let nextstate = cS "d_rBasicreply_Reject_cpdqLogin" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_p_Reject_cpdqLogin_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "p_Reject_cpdqLogin" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_p_wRedirect_cpdqLogin_w = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hw hashes in
  let nextstate = cS "p_wRedirect_cpdqLogin" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_c_qRequest_cpdwRedirect_q = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hq hashes in
  let nextstate = cS "c_qRequest_cpdwRedirect" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_p_wRedirect_cpdqLogin_cpdw = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hw hashes in
  let hashes = concat store.hashes.hd hashes in
  let hashes = concat store.hashes.hp hashes in
  let hashes = concat store.hashes.hc hashes in
  let nextstate = cS "p_wRedirect_cpdqLogin" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_w_Fault_qRequest_cpdwRedirect_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "w_Fault_qRequest_cpdwRedirect" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_w_rReply_qRequest_cpdwRedirect_r = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hr hashes in
  let nextstate = cS "w_rReply_qRequest_cpdwRedirect" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_c_qExtra_rReply_cpdwRedirect_q = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hq hashes in
  let nextstate = cS "c_qExtra_rReply_cpdwRedirect" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_w_rReply_qExtra_cpdwRedirect_r = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hr hashes in
  let nextstate = cS "w_rReply_qExtra_cpdwRedirect" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let content_w_Fault_rqExtra_cpdwRedirect_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "w_Fault_rqExtra_cpdwRedirect" in
  let nextstate_string = utf8 nextstate in
  let payload = concat nextstate_string hashes in
  let ts_string = string_of_int ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let content = concat header payload in
  content

let mac_verify_p_c_cpdqLogin_cpdq = fun ts store k m ->
  let content = content_c_cpdqLogin_cpdq ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_d_p_Reject_cpdqLogin_ = fun ts store k m ->
  let content = content_p_Reject_cpdqLogin_ ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_d_c_cpdqLogin_cpdq = fun ts store k m ->
  let content = content_c_cpdqLogin_cpdq ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_c_d_rBasicreply_Reject_cpdqLogin_r = fun ts store k m ->
  let content = content_d_rBasicreply_Reject_cpdqLogin_r ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_c_p_Reject_cpdqLogin_ = fun ts store k m ->
  let content = content_p_Reject_cpdqLogin_ ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_c_p_wRedirect_cpdqLogin_w = fun ts store k m ->
  let content = content_p_wRedirect_cpdqLogin_w ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_w_c_qRequest_cpdwRedirect_q = fun ts store k m ->
  let content = content_c_qRequest_cpdwRedirect_q ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_w_p_wRedirect_cpdqLogin_cpdw = fun ts store k m ->
  let content = content_p_wRedirect_cpdqLogin_cpdw ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_c_w_Fault_qRequest_cpdwRedirect_ = fun ts store k m ->
  let content = content_w_Fault_qRequest_cpdwRedirect_ ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_c_w_rReply_qRequest_cpdwRedirect_r = fun ts store k m ->
  let content = content_w_rReply_qRequest_cpdwRedirect_r ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_w_c_qExtra_rReply_cpdwRedirect_q = fun ts store k m ->
  let content = content_c_qExtra_rReply_cpdwRedirect_q ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_c_w_rReply_qExtra_cpdwRedirect_r = fun ts store k m ->
  let content = content_w_rReply_qExtra_cpdwRedirect_r ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up

let mac_verify_c_w_Fault_rqExtra_cpdwRedirect_ = fun ts store k m ->
  let content = content_w_Fault_rqExtra_cpdwRedirect_ ts store in
  let cc = mac_verify k m content in
  let pc = pickle content in
  let _ = test_eq cc pc "MAC incorrect" in
  let up = unpickle cc in
  up



type wired_p_start =
  | Wired_in_p_start_of_c_cpdqLogin_cpdq__ of (principal * principal * principal * string) * store

type wired_d_start =
  | Wired_in_d_start_of_p_Reject_cpdqLogin___c_cpdqLogin_cpdq__ of (principal * principal * principal) * store

type wired_c_cpdqLogin =
  | Wired_in_c_cpdqLogin_of_d_rBasicreply_Reject_cpdqLogin_r__p_Reject_cpdqLogin___ of (int) * store
  | Wired_in_c_cpdqLogin_of_p_wRedirect_cpdqLogin_w__ of (principal) * store

type wired_w_start =
  | Wired_in_w_start_of_c_qRequest_cpdwRedirect_q__p_wRedirect_cpdqLogin_cpdw__ of (principal * principal * principal * string) * store

type wired_c_qRequest_cpdwRedirect =
  | Wired_in_c_qRequest_cpdwRedirect_of_w_Fault_qRequest_cpdwRedirect___ of (unit) * store
  | Wired_in_c_qRequest_cpdwRedirect_of_w_rReply_qRequest_cpdwRedirect_r__ of (int) * store

type wired_w_rReply_qRequest_cpdwRedirect =
  | Wired_in_w_rReply_qRequest_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__ of (string) * store

type wired_w_rReply_qExtra_cpdwRedirect =
  | Wired_in_w_rReply_qExtra_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__ of (string) * store

type wired_c_qExtra_rReply_cpdwRedirect =
  | Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_rReply_qExtra_cpdwRedirect_r__ of (int) * store
  | Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_Fault_rqExtra_cpdwRedirect___ of (unit) * store


let receiveWired_p_start : store -> wired_p_start = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.p in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let () = check_cache store.vars.p "p" sid in
  let oldts = store.header.ts in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {sid = sid; ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "c_cpdqLogin_cpdq__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let mar_p,variables = iconcat variables in
  let string_p = iutf8 mar_p in
  let p = iS string_p in
  let hp = sha1 mar_p in
  let mar_d,variables = iconcat variables in
  let string_d = iutf8 mar_d in
  let d = iS string_d in
  let hd = sha1 mar_d in
  let mar_c,variables = iconcat variables in
  let string_c = iutf8 mar_c in
  let c = iS string_c in
  let hc = sha1 mar_c in
  let encr_q,variables = iconcat variables in
  let store = { 
      vars = {store.vars with p = p; d = d; c = c; };
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Registering new keys *)
  let key_cp,keys = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.p) key_cp in
  let key_cd,_ = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.d) key_cd in
  (* Decrypting variables *)
  let keycp = get_symkey (cS store.vars.c) (cS store.vars.p) in
  let mar_q = unpickle (sym_decrypt keycp encr_q) in
  let string_q = iutf8 mar_q in
  let q = iS string_q in
  let hq = sha1 mar_q in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = {store.hashes with hp = hp; hd = hd; hc = hc; hq = hq; };
      macs = store.macs; 
      keys = {store.keys with key_cp = key_cp; key_cd = key_cd; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let pLogincpdq,macs = iconcat macs in
  let dLogincpdq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pLogincpdq = pLogincpdq; dLogincpdq = dLogincpdq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_cpdqLogin with variables cpdq*)
  let macheader,maccontent = iconcat store.macs.pLogincpdq in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid sid "MAC verification" in
  let mackeycp = get_mackey store.vars.c store.vars.p in
  let content = mac_verify_p_c_cpdqLogin_cpdq ts store mackeycp maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_p_start_of_c_cpdqLogin_cpdq__((p,d,c,q),store) in
    wired

let receiveWired_d_start : store -> wired_d_start = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.d in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let () = check_cache store.vars.d "d" sid in
  let oldts = store.header.ts in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {sid = sid; ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "p_Reject_cpdqLogin___c_cpdqLogin_cpdq__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let mar_p,variables = iconcat variables in
  let string_p = iutf8 mar_p in
  let p = iS string_p in
  let hp = sha1 mar_p in
  let mar_d,variables = iconcat variables in
  let string_d = iutf8 mar_d in
  let d = iS string_d in
  let hd = sha1 mar_d in
  let mar_c,variables = iconcat variables in
  let string_c = iutf8 mar_c in
  let c = iS string_c in
  let hc = sha1 mar_c in
  let store = { 
      vars = {store.vars with p = p; d = d; c = c; };
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Registering new keys *)
  let key_pd,keys = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.d) key_pd in
  let key_cd,keys = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.d) key_cd in
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hp = hp; hd = hd; hc = hc; };
      macs = store.macs; 
      keys = {store.keys with key_pd = key_pd; key_cd = key_cd; key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  let hq,_ = iconcat hashes in
  (* Unmarshalling MACs *)
  let dLogincpdq,macs = iconcat macs in
  let dReject,macs = iconcat macs in
  let cReject,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hq = hq; };
      macs = {store.macs with dLogincpdq = dLogincpdq; dReject = dReject; cReject = cReject; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_cpdqLogin with variables cpdq*)
  let macheader,maccontent = iconcat store.macs.dLogincpdq in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid sid "MAC verification" in
  let mackeycd = get_mackey store.vars.c store.vars.d in
  let content = mac_verify_d_c_cpdqLogin_cpdq ts store mackeycd maccontent in
  (* Verification of a MAC from state p_Reject_cpdqLogin with variables *)
  let macheader,maccontent = iconcat store.macs.dReject in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid sid "MAC verification" in
  let mackeypd = get_mackey store.vars.p store.vars.d in
  let content = mac_verify_d_p_Reject_cpdqLogin_ ts store mackeypd maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_d_start_of_p_Reject_cpdqLogin___c_cpdqLogin_cpdq__((p,d,c),store) in
    wired

let receiveWired_c_cpdqLogin : store -> wired_c_cpdqLogin = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.c in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let oldts = store.header.ts in
  let _ = test_inf oldts ts "Replay attack!" in
  let _ = test_eq store.header.sid sid "Session confusion attack!" in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "d_rBasicreply_Reject_cpdqLogin_r__p_Reject_cpdqLogin___" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_r,variables = iconcat variables in
  (* Registering new keys *)
  let key_dc,keys = iconcat keys in
  let () = reg_keys (cS store.vars.d) (cS store.vars.c) key_dc in
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let keydc = get_symkey (cS store.vars.d) (cS store.vars.c) in
  let mar_r = unpickle (sym_decrypt keydc encr_r) in
  let string_r = iutf8 mar_r in
  let marred_r = iS string_r in
  let r = int_of_string marred_r in
  let hr = sha1 mar_r in
  let store = { 
      vars = {store.vars with r = r; };
      hashes = {store.hashes with hr = hr; };
      macs = store.macs; 
      keys = {store.keys with key_dc = key_dc; key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cBasicreplyr,macs = iconcat macs in
  let cReject,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cBasicreplyr = cBasicreplyr; cReject = cReject; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_Reject_cpdqLogin with variables *)
  let macheader,maccontent = iconcat store.macs.cReject in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeypc = get_mackey store.vars.p store.vars.c in
  let content = mac_verify_c_p_Reject_cpdqLogin_ ts store mackeypc maccontent in
  (* Verification of a MAC from state d_rBasicreply_Reject_cpdqLogin with variables r*)
  let macheader,maccontent = iconcat store.macs.cBasicreplyr in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeydc = get_mackey store.vars.d store.vars.c in
  let content = mac_verify_c_d_rBasicreply_Reject_cpdqLogin_r ts store mackeydc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_cpdqLogin_of_d_rBasicreply_Reject_cpdqLogin_r__p_Reject_cpdqLogin___((r),store) in
    wired
  | "p_wRedirect_cpdqLogin_w__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let mar_w,variables = iconcat variables in
  let string_w = iutf8 mar_w in
  let w = iS string_w in
  let hw = sha1 mar_w in
  let store = { 
      vars = {store.vars with w = w; };
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Registering new keys *)
  let key_pc,keys = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  let key_pw,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.w) key_pw in
  (* Decrypting variables *)
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hw = hw; };
      macs = store.macs; 
      keys = {store.keys with key_pc = key_pc; key_pw = key_pw; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cRedirectw,macs = iconcat macs in
  let wRedirectcpdw,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cRedirectw = cRedirectw; wRedirectcpdw = wRedirectcpdw; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_wRedirect_cpdqLogin with variables w*)
  let macheader,maccontent = iconcat store.macs.cRedirectw in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeypc = get_mackey store.vars.p store.vars.c in
  let content = mac_verify_c_p_wRedirect_cpdqLogin_w ts store mackeypc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_cpdqLogin_of_p_wRedirect_cpdqLogin_w__((w),store) in
    wired

let receiveWired_w_start : store -> wired_w_start = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.w in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let () = check_cache store.vars.w "w" sid in
  let oldts = store.header.ts in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {sid = sid; ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "c_qRequest_cpdwRedirect_q__p_wRedirect_cpdqLogin_cpdw__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let mar_c,variables = iconcat variables in
  let string_c = iutf8 mar_c in
  let c = iS string_c in
  let hc = sha1 mar_c in
  let mar_p,variables = iconcat variables in
  let string_p = iutf8 mar_p in
  let p = iS string_p in
  let hp = sha1 mar_p in
  let mar_w,variables = iconcat variables in
  let string_w = iutf8 mar_w in
  let w = iS string_w in
  let hw = sha1 mar_w in
  let encr_q,variables = iconcat variables in
  let store = { 
      vars = {store.vars with c = c; p = p; w = w; };
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Registering new keys *)
  let key_cw,keys = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.w) key_cw in
  let key_pw,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.w) key_pw in
  (* Decrypting variables *)
  let keycw = get_symkey (cS store.vars.c) (cS store.vars.w) in
  let mar_q = unpickle (sym_decrypt keycw encr_q) in
  let string_q = iutf8 mar_q in
  let q = iS string_q in
  let hq = sha1 mar_q in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = {store.hashes with hc = hc; hp = hp; hw = hw; hq = hq; };
      macs = store.macs; 
      keys = {store.keys with key_cw = key_cw; key_pw = key_pw; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  let hd,_ = iconcat hashes in
  (* Unmarshalling MACs *)
  let wRedirectcpdw,macs = iconcat macs in
  let wRequestq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hd = hd; };
      macs = {store.macs with wRedirectcpdw = wRedirectcpdw; wRequestq = wRequestq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_wRedirect_cpdqLogin with variables cpdw*)
  let macheader,maccontent = iconcat store.macs.wRedirectcpdw in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid sid "MAC verification" in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let content = mac_verify_w_p_wRedirect_cpdqLogin_cpdw ts store mackeypw maccontent in
  (* Verification of a MAC from state c_qRequest_cpdwRedirect with variables q*)
  let macheader,maccontent = iconcat store.macs.wRequestq in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid sid "MAC verification" in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let content = mac_verify_w_c_qRequest_cpdwRedirect_q ts store mackeycw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_start_of_c_qRequest_cpdwRedirect_q__p_wRedirect_cpdqLogin_cpdw__((c,p,w,q),store) in
    wired

let receiveWired_c_qRequest_cpdwRedirect : store -> wired_c_qRequest_cpdwRedirect = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.c in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let oldts = store.header.ts in
  let _ = test_inf oldts ts "Replay attack!" in
  let _ = test_eq store.header.sid sid "Session confusion attack!" in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "w_Fault_qRequest_cpdwRedirect___" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  (* Registering new keys *)
  let key_wc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.w) (cS store.vars.c) key_wc in
  (* Decrypting variables *)
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = {store.keys with key_wc = key_wc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cFault,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cFault = cFault; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_Fault_qRequest_cpdwRedirect with variables *)
  let macheader,maccontent = iconcat store.macs.cFault in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let content = mac_verify_c_w_Fault_qRequest_cpdwRedirect_ ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_qRequest_cpdwRedirect_of_w_Fault_qRequest_cpdwRedirect___((),store) in
    wired
  | "w_rReply_qRequest_cpdwRedirect_r__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_r,variables = iconcat variables in
  (* Registering new keys *)
  let key_wc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.w) (cS store.vars.c) key_wc in
  (* Decrypting variables *)
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let mar_r = unpickle (sym_decrypt keywc encr_r) in
  let string_r = iutf8 mar_r in
  let marred_r = iS string_r in
  let r = int_of_string marred_r in
  let hr = sha1 mar_r in
  let store = { 
      vars = {store.vars with r = r; };
      hashes = {store.hashes with hr = hr; };
      macs = store.macs; 
      keys = {store.keys with key_wc = key_wc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cReplyr,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyr = cReplyr; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_rReply_qRequest_cpdwRedirect with variables r*)
  let macheader,maccontent = iconcat store.macs.cReplyr in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let content = mac_verify_c_w_rReply_qRequest_cpdwRedirect_r ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_qRequest_cpdwRedirect_of_w_rReply_qRequest_cpdwRedirect_r__((r),store) in
    wired

let receiveWired_w_rReply_qRequest_cpdwRedirect : store -> wired_w_rReply_qRequest_cpdwRedirect = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.w in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let oldts = store.header.ts in
  let _ = test_inf oldts ts "Replay attack!" in
  let _ = test_eq store.header.sid sid "Session confusion attack!" in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "c_qExtra_rReply_cpdwRedirect_q__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_q,variables = iconcat variables in
  (* Registering new keys *)
  (* Decrypting variables *)
  let keycw = get_symkey (cS store.vars.c) (cS store.vars.w) in
  let mar_q = unpickle (sym_decrypt keycw encr_q) in
  let string_q = iutf8 mar_q in
  let q = iS string_q in
  let hq = sha1 mar_q in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = {store.hashes with hq = hq; };
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wExtraq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wExtraq = wExtraq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_qExtra_rReply_cpdwRedirect with variables q*)
  let macheader,maccontent = iconcat store.macs.wExtraq in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let content = mac_verify_w_c_qExtra_rReply_cpdwRedirect_q ts store mackeycw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_rReply_qRequest_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__((q),store) in
    wired

let receiveWired_w_rReply_qExtra_cpdwRedirect : store -> wired_w_rReply_qExtra_cpdwRedirect = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.w in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let oldts = store.header.ts in
  let _ = test_inf oldts ts "Replay attack!" in
  let _ = test_eq store.header.sid sid "Session confusion attack!" in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "c_qExtra_rReply_cpdwRedirect_q__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_q,variables = iconcat variables in
  (* Registering new keys *)
  (* Decrypting variables *)
  let keycw = get_symkey (cS store.vars.c) (cS store.vars.w) in
  let mar_q = unpickle (sym_decrypt keycw encr_q) in
  let string_q = iutf8 mar_q in
  let q = iS string_q in
  let hq = sha1 mar_q in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = {store.hashes with hq = hq; };
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wExtraq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wExtraq = wExtraq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_qExtra_rReply_cpdwRedirect with variables q*)
  let macheader,maccontent = iconcat store.macs.wExtraq in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let content = mac_verify_w_c_qExtra_rReply_cpdwRedirect_q ts store mackeycw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_rReply_qExtra_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__((q),store) in
    wired

let receiveWired_c_qExtra_rReply_cpdwRedirect : store -> wired_c_qExtra_rReply_cpdwRedirect = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let msg = precv  store.vars.c in
  let header,content = iconcat (ibase64 msg) in
  let sid,ts_mar = iconcat header in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let oldts = store.header.ts in
  let _ = test_inf oldts ts "Replay attack!" in
  let _ = test_eq store.header.sid sid "Session confusion attack!" in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let tag,payload = iconcat content in
  match iS (iutf8 tag) with
  | "w_rReply_qExtra_cpdwRedirect_r__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_r,variables = iconcat variables in
  (* Registering new keys *)
  (* Decrypting variables *)
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let mar_r = unpickle (sym_decrypt keywc encr_r) in
  let string_r = iutf8 mar_r in
  let marred_r = iS string_r in
  let r = int_of_string marred_r in
  let hr = sha1 mar_r in
  let store = { 
      vars = {store.vars with r = r; };
      hashes = {store.hashes with hr = hr; };
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cReplyr,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyr = cReplyr; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_rReply_qExtra_cpdwRedirect with variables r*)
  let macheader,maccontent = iconcat store.macs.cReplyr in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let content = mac_verify_c_w_rReply_qExtra_cpdwRedirect_r ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_rReply_qExtra_cpdwRedirect_r__((r),store) in
    wired
  | "w_Fault_rqExtra_cpdwRedirect___" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  (* Registering new keys *)
  (* Decrypting variables *)
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cFault,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cFault = cFault; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_Fault_rqExtra_cpdwRedirect with variables *)
  let macheader,maccontent = iconcat store.macs.cFault in
  let macsid,ts_mar = iconcat macheader in
  let ts_str = iutf8 ts_mar in
  let ts_string = iS ts_str in
  let ts = int_of_string ts_string in
  let _ = test_inf oldts ts "MAC verification" in
  let oldts = ts in
  let _ = test_eq macsid store.header.sid "MAC verification" in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let content = mac_verify_c_w_Fault_rqExtra_cpdwRedirect_ ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_Fault_rqExtra_cpdwRedirect___((),store) in
    wired
  | _ -> failwith "Critical Error"


(* Sending message from c to p *)
(* Message has to be MACed for p d *)
let sendWired_Login_c_start = fun c -> fun p -> fun d -> fun q -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_c = cS c in
  let mar_c = utf8 string_c in
  let hc = sha1 mar_c in
  let string_p = cS p in
  let mar_p = utf8 string_p in
  let hp = sha1 mar_p in
  let string_d = cS d in
  let mar_d = utf8 string_d in
  let hd = sha1 mar_d in
  let string_q = cS q in
  let mar_q = utf8 string_q in
  let hq = sha1 mar_q in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with c = c; p = p; d = d; q = q; };
      hashes = {store.hashes with hc = hc; hp = hp; hd = hd; hq = hq; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  let keycd = gen_keys (cS store.vars.c) (cS store.vars.d) in
  let keys = concat keycd keys in
  let keycp = gen_keys (cS store.vars.c) (cS store.vars.p) in
  let keys = concat keycp keys in
  (* Generation of a MAC from state c_start to role p *)
  let content = content_c_cpdqLogin_cpdq store.header.ts store in
  let mackeycp = get_mackey store.vars.c store.vars.p in
  let macmsg = mac mackeycp (pickle content) in
  let pLogincpdq = concat header macmsg in
  (* Generation of a MAC from state c_start to role d *)
  let content = content_c_cpdqLogin_cpdq store.header.ts store in
  let mackeycd = get_mackey store.vars.c store.vars.d in
  let macmsg = mac mackeycd (pickle content) in
  let dLogincpdq = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pLogincpdq = pLogincpdq; dLogincpdq = dLogincpdq; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.dLogincpdq macs in
  let macs = concat store.macs.pLogincpdq macs in
  let hashes = nil in
  let variables = nil in
  let string_q = cS store.vars.q in
  let mar_q = utf8 string_q in
  let keycp = get_symkey (cS store.vars.c) (cS store.vars.p) in
  let encr_q = sym_encrypt keycp (pickle mar_q) in
  let variables = concat encr_q variables in
  let string_c = cS store.vars.c in
  let mar_c = utf8 string_c in
  let variables = concat mar_c variables in
  let string_d = cS store.vars.d in
  let mar_d = utf8 string_d in
  let variables = concat mar_d variables in
  let string_p = cS store.vars.p in
  let mar_p = utf8 string_p in
  let variables = concat mar_p variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "c_cpdqLogin_cpdq__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.p msg in 
  store 

(* Sending message from p to d *)
(* Message has to be MACed for d c *)
let sendWired_Reject_p_cpdqLogin = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  let keypc = gen_keys (cS store.vars.p) (cS store.vars.c) in
  let keys = concat keypc keys in
  let keys = concat store.keys.key_cd keys in
  let keypd = gen_keys (cS store.vars.p) (cS store.vars.d) in
  let keys = concat keypd keys in
  (* Generation of a MAC from state p_cpdqLogin to role d *)
  let content = content_p_Reject_cpdqLogin_ store.header.ts store in
  let mackeypd = get_mackey store.vars.p store.vars.d in
  let macmsg = mac mackeypd (pickle content) in
  let dReject = concat header macmsg in
  (* Generation of a MAC from state p_cpdqLogin to role c *)
  let content = content_p_Reject_cpdqLogin_ store.header.ts store in
  let mackeypc = get_mackey store.vars.p store.vars.c in
  let macmsg = mac mackeypc (pickle content) in
  let cReject = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with dReject = dReject; cReject = cReject; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cReject macs in
  let macs = concat store.macs.dReject macs in
  let macs = concat store.macs.dLogincpdq macs in
  let hashes = nil in
  let hashes = concat store.hashes.hq hashes in
  let variables = nil in
  let string_c = cS store.vars.c in
  let mar_c = utf8 string_c in
  let variables = concat mar_c variables in
  let string_d = cS store.vars.d in
  let mar_d = utf8 string_d in
  let variables = concat mar_d variables in
  let string_p = cS store.vars.p in
  let mar_p = utf8 string_p in
  let variables = concat mar_p variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "p_Reject_cpdqLogin___c_cpdqLogin_cpdq__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.d msg in 
  store 

(* Sending message from d to c *)
(* Message has to be MACed for c *)
let sendWired_Basicreply_d_Reject_cpdqLogin = fun r -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let marred_r = string_of_int r in
  let string_r = cS marred_r in
  let mar_r = utf8 string_r in
  let hr = sha1 mar_r in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with r = r; };
      hashes = {store.hashes with hr = hr; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  let keys = concat store.keys.key_pc keys in
  let keydc = gen_keys (cS store.vars.d) (cS store.vars.c) in
  let keys = concat keydc keys in
  (* Generation of a MAC from state d_Reject_cpdqLogin to role c *)
  let content = content_d_rBasicreply_Reject_cpdqLogin_r store.header.ts store in
  let mackeydc = get_mackey store.vars.d store.vars.c in
  let macmsg = mac mackeydc (pickle content) in
  let cBasicreplyr = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cBasicreplyr = cBasicreplyr; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cReject macs in
  let macs = concat store.macs.cBasicreplyr macs in
  let hashes = nil in
  let variables = nil in
  let marred_r = string_of_int store.vars.r in
  let string_r = cS marred_r in
  let mar_r = utf8 string_r in
  let keydc = get_symkey (cS store.vars.d) (cS store.vars.c) in
  let encr_r = sym_encrypt keydc (pickle mar_r) in
  let variables = concat encr_r variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "d_rBasicreply_Reject_cpdqLogin_r__p_Reject_cpdqLogin___" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.c msg in 
  store 

(* Sending message from p to c *)
(* Message has to be MACed for c w *)
let sendWired_Redirect_p_cpdqLogin = fun w -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_w = cS w in
  let mar_w = utf8 string_w in
  let hw = sha1 mar_w in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with w = w; };
      hashes = {store.hashes with hw = hw; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  let keypw = gen_keys (cS store.vars.p) (cS store.vars.w) in
  let keys = concat keypw keys in
  let keypc = gen_keys (cS store.vars.p) (cS store.vars.c) in
  let keys = concat keypc keys in
  (* Generation of a MAC from state p_cpdqLogin to role c *)
  let content = content_p_wRedirect_cpdqLogin_w store.header.ts store in
  let mackeypc = get_mackey store.vars.p store.vars.c in
  let macmsg = mac mackeypc (pickle content) in
  let cRedirectw = concat header macmsg in
  (* Generation of a MAC from state p_cpdqLogin to role w *)
  let content = content_p_wRedirect_cpdqLogin_cpdw store.header.ts store in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let macmsg = mac mackeypw (pickle content) in
  let wRedirectcpdw = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cRedirectw = cRedirectw; wRedirectcpdw = wRedirectcpdw; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRedirectcpdw macs in
  let macs = concat store.macs.cRedirectw macs in
  let hashes = nil in
  let variables = nil in
  let string_w = cS store.vars.w in
  let mar_w = utf8 string_w in
  let variables = concat mar_w variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "p_wRedirect_cpdqLogin_w__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.c msg in 
  store 

(* Sending message from c to w *)
(* Message has to be MACed for w *)
let sendWired_Request_c_wRedirect_cpdqLogin = fun q -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_q = cS q in
  let mar_q = utf8 string_q in
  let hq = sha1 mar_q in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = {store.hashes with hq = hq; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  let keys = concat store.keys.key_pw keys in
  let keycw = gen_keys (cS store.vars.c) (cS store.vars.w) in
  let keys = concat keycw keys in
  (* Generation of a MAC from state c_wRedirect_cpdqLogin to role w *)
  let content = content_c_qRequest_cpdwRedirect_q store.header.ts store in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let macmsg = mac mackeycw (pickle content) in
  let wRequestq = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wRequestq = wRequestq; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRequestq macs in
  let macs = concat store.macs.wRedirectcpdw macs in
  let hashes = nil in
  let hashes = concat store.hashes.hd hashes in
  let variables = nil in
  let string_q = cS store.vars.q in
  let mar_q = utf8 string_q in
  let keycw = get_symkey (cS store.vars.c) (cS store.vars.w) in
  let encr_q = sym_encrypt keycw (pickle mar_q) in
  let variables = concat encr_q variables in
  let string_w = cS store.vars.w in
  let mar_w = utf8 string_w in
  let variables = concat mar_w variables in
  let string_p = cS store.vars.p in
  let mar_p = utf8 string_p in
  let variables = concat mar_p variables in
  let string_c = cS store.vars.c in
  let mar_c = utf8 string_c in
  let variables = concat mar_c variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "c_qRequest_cpdwRedirect_q__p_wRedirect_cpdqLogin_cpdw__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.w msg in 
  store 

(* Sending message from w to c *)
(* Message has to be MACed for c *)
let sendWired_Fault_w_qRequest_cpdwRedirect = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  let keywc = gen_keys (cS store.vars.w) (cS store.vars.c) in
  let keys = concat keywc keys in
  (* Generation of a MAC from state w_qRequest_cpdwRedirect to role c *)
  let content = content_w_Fault_qRequest_cpdwRedirect_ store.header.ts store in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let macmsg = mac mackeywc (pickle content) in
  let cFault = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cFault = cFault; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cFault macs in
  let hashes = nil in
  let variables = nil in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_Fault_qRequest_cpdwRedirect___" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.c msg in 
  store 

(* Sending message from w to c *)
(* Message has to be MACed for c *)
let sendWired_Reply_w_qRequest_cpdwRedirect = fun r -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let marred_r = string_of_int r in
  let string_r = cS marred_r in
  let mar_r = utf8 string_r in
  let hr = sha1 mar_r in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with r = r; };
      hashes = {store.hashes with hr = hr; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  let keywc = gen_keys (cS store.vars.w) (cS store.vars.c) in
  let keys = concat keywc keys in
  (* Generation of a MAC from state w_qRequest_cpdwRedirect to role c *)
  let content = content_w_rReply_qRequest_cpdwRedirect_r store.header.ts store in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let macmsg = mac mackeywc (pickle content) in
  let cReplyr = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyr = cReplyr; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cReplyr macs in
  let hashes = nil in
  let variables = nil in
  let marred_r = string_of_int store.vars.r in
  let string_r = cS marred_r in
  let mar_r = utf8 string_r in
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let encr_r = sym_encrypt keywc (pickle mar_r) in
  let variables = concat encr_r variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_rReply_qRequest_cpdwRedirect_r__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.c msg in 
  store 

(* Sending message from c to w *)
(* Message has to be MACed for w *)
let sendWired_Extra_c_rReply_qRequest_cpdwRedirect = fun q -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_q = cS q in
  let mar_q = utf8 string_q in
  let hq = sha1 mar_q in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = {store.hashes with hq = hq; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  (* Generation of a MAC from state c_rReply_qRequest_cpdwRedirect to role w *)
  let content = content_c_qExtra_rReply_cpdwRedirect_q store.header.ts store in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let macmsg = mac mackeycw (pickle content) in
  let wExtraq = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wExtraq = wExtraq; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wExtraq macs in
  let hashes = nil in
  let variables = nil in
  let string_q = cS store.vars.q in
  let mar_q = utf8 string_q in
  let keycw = get_symkey (cS store.vars.c) (cS store.vars.w) in
  let encr_q = sym_encrypt keycw (pickle mar_q) in
  let variables = concat encr_q variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "c_qExtra_rReply_cpdwRedirect_q__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.w msg in 
  store 

(* Sending message from w to c *)
(* Message has to be MACed for c *)
let sendWired_Reply_w_qExtra_rReply_cpdwRedirect = fun r -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let marred_r = string_of_int r in
  let string_r = cS marred_r in
  let mar_r = utf8 string_r in
  let hr = sha1 mar_r in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with r = r; };
      hashes = {store.hashes with hr = hr; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  (* Generation of a MAC from state w_qExtra_rReply_cpdwRedirect to role c *)
  let content = content_w_rReply_qExtra_cpdwRedirect_r store.header.ts store in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let macmsg = mac mackeywc (pickle content) in
  let cReplyr = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyr = cReplyr; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cReplyr macs in
  let hashes = nil in
  let variables = nil in
  let marred_r = string_of_int store.vars.r in
  let string_r = cS marred_r in
  let mar_r = utf8 string_r in
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let encr_r = sym_encrypt keywc (pickle mar_r) in
  let variables = concat encr_r variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_rReply_qExtra_cpdwRedirect_r__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.c msg in 
  store 

(* Sending message from c to w *)
(* Message has to be MACed for w *)
let sendWired_Extra_c_rReply_qExtra_cpdwRedirect = fun q -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_q = cS q in
  let mar_q = utf8 string_q in
  let hq = sha1 mar_q in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = {store.hashes with hq = hq; };
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  (* Generation of a MAC from state c_rReply_qExtra_cpdwRedirect to role w *)
  let content = content_c_qExtra_rReply_cpdwRedirect_q store.header.ts store in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let macmsg = mac mackeycw (pickle content) in
  let wExtraq = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wExtraq = wExtraq; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wExtraq macs in
  let hashes = nil in
  let variables = nil in
  let string_q = cS store.vars.q in
  let mar_q = utf8 string_q in
  let keycw = get_symkey (cS store.vars.c) (cS store.vars.w) in
  let encr_q = sym_encrypt keycw (pickle mar_q) in
  let variables = concat encr_q variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "c_qExtra_rReply_cpdwRedirect_q__" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.w msg in 
  store 

(* Sending message from w to c *)
(* Message has to be MACed for c *)
let sendWired_Fault_w_qExtra_rReply_cpdwRedirect = fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = {store.header with ts = ts; }} in
  let ts_string = string_of_int store.header.ts in
  let ts_str = cS ts_string in
  let ts_mar = utf8 ts_str in
  let header = concat store.header.sid ts_mar in
  let keys = nil in
  (* Generation of a MAC from state w_qExtra_rReply_cpdwRedirect to role c *)
  let content = content_w_Fault_rqExtra_cpdwRedirect_ store.header.ts store in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let macmsg = mac mackeywc (pickle content) in
  let cFault = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cFault = cFault; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cFault macs in
  let hashes = nil in
  let variables = nil in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_Fault_rqExtra_cpdwRedirect___" in
  let visib_string = utf8 visib in
  let content = concat visib_string payload in
  let msg = base64 (concat header content) in
  let () = psend  store.vars.c msg in 
  store