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_cpwqRequest),({c,p,w,q}Request{c,p,w,q}),(p_start,p_cpwqRequest))(p_cpwqRequest,p_Audit_cpwqRequest),({}Audit{c,p,w}),(w_start,w_Audit_cpwqRequest))(w_Audit_cpwqRequest,w_dDetails_Audit_cpwqRequest),({d}Details{d}),(p_Audit_cpwqRequest,p_dDetails_Audit_cpwqRequest))(p_dDetails_Audit_cpwqRequest,p_Resume_dDetails_cpwqRequest),({}Resume{q}),(w_dDetails_Audit_cpwqRequest,w_Resume_dDetails_cpwqRequest))(w_Resume_dDetails_cpwqRequest,w_xReply_dResume_cpwqRequest),({x}Reply{x}),(c_cpwqRequest,c_xReply_dResume_cpwqRequest))(p_dDetails_Audit_cpwqRequest,p_oRetry_dDetails_cpwqRequest),({o}Retry{o}),(w_dDetails_Audit_cpwqRequest,w_oRetry_dDetails_cpwqRequest))(w_oRetry_dDetails_cpwqRequest,w_dDetails_oRetry_cpwqRequest),({d}Details{d}),(p_oRetry_dDetails_cpwqRequest,p_dDetails_oRetry_cpwqRequest))(p_dDetails_oRetry_cpwqRequest,p_Resume_odDetails_cpwqRequest),({}Resume{q}),(w_dDetails_oRetry_cpwqRequest,w_Resume_odDetails_cpwqRequest))(w_Resume_odDetails_cpwqRequest,w_xReply_odResume_cpwqRequest),({x}Reply{x}),(c_cpwqRequest,c_xReply_odResume_cpwqRequest))(p_dDetails_oRetry_cpwqRequest,p_oRetry_dDetails_cpwqRequest),({o}Retry{o}),(w_dDetails_oRetry_cpwqRequest,w_oRetry_dDetails_cpwqRequest))(p_cpwqRequest,p_Forward_cpwqRequest),({}Forward{c,p,w,q}),(w_start,w_Forward_cpwqRequest))(w_Forward_cpwqRequest,w_xReply_Forward_cpwqRequest),({x}Reply{x}),(c_cpwqRequest,c_xReply_Forward_cpwqRequest))"))


type vars = {
  c : principal ;
  p : principal ;
  w : principal ;
  q : string ;
  x : string ;
  d : string ;
  o : string }
type hashes = {
  hc : bytes ;
  hp : bytes ;
  hw : bytes ;
  hq : bytes ;
  hx : bytes ;
  hd : bytes ;
  ho : bytes }
type macs = {
  pRequestcpwq : bytes ;
  wRequestcpwq : bytes ;
  wAudit : bytes ;
  cResumed : bytes ;
  pDetailsd : bytes ;
  wResume : bytes ;
  cResumeod : bytes ;
  wRetryo : bytes ;
  wForward : bytes ;
  cForward : bytes ;
  cReplyx : bytes }
type keys = {
  key_cp : bytes ;
  key_cw : bytes ;
  key_pc : bytes ;
  key_pw : bytes ;
  key_wc : bytes ;
  key_wp : 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 ; p = "" ; w = "" ; q = "" ; x = "" ; d = "" ; o = "" };
   hashes = { hc = utf8 (cS "") ; hp = utf8 (cS "") ; hw = utf8 (cS "") ; hq = utf8 (cS "") ; hx = utf8 (cS "") ; hd = utf8 (cS "") ; ho = utf8 (cS "") };
   macs = { pRequestcpwq = utf8 (cS "") ; wRequestcpwq = utf8 (cS "") ; wAudit = utf8 (cS "") ; cResumed = utf8 (cS "") ; pDetailsd = utf8 (cS "") ; wResume = utf8 (cS "") ; cResumeod = utf8 (cS "") ; wRetryo = utf8 (cS "") ; wForward = utf8 (cS "") ; cForward = utf8 (cS "") ; cReplyx = utf8 (cS "") };
   keys = { key_cp = utf8 (cS "") ;
  key_cw = utf8 (cS "") ;
  key_pc = utf8 (cS "") ;
  key_pw = utf8 (cS "") ;
  key_wc = utf8 (cS "") ;
  key_wp = utf8 (cS "") };
   header = { sid = if starting then sha1 (concat (mkNonce()) session) else utf8 (cS ""); ts = 0 } }

