cpsa-4.4.4: tst/wrap_decrypt_shapes.tst

(comment "CPSA 4.3.1")
(comment "Extracted shapes")

(herald wrap-decrypt (bound 8))

(comment "CPSA 4.3.0")

(comment "All input read from tst/wrap_decrypt.lsp")

(defprotocol wrap-decrypt basic
  (defrole make
    (vars (k skey) (old mesg) (lk locn))
    (trace (load lk old) (stor lk (cat k "init")) (send (hash k)))
    (uniq-gen k))
  (defrole set-wrap
    (vars (k skey) (cur mesg) (lk locn))
    (trace (load lk (cat k cur)) (stor lk (cat k "wrap")))
    (gen-st (cat k cur))
    (facts (neq cur "wrap")))
  (defrole set-decrypt
    (vars (k skey) (cur mesg) (lk locn))
    (trace (load lk (cat k cur)) (stor lk (cat k "decrypt")))
    (gen-st (cat k cur))
    (facts (neq cur "decrypt")))
  (defrole wrap
    (vars (k0 k1 skey) (lk locn) (cur mesg))
    (trace (recv (hash k0)) (recv (hash k1)) (load lk (cat k0 cur))
      (load lk (cat k1 "wrap")) (send (enc k0 k1)))
    (gen-st (cat k0 cur))
    (gen-st (cat k1 "wrap")))
  (defrole decrypt
    (vars (x mesg) (k skey) (lk locn))
    (trace (recv (enc x k)) (recv (hash k)) (load lk (cat k "decrypt"))
      (send x))
    (gen-st (cat k "decrypt")))
  (defrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
        (false))))
  (defrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defrule trRl_make-at-1
    (forall ((z strd)) (implies (p "make" z 2) (trans z 1))))
  (defrule trRl_make-at-0
    (forall ((z strd)) (implies (p "make" z 1) (trans z 0))))
  (defrule fact-set-wrap-neq0
    (forall ((z strd) (cur mesg))
      (implies
        (and (p "set-wrap" z 1) (p "set-wrap" "cur" z cur))
        (fact neq cur "wrap"))))
  (defrule gen-st-set-wrap-0
    (forall ((z strd) (cur mesg) (k skey))
      (implies
        (and (p "set-wrap" z 1) (p "set-wrap" "cur" z cur)
          (p "set-wrap" "k" z k))
        (gen-st (cat k cur)))))
  (defrule trRl_set-wrap-at-1
    (forall ((z strd)) (implies (p "set-wrap" z 2) (trans z 1))))
  (defrule trRl_set-wrap-at-0
    (forall ((z strd)) (implies (p "set-wrap" z 1) (trans z 0))))
  (defrule fact-set-decrypt-neq0
    (forall ((z strd) (cur mesg))
      (implies
        (and (p "set-decrypt" z 1) (p "set-decrypt" "cur" z cur))
        (fact neq cur "decrypt"))))
  (defrule gen-st-set-decrypt-0
    (forall ((z strd) (cur mesg) (k skey))
      (implies
        (and (p "set-decrypt" z 1) (p "set-decrypt" "cur" z cur)
          (p "set-decrypt" "k" z k))
        (gen-st (cat k cur)))))
  (defrule trRl_set-decrypt-at-1
    (forall ((z strd)) (implies (p "set-decrypt" z 2) (trans z 1))))
  (defrule trRl_set-decrypt-at-0
    (forall ((z strd)) (implies (p "set-decrypt" z 1) (trans z 0))))
  (defrule gen-st-wrap-1
    (forall ((z strd) (cur mesg) (k0 skey))
      (implies
        (and (p "wrap" z 3) (p "wrap" "cur" z cur) (p "wrap" "k0" z k0))
        (gen-st (cat k0 cur)))))
  (defrule gen-st-wrap-0
    (forall ((z strd) (k1 skey))
      (implies
        (and (p "wrap" z 2) (p "wrap" "k1" z k1))
        (gen-st (cat k1 "wrap")))))
  (defrule gen-st-decrypt-0
    (forall ((z strd) (k skey))
      (implies
        (and (p "decrypt" z 1) (p "decrypt" "k" z k))
        (gen-st (cat k "decrypt")))))
  (defrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))

