(herald "Wrap-Decrypt example" (bound 24) (limit 2000) (goals-sat))

(comment "CPSA 3.6.8")
(comment "All input read from tst/wd-goalssat.scm")
(comment "Strand count bounded at 24")
(comment "Stop when goals satisfied")

(defprotocol wrap-decrypt basic
  (defrole create-key
    (vars (k skey))
    (trace (recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    (uniq-gen k))
  (defrole set-wrap
    (vars (k skey) (type mesg))
    (trace (recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k)) (send "SET-WRAP-DONE")))
  (defrole set-decrypt
    (vars (k skey) (type mesg))
    (trace (recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat type k) (cat "decrypt" k)) (send "SET-DECRYPT-DONE")))
  (defrole do-decrypt
    (vars (k skey) (m mesg))
    (trace (recv (cat "DECRYPT" (hash k) (enc m k)))
      (obsv (cat "decrypt" k)) (send m)))
  (defrole do-wrap
    (vars (wk ck skey) (cktype mesg))
    (trace (recv (cat "WRAP" (hash wk) (hash ck)))
      (obsv (cat "wrap" wk)) (obsv (cat cktype ck)) (send (enc ck wk))))
  (defrule no-key-cycle
    (forall ((z strd) (k skey))
      (implies
        (and (p "do-wrap" z 4) (p "do-wrap" "ck" z k)
          (p "do-wrap" "wk" z k))
        (fact falseFact))))
  (defrule no-set-wrap-noops
    (forall ((z strd))
      (implies
        (and (p "set-wrap" z 2) (p "set-wrap" "type" z "wrap"))
        (fact falseFact))))
  (defrule no-set-decrypt-noops
    (forall ((z strd))
      (implies
        (and (p "set-decrypt" z 2) (p "set-decrypt" "type" z "decrypt"))
        (fact falseFact))))
  (defrule secure-mode
    (forall ((z strd))
      (implies
        (and (fact secureMode) (p "set-decrypt" z 1)
          (p "set-decrypt" "type" z "wrap"))
        (fact falseFact))))
  (defrule conclusion-of-simple
    (forall ((z0 z1 strd) (k skey))
      (implies
        (and (p "create-key" z0 3) (p "create-key" "k" z0 k) (p "" z1 1)
          (p "" "x" z1 k))
        (exists ((z2 z3 strd) (k2 skey))
          (and (p "do-decrypt" z2 1) (p "do-wrap" z3 4)
            (p "do-decrypt" "k" z2 k2) (p "do-wrap" "wk" z3 k2)
            (prec z3 3 z2 0) (prec z2 0 z1 0)))))))