let empty_store_p role starting = 
  {vars = { c = "" ; p = role ; w = "" ; q = "" ; x = "" ; d = "" ; o = "" };
   hashes = { hc = utf8 (cS "") ; hp = utf8 (cS "") ; hw = utf8 (cS "") ; hq = utf8 (cS "") ; hx = utf8 (cS "") ; hd = utf8 (cS "") ; ho = utf8 (cS "") };
   macs = { pRequestcpwq = utf8 (cS "") ; wRequestcpwq = utf8 (cS "") ; wAudit = utf8 (cS "") ; cResumed = utf8 (cS "") ; pDetailsd = utf8 (cS "") ; wResume = utf8 (cS "") ; cResumeod = utf8 (cS "") ; wRetryo = utf8 (cS "") ; wForward = utf8 (cS "") ; cForward = utf8 (cS "") ; cReplyx = utf8 (cS "") };
   keys = { key_cp = utf8 (cS "") ;
  key_cw = utf8 (cS "") ;
  key_pc = utf8 (cS "") ;
  key_pw = utf8 (cS "") ;
  key_wc = utf8 (cS "") ;
  key_wp = utf8 (cS "") };
   header = { sid = if starting then sha1 (concat (mkNonce()) session) else utf8 (cS ""); ts = 0 } }

let empty_store_w role starting = 
  {vars = { c = "" ; p = "" ; w = role ; q = "" ; x = "" ; d = "" ; o = "" };
   hashes = { hc = utf8 (cS "") ; hp = utf8 (cS "") ; hw = utf8 (cS "") ; hq = utf8 (cS "") ; hx = utf8 (cS "") ; hd = utf8 (cS "") ; ho = utf8 (cS "") };
   macs = { pRequestcpwq = utf8 (cS "") ; wRequestcpwq = utf8 (cS "") ; wAudit = utf8 (cS "") ; cResumed = utf8 (cS "") ; pDetailsd = utf8 (cS "") ; wResume = utf8 (cS "") ; cResumeod = utf8 (cS "") ; wRetryo = utf8 (cS "") ; wForward = utf8 (cS "") ; cForward = utf8 (cS "") ; cReplyx = utf8 (cS "") };
   keys = { key_cp = utf8 (cS "") ;
  key_cw = utf8 (cS "") ;
  key_pc = utf8 (cS "") ;
  key_pw = utf8 (cS "") ;
  key_wc = utf8 (cS "") ;
  key_wp = utf8 (cS "") };
   header = { sid = if starting then sha1 (concat (mkNonce()) session) else utf8 (cS ""); ts = 0 } }

type preds = 
| Send_Request of (principal * bytes * int* principal * principal * principal * string)
| Send_Forward of (principal * bytes * int)
| Send_Reply of (principal * bytes * int* string)
| Send_Audit of (principal * bytes * int)
| Send_Details of (principal * bytes * int* string)
| Send_Retry of (principal * bytes * int* string)
| Send_Resume of (principal * bytes * int)
| Recv_Request of (principal * bytes * int * principal * principal * principal * string)
| Recv_Forward of (principal * bytes * int * principal * principal * principal * string)
| Recv_Reply of (principal * bytes * int * string)
| Recv_Audit of (principal * bytes * int * principal * principal * principal)
| Recv_Details of (principal * bytes * int * string)
| Recv_Retry of (principal * bytes * int * string)
| Recv_Resume of (principal * bytes * int * string)



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

let content_w_dDetails_Audit_cpwqRequest_d = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hd hashes in
  let nextstate = cS "w_dDetails_Audit_cpwqRequest" 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_Resume_dDetails_cpwqRequest_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "p_Resume_dDetails_cpwqRequest" 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_dDetails_oRetry_cpwqRequest_d = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hd hashes in
  let nextstate = cS "w_dDetails_oRetry_cpwqRequest" 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_Resume_odDetails_cpwqRequest_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "p_Resume_odDetails_cpwqRequest" 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_oRetry_dDetails_cpwqRequest_o = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.ho hashes in
  let nextstate = cS "p_oRetry_dDetails_cpwqRequest" 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_Audit_cpwqRequest_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "p_Audit_cpwqRequest" 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_cpwqRequest_cpwq = 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.hw hashes in
  let hashes = concat store.hashes.hp hashes in
  let hashes = concat store.hashes.hc hashes in
  let nextstate = cS "c_cpwqRequest" 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_xReply_dResume_cpwqRequest_x = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hx hashes in
  let nextstate = cS "w_xReply_dResume_cpwqRequest" 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_Resume_dDetails_cpwqRequest_d = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hd hashes in
  let nextstate = cS "p_Resume_dDetails_cpwqRequest" 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_xReply_odResume_cpwqRequest_x = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hx hashes in
  let nextstate = cS "w_xReply_odResume_cpwqRequest" 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_Resume_odDetails_cpwqRequest_od = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hd hashes in
  let hashes = concat store.hashes.ho hashes in
  let nextstate = cS "p_Resume_odDetails_cpwqRequest" 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_xReply_Forward_cpwqRequest_x = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let hashes = concat store.hashes.hx hashes in
  let nextstate = cS "w_xReply_Forward_cpwqRequest" 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_Forward_cpwqRequest_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "p_Forward_cpwqRequest" 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_cpwqRequest_cpwq = fun ts store k m ->
  let content = content_c_cpwqRequest_cpwq 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_p_w_dDetails_Audit_cpwqRequest_d = fun ts store k m ->
  let content = content_w_dDetails_Audit_cpwqRequest_d 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_Resume_dDetails_cpwqRequest_ = fun ts store k m ->
  let content = content_p_Resume_dDetails_cpwqRequest_ 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_p_w_dDetails_oRetry_cpwqRequest_d = fun ts store k m ->
  let content = content_w_dDetails_oRetry_cpwqRequest_d 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_Resume_odDetails_cpwqRequest_ = fun ts store k m ->
  let content = content_p_Resume_odDetails_cpwqRequest_ 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_oRetry_dDetails_cpwqRequest_o = fun ts store k m ->
  let content = content_p_oRetry_dDetails_cpwqRequest_o 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_Audit_cpwqRequest_ = fun ts store k m ->
  let content = content_p_Audit_cpwqRequest_ 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_Forward_cpwqRequest_ = fun ts store k m ->
  let content = content_p_Forward_cpwqRequest_ 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_cpwqRequest_cpwq = fun ts store k m ->
  let content = content_c_cpwqRequest_cpwq 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_xReply_dResume_cpwqRequest_x = fun ts store k m ->
  let content = content_w_xReply_dResume_cpwqRequest_x 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_Resume_dDetails_cpwqRequest_d = fun ts store k m ->
  let content = content_p_Resume_dDetails_cpwqRequest_d 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_xReply_odResume_cpwqRequest_x = fun ts store k m ->
  let content = content_w_xReply_odResume_cpwqRequest_x 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_Resume_odDetails_cpwqRequest_od = fun ts store k m ->
  let content = content_p_Resume_odDetails_cpwqRequest_od 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_xReply_Forward_cpwqRequest_x = fun ts store k m ->
  let content = content_w_xReply_Forward_cpwqRequest_x 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_Forward_cpwqRequest_ = fun ts store k m ->
  let content = content_p_Forward_cpwqRequest_ 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_cpwqRequest_cpwq__ of (principal * principal * principal * string) * store