(defskeleton wrap-decrypt
  (vars (old old-0 mesg)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval) (k kp skey)
    (lk lk-0 lk-1 lk-2 lk-3 lk-4 locn))
  (deflistener k)
  (defstrand decrypt 4 (x k) (k kp) (lk lk))
  (defstrand make 2 (old old) (k kp) (lk lk-0))
  (defstrand set-decrypt 1 (cur "wrap") (k kp) (lk lk-1))
  (defstrand set-wrap 1 (cur "init") (k kp) (lk lk-2))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 kp) (lk lk-3))
  (defstrand make 2 (old old-0) (k k) (lk lk-4))
  (traces ((recv k) (send k))
    ((recv (enc k kp)) (recv (hash kp)) (load lk (cat pt kp "decrypt"))
      (send k))
    ((load lk-0 (cat pt-0 old)) (stor lk-0 (cat pt-1 kp "init")))
    ((load lk-1 (cat pt-2 kp "wrap")))
    ((load lk-2 (cat pt-3 kp "init")))
    ((recv (hash k)) (recv (hash kp)) (load lk-3 (cat pt-4 k "init"))
      (load lk-3 (cat pt-5 kp "wrap")) (send (enc k kp)))
    ((load lk-4 (cat pt-6 old-0)) (stor lk-4 (cat pt-7 k "init"))))
  (label 0)
  (realized)
  (origs (pt-7 (6 1)) (pt-1 (2 1)))
  (comment "Not closed under rules"))

(comment "Nothing left to do")

(defprotocol wrap-decrypt basic
  (defrole make
    (vars (k skey) (old mesg) (lk locn))
    (trace (load lk old) (stor lk (cat k "init")) (send (hash k)))
    (uniq-gen k))
  (defrole set-wrap
    (vars (k skey) (cur mesg) (lk locn))
    (trace (load lk (cat k cur)) (stor lk (cat k "wrap")))
    (gen-st (cat k cur))
    (facts (neq cur "wrap")))
  (defrole set-decrypt
    (vars (k skey) (cur mesg) (lk locn))
    (trace (load lk (cat k cur)) (stor lk (cat k "decrypt")))
    (gen-st (cat k cur))
    (facts (neq cur "decrypt")))
  (defrole wrap
    (vars (k0 k1 skey) (lk locn) (cur mesg))
    (trace (recv (hash k0)) (recv (hash k1)) (load lk (cat k0 cur))
      (load lk (cat k1 "wrap")) (send (enc k0 k1)))
    (gen-st (cat k0 cur))
    (gen-st (cat k1 "wrap")))
  (defrole decrypt
    (vars (x mesg) (k skey) (lk locn))
    (trace (recv (enc x k)) (recv (hash k)) (load lk (cat k "decrypt"))
      (send x))
    (gen-st (cat k "decrypt")))
  (defrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
        (false))))
  (defrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defrule trRl_make-at-1
    (forall ((z strd)) (implies (p "make" z 2) (trans z 1))))
  (defrule trRl_make-at-0
    (forall ((z strd)) (implies (p "make" z 1) (trans z 0))))
  (defrule fact-set-wrap-neq0
    (forall ((z strd) (cur mesg))
      (implies
        (and (p "set-wrap" z 1) (p "set-wrap" "cur" z cur))
        (fact neq cur "wrap"))))
  (defrule gen-st-set-wrap-0
    (forall ((z strd) (cur mesg) (k skey))
      (implies
        (and (p "set-wrap" z 1) (p "set-wrap" "cur" z cur)
          (p "set-wrap" "k" z k))
        (gen-st (cat k cur)))))
  (defrule trRl_set-wrap-at-1
    (forall ((z strd)) (implies (p "set-wrap" z 2) (trans z 1))))
  (defrule trRl_set-wrap-at-0
    (forall ((z strd)) (implies (p "set-wrap" z 1) (trans z 0))))
  (defrule fact-set-decrypt-neq0
    (forall ((z strd) (cur mesg))
      (implies
        (and (p "set-decrypt" z 1) (p "set-decrypt" "cur" z cur))
        (fact neq cur "decrypt"))))
  (defrule gen-st-set-decrypt-0
    (forall ((z strd) (cur mesg) (k skey))
      (implies
        (and (p "set-decrypt" z 1) (p "set-decrypt" "cur" z cur)
          (p "set-decrypt" "k" z k))
        (gen-st (cat k cur)))))
  (defrule trRl_set-decrypt-at-1
    (forall ((z strd)) (implies (p "set-decrypt" z 2) (trans z 1))))
  (defrule trRl_set-decrypt-at-0
    (forall ((z strd)) (implies (p "set-decrypt" z 1) (trans z 0))))
  (defrule gen-st-wrap-1
    (forall ((z strd) (cur mesg) (k0 skey))
      (implies
        (and (p "wrap" z 3) (p "wrap" "cur" z cur) (p "wrap" "k0" z k0))
        (gen-st (cat k0 cur)))))
  (defrule gen-st-wrap-0
    (forall ((z strd) (k1 skey))
      (implies
        (and (p "wrap" z 2) (p "wrap" "k1" z k1))
        (gen-st (cat k1 "wrap")))))
  (defrule gen-st-decrypt-0
    (forall ((z strd) (k skey))
      (implies
        (and (p "decrypt" z 1) (p "decrypt" "k" z k))
        (gen-st (cat k "decrypt")))))
  (defrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))

