(herald wrap-decrypt (bound 10))

(comment "CPSA 3.2.2")
(comment "All input read from wrap_decrypt.lsp")
(comment "Strand count bounded at 10")

(defprotocol wrap-decrypt basic
  (defrole make
    (vars (k skey))
    (trace (init (cat k "init")) (send (hash k)))
    (uniq-gen k))
  (defrole set-wrap
    (vars (k skey) (cur mesg))
    (trace (tran (cat k cur) (cat k "wrap")))
    (neq (cur "wrap")))
  (defrole set-decrypt
    (vars (k skey) (cur mesg))
    (trace (tran (cat k cur) (cat k "decrypt")))
    (neq (cur "decrypt")))
  (defrole wrap
    (vars (k0 k1 skey) (cur mesg))
    (trace (recv (hash k0)) (recv (hash k1)) (obsv (cat k0 cur))
      (obsv (cat k1 "wrap")) (send (enc k0 k1))))
  (defrole decrypt
    (vars (x mesg) (k skey))
    (trace (recv (enc x k)) (recv (hash k)) (obsv (cat k "decrypt"))
      (send x))))

(defskeleton wrap-decrypt
  (vars (k kp skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k kp))
  (defstrand make 2 (k kp))
  (defstrand set-decrypt 1 (cur "wrap") (k kp))
  (defstrand set-wrap 1 (cur "init") (k kp))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 kp))
  (defstrand make 2 (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k kp)
  (traces ((recv k) (send k))
    ((recv (enc k kp)) (recv (hash kp)) (obsv (cat kp "decrypt"))
      (send k)) ((init (cat kp "init")) (send (hash kp)))
    ((tran (cat kp "wrap") (cat kp "decrypt")))
    ((tran (cat kp "init") (cat kp "wrap")))
    ((recv (hash k)) (recv (hash kp)) (obsv (cat k "init"))
      (obsv (cat kp "wrap")) (send (enc k kp)))
    ((init (cat k "init")) (send (hash k))))
  (label 0)
  (unrealized (1 2) (3 0) (4 0) (5 2) (5 3))
  (preskeleton)
  (comment "Not a skeleton"))