(defskeleton wrap-decrypt
  (vars (cktype m mesg) (k ck skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m m) (k k))
  (precedes ((0 3) (1 0)))
  (facts (secureMode))
  (goals
    (forall ((z0 z1 strd) (k skey))
      (implies
        (and (fact secureMode) (p "do-decrypt" z0 3)
          (p "do-decrypt" "k" z0 k) (p "do-wrap" z1 4)
          (p "do-wrap" "wk" z1 k) (prec z1 3 z0 0))
        (or (fact falseFact)
          (exists ((z2 z3 z4 z5 strd) (k0 k1 skey))
            (and (p "do-decrypt" z2 3) (p "do-decrypt" "k" z2 k0)
              (p "do-wrap" z3 4) (p "do-wrap" "wk" z3 k0)
              (prec z2 3 z3 0) (p "do-decrypt" z4 3)
              (p "do-decrypt" "k" z4 k1) (p "do-wrap" z5 4)
              (p "do-wrap" "wk" z5 k1) (prec z4 3 z5 0)
              (prec z2 3 z4 0)))))))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc m k))) (obsv (cat "decrypt" k))
      (send m)))
  (label 0)
  (unrealized (0 1) (0 2) (1 1))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype m type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m m) (k k))
  (defstrand set-decrypt 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)))
  (leadsto ((2 1) (1 1)))
  (facts (secureMode))
  (operation state-passing-test (added-strand set-decrypt 2)
    (cat "decrypt" k) (1 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc m k))) (obsv (cat "decrypt" k))
      (send m))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat type k) (cat "decrypt" k))))
  (label 1)
  (parent 0)
  (unrealized (0 1) (0 2) (2 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype m mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m m) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 2) (2 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)))
  (uniq-gen k)
  (facts (secureMode))
  (operation state-passing-test (added-strand create-key 3)
    (cat "init" k) (2 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc m k))) (obsv (cat "decrypt" k))
      (send m))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k))))
  (label 2)
  (parent 1)
  (unrealized (0 1) (0 2) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype m type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m m) (k k))
  (defstrand set-decrypt 2 (type "wrap") (k k))
  (defstrand set-wrap 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (2 1)))
  (leadsto ((2 1) (1 1)) ((3 1) (2 1)))
  (facts (falseFact) (secureMode))
  (rule secure-mode)
  (operation state-passing-test (added-strand set-wrap 2) (cat "wrap" k)
    (2 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc m k))) (obsv (cat "decrypt" k))
      (send m))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "wrap" k) (cat "decrypt" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k))))
  (label 3)
  (parent 1)
  (unrealized (0 1) (0 2) (3 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m m))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt
  (vars (cktype m type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m m) (k k))
  (defstrand set-decrypt 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (2 1)))
  (leadsto ((2 1) (1 1)) ((3 1) (2 1)))
  (facts (falseFact) (secureMode))
  (rule no-set-decrypt-noops)
  (operation state-passing-test (added-strand set-decrypt 2)
    (cat "decrypt" k) (2 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc m k))) (obsv (cat "decrypt" k))
      (send m))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "decrypt" k) (cat "decrypt" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat type k) (cat "decrypt" k))))
  (label 4)
  (parent 1)
  (unrealized (0 1) (0 2) (3 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m m))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt
  (vars (cktype mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 2) (2 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)))
  (uniq-gen k)
  (facts (secureMode))
  (operation encryption-test (displaced 4 0 do-wrap 4) (enc ck-0 k)
    (1 0))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck k))) (obsv (cat "decrypt" k))
      (send ck))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k))))
  (label 5)
  (parent 2)
  (unrealized (0 1) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype cktype-0 mesg) (ck k ck-0 skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck-0) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (cktype cktype-0) (wk k) (ck ck-0))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 2) (2 1)) ((4 3) (1 0)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)))
  (uniq-gen k)
  (facts (secureMode))
  (operation encryption-test (added-strand do-wrap 4) (enc ck-0 k)
    (1 0))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck-0 k)))
      (obsv (cat "decrypt" k)) (send ck-0))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "WRAP" (hash k) (hash ck-0))) (obsv (cat "wrap" k))
      (obsv (cat cktype-0 ck-0)) (send (enc ck-0 k))))
  (label 6)
  (parent 2)
  (unrealized (0 1) (0 2) (4 1) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand set-wrap 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 2) (2 1)) ((4 1) (0 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((4 1) (0 1)))
  (uniq-gen k)
  (facts (secureMode))
  (operation state-passing-test (added-strand set-wrap 2) (cat "wrap" k)
    (0 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck k))) (obsv (cat "decrypt" k))
      (send ck))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k))))
  (label 7)
  (parent 5)
  (unrealized (0 2) (4 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype cktype-0 type mesg) (ck ck-0 k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck-0) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (cktype cktype-0) (wk k) (ck ck-0))
  (defstrand set-wrap 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 2) (2 1)) ((4 3) (1 0))
    ((5 1) (4 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((5 1) (4 1)))
  (uniq-gen k)
  (facts (secureMode))
  (operation state-passing-test (added-strand set-wrap 2) (cat "wrap" k)
    (4 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck-0 k)))
      (obsv (cat "decrypt" k)) (send ck-0))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "WRAP" (hash k) (hash ck-0))) (obsv (cat "wrap" k))
      (obsv (cat cktype-0 ck-0)) (send (enc ck-0 k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k))))
  (label 8)
  (parent 6)
  (unrealized (0 1) (0 2) (4 2) (5 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand set-wrap 2 (type "wrap") (k k))
  (defstrand set-wrap 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 2) (2 1)) ((4 1) (0 1))
    ((5 1) (4 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((4 1) (0 1)) ((5 1) (4 1)))
  (uniq-gen k)
  (facts (falseFact) (secureMode))
  (rule no-set-wrap-noops)
  (operation state-passing-test (added-strand set-wrap 2) (cat "wrap" k)
    (4 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck k))) (obsv (cat "decrypt" k))
      (send ck))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "wrap" k) (cat "wrap" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k))))
  (label 9)
  (parent 7)
  (unrealized (0 2) (5 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m ck))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt
  (vars (cktype type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand set-wrap 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 2) (2 1)) ((4 1) (0 1))
    ((5 1) (4 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((4 1) (0 1)) ((5 1) (4 1)))
  (uniq-gen k)
  (facts (secureMode))
  (operation state-passing-test (added-strand set-decrypt 2)
    (cat "decrypt" k) (4 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck k))) (obsv (cat "decrypt" k))
      (send ck))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "decrypt" k) (cat "wrap" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat type k) (cat "decrypt" k))))
  (label 10)
  (parent 7)
  (unrealized (0 2) (5 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype cktype-0 type mesg) (ck ck-0 k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck-0) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (cktype cktype-0) (wk k) (ck ck-0))
  (defstrand set-wrap 2 (type "wrap") (k k))
  (defstrand set-wrap 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 1) (6 0)) ((3 2) (2 1))
    ((4 3) (1 0)) ((5 1) (4 1)) ((6 1) (5 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((5 1) (4 1)) ((6 1) (5 1)))
  (uniq-gen k)
  (facts (falseFact) (secureMode))
  (rule no-set-wrap-noops)
  (operation state-passing-test (added-strand set-wrap 2) (cat "wrap" k)
    (5 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck-0 k)))
      (obsv (cat "decrypt" k)) (send ck-0))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "WRAP" (hash k) (hash ck-0))) (obsv (cat "wrap" k))
      (obsv (cat cktype-0 ck-0)) (send (enc ck-0 k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "wrap" k) (cat "wrap" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k))))
  (label 11)
  (parent 8)
  (unrealized (0 1) (0 2) (4 2) (6 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m ck-0))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt
  (vars (cktype cktype-0 type mesg) (ck ck-0 k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck-0) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (cktype cktype-0) (wk k) (ck ck-0))
  (defstrand set-wrap 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 1) (6 0)) ((3 2) (2 1))
    ((4 3) (1 0)) ((5 1) (4 1)) ((6 1) (5 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((5 1) (4 1)) ((6 1) (5 1)))
  (uniq-gen k)
  (facts (secureMode))
  (operation state-passing-test (added-strand set-decrypt 2)
    (cat "decrypt" k) (5 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck-0 k)))
      (obsv (cat "decrypt" k)) (send ck-0))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "WRAP" (hash k) (hash ck-0))) (obsv (cat "wrap" k))
      (obsv (cat cktype-0 ck-0)) (send (enc ck-0 k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "decrypt" k) (cat "wrap" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat type k) (cat "decrypt" k))))
  (label 12)
  (parent 8)
  (unrealized (0 1) (0 2) (4 2) (6 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt
  (vars (cktype type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand set-wrap 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type "wrap") (k k))
  (defstrand set-wrap 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 1) (6 0)) ((3 2) (2 1))
    ((4 1) (0 1)) ((5 1) (4 1)) ((6 1) (5 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((4 1) (0 1)) ((5 1) (4 1))
    ((6 1) (5 1)))
  (uniq-gen k)
  (facts (falseFact) (secureMode))
  (rule secure-mode)
  (operation state-passing-test (added-strand set-wrap 2) (cat "wrap" k)
    (5 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck k))) (obsv (cat "decrypt" k))
      (send ck))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "decrypt" k) (cat "wrap" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "wrap" k) (cat "decrypt" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k))))
  (label 13)
  (parent 10)
  (unrealized (0 2) (6 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m ck))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt
  (vars (cktype type mesg) (ck k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand set-wrap 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 1) (6 0)) ((3 2) (2 1))
    ((4 1) (0 1)) ((5 1) (4 1)) ((6 1) (5 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((4 1) (0 1)) ((5 1) (4 1))
    ((6 1) (5 1)))
  (uniq-gen k)
  (facts (falseFact) (secureMode))
  (rule no-set-decrypt-noops)
  (operation state-passing-test (added-strand set-decrypt 2)
    (cat "decrypt" k) (5 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck k))) (obsv (cat "decrypt" k))
      (send ck))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "decrypt" k) (cat "wrap" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "decrypt" k) (cat "decrypt" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat type k) (cat "decrypt" k))))
  (label 14)
  (parent 10)
  (unrealized (0 2) (6 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m ck))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt
  (vars (cktype cktype-0 type mesg) (ck ck-0 k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck-0) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (cktype cktype-0) (wk k) (ck ck-0))
  (defstrand set-wrap 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type "wrap") (k k))
  (defstrand set-wrap 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 1) (6 0)) ((3 1) (7 0))
    ((3 2) (2 1)) ((4 3) (1 0)) ((5 1) (4 1)) ((6 1) (5 1))
    ((7 1) (6 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((5 1) (4 1)) ((6 1) (5 1))
    ((7 1) (6 1)))
  (uniq-gen k)
  (facts (falseFact) (secureMode))
  (rule secure-mode)
  (operation state-passing-test (added-strand set-wrap 2) (cat "wrap" k)
    (6 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck-0 k)))
      (obsv (cat "decrypt" k)) (send ck-0))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "WRAP" (hash k) (hash ck-0))) (obsv (cat "wrap" k))
      (obsv (cat cktype-0 ck-0)) (send (enc ck-0 k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "decrypt" k) (cat "wrap" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "wrap" k) (cat "decrypt" k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat type k) (cat "wrap" k))))
  (label 15)
  (parent 12)
  (unrealized (0 1) (0 2) (4 2) (7 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m ck-0))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt
  (vars (cktype cktype-0 type mesg) (ck ck-0 k skey))
  (defstrand do-wrap 4 (cktype cktype) (wk k) (ck ck))
  (defstrand do-decrypt 3 (m ck-0) (k k))
  (defstrand set-decrypt 2 (type "init") (k k))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (cktype cktype-0) (wk k) (ck ck-0))
  (defstrand set-wrap 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type "decrypt") (k k))
  (defstrand set-decrypt 2 (type type) (k k))
  (precedes ((0 3) (1 0)) ((2 1) (1 1)) ((3 1) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 1) (5 0)) ((3 1) (6 0)) ((3 1) (7 0))
    ((3 2) (2 1)) ((4 3) (1 0)) ((5 1) (4 1)) ((6 1) (5 1))
    ((7 1) (6 1)))
  (leadsto ((2 1) (1 1)) ((3 2) (2 1)) ((5 1) (4 1)) ((6 1) (5 1))
    ((7 1) (6 1)))
  (uniq-gen k)
  (facts (falseFact) (secureMode))
  (rule no-set-decrypt-noops)
  (operation state-passing-test (added-strand set-decrypt 2)
    (cat "decrypt" k) (6 1))
  (traces
    ((recv (cat "WRAP" (hash k) (hash ck))) (obsv (cat "wrap" k))
      (obsv (cat cktype ck)) (send (enc ck k)))
    ((recv (cat "DECRYPT" (hash k) (enc ck-0 k)))
      (obsv (cat "decrypt" k)) (send ck-0))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "init" k) (cat "decrypt" k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k)))
      (init (cat "init" k)))
    ((recv (cat "WRAP" (hash k) (hash ck-0))) (obsv (cat "wrap" k))
      (obsv (cat cktype-0 ck-0)) (send (enc ck-0 k)))
    ((recv (cat "SET-WRAP" (hash k)))
      (tran (cat "decrypt" k) (cat "wrap" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat "decrypt" k) (cat "decrypt" k)))
    ((recv (cat "SET-DECRYPT" (hash k)))
      (tran (cat type k) (cat "decrypt" k))))
  (label 16)
  (parent 12)
  (unrealized (0 1) (0 2) (4 2) (7 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k) (ck ck) (cktype cktype) (m ck-0))))
  (origs)
  (comment "satisfies all"))

(comment "Nothing left to do")