(defskeleton wrap-decrypt
  (vars (k skey))
  (deflistener k)
  (pen-non-orig k)
  (traces ((recv k) (send k)))
  (label 2)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wrap-decrypt
  (vars (old old-0 mesg) (pt pt-0 pt-1 pt-2 pt-3 pval) (k k1 skey)
    (lk locn))
  (deflistener k)
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k1) (lk lk))
  (defstrand make 3 (old old) (k k) (lk lk))
  (defstrand set-wrap 2 (cur "init") (k k1) (lk lk))
  (defstrand make 2 (old old-0) (k k1) (lk lk))
  (precedes ((1 4) (0 0)) ((2 1) (4 0)) ((2 2) (1 0)) ((3 1) (1 3))
    ((4 1) (3 0)))
  (pen-non-orig k)
  (genStV (cat k "init") (cat k1 "init") (cat k1 "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (rule invShearsRule trRl_make-at-0 trRl_make-at-1)
  (operation channel-test (added-strand make 2)
    (ch-msg lk (cat pt-2 k1 "init")) (3 0))
  (traces ((recv k) (send k))
    ((recv (hash k)) (recv (hash k1)) (load lk (cat pt-1 k "init"))
      (load lk (cat pt k1 "wrap")) (send (enc k k1)))
    ((load lk (cat pt-0 old)) (stor lk (cat pt-1 k "init"))
      (send (hash k)))
    ((load lk (cat pt-2 k1 "init")) (stor lk (cat pt k1 "wrap")))
    ((load lk (cat pt-3 old-0)) (stor lk (cat pt-2 k1 "init"))))
  (label 96)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-2 (4 1)) (pt (3 1)) (pt-1 (2 1))))

(defskeleton wrap-decrypt
  (vars (old old-0 old-1 mesg) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
    (k k1 skey) (lk lk-0 locn))
  (deflistener k)
  (defstrand make 2 (old old) (k k) (lk lk))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k1) (lk lk))
  (defstrand make 3 (old old-0) (k k) (lk lk-0))
  (defstrand set-wrap 2 (cur "init") (k k1) (lk lk))
  (defstrand make 2 (old old-1) (k k1) (lk lk))
  (precedes ((1 1) (2 2)) ((1 1) (5 0)) ((2 4) (0 0)) ((3 2) (2 0))
    ((4 1) (2 3)) ((5 1) (4 0)))
  (pen-non-orig k)
  (genStV (cat k "init") (cat k1 "init") (cat k1 "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (rule invShearsRule trRl_make-at-0 trRl_make-at-1)
  (operation channel-test (added-strand make 2)
    (ch-msg lk (cat pt-4 k1 "init")) (4 0))
  (traces ((recv k) (send k))
    ((load lk (cat pt old)) (stor lk (cat pt-0 k "init")))
    ((recv (hash k)) (recv (hash k1)) (load lk (cat pt-0 k "init"))
      (load lk (cat pt-1 k1 "wrap")) (send (enc k k1)))
    ((load lk-0 (cat pt-2 old-0)) (stor lk-0 (cat pt-3 k "init"))
      (send (hash k)))
    ((load lk (cat pt-4 k1 "init")) (stor lk (cat pt-1 k1 "wrap")))
    ((load lk (cat pt-5 old-1)) (stor lk (cat pt-4 k1 "init"))))
  (label 97)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-4 (5 1)) (pt-1 (4 1)) (pt-3 (3 1)) (pt-0 (1 1))))