type wired_p_Audit_cpwqRequest =
  | Wired_in_p_Audit_cpwqRequest_of_w_dDetails_Audit_cpwqRequest_d__ of (string) * store

type wired_w_dDetails_Audit_cpwqRequest =
  | Wired_in_w_dDetails_Audit_cpwqRequest_of_p_Resume_dDetails_cpwqRequest___ of (string) * store
  | Wired_in_w_dDetails_Audit_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__ of (string) * store

type wired_p_oRetry_dDetails_cpwqRequest =
  | Wired_in_p_oRetry_dDetails_cpwqRequest_of_w_dDetails_oRetry_cpwqRequest_d__ of (string) * store

type wired_w_dDetails_oRetry_cpwqRequest =
  | Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_Resume_odDetails_cpwqRequest___ of (string) * store
  | Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__ of (string) * store

type wired_w_start =
  | Wired_in_w_start_of_p_Audit_cpwqRequest___c_cpwqRequest_cpwq__ of (principal * principal * principal) * store
  | Wired_in_w_start_of_p_Forward_cpwqRequest___c_cpwqRequest_cpwq__ of (principal * principal * principal * string) * store

type wired_c_cpwqRequest =
  | Wired_in_c_cpwqRequest_of_w_xReply_dResume_cpwqRequest_x__p_Resume_dDetails_cpwqRequest_d__ of (string) * store
  | Wired_in_c_cpwqRequest_of_w_xReply_odResume_cpwqRequest_x__p_Resume_odDetails_cpwqRequest_od__ of (string) * store
  | Wired_in_c_cpwqRequest_of_w_xReply_Forward_cpwqRequest_x__p_Forward_cpwqRequest___ of (string) * 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_cpwqRequest_cpwq__" ->
  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_cp,keys = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.p) key_cp in
  let key_cw,_ = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.w) key_cw 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 hc = hc; hp = hp; hw = hw; hq = hq; };
      macs = store.macs; 
      keys = {store.keys with key_cp = key_cp; key_cw = key_cw; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let pRequestcpwq,macs = iconcat macs in
  let wRequestcpwq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pRequestcpwq = pRequestcpwq; wRequestcpwq = wRequestcpwq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_cpwqRequest with variables cpwq*)
  let macheader,maccontent = iconcat store.macs.pRequestcpwq 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_cpwqRequest_cpwq 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_cpwqRequest_cpwq__((c,p,w,q),store) in
    wired

