(herald "Wrap-Decrypt example, simplified" (bound 24) (limit 500)
  (goals-sat))

(comment "CPSA 3.6.8")
(comment "All input read from tst/wd-gs-simple.scm")
(comment "Step count limited to 500")
(comment "Strand count bounded at 24")
(comment "Stop when goals satisfied")

(defprotocol wrap-decrypt-simple basic
  (defrole create-key
    (vars (k skey))
    (trace (recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    (uniq-gen k))
  (defrole do-decrypt
    (vars (k skey) (m mesg))
    (trace (recv (cat "DECRYPT" (hash k) (enc m k))) (obsv k) (send m)))
  (defrole do-wrap
    (vars (wk ck skey))
    (trace (recv (cat "WRAP" (hash wk) (hash ck))) (obsv wk) (obsv ck)
      (send (enc ck wk)))
    (neq (ck wk))))

(defskeleton wrap-decrypt-simple
  (vars (k skey))
  (deflistener k)
  (defstrand create-key 3 (k k))
  (uniq-gen k)
  (goals
    (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))
        (or
          (exists ((z2 z3 z4 z5 strd) (k2 k3 skey))
            (and (p "create-key" z2 2) (p "create-key" "k" z2 k2)
              (p "create-key" z4 2) (p "create-key" "k" z4 k3)
              (p "" z3 1) (p "" "x" z3 k2) (p "" z5 1) (p "" "x" z5 k3)
              (prec z3 1 z5 0)))
          (exists ((z2 z3 strd) (k2 skey))
            (and (p "do-decrypt" z2 3) (p "do-decrypt" "k" z2 k2)
              (p "do-wrap" z3 4) (p "do-wrap" "wk" z3 k2)
              (prec z3 3 z2 0)))))))
  (traces ((recv k))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k)))
  (label 0)
  (unrealized (0 0))
  (preskeleton)
  (origs)
  (comment "Not a skeleton"))