(defskeleton wrap-decrypt
  (vars (old old-0 mesg) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (k k1 skey)
    (lk locn))
  (deflistener k)
  (defstrand set-wrap 2 (cur "init") (k k) (lk lk))
  (defstrand wrap 5 (cur "wrap") (k0 k) (k1 k1) (lk lk))
  (defstrand make 3 (old old) (k k) (lk lk))
  (defstrand set-wrap 2 (cur "init") (k k1) (lk lk))
  (defstrand make 2 (old old-0) (k k1) (lk lk))
  (precedes ((1 1) (2 2)) ((1 1) (5 0)) ((2 4) (0 0)) ((3 1) (1 0))
    ((3 2) (2 0)) ((4 1) (2 3)) ((5 1) (4 0)))
  (pen-non-orig k)
  (genStV (cat k "init") (cat k "wrap") (cat k1 "init") (cat k1 "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (rule invShearsRule trRl_make-at-0 trRl_make-at-1)
  (operation channel-test (added-strand make 2)
    (ch-msg lk (cat pt-3 k1 "init")) (4 0))
  (traces ((recv k) (send k))
    ((load lk (cat pt-2 k "init")) (stor lk (cat pt k "wrap")))
    ((recv (hash k)) (recv (hash k1)) (load lk (cat pt k "wrap"))
      (load lk (cat pt-0 k1 "wrap")) (send (enc k k1)))
    ((load lk (cat pt-1 old)) (stor lk (cat pt-2 k "init"))
      (send (hash k)))
    ((load lk (cat pt-3 k1 "init")) (stor lk (cat pt-0 k1 "wrap")))
    ((load lk (cat pt-4 old-0)) (stor lk (cat pt-3 k1 "init"))))
  (label 152)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-3 (5 1)) (pt-0 (4 1)) (pt-2 (3 1)) (pt (1 1))))

(defskeleton wrap-decrypt
  (vars (old old-0 old-1 mesg)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval) (k k1 skey)
    (lk lk-0 locn))
  (deflistener k)
  (defstrand make 2 (old old) (k k) (lk lk))
  (defstrand set-wrap 2 (cur "init") (k k) (lk lk))
  (defstrand wrap 5 (cur "wrap") (k0 k) (k1 k1) (lk lk))
  (defstrand make 3 (old old-0) (k k) (lk lk-0))
  (defstrand set-wrap 2 (cur "init") (k k1) (lk lk))
  (defstrand make 2 (old old-1) (k k1) (lk lk))
  (precedes ((1 1) (2 0)) ((2 1) (3 2)) ((2 1) (6 0)) ((3 4) (0 0))
    ((4 2) (3 0)) ((5 1) (3 3)) ((6 1) (5 0)))
  (pen-non-orig k)
  (genStV (cat k "init") (cat k "wrap") (cat k1 "init") (cat k1 "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (rule invShearsRule trRl_make-at-0 trRl_make-at-1)
  (operation channel-test (added-strand make 2)
    (ch-msg lk (cat pt-5 k1 "init")) (5 0))
  (traces ((recv k) (send k))
    ((load lk (cat pt old)) (stor lk (cat pt-0 k "init")))
    ((load lk (cat pt-0 k "init")) (stor lk (cat pt-1 k "wrap")))
    ((recv (hash k)) (recv (hash k1)) (load lk (cat pt-1 k "wrap"))
      (load lk (cat pt-2 k1 "wrap")) (send (enc k k1)))
    ((load lk-0 (cat pt-3 old-0)) (stor lk-0 (cat pt-4 k "init"))
      (send (hash k)))
    ((load lk (cat pt-5 k1 "init")) (stor lk (cat pt-2 k1 "wrap")))
    ((load lk (cat pt-6 old-1)) (stor lk (cat pt-5 k1 "init"))))
  (label 160)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-5 (6 1)) (pt-2 (5 1)) (pt-4 (4 1)) (pt-1 (2 1))
    (pt-0 (1 1))))

