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_cwqRequest),({c,w,q}Request{c,w,q}),(w_start,w_cwqRequest))(w_cwqRequest,w_Fault_cwqRequest),({}Fault{}),(c_cwqRequest,c_Fault_cwqRequest))(w_cwqRequest,w_xReply_cwqRequest),({x}Reply{x}),(c_cwqRequest,c_xReply_cwqRequest))(c_xReply_cwqRequest,c_qExtra_cwxReply),({q}Extra{q}),(w_xReply_cwqRequest,w_qExtra_cwxReply))(w_qExtra_cwxReply,w_xReply_cwqExtra),({x}Reply{x}),(c_qExtra_cwxReply,c_xReply_cwqExtra))(c_xReply_cwqExtra,c_qExtra_cwxReply),({q}Extra{q}),(w_xReply_cwqExtra,w_qExtra_cwxReply))(w_qExtra_cwxReply,w_Fault_cwxqExtra),({}Fault{}),(c_qExtra_cwxReply,c_Fault_cwxqExtra))"))


type vars = {
  c : principal ;
  w : principal ;
  q : string ;
  x : int }
type hashes = {
  hc : bytes ;
  hw : bytes ;
  hq : bytes ;
  hx : bytes }
type macs = {
  wRequestcwq : bytes ;
  cReplyx : bytes ;
  wExtraq : bytes ;
  cFault : bytes }
type keys = {
  key_cw : bytes ;
  key_wc : 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 = "" ; q = "" ; x = 0 };
   hashes = { hc = utf8 (cS "") ; hw = utf8 (cS "") ; hq = utf8 (cS "") ; hx = utf8 (cS "") };
   macs = { wRequestcwq = utf8 (cS "") ; cReplyx = utf8 (cS "") ; wExtraq = utf8 (cS "") ; cFault = utf8 (cS "") };
   keys = { key_cw = utf8 (cS "") ;
  key_wc = 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 ; q = "" ; x = 0 };
   hashes = { hc = utf8 (cS "") ; hw = utf8 (cS "") ; hq = utf8 (cS "") ; hx = utf8 (cS "") };
   macs = { wRequestcwq = utf8 (cS "") ; cReplyx = utf8 (cS "") ; wExtraq = utf8 (cS "") ; cFault = utf8 (cS "") };
   keys = { key_cw = utf8 (cS "") ;
  key_wc = 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 * string)
| Send_Reply of (principal * bytes * int* int)
| Send_Extra of (principal * bytes * int* string)
| Send_Fault of (principal * bytes * int)
| Recv_Request of (principal * bytes * int * principal * principal * string)
| Recv_Reply of (principal * bytes * int * int)
| Recv_Extra of (principal * bytes * int * string)
| Recv_Fault of (principal * bytes * int)



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

let content_c_cwqRequest_cwq = 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.hc hashes in
  let nextstate = cS "c_cwqRequest" 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_cwqRequest_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "w_Fault_cwqRequest" 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_cwqRequest_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_cwqRequest" 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_cwxReply_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_cwxReply" 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_cwqExtra_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_cwqExtra" 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_cwxqExtra_ = fun ts store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let hashes = nil in
  let nextstate = cS "w_Fault_cwxqExtra" 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_w_c_cwqRequest_cwq = fun ts store k m ->
  let content = content_c_cwqRequest_cwq 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_cwqRequest_ = fun ts store k m ->
  let content = content_w_Fault_cwqRequest_ 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_cwqRequest_x = fun ts store k m ->
  let content = content_w_xReply_cwqRequest_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_w_c_qExtra_cwxReply_q = fun ts store k m ->
  let content = content_c_qExtra_cwxReply_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_xReply_cwqExtra_x = fun ts store k m ->
  let content = content_w_xReply_cwqExtra_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_w_Fault_cwxqExtra_ = fun ts store k m ->
  let content = content_w_Fault_cwxqExtra_ 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_w_start =
  | Wired_in_w_start_of_c_cwqRequest_cwq__ of (principal * principal * string) * store

type wired_c_cwqRequest =
  | Wired_in_c_cwqRequest_of_w_Fault_cwqRequest___ of (unit) * store
  | Wired_in_c_cwqRequest_of_w_xReply_cwqRequest_x__ of (int) * store

type wired_w_xReply_cwqRequest =
  | Wired_in_w_xReply_cwqRequest_of_c_qExtra_cwxReply_q__ of (string) * store

type wired_w_xReply_cwqExtra =
  | Wired_in_w_xReply_cwqExtra_of_c_qExtra_cwxReply_q__ of (string) * store

type wired_c_qExtra_cwxReply =
  | Wired_in_c_qExtra_cwxReply_of_w_xReply_cwqExtra_x__ of (int) * store
  | Wired_in_c_qExtra_cwxReply_of_w_Fault_cwxqExtra___ of (unit) * store


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_cwqRequest_cwq__" ->
  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_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; w = w; };
      hashes = store.hashes;
      macs = store.macs; 
      keys = store.keys; 
      header = store.header} in
  (* Registering new keys *)
  let key_cw,_ = iconcat keys in
  let () = reg_keys (cS store.vars.c) (cS store.vars.w) key_cw 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; hw = hw; hq = hq; };
      macs = store.macs; 
      keys = {store.keys with key_cw = key_cw; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let wRequestcwq,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wRequestcwq = wRequestcwq; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state c_cwqRequest with variables cwq*)
  let macheader,maccontent = iconcat store.macs.wRequestcwq 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_cwqRequest_cwq 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_cwqRequest_cwq__((c,w,q),store) in
    wired