(defskeleton wrap-decrypt-simple
  (vars (k skey))
  (deflistener k)
  (defstrand create-key 3 (k k))
  (precedes ((1 1) (0 0)))
  (uniq-gen k)
  (goals
    (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))
        (or
          (exists ((z2 z3 z4 z5 strd) (k2 k3 skey))
            (and (p "create-key" z2 2) (p "create-key" "k" z2 k2)
              (p "create-key" z4 2) (p "create-key" "k" z4 k3)
              (p "" z3 1) (p "" "x" z3 k2) (p "" z5 1) (p "" "x" z5 k3)
              (prec z3 1 z5 0)))
          (exists ((z2 z3 strd) (k2 skey))
            (and (p "do-decrypt" z2 3) (p "do-decrypt" "k" z2 k2)
              (p "do-wrap" z3 4) (p "do-wrap" "wk" z3 k2)
              (prec z3 3 z2 0)))))))
  (traces ((recv k))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k)))
  (label 1)
  (parent 0)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k wk skey))
  (deflistener k)
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (wk wk) (ck k))
  (precedes ((1 1) (2 0)) ((2 3) (0 0)))
  (neq (k wk))
  (uniq-gen k)
  (operation nonce-test (added-strand do-wrap 4) k (0 0))
  (traces ((recv k))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "WRAP" (hash wk) (hash k))) (obsv wk) (obsv k)
      (send (enc k wk))))
  (label 2)
  (parent 1)
  (unrealized (2 1) (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k)
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (wk k-0) (ck k))
  (defstrand create-key 3 (k k-0))
  (precedes ((1 1) (2 0)) ((2 3) (0 0)) ((3 1) (2 0)) ((3 2) (2 1)))
  (leadsto ((3 2) (2 1)))
  (neq (k k-0))
  (uniq-gen k k-0)
  (operation state-passing-test (added-strand create-key 3) k-0 (2 1))
  (traces ((recv k))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "WRAP" (hash k-0) (hash k))) (obsv k-0) (obsv k)
      (send (enc k k-0)))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0)))
  (label 3)
  (parent 2)
  (unrealized (0 0) (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (precedes ((1 1) (2 0)) ((1 2) (2 2)) ((2 3) (0 0)) ((3 1) (2 0))
    ((3 2) (2 1)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)))
  (neq (k-0 k))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 4 1 create-key 3) k-0 (2 2))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k)))
  (label 4)
  (parent 3)
  (unrealized (0 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (defstrand do-decrypt 3 (m k-0) (k k))
  (precedes ((1 1) (2 0)) ((1 1) (4 0)) ((1 2) (2 2)) ((2 3) (0 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((3 2) (2 1)) ((4 2) (0 0)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)))
  (neq (k-0 k))
  (uniq-gen k k-0)
  (operation nonce-test (added-strand do-decrypt 3) k-0 (0 0)
    (enc k-0 k))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "DECRYPT" (hash k) (enc k-0 k))) (obsv k) (send k-0)))
  (label 5)
  (parent 4)
  (unrealized (4 0) (4 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 wk skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (wk wk) (ck k-0))
  (precedes ((1 1) (2 0)) ((1 1) (4 0)) ((1 2) (2 2)) ((2 3) (0 0))
    ((3 1) (2 0)) ((3 2) (2 1)) ((4 3) (0 0)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)))
  (neq (k-0 wk) (k-0 k))
  (uniq-gen k k-0)
  (operation nonce-test (added-strand do-wrap 4) k-0 (0 0) (enc k-0 k))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "WRAP" (hash wk) (hash k-0))) (obsv wk) (obsv k-0)
      (send (enc k-0 wk))))
  (label 6)
  (parent 4)
  (unrealized (4 1) (4 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (deflistener k)
  (precedes ((1 1) (2 0)) ((1 2) (2 2)) ((2 3) (0 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((3 2) (2 1)) ((4 1) (0 0)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)))
  (neq (k-0 k))
  (uniq-gen k k-0)
  (operation nonce-test (added-listener k) k-0 (0 0) (enc k-0 k))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv k) (send k)))
  (label 7)
  (parent 4)
  (unrealized (4 0))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k-0))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (defstrand do-decrypt 3 (m k-0) (k k))
  (precedes ((1 1) (2 0)) ((1 2) (2 2)) ((2 3) (4 0)) ((3 1) (2 0))
    ((3 2) (2 1)) ((4 2) (0 0)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)))
  (neq (k-0 k))
  (uniq-gen k k-0)
  (operation encryption-test (displaced 5 2 do-wrap 4) (enc k-0 k)
    (4 0))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "DECRYPT" (hash k) (enc k-0 k))) (obsv k) (send k-0)))
  (label 8)
  (parent 5)
  (unrealized (4 1))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k-0))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (defstrand do-decrypt 3 (m k-0) (k k))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (precedes ((1 1) (2 0)) ((1 1) (5 0)) ((1 2) (2 2)) ((2 3) (0 0))
    ((3 1) (2 0)) ((3 1) (5 0)) ((3 2) (2 1)) ((4 2) (0 0))
    ((5 3) (4 0)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)))
  (neq (k-0 k))
  (uniq-gen k k-0)
  (operation encryption-test (added-strand do-wrap 4) (enc k-0 k) (4 0))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "DECRYPT" (hash k) (enc k-0 k))) (obsv k) (send k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k))))
  (label 9)
  (parent 5)
  (unrealized (4 1) (5 1) (5 2))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k-0))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (defstrand do-decrypt 3 (m k-0) (k k))
  (deflistener k)
  (precedes ((1 1) (2 0)) ((1 1) (4 0)) ((1 2) (2 2)) ((2 3) (0 0))
    ((3 1) (2 0)) ((3 1) (5 0)) ((3 2) (2 1)) ((4 2) (0 0))
    ((5 1) (4 0)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)))
  (neq (k-0 k))
  (uniq-gen k k-0)
  (operation encryption-test (added-listener k) (enc k-0 k) (4 0))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "DECRYPT" (hash k) (enc k-0 k))) (obsv k) (send k-0))
    ((recv k) (send k)))
  (label 10)
  (parent 5)
  (unrealized (4 0) (4 1) (5 0))
  (fringe)
  (satisfies-all)
  (maps ((0 1) ((k k-0))))
  (origs)
  (comment "satisfies all"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (precedes ((1 1) (2 0)) ((1 1) (4 0)) ((1 2) (2 2)) ((2 3) (0 0))
    ((3 1) (2 0)) ((3 1) (4 0)) ((3 2) (2 1)) ((3 2) (4 1))
    ((4 3) (0 0)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)) ((3 2) (4 1)))
  (neq (k-0 k))
  (uniq-gen k k-0)
  (operation state-passing-test (displaced 5 3 create-key 3) k-1 (4 1))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k))))
  (label 11)
  (parent 6)
  (seen 4)
  (unrealized (0 0) (4 2))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 k-1 skey))
  (deflistener k-0)
  (defstrand create-key 3 (k k-0))
  (defstrand do-wrap 4 (wk k) (ck k-0))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (wk k-1) (ck k-0))
  (defstrand create-key 3 (k k-1))
  (precedes ((1 1) (2 0)) ((1 1) (4 0)) ((1 2) (2 2)) ((2 3) (0 0))
    ((3 1) (2 0)) ((3 2) (2 1)) ((4 3) (0 0)) ((5 1) (4 0))
    ((5 2) (4 1)))
  (leadsto ((1 2) (2 2)) ((3 2) (2 1)) ((5 2) (4 1)))
  (neq (k-0 k-1) (k-0 k))
  (uniq-gen k k-0 k-1)
  (operation state-passing-test (added-strand create-key 3) k-1 (4 1))
  (traces ((recv k-0))
    ((recv "CREATE") (send (cat "CREATED" (hash k-0))) (init k-0))
    ((recv (cat "WRAP" (hash k) (hash k-0))) (obsv k) (obsv k-0)
      (send (enc k-0 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "WRAP" (hash k-1) (hash k-0))) (obsv k-1) (obsv k-0)
      (send (enc k-0 k-1)))
    ((recv "CREATE") (send (cat "CREATED" (hash k-1))) (init k-1)))
  (label 12)
  (parent 6)
  (unrealized (0 0) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt-simple
  (vars (k k-0 k-1 skey))
  (deflistener k-1)
  (defstrand create-key 3 (k k-1))
  (defstrand do-wrap 4 (wk k) (ck k-1))
  (defstrand create-key 3 (k k))
  (defstrand do-wrap 4 (wk k-0) (ck k-1))
  (precedes ((1 1) (2 0)) ((1 1) (4 0)) ((1 2) (2 2)) ((1 2) (4 2))
    ((2 3) (0 0)) ((3 1) (2 0)) ((3 2) (2 1)) ((4 3) (0 0)))
  (leadsto ((1 2) (2 2)) ((1 2) (4 2)) ((3 2) (2 1)))
  (neq (k-1 k-0) (k-1 k))
  (uniq-gen k k-1)
  (operation state-passing-test (displaced 6 1 create-key 3) k-1 (4 2))
  (traces ((recv k-1))
    ((recv "CREATE") (send (cat "CREATED" (hash k-1))) (init k-1))
    ((recv (cat "WRAP" (hash k) (hash k-1))) (obsv k) (obsv k-1)
      (send (enc k-1 k)))
    ((recv "CREATE") (send (cat "CREATED" (hash k))) (init k))
    ((recv (cat "WRAP" (hash k-0) (hash k-1))) (obsv k-0) (obsv k-1)
      (send (enc k-1 k-0))))
  (label 13)
  (parent 12)
  (seen 4)
  (unrealized (4 1))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")