(defskeleton wrap-decrypt
  (vars (old old-0 mesg) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (k k1 skey)
    (lk locn))
  (deflistener k)
  (defstrand set-decrypt 2 (cur "init") (k k) (lk lk))
  (defstrand wrap 5 (cur "decrypt") (k0 k) (k1 k1) (lk lk))
  (defstrand make 3 (old old) (k k) (lk lk))
  (defstrand set-wrap 2 (cur "init") (k k1) (lk lk))
  (defstrand make 2 (old old-0) (k k1) (lk lk))
  (precedes ((1 1) (2 2)) ((1 1) (5 0)) ((2 4) (0 0)) ((3 1) (1 0))
    ((3 2) (2 0)) ((4 1) (2 3)) ((5 1) (4 0)))
  (pen-non-orig k)
  (genStV (cat k "decrypt") (cat k "init") (cat k1 "init")
    (cat k1 "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (rule invShearsRule trRl_make-at-0 trRl_make-at-1)
  (operation channel-test (added-strand make 2)
    (ch-msg lk (cat pt-3 k1 "init")) (4 0))
  (traces ((recv k) (send k))
    ((load lk (cat pt-2 k "init")) (stor lk (cat pt k "decrypt")))
    ((recv (hash k)) (recv (hash k1)) (load lk (cat pt k "decrypt"))
      (load lk (cat pt-0 k1 "wrap")) (send (enc k k1)))
    ((load lk (cat pt-1 old)) (stor lk (cat pt-2 k "init"))
      (send (hash k)))
    ((load lk (cat pt-3 k1 "init")) (stor lk (cat pt-0 k1 "wrap")))
    ((load lk (cat pt-4 old-0)) (stor lk (cat pt-3 k1 "init"))))
  (label 199)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-3 (5 1)) (pt-0 (4 1)) (pt-2 (3 1)) (pt (1 1))))

(defskeleton wrap-decrypt
  (vars (old old-0 old-1 mesg)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval) (k k1 skey)
    (lk lk-0 locn))
  (deflistener k)
  (defstrand make 2 (old old) (k k) (lk lk))
  (defstrand set-decrypt 2 (cur "init") (k k) (lk lk))
  (defstrand wrap 5 (cur "decrypt") (k0 k) (k1 k1) (lk lk))
  (defstrand make 3 (old old-0) (k k) (lk lk-0))
  (defstrand set-wrap 2 (cur "init") (k k1) (lk lk))
  (defstrand make 2 (old old-1) (k k1) (lk lk))
  (precedes ((1 1) (2 0)) ((2 1) (3 2)) ((2 1) (6 0)) ((3 4) (0 0))
    ((4 2) (3 0)) ((5 1) (3 3)) ((6 1) (5 0)))
  (pen-non-orig k)
  (genStV (cat k "decrypt") (cat k "init") (cat k1 "init")
    (cat k1 "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (rule invShearsRule trRl_make-at-0 trRl_make-at-1)
  (operation channel-test (added-strand make 2)
    (ch-msg lk (cat pt-5 k1 "init")) (5 0))
  (traces ((recv k) (send k))
    ((load lk (cat pt old)) (stor lk (cat pt-0 k "init")))
    ((load lk (cat pt-0 k "init")) (stor lk (cat pt-1 k "decrypt")))
    ((recv (hash k)) (recv (hash k1)) (load lk (cat pt-1 k "decrypt"))
      (load lk (cat pt-2 k1 "wrap")) (send (enc k k1)))
    ((load lk-0 (cat pt-3 old-0)) (stor lk-0 (cat pt-4 k "init"))
      (send (hash k)))
    ((load lk (cat pt-5 k1 "init")) (stor lk (cat pt-2 k1 "wrap")))
    ((load lk (cat pt-6 old-1)) (stor lk (cat pt-5 k1 "init"))))
  (label 200)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-5 (6 1)) (pt-2 (5 1)) (pt-4 (4 1)) (pt-1 (2 1))
    (pt-0 (1 1))))