let receiveWired_p_Audit_cpwqRequest : store -> wired_p_Audit_cpwqRequest = 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 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_dDetails_Audit_cpwqRequest_d__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_d,variables = iconcat variables in
  (* Registering new keys *)
  let key_wp,_ = iconcat keys in
  let () = reg_keys (cS store.vars.w) (cS store.vars.p) key_wp in
  (* Decrypting variables *)
  let keywp = get_symkey (cS store.vars.w) (cS store.vars.p) in
  let mar_d = unpickle (sym_decrypt keywp encr_d) in
  let string_d = iutf8 mar_d in
  let d = iS string_d in
  let hd = sha1 mar_d in
  let store = { 
      vars = {store.vars with d = d; };
      hashes = {store.hashes with hd = hd; };
      macs = store.macs; 
      keys = {store.keys with key_wp = key_wp; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let pDetailsd,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pDetailsd = pDetailsd; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_dDetails_Audit_cpwqRequest with variables d*)
  let macheader,maccontent = iconcat store.macs.pDetailsd 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 mackeywp = get_mackey store.vars.w store.vars.p in
  let content = mac_verify_p_w_dDetails_Audit_cpwqRequest_d ts store mackeywp maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_p_Audit_cpwqRequest_of_w_dDetails_Audit_cpwqRequest_d__((d),store) in
    wired

let receiveWired_w_dDetails_Audit_cpwqRequest : store -> wired_w_dDetails_Audit_cpwqRequest = 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
  | "p_Resume_dDetails_cpwqRequest___" ->
  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 *)
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let mar_q = unpickle (sym_decrypt (get_symkey (cS store.vars.p) (cS store.vars.w)) encr_q) in
  let string_q = iutf8 mar_q in
  let q = iS string_q in
  let string_q = cS q in
  let mar_q = utf8 string_q in
    let () = sha1_verify mar_q store.hashes.hq in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = store.hashes;
      macs = store.macs; 
      keys = {store.keys with key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wResume,macs = iconcat macs in
  let cResumed,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wResume = wResume; cResumed = cResumed; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_Resume_dDetails_cpwqRequest with variables *)
  let macheader,maccontent = iconcat store.macs.wResume 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 mackeypw = get_mackey store.vars.p store.vars.w in
  let content = mac_verify_w_p_Resume_dDetails_cpwqRequest_ ts store mackeypw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_dDetails_Audit_cpwqRequest_of_p_Resume_dDetails_cpwqRequest___((q),store) in
    wired
  | "p_oRetry_dDetails_cpwqRequest_o__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_o,variables = iconcat variables in
  (* Registering new keys *)
  (* Decrypting variables *)
  let keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let mar_o = unpickle (sym_decrypt keypw encr_o) in
  let string_o = iutf8 mar_o in
  let o = iS string_o in
  let ho = sha1 mar_o in
  let store = { 
      vars = {store.vars with o = o; };
      hashes = {store.hashes with ho = ho; };
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wRetryo,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wRetryo = wRetryo; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_oRetry_dDetails_cpwqRequest with variables o*)
  let macheader,maccontent = iconcat store.macs.wRetryo 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 mackeypw = get_mackey store.vars.p store.vars.w in
  let content = mac_verify_w_p_oRetry_dDetails_cpwqRequest_o ts store mackeypw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_dDetails_Audit_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__((o),store) in
    wired

let receiveWired_p_oRetry_dDetails_cpwqRequest : store -> wired_p_oRetry_dDetails_cpwqRequest = 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 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_dDetails_oRetry_cpwqRequest_d__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_d,variables = iconcat variables in
  (* Registering new keys *)
  (* Decrypting variables *)
  let keywp = get_symkey (cS store.vars.w) (cS store.vars.p) in
  let mar_d = unpickle (sym_decrypt keywp encr_d) in
  let string_d = iutf8 mar_d in
  let d = iS string_d in
  let hd = sha1 mar_d in
  let store = { 
      vars = {store.vars with d = d; };
      hashes = {store.hashes with hd = hd; };
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let pDetailsd,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pDetailsd = pDetailsd; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_dDetails_oRetry_cpwqRequest with variables d*)
  let macheader,maccontent = iconcat store.macs.pDetailsd 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 mackeywp = get_mackey store.vars.w store.vars.p in
  let content = mac_verify_p_w_dDetails_oRetry_cpwqRequest_d ts store mackeywp maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_p_oRetry_dDetails_cpwqRequest_of_w_dDetails_oRetry_cpwqRequest_d__((d),store) in
    wired