(defskeleton wrap-decrypt
  (vars (k kp skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k kp))
  (defstrand make 2 (k kp))
  (defstrand set-decrypt 1 (cur "wrap") (k kp))
  (defstrand set-wrap 1 (cur "init") (k kp))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 kp))
  (defstrand make 2 (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)) ((6 1) (5 0)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k kp)
  (traces ((recv k) (send k))
    ((recv (enc k kp)) (recv (hash kp)) (obsv (cat kp "decrypt"))
      (send k)) ((init (cat kp "init")) (send (hash kp)))
    ((tran (cat kp "wrap") (cat kp "decrypt")))
    ((tran (cat kp "init") (cat kp "wrap")))
    ((recv (hash k)) (recv (hash kp)) (obsv (cat k "init"))
      (obsv (cat kp "wrap")) (send (enc k kp)))
    ((init (cat k "init")) (send (hash k))))
  (label 1)
  (parent 0)
  (unrealized (1 2) (3 0) (4 0) (5 2) (5 3))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (kp skey))
  (deflistener kp)
  (defstrand decrypt 4 (x kp) (k kp))
  (defstrand make 2 (k kp))
  (defstrand set-decrypt 1 (cur "wrap") (k kp))
  (defstrand set-wrap 1 (cur "init") (k kp))
  (defstrand wrap 5 (cur "init") (k0 kp) (k1 kp))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 0)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen kp)
  (operation collapsed 6 2)
  (traces ((recv kp) (send kp))
    ((recv (enc kp kp)) (recv (hash kp)) (obsv (cat kp "decrypt"))
      (send kp)) ((init (cat kp "init")) (send (hash kp)))
    ((tran (cat kp "wrap") (cat kp "decrypt")))
    ((tran (cat kp "init") (cat kp "wrap")))
    ((recv (hash kp)) (recv (hash kp)) (obsv (cat kp "init"))
      (obsv (cat kp "wrap")) (send (enc kp kp))))
  (label 2)
  (parent 1)
  (unrealized (1 2) (3 0) (4 0) (5 2) (5 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (kp k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k kp))
  (defstrand make 2 (k kp))
  (defstrand set-decrypt 1 (cur "wrap") (k kp))
  (defstrand set-wrap 1 (cur "init") (k kp))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 kp))
  (defstrand make 2 (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)))
  (leadsto ((6 0) (5 2)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen kp k)
  (operation state-passing-test (displaced 7 6 make 1) (cat k "init")
    (5 2))
  (traces ((recv k) (send k))
    ((recv (enc k kp)) (recv (hash kp)) (obsv (cat kp "decrypt"))
      (send k)) ((init (cat kp "init")) (send (hash kp)))
    ((tran (cat kp "wrap") (cat kp "decrypt")))
    ((tran (cat kp "init") (cat kp "wrap")))
    ((recv (hash k)) (recv (hash kp)) (obsv (cat k "init"))
      (obsv (cat kp "wrap")) (send (enc k kp)))
    ((init (cat k "init")) (send (hash k))))
  (label 3)
  (parent 1)
  (unrealized (1 2) (3 0) (4 0) (5 3))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)))
  (leadsto ((2 0) (5 2)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (displaced 6 2 make 1) (cat k "init")
    (5 2))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k))))
  (label 4)
  (parent 2)
  (unrealized (1 2) (3 0) (4 0) (5 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)))
  (leadsto ((4 0) (5 3)) ((6 0) (5 2)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 7 4 set-wrap 1)
    (cat k-0 "wrap") (5 3))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k))))
  (label 5)
  (parent 3)
  (unrealized (1 2) (3 0) (4 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (7 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (5 3)))
  (leadsto ((6 0) (5 2)) ((7 0) (5 3)))
  (neq (cur "wrap") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-wrap 1)
    (cat k-0 "wrap") (5 3))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 cur) (cat k-0 "wrap"))))
  (label 6)
  (parent 3)
  (unrealized (1 2) (3 0) (4 0) (7 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)))
  (leadsto ((2 0) (5 2)) ((4 0) (5 3)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (displaced 6 4 set-wrap 1)
    (cat k "wrap") (5 3))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k))))
  (label 7)
  (parent 4)
  (unrealized (1 2) (3 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (6 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 4) (1 0)) ((6 0) (5 3)))
  (leadsto ((2 0) (5 2)) ((6 0) (5 3)))
  (neq (cur "wrap") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-wrap 1) (cat k "wrap")
    (5 3))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k cur) (cat k "wrap"))))
  (label 8)
  (parent 4)
  (unrealized (1 2) (3 0) (4 0) (6 0))
  (origs)
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (5 3)) ((6 0) (5 2)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 7 2 make 1) (cat k-0 "init")
    (4 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k))))
  (label 9)
  (parent 5)
  (unrealized (1 2) (3 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (7 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (5 3)))
  (leadsto ((2 0) (7 0)) ((6 0) (5 2)) ((7 0) (5 3)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 8 2 make 1) (cat k-0 "init")
    (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "init") (cat k-0 "wrap"))))
  (label 10)
  (parent 6)
  (unrealized (1 2) (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (7 0))
    ((4 0) (3 0)) ((5 4) (1 0)) ((6 0) (5 2)) ((6 1) (5 0))
    ((7 0) (5 3)))
  (leadsto ((3 0) (7 0)) ((6 0) (5 2)) ((7 0) (5 3)))
  (neq ("wrap" "decrypt") ("decrypt" "wrap") ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 8 3 set-decrypt 1)
    (cat k-0 "decrypt") (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap"))))
  (label 11)
  (parent 6)
  (unrealized (1 2) (3 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (8 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (7 0)))
  (leadsto ((6 0) (5 2)) ((7 0) (5 3)) ((8 0) (7 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k-0 "decrypt") (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 cur) (cat k-0 "decrypt"))))
  (label 12)
  (parent 6)
  (unrealized (1 2) (3 0) (4 0) (8 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 2) (4 0))
    ((5 4) (1 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (5 3)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (displaced 6 2 make 1) (cat k "init")
    (4 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k))))
  (label 13)
  (parent 7)
  (unrealized (1 2) (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (6 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (6 0)) ((5 4) (1 0)) ((6 0) (5 3)))
  (leadsto ((2 0) (5 2)) ((2 0) (6 0)) ((6 0) (5 3)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (displaced 7 2 make 1) (cat k "init")
    (6 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "init") (cat k "wrap"))))
  (label 14)
  (parent 8)
  (unrealized (1 2) (3 0) (4 0))
  (origs)
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (6 0)) ((4 0) (3 0)) ((5 4) (1 0)) ((6 0) (5 3)))
  (leadsto ((2 0) (5 2)) ((3 0) (6 0)) ((6 0) (5 3)))
  (neq ("wrap" "decrypt") ("decrypt" "wrap") ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 7 3 set-decrypt 1)
    (cat k "decrypt") (6 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap"))))
  (label 15)
  (parent 8)
  (unrealized (1 2) (3 0) (4 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (7 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (6 0)))
  (leadsto ((2 0) (5 2)) ((6 0) (5 3)) ((7 0) (6 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (6 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 16)
  (parent 8)
  (unrealized (1 2) (3 0) (4 0) (7 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 3) (3 0)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (3 0)) ((4 0) (5 3)) ((6 0) (5 2)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 7 4 set-wrap 1)
    (cat k-0 "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k))))
  (label 17)
  (parent 9)
  (unrealized (1 2))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (7 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (3 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (5 3)) ((6 0) (5 2)) ((7 0) (3 0)))
  (neq (cur "wrap") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-wrap 1)
    (cat k-0 "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 cur) (cat k-0 "wrap"))))
  (label 18)
  (parent 9)
  (unrealized (1 2) (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (7 0))
    ((4 0) (3 0)) ((5 4) (1 0)) ((6 0) (5 2)) ((6 1) (5 0))
    ((7 0) (5 3)))
  (leadsto ((2 0) (4 0)) ((3 0) (7 0)) ((6 0) (5 2)) ((7 0) (5 3)))
  (neq ("wrap" "decrypt") ("decrypt" "wrap") ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 8 2 make 1) (cat k-0 "init")
    (4 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap"))))
  (label 19)
  (parent 11)
  (unrealized (1 2) (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "init") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (8 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (7 0)))
  (leadsto ((2 0) (8 0)) ((6 0) (5 2)) ((7 0) (5 3)) ((8 0) (7 0)))
  (neq ("init" "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 9 2 make 1) (cat k-0 "init")
    (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "init") (cat k-0 "decrypt"))))
  (label 20)
  (parent 12)
  (unrealized (1 2) (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (8 0)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (7 0)))
  (leadsto ((4 0) (8 0)) ((6 0) (5 2)) ((7 0) (5 3)) ((8 0) (7 0)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 9 4 set-wrap 1)
    (cat k-0 "wrap") (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt"))))
  (label 21)
  (parent 12)
  (unrealized (1 2) (3 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 2) (4 0))
    ((5 3) (3 0)) ((5 4) (1 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (3 0)) ((4 0) (5 3)))
  (neq ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (displaced 6 4 set-wrap 1)
    (cat k "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k))))
  (label 23)
  (parent 13)
  (unrealized (1 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (6 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (4 0)) ((5 4) (1 0)) ((6 0) (3 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (5 3)) ((6 0) (3 0)))
  (neq (cur "wrap") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-wrap 1) (cat k "wrap")
    (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k cur) (cat k "wrap"))))
  (label 24)
  (parent 13)
  (unrealized (1 2) (6 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (6 0)) ((4 0) (3 0)) ((5 2) (4 0)) ((5 4) (1 0))
    ((6 0) (5 3)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((3 0) (6 0)) ((6 0) (5 3)))
  (neq ("wrap" "decrypt") ("decrypt" "wrap") ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 7 2 make 1) (cat k "init")
    (4 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap"))))
  (label 25)
  (parent 15)
  (unrealized (1 2) (3 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "init") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (7 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (7 0)) ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (6 0)))
  (leadsto ((2 0) (5 2)) ((2 0) (7 0)) ((6 0) (5 3)) ((7 0) (6 0)))
  (neq ("init" "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (displaced 8 2 make 1) (cat k "init")
    (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "init") (cat k "decrypt"))))
  (label 26)
  (parent 16)
  (unrealized (1 2) (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (7 0)) ((5 4) (1 0))
    ((6 0) (5 3)) ((7 0) (6 0)))
  (leadsto ((2 0) (5 2)) ((4 0) (7 0)) ((6 0) (5 3)) ((7 0) (6 0)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 8 4 set-wrap 1)
    (cat k "wrap") (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt"))))
  (label 27)
  (parent 16)
  (unrealized (1 2) (3 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (8 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (6 0)) ((8 0) (7 0)))
  (leadsto ((2 0) (5 2)) ((6 0) (5 3)) ((7 0) (6 0)) ((8 0) (7 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("decrypt" "wrap")
    ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-wrap 1) (cat k "wrap")
    (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k cur) (cat k "wrap"))))
  (label 28)
  (parent 16)
  (unrealized (1 2) (3 0) (4 0) (8 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (5 3)) ((5 3) (3 0)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)))
  (leadsto ((2 0) (4 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((6 0) (5 2)))
  (neq ("wrap" "decrypt") ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 7 3 set-decrypt 1)
    (cat k-0 "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k))))
  (label 29)
  (parent 17)
  (unrealized)
  (shape)
  (maps ((0 1 2 3 4 5 6) ((k k) (kp k-0))))
  (origs))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (7 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 3) (3 0))
    ((5 4) (1 0)) ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((4 0) (3 0)) ((4 0) (5 3)) ((6 0) (5 2))
    ((7 0) (1 2)))
  (neq (cur "decrypt") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k-0 "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 cur) (cat k-0 "decrypt"))))
  (label 30)
  (parent 17)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (8 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (3 0)) ((8 0) (7 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (5 3)) ((6 0) (5 2)) ((7 0) (3 0))
    ((8 0) (7 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k-0 "decrypt") (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 cur) (cat k-0 "decrypt"))))
  (label 31)
  (parent 18)
  (unrealized (1 2) (8 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (7 0))
    ((4 0) (3 0)) ((5 4) (1 0)) ((6 0) (5 2)) ((6 1) (5 0))
    ((7 0) (5 3)))
  (leadsto ((2 0) (4 0)) ((3 0) (7 0)) ((4 0) (3 0)) ((6 0) (5 2))
    ((7 0) (5 3)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 8 4 set-wrap 1)
    (cat k-0 "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap"))))
  (label 32)
  (parent 19)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-wrap 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (8 0)) ((2 1) (5 1))
    ((3 0) (7 0)) ((4 0) (3 0)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (3 0)))
  (leadsto ((2 0) (4 0)) ((3 0) (7 0)) ((6 0) (5 2)) ((7 0) (5 3))
    ((8 0) (3 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("decrypt" "wrap")
    ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-wrap 1)
    (cat k-0 "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 cur) (cat k-0 "wrap"))))
  (label 33)
  (parent 19)
  (unrealized (1 2) (8 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (3 0)) ((4 0) (8 0)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (7 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (8 0)) ((6 0) (5 2)) ((7 0) (5 3))
    ((8 0) (7 0)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 9 2 make 1) (cat k-0 "init")
    (4 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt"))))
  (label 34)
  (parent 21)
  (unrealized (1 2) (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 2) (4 0))
    ((5 3) (3 0)) ((5 4) (1 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((3 0) (1 2)) ((4 0) (3 0))
    ((4 0) (5 3)))
  (neq ("wrap" "decrypt") ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 6 3 set-decrypt 1)
    (cat k "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k))))
  (label 35)
  (parent 23)
  (unrealized)
  (shape)
  (maps ((0 1 2 3 4 5 2) ((k k) (kp k))))
  (origs))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (6 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (4 0)) ((5 3) (3 0)) ((5 4) (1 0)) ((6 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((6 0) (1 2)))
  (neq (cur "decrypt") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 36)
  (parent 23)
  (unrealized (6 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (7 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (4 0)) ((5 4) (1 0)) ((6 0) (3 0)) ((7 0) (6 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (5 3)) ((6 0) (3 0))
    ((7 0) (6 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (6 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 37)
  (parent 24)
  (unrealized (1 2) (7 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (6 0)) ((4 0) (3 0)) ((5 2) (4 0)) ((5 4) (1 0))
    ((6 0) (5 3)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((3 0) (6 0)) ((4 0) (3 0))
    ((6 0) (5 3)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 7 4 set-wrap 1)
    (cat k "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap"))))
  (label 38)
  (parent 25)
  (unrealized (1 2))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-wrap 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (7 0))
    ((2 1) (5 0)) ((3 0) (6 0)) ((4 0) (3 0)) ((5 2) (4 0))
    ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (3 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((3 0) (6 0)) ((6 0) (5 3))
    ((7 0) (3 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("decrypt" "wrap")
    ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-wrap 1) (cat k "wrap")
    (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k cur) (cat k "wrap"))))
  (label 39)
  (parent 25)
  (unrealized (1 2) (7 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (7 0)) ((5 2) (4 0))
    ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (6 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (7 0)) ((6 0) (5 3))
    ((7 0) (6 0)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 8 2 make 1) (cat k "init")
    (4 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt"))))
  (label 40)
  (parent 27)
  (unrealized (1 2) (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (8 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (8 0)) ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (6 0))
    ((8 0) (7 0)))
  (leadsto ((2 0) (5 2)) ((2 0) (8 0)) ((6 0) (5 3)) ((7 0) (6 0))
    ((8 0) (7 0)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 9 2 make 1) (cat k "init")
    (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap"))))
  (label 41)
  (parent 28)
  (unrealized (1 2) (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (8 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 3) (3 0))
    ((5 4) (1 0)) ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (1 2))
    ((8 0) (7 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (3 0)) ((4 0) (5 3)) ((6 0) (5 2))
    ((7 0) (1 2)) ((8 0) (7 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-wrap 1)
    (cat k-0 "wrap") (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 cur) (cat k-0 "wrap"))))
  (label 42)
  (parent 30)
  (unrealized (8 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (5 3)) ((4 0) (8 0)) ((5 3) (8 0)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (3 0)) ((8 0) (7 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (5 3)) ((4 0) (8 0)) ((6 0) (5 2))
    ((7 0) (3 0)) ((8 0) (7 0)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 9 4 set-wrap 1)
    (cat k-0 "wrap") (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt"))))
  (label 43)
  (parent 31)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (8 0)) ((2 1) (5 1))
    ((3 0) (7 0)) ((4 0) (3 0)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((3 0) (7 0)) ((4 0) (3 0)) ((6 0) (5 2))
    ((7 0) (5 3)) ((8 0) (1 2)))
  (neq (cur "decrypt") ("init" "wrap") ("wrap" "decrypt")
    ("decrypt" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k-0 "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 cur) (cat k-0 "decrypt"))))
  (label 45)
  (parent 32)
  (unrealized (8 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 1) (5 1)) ((3 0) (1 2))
    ((4 0) (8 0)) ((5 3) (3 0)) ((5 4) (1 0)) ((6 0) (5 2))
    ((6 1) (5 0)) ((7 0) (3 0)) ((7 0) (5 3)) ((8 0) (7 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (8 0)) ((6 0) (5 2)) ((7 0) (3 0))
    ((7 0) (5 3)) ((8 0) (7 0)))
  (neq ("decrypt" "wrap") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 9 7 set-wrap 1)
    (cat k-0 "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt"))))
  (label 46)
  (parent 34)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (7 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (4 0)) ((5 3) (3 0)) ((5 4) (1 0)) ((6 0) (1 2))
    ((7 0) (6 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((6 0) (1 2)) ((7 0) (6 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-wrap 1) (cat k "wrap")
    (6 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k cur) (cat k "wrap"))))
  (label 48)
  (parent 36)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (5 3)) ((4 0) (7 0)) ((5 2) (4 0))
    ((5 3) (7 0)) ((5 4) (1 0)) ((6 0) (3 0)) ((7 0) (6 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (5 3)) ((4 0) (7 0))
    ((6 0) (3 0)) ((7 0) (6 0)))
  (neq ("init" "wrap") ("wrap" "decrypt") ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (displaced 8 4 set-wrap 1)
    (cat k "wrap") (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt"))))
  (label 49)
  (parent 37)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (8 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (4 0)) ((5 4) (1 0)) ((6 0) (3 0)) ((7 0) (6 0))
    ((8 0) (7 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (5 3)) ((6 0) (3 0))
    ((7 0) (6 0)) ((8 0) (7 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("decrypt" "wrap")
    ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-wrap 1) (cat k "wrap")
    (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k cur) (cat k "wrap"))))
  (label 50)
  (parent 37)
  (unrealized (1 2) (8 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (7 0))
    ((2 1) (5 0)) ((3 0) (6 0)) ((4 0) (3 0)) ((5 2) (4 0))
    ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((3 0) (6 0)) ((4 0) (3 0))
    ((6 0) (5 3)) ((7 0) (1 2)))
  (neq (cur "decrypt") ("init" "wrap") ("wrap" "decrypt")
    ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 51)
  (parent 38)
  (unrealized (7 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 1) (5 0))
    ((3 0) (1 2)) ((4 0) (7 0)) ((5 2) (4 0)) ((5 3) (3 0))
    ((5 4) (1 0)) ((6 0) (3 0)) ((6 0) (5 3)) ((7 0) (6 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (7 0)) ((6 0) (3 0))
    ((6 0) (5 3)) ((7 0) (6 0)))
  (neq ("decrypt" "wrap") ("init" "wrap") ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (displaced 8 6 set-wrap 1)
    (cat k "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt"))))
  (label 52)
  (parent 40)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (8 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (7 0))
    ((5 2) (4 0)) ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (6 0))
    ((8 0) (3 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (7 0)) ((6 0) (5 3))
    ((7 0) (6 0)) ((8 0) (3 0)))
  (neq (cur "wrap") ("init" "wrap") ("wrap" "decrypt")
    ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-wrap 1) (cat k "wrap")
    (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k cur) (cat k "wrap"))))
  (label 53)
  (parent 40)
  (unrealized (1 2) (8 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (8 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (4 0)) ((5 3) (3 0)) ((5 4) (1 0)) ((6 0) (1 2))
    ((7 0) (6 0)) ((8 0) (7 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((6 0) (1 2)) ((7 0) (6 0)) ((8 0) (7 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("wrap" "decrypt")
    ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (7 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 57)
  (parent 48)
  (unrealized (8 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (8 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (5 3)) ((4 0) (7 0))
    ((5 2) (4 0)) ((5 3) (7 0)) ((5 4) (1 0)) ((6 0) (3 0))
    ((7 0) (6 0)) ((8 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (5 3)) ((4 0) (7 0))
    ((6 0) (3 0)) ((7 0) (6 0)) ((8 0) (1 2)))
  (neq (cur "decrypt") ("init" "wrap") ("wrap" "decrypt")
    ("decrypt" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 58)
  (parent 49)
  (unrealized (8 0))
  (comment "empty cohort"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (8 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (7 0)) ((5 2) (4 0))
    ((5 3) (3 0)) ((5 4) (1 0)) ((6 0) (3 0)) ((6 0) (5 3))
    ((7 0) (6 0)) ((8 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (7 0)) ((6 0) (3 0))
    ((6 0) (5 3)) ((7 0) (6 0)) ((8 0) (1 2)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 60)
  (parent 52)
  (unrealized (8 0))
  (comment "empty cohort"))

(comment "Strand bound exceeded--aborting run")

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (9 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (7 0))
    ((9 0) (8 0)))
  (leadsto ((6 0) (5 2)) ((7 0) (5 3)) ((8 0) (7 0)) ((9 0) (8 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("decrypt" "wrap")
    ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-wrap 1)
    (cat k-0 "wrap") (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 cur) (cat k-0 "wrap"))))
  (label 22)
  (parent 12)
  (unrealized (1 2) (3 0) (4 0) (9 0))
  (comment "aborted"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (9 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (3 0)) ((8 0) (7 0))
    ((9 0) (8 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (5 3)) ((6 0) (5 2)) ((7 0) (3 0))
    ((8 0) (7 0)) ((9 0) (8 0)))
  (neq (cur "wrap") ("wrap" "decrypt") ("decrypt" "wrap")
    ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-wrap 1)
    (cat k-0 "wrap") (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 cur) (cat k-0 "wrap"))))
  (label 44)
  (parent 31)
  (unrealized (1 2) (9 0))
  (comment "aborted"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (9 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (8 0)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (5 3)) ((8 0) (7 0))
    ((9 0) (3 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (8 0)) ((6 0) (5 2)) ((7 0) (5 3))
    ((8 0) (7 0)) ((9 0) (3 0)))
  (neq (cur "wrap") ("init" "wrap") ("wrap" "decrypt")
    ("decrypt" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-wrap 1)
    (cat k-0 "wrap") (3 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 cur) (cat k-0 "wrap"))))
  (label 47)
  (parent 34)
  (unrealized (1 2) (9 0))
  (comment "aborted"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (9 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3)) ((5 3) (3 0))
    ((5 4) (1 0)) ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (1 2))
    ((8 0) (7 0)) ((9 0) (8 0)))
  (leadsto ((2 0) (4 0)) ((4 0) (3 0)) ((4 0) (5 3)) ((6 0) (5 2))
    ((7 0) (1 2)) ((8 0) (7 0)) ((9 0) (8 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("wrap" "decrypt")
    ("init" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k-0 "decrypt") (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 cur) (cat k-0 "decrypt"))))
  (label 54)
  (parent 42)
  (unrealized (9 0))
  (comment "aborted"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-decrypt 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (9 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (5 3)) ((4 0) (8 0)) ((5 3) (8 0))
    ((5 4) (1 0)) ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (3 0))
    ((8 0) (7 0)) ((9 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((4 0) (5 3)) ((4 0) (8 0)) ((6 0) (5 2))
    ((7 0) (3 0)) ((8 0) (7 0)) ((9 0) (1 2)))
  (neq (cur "decrypt") ("init" "wrap") ("wrap" "decrypt")
    ("decrypt" "wrap"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k-0 "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 cur) (cat k-0 "decrypt"))))
  (label 55)
  (parent 43)
  (unrealized (9 0))
  (comment "aborted"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k k-0 skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k-0))
  (defstrand make 2 (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-wrap 1 (cur "init") (k k-0))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k-0))
  (defstrand make 2 (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k-0))
  (defstrand set-decrypt 1 (cur "wrap") (k k-0))
  (defstrand set-decrypt 1 (cur cur) (k k-0))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (9 0)) ((2 1) (5 1))
    ((3 0) (1 2)) ((4 0) (8 0)) ((5 3) (3 0)) ((5 4) (1 0))
    ((6 0) (5 2)) ((6 1) (5 0)) ((7 0) (3 0)) ((7 0) (5 3))
    ((8 0) (7 0)) ((9 0) (1 2)))
  (leadsto ((2 0) (4 0)) ((4 0) (8 0)) ((6 0) (5 2)) ((7 0) (3 0))
    ((7 0) (5 3)) ((8 0) (7 0)) ((9 0) (1 2)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k-0 "decrypt") (1 2))
  (traces ((recv k) (send k))
    ((recv (enc k k-0)) (recv (hash k-0)) (obsv (cat k-0 "decrypt"))
      (send k)) ((init (cat k-0 "init")) (send (hash k-0)))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 "init") (cat k-0 "wrap")))
    ((recv (hash k)) (recv (hash k-0)) (obsv (cat k "init"))
      (obsv (cat k-0 "wrap")) (send (enc k k-0)))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k-0 "decrypt") (cat k-0 "wrap")))
    ((tran (cat k-0 "wrap") (cat k-0 "decrypt")))
    ((tran (cat k-0 cur) (cat k-0 "decrypt"))))
  (label 56)
  (parent 46)
  (unrealized (9 0))
  (comment "aborted"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (9 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (3 0)) ((4 0) (5 3))
    ((5 2) (4 0)) ((5 4) (1 0)) ((6 0) (3 0)) ((7 0) (6 0))
    ((8 0) (7 0)) ((9 0) (8 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (5 3)) ((6 0) (3 0))
    ((7 0) (6 0)) ((8 0) (7 0)) ((9 0) (8 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("wrap" "decrypt")
    ("init" "wrap"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 59)
  (parent 50)
  (unrealized (1 2) (9 0))
  (comment "aborted"))

(defskeleton wrap-decrypt
  (vars (cur mesg) (k skey))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k k))
  (defstrand make 2 (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "init") (k k))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur "wrap") (k k))
  (defstrand set-wrap 1 (cur "decrypt") (k k))
  (defstrand set-decrypt 1 (cur cur) (k k))
  (precedes ((1 3) (0 0)) ((2 0) (4 0)) ((2 0) (5 2)) ((2 0) (9 0))
    ((2 1) (5 0)) ((3 0) (1 2)) ((4 0) (7 0)) ((5 2) (4 0))
    ((5 3) (3 0)) ((5 4) (1 0)) ((6 0) (5 3)) ((7 0) (6 0))
    ((8 0) (3 0)) ((9 0) (8 0)))
  (leadsto ((2 0) (4 0)) ((2 0) (5 2)) ((4 0) (7 0)) ((6 0) (5 3))
    ((7 0) (6 0)) ((8 0) (3 0)) ((9 0) (8 0)))
  (neq (cur "decrypt") ("decrypt" "wrap") ("init" "wrap")
    ("wrap" "decrypt"))
  (uniq-gen k)
  (operation state-passing-test (added-strand set-decrypt 1)
    (cat k "decrypt") (8 0))
  (traces ((recv k) (send k))
    ((recv (enc k k)) (recv (hash k)) (obsv (cat k "decrypt")) (send k))
    ((init (cat k "init")) (send (hash k)))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "init") (cat k "wrap")))
    ((recv (hash k)) (recv (hash k)) (obsv (cat k "init"))
      (obsv (cat k "wrap")) (send (enc k k)))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k "wrap") (cat k "decrypt")))
    ((tran (cat k "decrypt") (cat k "wrap")))
    ((tran (cat k cur) (cat k "decrypt"))))
  (label 61)
  (parent 53)
  (unrealized (1 2) (9 0))
  (comment "aborted"))