(defskeleton wrap-decrypt
  (vars (old old-0 mesg) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (k skey)
    (lk lk-0 locn))
  (deflistener k)
  (defstrand make 2 (old old) (k k) (lk lk))
  (defstrand set-wrap 2 (cur "init") (k k) (lk lk))
  (defstrand wrap 5 (cur "wrap") (k0 k) (k1 k) (lk lk))
  (defstrand make 3 (old old-0) (k k) (lk lk-0))
  (defstrand set-decrypt 2 (cur "init") (k k) (lk lk-0))
  (defstrand decrypt 4 (x k) (k k) (lk lk-0))
  (precedes ((1 1) (2 0)) ((2 1) (3 2)) ((3 4) (6 0)) ((4 1) (5 0))
    ((4 2) (3 0)) ((5 1) (6 2)) ((6 3) (0 0)))
  (pen-non-orig k)
  (genStV (cat k "decrypt") (cat k "init") (cat k "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (operation encryption-test (displaced 7 3 wrap 5) (enc k k) (6 0))
  (traces ((recv k) (send k))
    ((load lk (cat pt old)) (stor lk (cat pt-0 k "init")))
    ((load lk (cat pt-0 k "init")) (stor lk (cat pt-1 k "wrap")))
    ((recv (hash k)) (recv (hash k)) (load lk (cat pt-1 k "wrap"))
      (load lk (cat pt-1 k "wrap")) (send (enc k k)))
    ((load lk-0 (cat pt-2 old-0)) (stor lk-0 (cat pt-3 k "init"))
      (send (hash k)))
    ((load lk-0 (cat pt-3 k "init")) (stor lk-0 (cat pt-4 k "decrypt")))
    ((recv (enc k k)) (recv (hash k)) (load lk-0 (cat pt-4 k "decrypt"))
      (send k)))
  (label 1039)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-4 (5 1)) (pt-1 (2 1)) (pt-3 (4 1)) (pt-0 (1 1))))

(defskeleton wrap-decrypt
  (vars (old old-0 mesg) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (k skey)
    (lk lk-0 locn))
  (deflistener k)
  (defstrand make 2 (old old) (k k) (lk lk))
  (defstrand set-wrap 2 (cur "init") (k k) (lk lk))
  (defstrand wrap 5 (cur "init") (k0 k) (k1 k) (lk lk))
  (defstrand make 3 (old old-0) (k k) (lk lk-0))
  (defstrand set-decrypt 2 (cur "init") (k k) (lk lk-0))
  (defstrand decrypt 4 (x k) (k k) (lk lk-0))
  (precedes ((1 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 3)) ((3 4) (6 0))
    ((4 1) (5 0)) ((4 2) (3 0)) ((5 1) (6 2)) ((6 3) (0 0)))
  (pen-non-orig k)
  (genStV (cat k "decrypt") (cat k "init") (cat k "wrap"))
  (facts (neq "init" "decrypt") (neq "init" "wrap"))
  (operation encryption-test (displaced 7 3 wrap 5) (enc k k) (6 0))
  (traces ((recv k) (send k))
    ((load lk (cat pt old)) (stor lk (cat pt-0 k "init")))
    ((load lk (cat pt-0 k "init")) (stor lk (cat pt-1 k "wrap")))
    ((recv (hash k)) (recv (hash k)) (load lk (cat pt-0 k "init"))
      (load lk (cat pt-1 k "wrap")) (send (enc k k)))
    ((load lk-0 (cat pt-2 old-0)) (stor lk-0 (cat pt-3 k "init"))
      (send (hash k)))
    ((load lk-0 (cat pt-3 k "init")) (stor lk-0 (cat pt-4 k "decrypt")))
    ((recv (enc k k)) (recv (hash k)) (load lk-0 (cat pt-4 k "decrypt"))
      (send k)))
  (label 1143)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((k k))))
  (origs (pt-4 (5 1)) (pt-1 (2 1)) (pt-3 (4 1)) (pt-0 (1 1))))

(comment "Step limit exceeded--aborting run")