let receiveWired_w_dDetails_oRetry_cpwqRequest : store -> wired_w_dDetails_oRetry_cpwqRequest = 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
  | "p_Resume_odDetails_cpwqRequest___" ->
  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 *)
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let mar_q = unpickle (sym_decrypt (get_symkey (cS store.vars.p) (cS store.vars.w)) encr_q) in
  let string_q = iutf8 mar_q in
  let q = iS string_q in
  let string_q = cS q in
  let mar_q = utf8 string_q in
    let () = sha1_verify mar_q store.hashes.hq in
  let store = { 
      vars = {store.vars with q = q; };
      hashes = store.hashes;
      macs = store.macs; 
      keys = {store.keys with key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wResume,macs = iconcat macs in
  let cResumeod,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wResume = wResume; cResumeod = cResumeod; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_Resume_odDetails_cpwqRequest with variables *)
  let macheader,maccontent = iconcat store.macs.wResume 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 mackeypw = get_mackey store.vars.p store.vars.w in
  let content = mac_verify_w_p_Resume_odDetails_cpwqRequest_ ts store mackeypw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_Resume_odDetails_cpwqRequest___((q),store) in
    wired
  | "p_oRetry_dDetails_cpwqRequest_o__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_o,variables = iconcat variables in
  (* Registering new keys *)
  (* Decrypting variables *)
  let keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let mar_o = unpickle (sym_decrypt keypw encr_o) in
  let string_o = iutf8 mar_o in
  let o = iS string_o in
  let ho = sha1 mar_o in
  let store = { 
      vars = {store.vars with o = o; };
      hashes = {store.hashes with ho = ho; };
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wRetryo,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wRetryo = wRetryo; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_oRetry_dDetails_cpwqRequest with variables o*)
  let macheader,maccontent = iconcat store.macs.wRetryo 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 mackeypw = get_mackey store.vars.p store.vars.w in
  let content = mac_verify_w_p_oRetry_dDetails_cpwqRequest_o ts store mackeypw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__((o),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
  | "p_Audit_cpwqRequest___c_cpwqRequest_cpwq__" ->
  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 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_pw,keys = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.w) key_pw in
  let key_cw,_ = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.w) key_cw in
  (* Decrypting variables *)
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hc = hc; hp = hp; hw = hw; };
      macs = store.macs; 
      keys = {store.keys with key_pw = key_pw; key_cw = key_cw; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  let hq,_ = iconcat hashes in
  (* Unmarshalling MACs *)
  let wAudit,macs = iconcat macs in
  let wRequestcpwq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hq = hq; };
      macs = {store.macs with wAudit = wAudit; wRequestcpwq = wRequestcpwq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_cpwqRequest with variables cpwq*)
  let macheader,maccontent = iconcat store.macs.wRequestcpwq 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_cpwqRequest_cpwq ts store mackeycw maccontent in
  (* Verification of a MAC from state p_Audit_cpwqRequest with variables *)
  let macheader,maccontent = iconcat store.macs.wAudit 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_Audit_cpwqRequest_ ts store mackeypw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_start_of_p_Audit_cpwqRequest___c_cpwqRequest_cpwq__((c,p,w),store) in
    wired
  | "p_Forward_cpwqRequest___c_cpwqRequest_cpwq__" ->
  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_pw,keys = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.w) key_pw in
  let key_cw,keys = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.w) key_cw in
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let mar_q = unpickle (sym_decrypt keypw 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_pw = key_pw; key_cw = key_cw; key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wForward,macs = iconcat macs in
  let cForward,macs = iconcat macs in
  let wRequestcpwq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wForward = wForward; cForward = cForward; wRequestcpwq = wRequestcpwq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_cpwqRequest with variables cpwq*)
  let macheader,maccontent = iconcat store.macs.wRequestcpwq 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_cpwqRequest_cpwq ts store mackeycw maccontent in
  (* Verification of a MAC from state p_Forward_cpwqRequest with variables *)
  let macheader,maccontent = iconcat store.macs.wForward 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_Forward_cpwqRequest_ ts store mackeypw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_start_of_p_Forward_cpwqRequest___c_cpwqRequest_cpwq__((c,p,w,q),store) in
    wired