let receiveWired_c_cwqRequest : store -> wired_c_cwqRequest = 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_cwqRequest___" ->
  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_cwqRequest 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_cwqRequest_ ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_cwqRequest_of_w_Fault_cwqRequest___((),store) in
    wired
  | "w_xReply_cwqRequest_x__" ->
  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,_ = 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_x = unpickle (sym_decrypt keywc encr_x) in
  let string_x = iutf8 mar_x in
  let marred_x = iS string_x in
  let x = int_of_string marred_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; }; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cReplyx,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyx = cReplyx; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_xReply_cwqRequest 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_cwqRequest_x ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_cwqRequest_of_w_xReply_cwqRequest_x__((x),store) in
    wired

let receiveWired_w_xReply_cwqRequest : store -> wired_w_xReply_cwqRequest = 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_cwxReply_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_cwxReply 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_cwxReply_q ts store mackeycw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_xReply_cwqRequest_of_c_qExtra_cwxReply_q__((q),store) in
    wired

let receiveWired_w_xReply_cwqExtra : store -> wired_w_xReply_cwqExtra = 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_cwxReply_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_cwxReply 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_cwxReply_q ts store mackeycw maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_w_xReply_cwqExtra_of_c_qExtra_cwxReply_q__((q),store) in
    wired

let receiveWired_c_qExtra_cwxReply : store -> wired_c_qExtra_cwxReply = 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_cwqExtra_x__" ->
  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 *)
  (* 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 marred_x = iS string_x in
  let x = int_of_string marred_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; 
      header = store.header} in
  (* Unmarshalling hashes *)
  (* Unmarshalling MACs *)
  let cReplyx,_ = iconcat macs in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with cReplyx = cReplyx; }; 
      keys = store.keys; 
      header = store.header} in
  (* Verification of a MAC from state w_xReply_cwqExtra 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_cwqExtra_x ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_qExtra_cwxReply_of_w_xReply_cwqExtra_x__((x),store) in
    wired
  | "w_Fault_cwxqExtra___" ->
  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_cwxqExtra 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_cwxqExtra_ ts store mackeywc maccontent in
  let _ = test_eq oldts store.header.ts "Time-stamp verification" in
  (* Verification Ended *)
    let wired = Wired_in_c_qExtra_cwxReply_of_w_Fault_cwxqExtra___((),store) in
    wired
  | _ -> failwith "Critical Error"


(* Sending message from c to w *)
(* Message has to be MACed for w *)
let sendWired_Request_c_start = fun c -> 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_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; w = w; q = q; };
      hashes = {store.hashes with hc = hc; 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
  (* Generation of a MAC from state c_start to role w *)
  let content = content_c_cwqRequest_cwq store.header.ts store in
  let mackeycw = get_mackey store.vars.c store.vars.w in
  let macmsg = mac mackeycw (pickle content) in
  let wRequestcwq = concat header macmsg in
  let store = { 
      vars = store.vars;
      hashes = store.hashes;
      macs = {store.macs with wRequestcwq = wRequestcwq; }; 
      keys = store.keys; 
      header = store.header} in
  let macs = nil in
  let macs = concat store.macs.wRequestcwq 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 string_w = cS store.vars.w in
  let mar_w = utf8 string_w in
  let variables = concat mar_w 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_cwqRequest_cwq__" 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_cwqRequest = 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_cwqRequest to role c *)
  let content = content_w_Fault_cwqRequest_ 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_cwqRequest___" 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_cwqRequest = fun x -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let marred_x = string_of_int x in
  let string_x = cS marred_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 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_cwqRequest to role c *)
  let content = content_w_xReply_cwqRequest_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 hashes = nil in
  let variables = nil in
  let marred_x = string_of_int store.vars.x in
  let string_x = cS marred_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_cwqRequest_x__" 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_xReply_cwqRequest = 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_xReply_cwqRequest to role w *)
  let content = content_c_qExtra_cwxReply_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_cwxReply_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_cwxReply = fun x -> fun store ->
  let empty_str = cS "" in
  let nil = utf8 empty_str in
  let marred_x = string_of_int x in
  let string_x = cS marred_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
  (* Generation of a MAC from state w_qExtra_cwxReply to role c *)
  let content = content_w_xReply_cwqExtra_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 hashes = nil in
  let variables = nil in
  let marred_x = string_of_int store.vars.x in
  let string_x = cS marred_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_cwqExtra_x__" 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_xReply_cwqExtra = 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_xReply_cwqExtra to role w *)
  let content = content_c_qExtra_cwxReply_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_cwxReply_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_cwxReply = 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_cwxReply to role c *)
  let content = content_w_Fault_cwxqExtra_ 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_cwxqExtra___" 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