let receiveWired_c_cpwqRequest : store -> wired_c_cpwqRequest = 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_xReply_dResume_cpwqRequest_x__p_Resume_dDetails_cpwqRequest_d__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_x,variables = iconcat variables in
  (* Registering new keys *)
  let key_wc,keys = iconcat keys in
  let () = reg_keys (cS store.vars.w) (cS store.vars.c) key_wc in
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let mar_x = unpickle (sym_decrypt keywc encr_x) in
  let string_x = iutf8 mar_x in
  let x = iS string_x in
  let hx = sha1 mar_x in
  let store = { 
      vars = {store.vars with x = x; };
      hashes = {store.hashes with hx = hx; };
      macs = store.macs; 
      keys = {store.keys with key_wc = key_wc; key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  let hd,_ = iconcat hashes in
  (* Unmarshalling MACs *)
  let cReplyx,macs = iconcat macs in
  let cResumed,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hd = hd; };
      macs = {store.macs with cReplyx = cReplyx; cResumed = cResumed; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_Resume_dDetails_cpwqRequest with variables d*)
  let macheader,maccontent = iconcat store.macs.cResumed 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_Resume_dDetails_cpwqRequest_d ts store mackeypc maccontent in
  (* Verification of a MAC from state w_xReply_dResume_cpwqRequest with variables x*)
  let macheader,maccontent = iconcat store.macs.cReplyx 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_xReply_dResume_cpwqRequest_x ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_cpwqRequest_of_w_xReply_dResume_cpwqRequest_x__p_Resume_dDetails_cpwqRequest_d__((x),store) in
    wired
  | "w_xReply_odResume_cpwqRequest_x__p_Resume_odDetails_cpwqRequest_od__" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_x,variables = iconcat variables in
  (* Registering new keys *)
  let key_wc,keys = iconcat keys in
  let () = reg_keys (cS store.vars.w) (cS store.vars.c) key_wc in
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let mar_x = unpickle (sym_decrypt keywc encr_x) in
  let string_x = iutf8 mar_x in
  let x = iS string_x in
  let hx = sha1 mar_x in
  let store = { 
      vars = {store.vars with x = x; };
      hashes = {store.hashes with hx = hx; };
      macs = store.macs; 
      keys = {store.keys with key_wc = key_wc; key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  let hd,hashes = iconcat hashes in
  let ho,_ = iconcat hashes in
  (* Unmarshalling MACs *)
  let cReplyx,macs = iconcat macs in
  let cResumeod,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = {store.hashes with hd = hd; ho = ho; };
      macs = {store.macs with cReplyx = cReplyx; cResumeod = cResumeod; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_Resume_odDetails_cpwqRequest with variables od*)
  let macheader,maccontent = iconcat store.macs.cResumeod 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_Resume_odDetails_cpwqRequest_od ts store mackeypc maccontent in
  (* Verification of a MAC from state w_xReply_odResume_cpwqRequest with variables x*)
  let macheader,maccontent = iconcat store.macs.cReplyx 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_xReply_odResume_cpwqRequest_x ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_cpwqRequest_of_w_xReply_odResume_cpwqRequest_x__p_Resume_odDetails_cpwqRequest_od__((x),store) in
    wired
  | "w_xReply_Forward_cpwqRequest_x__p_Forward_cpwqRequest___" ->
  let variables,security = iconcat payload in
  let keys,protocol = iconcat security in
  let hashes,macs = iconcat protocol in
  (* Unmarshalling variables *)
  let encr_x,variables = iconcat variables in
  (* Registering new keys *)
  let key_wc,keys = iconcat keys in
  let () = reg_keys (cS store.vars.w) (cS store.vars.c) key_wc in
  let key_pc,_ = iconcat keys in
  let () = reg_keys (cS store.vars.p) (cS store.vars.c) key_pc in
  (* Decrypting variables *)
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let mar_x = unpickle (sym_decrypt keywc encr_x) in
  let string_x = iutf8 mar_x in
  let x = iS string_x in
  let hx = sha1 mar_x in
  let store = { 
      vars = {store.vars with x = x; };
      hashes = {store.hashes with hx = hx; };
      macs = store.macs; 
      keys = {store.keys with key_wc = key_wc; key_pc = key_pc; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cForward,macs = iconcat macs in
  let cReplyx,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cForward = cForward; cReplyx = cReplyx; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state p_Forward_cpwqRequest with variables *)
  let macheader,maccontent = iconcat store.macs.cForward 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_Forward_cpwqRequest_ ts store mackeypc maccontent in
  (* Verification of a MAC from state w_xReply_Forward_cpwqRequest with variables x*)
  let macheader,maccontent = iconcat store.macs.cReplyx 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_xReply_Forward_cpwqRequest_x ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_cpwqRequest_of_w_xReply_Forward_cpwqRequest_x__p_Forward_cpwqRequest___((x),store) in
    wired
  | _ -> failwith "Critical Error"


(* Sending message from c to p *)
(* Message has to be MACed for p w *)
let sendWired_Request_c_start = fun c -> fun p -> fun w -> 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_w = cS w in
  let mar_w = utf8 string_w in
  let hw = sha1 mar_w 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; w = w; q = q; };
      hashes = {store.hashes with hc = hc; hp = hp; hw = hw; 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 keycw = gen_keys (cS store.vars.c) (cS store.vars.w) in
  let keys = concat keycw 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_cpwqRequest_cpwq store.header.ts store in
  let mackeycp = get_mackey store.vars.c store.vars.p in
  let macmsg = mac mackeycp (pickle content) in
  let pRequestcpwq = concat header macmsg in
  (* Generation of a MAC from state c_start to role w *)
  let content = content_c_cpwqRequest_cpwq store.header.ts store in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let macmsg = mac mackeycw (pickle content) in
  let wRequestcpwq = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pRequestcpwq = pRequestcpwq; wRequestcpwq = wRequestcpwq; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRequestcpwq macs in
  let macs = concat store.macs.pRequestcpwq 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_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_cpwqRequest_cpwq__" 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 w *)
(* Message has to be MACed for w *)
let sendWired_Audit_p_cpwqRequest = 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 keys = concat store.keys.key_cw keys in
  let keypw = gen_keys (cS store.vars.p) (cS store.vars.w) in
  let keys = concat keypw keys in
  (* Generation of a MAC from state p_cpwqRequest to role w *)
  let content = content_p_Audit_cpwqRequest_ store.header.ts store in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let macmsg = mac mackeypw (pickle content) in
  let wAudit = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wAudit = wAudit; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRequestcpwq macs in
  let macs = concat store.macs.wAudit macs in
  let hashes = nil in
  let hashes = concat store.hashes.hq hashes 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 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 "p_Audit_cpwqRequest___c_cpwqRequest_cpwq__" 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 p *)
(* Message has to be MACed for p *)
let sendWired_Details_w_Audit_cpwqRequest = fun d -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_d = cS d in
  let mar_d = utf8 string_d in
  let hd = sha1 mar_d in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with d = d; };
      hashes = {store.hashes with hd = hd; };
      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 keywp = gen_keys (cS store.vars.w) (cS store.vars.p) in
  let keys = concat keywp keys in
  (* Generation of a MAC from state w_Audit_cpwqRequest to role p *)
  let content = content_w_dDetails_Audit_cpwqRequest_d store.header.ts store in
  let mackeywp = get_mackey store.vars.w store.vars.p in
  let macmsg = mac mackeywp (pickle content) in
  let pDetailsd = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pDetailsd = pDetailsd; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.pDetailsd macs in
  let hashes = nil in
  let variables = nil in
  let string_d = cS store.vars.d in
  let mar_d = utf8 string_d in
  let keywp = get_symkey (cS store.vars.w) (cS store.vars.p) in
  let encr_d = sym_encrypt keywp (pickle mar_d) in
  let variables = concat encr_d variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_dDetails_Audit_cpwqRequest_d__" 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 w *)
(* Message has to be MACed for w c *)
let sendWired_Resume_p_dDetails_Audit_cpwqRequest = 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
  (* Generation of a MAC from state p_dDetails_Audit_cpwqRequest to role w *)
  let content = content_p_Resume_dDetails_cpwqRequest_ store.header.ts store in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let macmsg = mac mackeypw (pickle content) in
  let wResume = concat header macmsg in
  (* Generation of a MAC from state p_dDetails_Audit_cpwqRequest to role c *)
  let content = content_p_Resume_dDetails_cpwqRequest_d store.header.ts store in
  let mackeypc = get_mackey store.vars.p store.vars.c in
  let macmsg = mac mackeypc (pickle content) in
  let cResumed = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wResume = wResume; cResumed = cResumed; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cResumed macs in
  let macs = concat store.macs.wResume 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 keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let encr_q = sym_encrypt keypw (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 "p_Resume_dDetails_cpwqRequest___" 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_Resume_dDetails_cpwqRequest = fun x -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_x = cS x in
  let mar_x = utf8 string_x in
  let hx = sha1 mar_x in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with x = x; };
      hashes = {store.hashes with hx = hx; };
      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 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_Resume_dDetails_cpwqRequest to role c *)
  let content = content_w_xReply_dResume_cpwqRequest_x store.header.ts store in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let macmsg = mac mackeywc (pickle content) in
  let cReplyx = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyx = cReplyx; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cResumed macs in
  let macs = concat store.macs.cReplyx macs in
  let hashes = nil in
  let hashes = concat store.hashes.hd hashes in
  let variables = nil in
  let string_x = cS store.vars.x in
  let mar_x = utf8 string_x in
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let encr_x = sym_encrypt keywc (pickle mar_x) in
  let variables = concat encr_x variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_xReply_dResume_cpwqRequest_x__p_Resume_dDetails_cpwqRequest_d__" 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 w *)
(* Message has to be MACed for w *)
let sendWired_Retry_p_dDetails_Audit_cpwqRequest = fun o -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_o = cS o in
  let mar_o = utf8 string_o in
  let ho = sha1 mar_o in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with o = o; };
      hashes = {store.hashes with ho = ho; };
      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 p_dDetails_Audit_cpwqRequest to role w *)
  let content = content_p_oRetry_dDetails_cpwqRequest_o store.header.ts store in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let macmsg = mac mackeypw (pickle content) in
  let wRetryo = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wRetryo = wRetryo; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRetryo macs in
  let hashes = nil in
  let variables = nil in
  let string_o = cS store.vars.o in
  let mar_o = utf8 string_o in
  let keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let encr_o = sym_encrypt keypw (pickle mar_o) in
  let variables = concat encr_o variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "p_oRetry_dDetails_cpwqRequest_o__" 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 p *)
(* Message has to be MACed for p *)
let sendWired_Details_w_oRetry_dDetails_cpwqRequest = fun d -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_d = cS d in
  let mar_d = utf8 string_d in
  let hd = sha1 mar_d in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with d = d; };
      hashes = {store.hashes with hd = hd; };
      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_oRetry_dDetails_cpwqRequest to role p *)
  let content = content_w_dDetails_oRetry_cpwqRequest_d store.header.ts store in
  let mackeywp = get_mackey store.vars.w store.vars.p in
  let macmsg = mac mackeywp (pickle content) in
  let pDetailsd = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with pDetailsd = pDetailsd; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.pDetailsd macs in
  let hashes = nil in
  let variables = nil in
  let string_d = cS store.vars.d in
  let mar_d = utf8 string_d in
  let keywp = get_symkey (cS store.vars.w) (cS store.vars.p) in
  let encr_d = sym_encrypt keywp (pickle mar_d) in
  let variables = concat encr_d variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_dDetails_oRetry_cpwqRequest_d__" 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 w *)
(* Message has to be MACed for w c *)
let sendWired_Resume_p_dDetails_oRetry_cpwqRequest = 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
  (* Generation of a MAC from state p_dDetails_oRetry_cpwqRequest to role w *)
  let content = content_p_Resume_odDetails_cpwqRequest_ store.header.ts store in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let macmsg = mac mackeypw (pickle content) in
  let wResume = concat header macmsg in
  (* Generation of a MAC from state p_dDetails_oRetry_cpwqRequest to role c *)
  let content = content_p_Resume_odDetails_cpwqRequest_od store.header.ts store in
  let mackeypc = get_mackey store.vars.p store.vars.c in
  let macmsg = mac mackeypc (pickle content) in
  let cResumeod = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wResume = wResume; cResumeod = cResumeod; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cResumeod macs in
  let macs = concat store.macs.wResume 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 keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let encr_q = sym_encrypt keypw (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 "p_Resume_odDetails_cpwqRequest___" 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_Resume_odDetails_cpwqRequest = fun x -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_x = cS x in
  let mar_x = utf8 string_x in
  let hx = sha1 mar_x in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with x = x; };
      hashes = {store.hashes with hx = hx; };
      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 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_Resume_odDetails_cpwqRequest to role c *)
  let content = content_w_xReply_odResume_cpwqRequest_x store.header.ts store in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let macmsg = mac mackeywc (pickle content) in
  let cReplyx = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyx = cReplyx; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cResumeod macs in
  let macs = concat store.macs.cReplyx macs in
  let hashes = nil in
  let hashes = concat store.hashes.ho hashes in
  let hashes = concat store.hashes.hd hashes in
  let variables = nil in
  let string_x = cS store.vars.x in
  let mar_x = utf8 string_x in
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let encr_x = sym_encrypt keywc (pickle mar_x) in
  let variables = concat encr_x variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_xReply_odResume_cpwqRequest_x__p_Resume_odDetails_cpwqRequest_od__" 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 w *)
(* Message has to be MACed for w *)
let sendWired_Retry_p_dDetails_oRetry_cpwqRequest = fun o -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_o = cS o in
  let mar_o = utf8 string_o in
  let ho = sha1 mar_o in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with o = o; };
      hashes = {store.hashes with ho = ho; };
      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 p_dDetails_oRetry_cpwqRequest to role w *)
  let content = content_p_oRetry_dDetails_cpwqRequest_o store.header.ts store in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let macmsg = mac mackeypw (pickle content) in
  let wRetryo = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wRetryo = wRetryo; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRetryo macs in
  let hashes = nil in
  let variables = nil in
  let string_o = cS store.vars.o in
  let mar_o = utf8 string_o in
  let keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let encr_o = sym_encrypt keypw (pickle mar_o) in
  let variables = concat encr_o variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "p_oRetry_dDetails_cpwqRequest_o__" 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 p to w *)
(* Message has to be MACed for w c *)
let sendWired_Forward_p_cpwqRequest = 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_cw keys in
  let keypw = gen_keys (cS store.vars.p) (cS store.vars.w) in
  let keys = concat keypw keys in
  (* Generation of a MAC from state p_cpwqRequest to role w *)
  let content = content_p_Forward_cpwqRequest_ store.header.ts store in
  let mackeypw = get_mackey store.vars.p store.vars.w in
  let macmsg = mac mackeypw (pickle content) in
  let wForward = concat header macmsg in
  (* Generation of a MAC from state p_cpwqRequest to role c *)
  let content = content_p_Forward_cpwqRequest_ store.header.ts store in
  let mackeypc = get_mackey store.vars.p store.vars.c in
  let macmsg = mac mackeypc (pickle content) in
  let cForward = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wForward = wForward; cForward = cForward; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRequestcpwq macs in
  let macs = concat store.macs.cForward macs in
  let macs = concat store.macs.wForward 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 keypw = get_symkey (cS store.vars.p) (cS store.vars.w) in
  let encr_q = sym_encrypt keypw (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 "p_Forward_cpwqRequest___c_cpwqRequest_cpwq__" 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_Forward_cpwqRequest = fun x -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let string_x = cS x in
  let mar_x = utf8 string_x in
  let hx = sha1 mar_x in
  let ts = store.header.ts + 1 in
  let store = { 
      vars = {store.vars with x = x; };
      hashes = {store.hashes with hx = hx; };
      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 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_Forward_cpwqRequest to role c *)
  let content = content_w_xReply_Forward_cpwqRequest_x store.header.ts store in
  let mackeywc = get_mackey store.vars.w store.vars.c in
  let macmsg = mac mackeywc (pickle content) in
  let cReplyx = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyx = cReplyx; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.cReplyx macs in
  let macs = concat store.macs.cForward macs in
  let hashes = nil in
  let variables = nil in
  let string_x = cS store.vars.x in
  let mar_x = utf8 string_x in
  let keywc = get_symkey (cS store.vars.w) (cS store.vars.c) in
  let encr_x = sym_encrypt keywc (pickle mar_x) in
  let variables = concat encr_x variables in
  let protocol = concat hashes macs in
  let security = concat keys protocol in
  let payload = concat variables security in
  let visib = cS "w_xReply_Forward_cpwqRequest_x__p_Forward_cpwqRequest___" 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