(herald open-closed-alt (bound 40))

(comment "CPSA 4.4.0")
(comment "All input read from open-closed.scm")
(comment "Strand count bounded at 40")

(defprotocol open-closed basic
  (defrole dev-up
    (vars (k skey) (d o name) (old old1 mesg) (start-ch chan)
      (lk ls locn))
    (trace (recv start-ch (cat "power-up" d o k)) (load lk old)
      (load ls old1) (stor lk (dev-key-state d o k))
      (stor ls (door-state d (closed o))) (send (enc "up" k)))
    (auth start-ch)
    (facts (same-dev ls lk)))
  (defrole owner-power-dev
    (vars (k skey) (d o name) (start-ch chan))
    (trace (send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    (conf start-ch))
  (defrole owner-delg-key
    (vars (k skey) (n nb text) (d o b name) (to-b from-b chan))
    (trace (recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k)))
      (recv (hash b nb n)))
    (uniq-orig n)
    (conf to-b)
    (auth from-b))
  (defrole passer-recv-key
    (vars (kp ign mesg) (n nb text) (d o b name) (to-b from-b chan)
      (del-key-locn locn))
    (trace (send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n kp)) (send (hash b nb n))
      (load del-key-locn ign)
      (stor del-key-locn (key-rec b d o nb n kp)))
    (uniq-orig nb)
    (auth to-b))
  (defrole passer-open
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b n (enc (open-req b d o nb n) kp)))
      (recv (hash (open-req b d o nb n)))))
  (defrole passer-close
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b n (enc (close-req b d o nb n) kp)))
      (recv (hash (close-req b d o nb n)))))
  (defrole dev-open
    (vars (k skey) (n nb text) (any mesg) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (door-state d any)) (load lk (dev-key-state d o k))
      (stor ls (door-state d (opened b nb n)))
      (send (hash (open-req b d o nb n))))
    (gen-st (dev-key-state d o k))
    (facts (same-dev ls lk)))
  (defrole dev-closed
    (vars (k skey) (n nb text) (any mesg) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (recv (cat b n (enc (close-req b d o nb n) (hash-dk b nb n k))))
      (load ls (door-state d any)) (load lk (dev-key-state d o k))
      (stor ls (door-state d (closed o)))
      (send (hash (close-req b d o nb n))))
    (gen-st (dev-key-state d o k))
    (facts (same-dev ls lk)))
  (defrole dev-pass
    (vars (k skey) (n nb text) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (load ls (door-state d (opened b nb n)))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
    (facts (same-dev ls lk)))
  (defrole passer-pass
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b nb n (enc "may I pass" kp)))
      (recv (enc "you may pass" kp))))
  (defrule power-deliver-once
    (forall ((z1 z2 strd) (k skey))
      (implies
        (and (p "dev-up" z1 (idx 2)) (p "dev-up" z2 (idx 2))
          (p "dev-up" "k" z1 k) (p "dev-up" "k" z2 k))
        (= z1 z2))))
  (defrule same-dev-ls-lk
    (forall ((ls lk lk-0 locn))
      (implies
        (and (fact same-dev ls lk) (fact same-dev ls lk-0))
        (= lk lk-0))))
  (defrule same-dev-lk-ls
    (forall ((lk ls ls-0 locn))
      (implies
        (and (fact same-dev ls lk) (fact same-dev ls-0 lk))
        (= ls ls-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule 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)))))
  (defgenrule 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))))
  (defgenrule 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))))
  (defgenrule 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)))))
  (defgenrule 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)))))
  (defgenrule fact-dev-up-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-up" z (idx 3)) (p "dev-up" "lk" z lk)
          (p "dev-up" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-open-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-open" z (idx 3)) (p "dev-open" "lk" z lk)
          (p "dev-open" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-closed-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-closed" z (idx 3)) (p "dev-closed" "lk" z lk)
          (p "dev-closed" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-pass-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-pass" z (idx 2)) (p "dev-pass" "lk" z lk)
          (p "dev-pass" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule trRl_dev-up-at-4
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-up-at-3
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 1)))))
  (defgenrule trRl_passer-recv-key-at-4
    (forall ((z strd))
      (implies (p "passer-recv-key" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_passer-recv-key-at-3
    (forall ((z strd))
      (implies (p "passer-recv-key" z (idx 5)) (trans z (idx 3)))))
  (defgenrule trRl_dev-open-at-4
    (forall ((z strd))
      (implies (p "dev-open" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-open-at-2
    (forall ((z strd))
      (implies (p "dev-open" z (idx 5)) (trans z (idx 2)))))
  (defgenrule trRl_dev-closed-at-4
    (forall ((z strd))
      (implies (p "dev-closed" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-closed-at-2
    (forall ((z strd))
      (implies (p "dev-closed" z (idx 5)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 5)) (prec z (idx 4) z1 i))))))
  (defgenrule cau-dev-up-2
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 3)) (prec z1 i z (idx 2)))
        (or (= z z1) (prec z1 i z (idx 1))))))
  (defgenrule cau-dev-open-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-open" z (idx 4)) (prec z1 i z (idx 3)))
        (or (= z z1) (prec z1 i z (idx 2))))))
  (defgenrule cau-dev-closed-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-closed" z (idx 4)) (prec z1 i z (idx 3)))
        (or (= z z1) (prec z1 i z (idx 2))))))
  (defgenrule cau-dev-pass-1
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o) (p "dev-open" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-closed-0
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-closed" z (idx 1)) (p "dev-closed" "k" z k)
          (p "dev-closed" "o" z o) (p "dev-closed" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o) (p "dev-pass" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (n nb text) (b d name))
      (implies
        (and (p "dev-pass" z (idx 2)) (p "dev-pass" "n" z n)
          (p "dev-pass" "nb" z nb) (p "dev-pass" "b" z b)
          (p "dev-pass" "d" z d))
        (gen-st (door-state d (opened b nb n))))))
  (lang (closed (tuple 1)) (opened (tuple 3)) (door-state (tuple 2))
    (dev-key-state (tuple 3)) (open-req (tuple 5)) (close-req (tuple 5))
    (key-rec (tuple 6)) (delegate (tuple 6)) (hash-dk hash)))

(defskeleton open-closed
  (vars (k skey) (d o name) (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (deflistener k)
  (uniq-orig k)
  (conf start-ch)
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((recv k) (send k)))
  (label 0)
  (unrealized (0 1) (1 0))
  (preskeleton)
  (origs (k (0 0)))
  (comment "Not a skeleton"))

(defskeleton open-closed
  (vars (k skey) (d o name) (start-ch chan))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (deflistener k)
  (precedes ((0 0) (1 0)))
  (uniq-orig k)
  (conf start-ch)
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((recv k) (send k)))
  (label 1)
  (parent 0)
  (unrealized (0 1) (1 0))
  (origs (k (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 mesg) (k skey) (d o name) (pt pt-0 pt-1 pt-2 pval)
    (start-ch chan) (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (deflistener k)
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (precedes ((0 0) (2 0)) ((2 4) (1 0)))
  (uniq-orig k)
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (rule eff-dev-up-3 fact-dev-up-same-dev0 trRl_dev-up-at-1
    trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation nonce-test (added-strand dev-up 4) k (1 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((recv k) (send k))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt old))
      (load ls (cat pt-0 old1))
      (stor lk (cat pt-1 (dev-key-state d o k)))
      (stor ls (cat pt-2 (door-state d (closed o))))))
  (label 2)
  (parent 1)
  (seen 2)
  (unrealized (0 1) (1 0))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol open-closed basic
  (defrole dev-up
    (vars (k skey) (d o name) (old old1 mesg) (start-ch chan)
      (lk ls locn))
    (trace (recv start-ch (cat "power-up" d o k)) (load lk old)
      (load ls old1) (stor lk (dev-key-state d o k))
      (stor ls (door-state d (closed o))) (send (enc "up" k)))
    (auth start-ch)
    (facts (same-dev ls lk)))
  (defrole owner-power-dev
    (vars (k skey) (d o name) (start-ch chan))
    (trace (send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    (conf start-ch))
  (defrole owner-delg-key
    (vars (k skey) (n nb text) (d o b name) (to-b from-b chan))
    (trace (recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k)))
      (recv (hash b nb n)))
    (uniq-orig n)
    (conf to-b)
    (auth from-b))
  (defrole passer-recv-key
    (vars (kp ign mesg) (n nb text) (d o b name) (to-b from-b chan)
      (del-key-locn locn))
    (trace (send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n kp)) (send (hash b nb n))
      (load del-key-locn ign)
      (stor del-key-locn (key-rec b d o nb n kp)))
    (uniq-orig nb)
    (auth to-b))
  (defrole passer-open
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b n (enc (open-req b d o nb n) kp)))
      (recv (hash (open-req b d o nb n)))))
  (defrole passer-close
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b n (enc (close-req b d o nb n) kp)))
      (recv (hash (close-req b d o nb n)))))
  (defrole dev-open
    (vars (k skey) (n nb text) (any mesg) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (door-state d any)) (load lk (dev-key-state d o k))
      (stor ls (door-state d (opened b nb n)))
      (send (hash (open-req b d o nb n))))
    (gen-st (dev-key-state d o k))
    (facts (same-dev ls lk)))
  (defrole dev-closed
    (vars (k skey) (n nb text) (any mesg) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (recv (cat b n (enc (close-req b d o nb n) (hash-dk b nb n k))))
      (load ls (door-state d any)) (load lk (dev-key-state d o k))
      (stor ls (door-state d (closed o)))
      (send (hash (close-req b d o nb n))))
    (gen-st (dev-key-state d o k))
    (facts (same-dev ls lk)))
  (defrole dev-pass
    (vars (k skey) (n nb text) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (load ls (door-state d (opened b nb n)))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
    (facts (same-dev ls lk)))
  (defrole passer-pass
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b nb n (enc "may I pass" kp)))
      (recv (enc "you may pass" kp))))
  (defrule power-deliver-once
    (forall ((z1 z2 strd) (k skey))
      (implies
        (and (p "dev-up" z1 (idx 2)) (p "dev-up" z2 (idx 2))
          (p "dev-up" "k" z1 k) (p "dev-up" "k" z2 k))
        (= z1 z2))))
  (defrule same-dev-ls-lk
    (forall ((ls lk lk-0 locn))
      (implies
        (and (fact same-dev ls lk) (fact same-dev ls lk-0))
        (= lk lk-0))))
  (defrule same-dev-lk-ls
    (forall ((lk ls ls-0 locn))
      (implies
        (and (fact same-dev ls lk) (fact same-dev ls-0 lk))
        (= ls ls-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule 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)))))
  (defgenrule 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))))
  (defgenrule 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))))
  (defgenrule 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)))))
  (defgenrule 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)))))
  (defgenrule fact-dev-up-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-up" z (idx 3)) (p "dev-up" "lk" z lk)
          (p "dev-up" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-open-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-open" z (idx 3)) (p "dev-open" "lk" z lk)
          (p "dev-open" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-closed-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-closed" z (idx 3)) (p "dev-closed" "lk" z lk)
          (p "dev-closed" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-pass-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-pass" z (idx 2)) (p "dev-pass" "lk" z lk)
          (p "dev-pass" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule trRl_dev-up-at-4
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-up-at-3
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 1)))))
  (defgenrule trRl_passer-recv-key-at-4
    (forall ((z strd))
      (implies (p "passer-recv-key" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_passer-recv-key-at-3
    (forall ((z strd))
      (implies (p "passer-recv-key" z (idx 5)) (trans z (idx 3)))))
  (defgenrule trRl_dev-open-at-4
    (forall ((z strd))
      (implies (p "dev-open" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-open-at-2
    (forall ((z strd))
      (implies (p "dev-open" z (idx 5)) (trans z (idx 2)))))
  (defgenrule trRl_dev-closed-at-4
    (forall ((z strd))
      (implies (p "dev-closed" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-closed-at-2
    (forall ((z strd))
      (implies (p "dev-closed" z (idx 5)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 5)) (prec z (idx 4) z1 i))))))
  (defgenrule cau-dev-up-2
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 3)) (prec z1 i z (idx 2)))
        (or (= z z1) (prec z1 i z (idx 1))))))
  (defgenrule cau-dev-open-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-open" z (idx 4)) (prec z1 i z (idx 3)))
        (or (= z z1) (prec z1 i z (idx 2))))))
  (defgenrule cau-dev-closed-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-closed" z (idx 4)) (prec z1 i z (idx 3)))
        (or (= z z1) (prec z1 i z (idx 2))))))
  (defgenrule cau-dev-pass-1
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o) (p "dev-open" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-closed-0
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-closed" z (idx 1)) (p "dev-closed" "k" z k)
          (p "dev-closed" "o" z o) (p "dev-closed" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o) (p "dev-pass" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (n nb text) (b d name))
      (implies
        (and (p "dev-pass" z (idx 2)) (p "dev-pass" "n" z n)
          (p "dev-pass" "nb" z nb) (p "dev-pass" "b" z b)
          (p "dev-pass" "d" z d))
        (gen-st (door-state d (opened b nb n))))))
  (lang (closed (tuple 1)) (opened (tuple 3)) (door-state (tuple 2))
    (dev-key-state (tuple 3)) (open-req (tuple 5)) (close-req (tuple 5))
    (key-rec (tuple 6)) (delegate (tuple 6)) (hash-dk hash)))

(defskeleton open-closed
  (vars (k skey) (n nb text) (d o b name) (pt pt-0 pval) (lk ls locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (traces
    ((load lk (cat pt (dev-key-state d o k)))
      (load ls (cat pt-0 (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k)))))
  (label 3)
  (realized)
  (origs)
  (comment "Not closed under rules"))

(defskeleton open-closed
  (vars (k skey) (n nb text) (d o b name) (pt pt-0 pval) (lk ls locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (facts (same-dev ls lk))
  (rule fact-dev-pass-same-dev0 gen-st-dev-pass-0 gen-st-dev-pass-1)
  (traces
    ((load lk (cat pt (dev-key-state d o k)))
      (load ls (cat pt-0 (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k)))))
  (label 4)
  (parent 3)
  (seen 5)
  (unrealized (0 0) (0 1))
  (origs)
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pval) (start-ch chan) (lk ls locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (precedes ((1 4) (0 0)))
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((1 3) (0 0)))
  (rule cau-dev-pass-1 eff-dev-up-3 fact-dev-pass-same-dev0
    fact-dev-up-same-dev0 same-dev-lk-ls trRl_dev-up-at-1
    trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand dev-up 4)
    (ch-msg lk (cat pt-2 (dev-key-state d o k))) (0 0))
  (traces
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o))))))
  (label 5)
  (parent 4)
  (unrealized (0 1) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pval) (start-ch chan) (lk ls locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k) (d d) (o o) (start-ch start-ch))
  (precedes ((1 4) (0 0)) ((2 0) (1 0)))
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((1 3) (0 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand owner-power-dev 1)
    (ch-msg start-ch (cat "power-up" d o k)) (1 0))
  (traces
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((send start-ch (cat "power-up" d o k))))
  (label 6)
  (parent 5)
  (seen 7)
  (unrealized (0 1))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k k-0 skey) (n nb text) (b d o o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval) (start-ch chan)
    (ls lk locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-open 5 (any any) (k k-0) (n n) (nb nb) (d d) (o o-0)
    (b b) (lk lk) (ls ls))
  (precedes ((1 4) (3 2)) ((2 0) (1 0)) ((3 4) (0 0)))
  (gen-st (dev-key-state d o k) (dev-key-state d o-0 k-0)
    (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((1 3) (0 0)) ((3 4) (0 1)))
  (rule cau-dev-open-3 cau-dev-pass-1 fact-dev-open-same-dev0
    fact-dev-pass-same-dev0 gen-st-dev-pass-1 invShearsRule
    same-dev-ls-lk trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand dev-open 5)
    (ch-msg ls (cat pt (door-state d (opened b nb n)))) (0 1))
  (traces
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((send start-ch (cat "power-up" d o k)))
    ((load lk (cat pt-4 (dev-key-state d o-0 k-0)))
      (recv
        (cat b n (enc (open-req b d o-0 nb n) (hash-dk b nb n k-0))))
      (load ls (cat pt-5 (door-state d any)))
      (load lk (cat pt-6 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt (door-state d (opened b nb n))))))
  (label 7)
  (parent 6)
  (seen 8 9)
  (unrealized (3 0) (3 3))
  (comment "118 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch chan)
    (ls lk locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (precedes ((1 4) (3 0)) ((2 0) (1 0)) ((3 4) (0 0)))
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((1 3) (0 0)) ((1 3) (3 0)) ((3 4) (0 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (displaced 4 1 dev-up 4)
    (ch-msg lk (cat pt-6 (dev-key-state d o-0 k-0))) (3 0))
  (traces
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((send start-ch (cat "power-up" d o k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n))))))
  (label 8)
  (parent 7)
  (seen 10)
  (unrealized (3 3))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any old-0 old1-0 mesg) (k k-0 skey) (n nb text)
    (b o d o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pt-8 pt-9 pval)
    (start-ch start-ch-0 chan) (lk ls locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-open 5 (any any) (k k-0) (n n) (nb nb) (d d) (o o-0)
    (b b) (lk lk) (ls ls))
  (defstrand dev-up 5 (old old-0) (old1 old1-0) (k k-0) (d d) (o o-0)
    (start-ch start-ch-0) (lk lk) (ls ls))
  (precedes ((1 4) (3 2)) ((2 0) (1 0)) ((3 4) (0 0)) ((4 4) (1 1))
    ((4 4) (3 0)))
  (gen-st (dev-key-state d o k) (dev-key-state d o-0 k-0)
    (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch start-ch-0)
  (facts (same-dev ls lk))
  (leads-to ((1 3) (0 0)) ((3 4) (0 1)) ((4 3) (3 0)))
  (rule cau-dev-open-3 cau-dev-up-2 eff-dev-up-3 fact-dev-pass-same-dev0
    fact-dev-up-same-dev0 invShearsRule same-dev-lk-ls
    trRl_dev-open-at-2 trRl_dev-open-at-4 trRl_dev-up-at-1
    trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand dev-up 4)
    (ch-msg lk (cat pt-8 (dev-key-state d o-0 k-0))) (3 0))
  (traces
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((send start-ch (cat "power-up" d o k)))
    ((load lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (recv
        (cat b n (enc (open-req b d o-0 nb n) (hash-dk b nb n k-0))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv start-ch-0 (cat "power-up" d o-0 k-0))
      (load lk (cat pt-6 old-0)) (load ls (cat pt-7 old1-0))
      (stor lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt-9 (door-state d (closed o-0))))))
  (label 9)
  (parent 7)
  (unrealized (3 3) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (start-ch chan) (ls lk locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (precedes ((1 4) (3 0)) ((2 0) (1 0)) ((3 4) (0 0)))
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((1 3) (0 0)) ((1 3) (3 0)) ((1 3) (3 3)) ((3 4) (0 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (displaced 4 1 dev-up 4)
    (ch-msg lk (cat pt-5 (dev-key-state d o k))) (3 3))
  (traces
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((send start-ch (cat "power-up" d o k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n))))))
  (label 10)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk) (ls ls))))
  (origs (pt-2 (1 3)) (pt-3 (1 4)) (pt (3 4))))

(defskeleton open-closed
  (vars (old old1 any old-0 old1-0 mesg) (k k-0 skey) (n nb text)
    (b o d o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pt-8 pt-9 pval)
    (start-ch start-ch-0 chan) (lk ls locn))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-open 5 (any any) (k k-0) (n n) (nb nb) (d d) (o o-0)
    (b b) (lk lk) (ls ls))
  (defstrand dev-up 5 (old old-0) (old1 old1-0) (k k-0) (d d) (o o-0)
    (start-ch start-ch-0) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k-0) (d d) (o o-0)
    (start-ch start-ch-0))
  (precedes ((1 4) (3 2)) ((2 0) (1 0)) ((3 4) (0 0)) ((4 4) (1 1))
    ((4 4) (3 0)) ((5 0) (4 0)))
  (gen-st (dev-key-state d o k) (dev-key-state d o-0 k-0)
    (door-state d (opened b nb n)))
  (conf start-ch start-ch-0)
  (auth start-ch start-ch-0)
  (facts (same-dev ls lk))
  (leads-to ((1 3) (0 0)) ((3 4) (0 1)) ((4 3) (3 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand owner-power-dev 1)
    (ch-msg start-ch-0 (cat "power-up" d o-0 k-0)) (4 0))
  (traces
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((send start-ch (cat "power-up" d o k)))
    ((load lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (recv
        (cat b n (enc (open-req b d o-0 nb n) (hash-dk b nb n k-0))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv start-ch-0 (cat "power-up" d o-0 k-0))
      (load lk (cat pt-6 old-0)) (load ls (cat pt-7 old1-0))
      (stor lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt-9 (door-state d (closed o-0)))))
    ((send start-ch-0 (cat "power-up" d o-0 k-0))))
  (label 11)
  (parent 9)
  (unrealized (3 3))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol open-closed basic
  (defrole dev-up
    (vars (k skey) (d o name) (old old1 mesg) (start-ch chan)
      (lk ls locn))
    (trace (recv start-ch (cat "power-up" d o k)) (load lk old)
      (load ls old1) (stor lk (dev-key-state d o k))
      (stor ls (door-state d (closed o))) (send (enc "up" k)))
    (auth start-ch)
    (facts (same-dev ls lk)))
  (defrole owner-power-dev
    (vars (k skey) (d o name) (start-ch chan))
    (trace (send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    (conf start-ch))
  (defrole owner-delg-key
    (vars (k skey) (n nb text) (d o b name) (to-b from-b chan))
    (trace (recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k)))
      (recv (hash b nb n)))
    (uniq-orig n)
    (conf to-b)
    (auth from-b))
  (defrole passer-recv-key
    (vars (kp ign mesg) (n nb text) (d o b name) (to-b from-b chan)
      (del-key-locn locn))
    (trace (send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n kp)) (send (hash b nb n))
      (load del-key-locn ign)
      (stor del-key-locn (key-rec b d o nb n kp)))
    (uniq-orig nb)
    (auth to-b))
  (defrole passer-open
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b n (enc (open-req b d o nb n) kp)))
      (recv (hash (open-req b d o nb n)))))
  (defrole passer-close
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b n (enc (close-req b d o nb n) kp)))
      (recv (hash (close-req b d o nb n)))))
  (defrole dev-open
    (vars (k skey) (n nb text) (any mesg) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (door-state d any)) (load lk (dev-key-state d o k))
      (stor ls (door-state d (opened b nb n)))
      (send (hash (open-req b d o nb n))))
    (gen-st (dev-key-state d o k))
    (facts (same-dev ls lk)))
  (defrole dev-closed
    (vars (k skey) (n nb text) (any mesg) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (recv (cat b n (enc (close-req b d o nb n) (hash-dk b nb n k))))
      (load ls (door-state d any)) (load lk (dev-key-state d o k))
      (stor ls (door-state d (closed o)))
      (send (hash (close-req b d o nb n))))
    (gen-st (dev-key-state d o k))
    (facts (same-dev ls lk)))
  (defrole dev-pass
    (vars (k skey) (n nb text) (d o b name) (lk ls locn))
    (trace (load lk (dev-key-state d o k))
      (load ls (door-state d (opened b nb n)))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
    (facts (same-dev ls lk)))
  (defrole passer-pass
    (vars (kp mesg) (n nb text) (d o b name) (del-key-locn locn))
    (trace (load del-key-locn (key-rec b d o nb n kp))
      (send (cat b nb n (enc "may I pass" kp)))
      (recv (enc "you may pass" kp))))
  (defrule power-deliver-once
    (forall ((z1 z2 strd) (k skey))
      (implies
        (and (p "dev-up" z1 (idx 2)) (p "dev-up" z2 (idx 2))
          (p "dev-up" "k" z1 k) (p "dev-up" "k" z2 k))
        (= z1 z2))))
  (defrule same-dev-ls-lk
    (forall ((ls lk lk-0 locn))
      (implies
        (and (fact same-dev ls lk) (fact same-dev ls lk-0))
        (= lk lk-0))))
  (defrule same-dev-lk-ls
    (forall ((lk ls ls-0 locn))
      (implies
        (and (fact same-dev ls lk) (fact same-dev ls-0 lk))
        (= ls ls-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule 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)))))
  (defgenrule 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))))
  (defgenrule 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))))
  (defgenrule 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)))))
  (defgenrule 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)))))
  (defgenrule fact-dev-up-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-up" z (idx 3)) (p "dev-up" "lk" z lk)
          (p "dev-up" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-open-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-open" z (idx 3)) (p "dev-open" "lk" z lk)
          (p "dev-open" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-closed-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-closed" z (idx 3)) (p "dev-closed" "lk" z lk)
          (p "dev-closed" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule fact-dev-pass-same-dev0
    (forall ((z strd) (lk ls locn))
      (implies
        (and (p "dev-pass" z (idx 2)) (p "dev-pass" "lk" z lk)
          (p "dev-pass" "ls" z ls)) (fact same-dev ls lk))))
  (defgenrule trRl_dev-up-at-4
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-up-at-3
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_dev-up-at-2
    (forall ((z strd))
      (implies (p "dev-up" z (idx 5)) (trans z (idx 2)))))
  (defgenrule trRl_dev-up-at-1
    (forall ((z strd))
      (implies (p "dev-up" z (idx 4)) (trans z (idx 1)))))
  (defgenrule trRl_passer-recv-key-at-4
    (forall ((z strd))
      (implies (p "passer-recv-key" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_passer-recv-key-at-3
    (forall ((z strd))
      (implies (p "passer-recv-key" z (idx 5)) (trans z (idx 3)))))
  (defgenrule trRl_dev-open-at-4
    (forall ((z strd))
      (implies (p "dev-open" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-open-at-2
    (forall ((z strd))
      (implies (p "dev-open" z (idx 5)) (trans z (idx 2)))))
  (defgenrule trRl_dev-closed-at-4
    (forall ((z strd))
      (implies (p "dev-closed" z (idx 5)) (trans z (idx 4)))))
  (defgenrule trRl_dev-closed-at-2
    (forall ((z strd))
      (implies (p "dev-closed" z (idx 5)) (trans z (idx 2)))))
  (defgenrule eff-dev-up-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "dev-up" z (idx 5)) (prec z (idx 4) z1 i))))))
  (defgenrule cau-dev-up-2
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-up" z (idx 3)) (prec z1 i z (idx 2)))
        (or (= z z1) (prec z1 i z (idx 1))))))
  (defgenrule cau-dev-open-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-open" z (idx 4)) (prec z1 i z (idx 3)))
        (or (= z z1) (prec z1 i z (idx 2))))))
  (defgenrule cau-dev-closed-3
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-closed" z (idx 4)) (prec z1 i z (idx 3)))
        (or (= z z1) (prec z1 i z (idx 2))))))
  (defgenrule cau-dev-pass-1
    (forall ((z z1 strd) (i indx))
      (implies (and (p "dev-pass" z (idx 2)) (prec z1 i z (idx 1)))
        (or (= z z1) (prec z1 i z (idx 0))))))
  (defgenrule gen-st-dev-open-0
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-open" z (idx 1)) (p "dev-open" "k" z k)
          (p "dev-open" "o" z o) (p "dev-open" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-closed-0
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-closed" z (idx 1)) (p "dev-closed" "k" z k)
          (p "dev-closed" "o" z o) (p "dev-closed" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-pass-1
    (forall ((z strd) (k skey) (o d name))
      (implies
        (and (p "dev-pass" z (idx 1)) (p "dev-pass" "k" z k)
          (p "dev-pass" "o" z o) (p "dev-pass" "d" z d))
        (gen-st (dev-key-state d o k)))))
  (defgenrule gen-st-dev-pass-0
    (forall ((z strd) (n nb text) (b d name))
      (implies
        (and (p "dev-pass" z (idx 2)) (p "dev-pass" "n" z n)
          (p "dev-pass" "nb" z nb) (p "dev-pass" "b" z b)
          (p "dev-pass" "d" z d))
        (gen-st (door-state d (opened b nb n))))))
  (lang (closed (tuple 1)) (opened (tuple 3)) (door-state (tuple 2))
    (dev-key-state (tuple 3)) (open-req (tuple 5)) (close-req (tuple 5))
    (key-rec (tuple 6)) (delegate (tuple 6)) (hash-dk hash)))

(defskeleton open-closed
  (vars (k skey) (n nb text) (d o d-0 o-0 b name) (pt pt-0 pval)
    (start-ch chan) (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (lk lk) (ls ls))
  (uniq-orig k)
  (conf start-ch)
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt (dev-key-state d-0 o-0 k)))
      (load ls (cat pt-0 (door-state d-0 (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k)))))
  (label 12)
  (unrealized (0 1) (1 0) (1 2))
  (preskeleton)
  (origs (k (0 0)))
  (comment "Not a skeleton"))

(defskeleton open-closed
  (vars (k skey) (n nb text) (d o d-0 o-0 b name) (pt pt-0 pval)
    (start-ch chan) (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (lk lk) (ls ls))
  (precedes ((0 0) (1 0)))
  (uniq-orig k)
  (conf start-ch)
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt (dev-key-state d-0 o-0 k)))
      (load ls (cat pt-0 (door-state d-0 (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k)))))
  (label 13)
  (parent 12)
  (unrealized (0 1) (1 0) (1 2))
  (origs (k (0 0)))
  (comment "Not closed under rules"))

(defskeleton open-closed
  (vars (k skey) (n nb text) (d o d-0 o-0 b name) (pt pt-0 pval)
    (start-ch chan) (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (lk lk) (ls ls))
  (precedes ((0 0) (1 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d-0 o-0 k) (door-state d-0 (opened b nb n)))
  (conf start-ch)
  (facts (same-dev ls lk))
  (rule fact-dev-pass-same-dev0 gen-st-dev-pass-0 gen-st-dev-pass-1)
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt (dev-key-state d-0 o-0 k)))
      (load ls (cat pt-0 (door-state d-0 (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k)))))
  (label 14)
  (parent 13)
  (seen 15)
  (unrealized (0 1) (1 0) (1 1) (1 2))
  (origs (k (0 0)))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pval) (start-ch start-ch-0 chan)
    (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (lk lk) (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d-0) (o o-0)
    (start-ch start-ch-0) (lk lk) (ls ls))
  (precedes ((0 0) (2 0)) ((2 4) (1 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d-0 o-0 k) (door-state d-0 (opened b nb n)))
  (conf start-ch)
  (auth start-ch-0)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)))
  (rule cau-dev-pass-1 eff-dev-up-3 fact-dev-pass-same-dev0
    fact-dev-up-same-dev0 same-dev-lk-ls trRl_dev-up-at-1
    trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand dev-up 4)
    (ch-msg lk (cat pt-2 (dev-key-state d-0 o-0 k))) (1 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d-0 o-0 k)))
      (load ls (cat pt (door-state d-0 (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch-0 (cat "power-up" d-0 o-0 k))
      (load lk (cat pt-0 old)) (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d-0 o-0 k)))
      (stor ls (cat pt-3 (door-state d-0 (closed o-0))))))
  (label 15)
  (parent 14)
  (unrealized (0 1) (1 1) (1 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pval) (start-ch chan) (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (precedes ((0 0) (2 0)) ((2 4) (1 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (displaced 3 0 owner-power-dev 1)
    (ch-msg start-ch-0 (cat "power-up" d-0 o-0 k)) (2 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o))))))
  (label 16)
  (parent 15)
  (seen 17)
  (unrealized (0 1) (1 1) (1 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k k-0 skey) (n nb text) (d o b o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval) (start-ch chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k-0) (n n) (nb nb) (d d) (o o-0)
    (b b) (lk lk) (ls ls))
  (precedes ((0 0) (2 0)) ((2 4) (3 2)) ((3 4) (1 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (dev-key-state d o-0 k-0)
    (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((3 4) (1 1)))
  (rule cau-dev-open-3 cau-dev-pass-1 fact-dev-open-same-dev0
    fact-dev-pass-same-dev0 gen-st-dev-pass-1 invShearsRule
    same-dev-ls-lk trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand dev-open 5)
    (ch-msg ls (cat pt (door-state d (opened b nb n)))) (1 1))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-4 (dev-key-state d o-0 k-0)))
      (recv
        (cat b n (enc (open-req b d o-0 nb n) (hash-dk b nb n k-0))))
      (load ls (cat pt-5 (door-state d any)))
      (load lk (cat pt-6 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt (door-state d (opened b nb n))))))
  (label 17)
  (parent 16)
  (seen 18 19)
  (unrealized (0 1) (1 2) (3 0) (3 3))
  (comment "118 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (displaced 4 2 dev-up 4)
    (ch-msg lk (cat pt-6 (dev-key-state d o-0 k-0))) (3 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n))))))
  (label 18)
  (parent 17)
  (unrealized (0 1) (1 2) (3 1) (3 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any old-0 old1-0 mesg) (k k-0 skey) (n nb text)
    (o b d o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pt-8 pt-9 pval)
    (start-ch start-ch-0 chan) (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k-0) (n n) (nb nb) (d d) (o o-0)
    (b b) (lk lk) (ls ls))
  (defstrand dev-up 5 (old old-0) (old1 old1-0) (k k-0) (d d) (o o-0)
    (start-ch start-ch-0) (lk lk) (ls ls))
  (precedes ((0 0) (2 0)) ((2 4) (3 2)) ((3 4) (1 0)) ((4 4) (2 1))
    ((4 4) (3 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (dev-key-state d o-0 k-0)
    (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch start-ch-0)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((3 4) (1 1)) ((4 3) (3 0)))
  (rule cau-dev-open-3 cau-dev-up-2 eff-dev-up-3 fact-dev-pass-same-dev0
    fact-dev-up-same-dev0 invShearsRule same-dev-lk-ls
    trRl_dev-open-at-2 trRl_dev-open-at-4 trRl_dev-up-at-1
    trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand dev-up 4)
    (ch-msg lk (cat pt-8 (dev-key-state d o-0 k-0))) (3 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (recv
        (cat b n (enc (open-req b d o-0 nb n) (hash-dk b nb n k-0))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv start-ch-0 (cat "power-up" d o-0 k-0))
      (load lk (cat pt-6 old-0)) (load ls (cat pt-7 old1-0))
      (stor lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt-9 (door-state d (closed o-0))))))
  (label 19)
  (parent 17)
  (unrealized (0 1) (1 2) (3 3) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval) (start-ch chan)
    (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-strand passer-open 2)
    (enc (open-req b d o nb n) (hash-dk b nb n k)) (3 1))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))))
  (label 20)
  (parent 18)
  (unrealized (0 1) (1 2) (3 3) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-listener (hash-dk b nb n k))
    (enc (open-req b d o nb n) (hash-dk b nb n k)) (3 1))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k))))
  (label 21)
  (parent 18)
  (unrealized (0 1) (3 3) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any old-0 old1-0 mesg) (k k-0 skey) (n nb text)
    (o b d o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pt-8 pt-9 pval)
    (start-ch start-ch-0 chan) (lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k-0) (n n) (nb nb) (d d) (o o-0)
    (b b) (lk lk) (ls ls))
  (defstrand dev-up 5 (old old-0) (old1 old1-0) (k k-0) (d d) (o o-0)
    (start-ch start-ch-0) (lk lk) (ls ls))
  (defstrand owner-power-dev 1 (k k-0) (d d) (o o-0)
    (start-ch start-ch-0))
  (precedes ((0 0) (2 0)) ((2 4) (3 2)) ((3 4) (1 0)) ((4 4) (2 1))
    ((4 4) (3 0)) ((5 0) (4 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (dev-key-state d o-0 k-0)
    (door-state d (opened b nb n)))
  (conf start-ch start-ch-0)
  (auth start-ch start-ch-0)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((3 4) (1 1)) ((4 3) (3 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand owner-power-dev 1)
    (ch-msg start-ch-0 (cat "power-up" d o-0 k-0)) (4 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (recv
        (cat b n (enc (open-req b d o-0 nb n) (hash-dk b nb n k-0))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv start-ch-0 (cat "power-up" d o-0 k-0))
      (load lk (cat pt-6 old-0)) (load ls (cat pt-7 old1-0))
      (stor lk (cat pt-8 (dev-key-state d o-0 k-0)))
      (stor ls (cat pt-9 (door-state d (closed o-0)))))
    ((send start-ch-0 (cat "power-up" d o-0 k-0))))
  (label 22)
  (parent 19)
  (unrealized (0 1) (1 2) (3 3))
  (dead)
  (comment "empty cohort"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (uniq-orig k n)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-strand owner-delg-key 2)
    (hash-dk b nb n k) (4 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))))
  (label 23)
  (parent 20)
  (unrealized (0 1) (1 2) (3 3) (4 0) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval) (start-ch chan)
    (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (4 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (4 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 24)
  (parent 20)
  (seen 28)
  (unrealized (0 1) (3 3) (5 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch to-b from-b chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (uniq-orig k n)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-strand owner-delg-key 2)
    (hash-dk b nb n k) (4 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))))
  (label 25)
  (parent 21)
  (unrealized (0 1) (1 2) (3 1) (3 3) (4 0) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (4 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (4 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 26)
  (parent 21)
  (seen 30)
  (unrealized (0 1) (3 3) (5 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 1 (nb nb) (b b) (from-b from-b))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 0) (5 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand passer-recv-key 1)
    (ch-msg from-b (cat "req-key" b nb)) (5 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))))
  (label 27)
  (parent 23)
  (unrealized (0 1) (1 2) (3 3) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval) (start-ch chan)
    (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (5 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (4 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation nonce-test (displaced 6 2 dev-up 4) k (5 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 28)
  (parent 24)
  (seen 28)
  (unrealized (0 1) (3 3) (5 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch to-b from-b chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 1 (nb nb) (b b) (from-b from-b))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 0) (5 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation channel-test (added-strand passer-recv-key 1)
    (ch-msg from-b (cat "req-key" b nb)) (5 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))))
  (label 29)
  (parent 25)
  (unrealized (0 1) (1 2) (3 1) (3 3) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (5 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (4 0)))
  (uniq-orig k)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch)
  (auth start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation nonce-test (displaced 6 2 dev-up 4) k (5 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 30)
  (parent 26)
  (seen 30)
  (unrealized (0 1) (3 3) (5 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text)
    (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pt-8 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d-0) (o o-0) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn-0))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (displaced 6 7 passer-recv-key 5)
    (hash-dk b nb n k) (4 0)
    (ch-msg to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn-0 (cat pt-7 ign))
      (stor del-key-locn-0
        (cat pt-8 (key-rec b d-0 o-0 nb n (hash-dk b nb n k))))))
  (label 31)
  (parent 27)
  (unrealized (0 1) (1 2) (3 3) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 1 (nb nb) (b b) (from-b from-b))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (7 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (7 0)) ((6 0) (5 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (4 0)
    (ch-msg to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 32)
  (parent 27)
  (seen 37)
  (unrealized (0 1) (3 3) (7 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text)
    (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d-0) (o o-0) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (displaced 6 7 passer-recv-key 5)
    (hash-dk b nb n k) (4 0)
    (ch-msg to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-6 ign))
      (stor del-key-locn
        (cat pt-7 (key-rec b d-0 o-0 nb n (hash-dk b nb n k))))))
  (label 33)
  (parent 29)
  (unrealized (0 1) (1 2) (3 1) (3 3) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch to-b from-b chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 1 (nb nb) (b b) (from-b from-b))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (7 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (7 0)) ((6 0) (5 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (4 0)
    (ch-msg to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 34)
  (parent 29)
  (seen 39)
  (unrealized (0 1) (3 3) (7 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)) ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test
    (contracted (d-0 d) (o-0 o) (del-key-locn-0 del-key-locn)
      (pt-8 pt-7)) (hash-dk b nb n k) (4 0)
    (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k)))
    (ch-msg del-key-locn
      (cat pt-7 (key-rec b d o nb n (hash-dk b nb n k)))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-7 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-6 ign))
      (stor del-key-locn
        (cat pt-7 (key-rec b d o nb n (hash-dk b nb n k))))))
  (label 35)
  (parent 31)
  (seen 40)
  (unrealized (0 1) (1 2) (3 3))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text)
    (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pt-8 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d-0) (o o-0) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn-0))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (7 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (7 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (4 0)
    (ch-msg to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
    (ch-msg del-key-locn-0
      (cat pt-8 (key-rec b d-0 o-0 nb n (hash-dk b nb n k)))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn-0 (cat pt-7 ign))
      (stor del-key-locn-0
        (cat pt-8 (key-rec b d-0 o-0 nb n (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 36)
  (parent 31)
  (seen 41)
  (unrealized (0 1) (3 3) (7 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 1 (nb nb) (b b) (from-b from-b))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (7 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (7 0)) ((6 0) (5 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation nonce-test (displaced 8 2 dev-up 4) k (7 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 37)
  (parent 32)
  (seen 37)
  (unrealized (0 1) (3 3) (7 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text)
    (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d-0) (o o-0) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (7 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (7 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (4 0)
    (ch-msg to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
    (ch-msg del-key-locn
      (cat pt-7 (key-rec b d-0 o-0 nb n (hash-dk b nb n k)))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-6 ign))
      (stor del-key-locn
        (cat pt-7 (key-rec b d-0 o-0 nb n (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 38)
  (parent 33)
  (seen 42)
  (unrealized (0 1) (3 3) (7 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any mesg) (k skey) (n nb text) (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval) (start-ch to-b from-b chan)
    (ls lk locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 1 (nb nb) (b b) (from-b from-b))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (7 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (7 0)) ((6 0) (5 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4)
  (operation nonce-test (displaced 8 2 dev-up 4) k (7 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 39)
  (parent 34)
  (seen 39)
  (unrealized (0 1) (3 3) (7 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation channel-test (displaced 7 2 dev-up 4)
    (ch-msg lk (cat pt-7 (dev-key-state d o k))) (3 3))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))))
  (label 40)
  (parent 35)
  (unrealized (0 1) (1 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text)
    (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pt-8 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d-0) (o o-0) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn-0))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (7 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (7 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4 trRl_passer-recv-key-at-3
    trRl_passer-recv-key-at-4)
  (operation nonce-test (displaced 8 2 dev-up 4) k (7 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn-0 (cat pt-7 ign))
      (stor del-key-locn-0
        (cat pt-8 (key-rec b d-0 o-0 nb n (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 41)
  (parent 36)
  (seen 41)
  (unrealized (0 1) (3 3) (7 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text)
    (d o b d-0 o-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (deflistener (hash-dk b nb n k))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d-0) (o o-0) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d-0) (o o-0) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (7 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (7 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (4 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((3 4) (1 1)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4 trRl_passer-recv-key-at-3
    trRl_passer-recv-key-at-4)
  (operation nonce-test (displaced 8 2 dev-up 4) k (7 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d-0 o-0 nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-6 ign))
      (stor del-key-locn
        (cat pt-7 (key-rec b d-0 o-0 nb n (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 42)
  (parent 38)
  (seen 42)
  (unrealized (0 1) (3 3) (7 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb n-0 nb-0 text)
    (b d o d-0 o-0 b-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n-0) (nb nb-0)
    (d d-0) (o o-0) (b b-0) (del-key-locn del-key-locn-0))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)) ((7 1) (1 2)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-strand passer-pass 2)
    (enc "may I pass" (hash-dk b nb n k)) (1 2))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn-0
       (cat pt-7 (key-rec b-0 d-0 o-0 nb-0 n-0 (hash-dk b nb n k))))
      (send (cat b-0 nb-0 n-0 (enc "may I pass" (hash-dk b nb n k))))))
  (label 43)
  (parent 40)
  (unrealized (0 1) (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (hash-dk b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)) ((7 1) (1 2)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener (hash-dk b nb n k))
    (enc "may I pass" (hash-dk b nb n k)) (1 2))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k))))
  (label 44)
  (parent 40)
  (unrealized (0 1) (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb n-0 nb-0 text)
    (b d o d-0 o-0 b-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n-0) (nb nb-0)
    (d d-0) (o o-0) (b b-0) (del-key-locn del-key-locn-0))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((5 1) (7 0)) ((6 0) (5 0)) ((6 4) (4 0))
    ((7 1) (1 2)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (displaced 8 5 owner-delg-key 2)
    (hash-dk b nb n k) (7 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn-0
       (cat pt-7 (key-rec b-0 d-0 o-0 nb-0 n-0 (hash-dk b nb n k))))
      (send (cat b-0 nb-0 n-0 (enc "may I pass" (hash-dk b nb n k))))))
  (label 45)
  (parent 43)
  (unrealized (0 1) (7 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (hash-dk b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((5 1) (7 0)) ((6 0) (5 0)) ((6 4) (4 0))
    ((7 1) (1 2)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (displaced 8 5 owner-delg-key 2)
    (hash-dk b nb n k) (7 0))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k))))
  (label 46)
  (parent 44)
  (unrealized (0 1) (7 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb n-0 nb-0 text)
    (b d o d-0 o-0 b-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n-0) (nb nb-0)
    (d d-0) (o o-0) (b b-0) (del-key-locn del-key-locn-0))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)) ((6 4) (7 0))
    ((7 1) (1 2)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (displaced 8 6 passer-recv-key 5)
    (hash-dk b nb n k) (7 0)
    (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn-0
       (cat pt-7 (key-rec b-0 d-0 o-0 nb-0 n-0 (hash-dk b nb n k))))
      (send (cat b-0 nb-0 n-0 (enc "may I pass" (hash-dk b nb n k))))))
  (label 47)
  (parent 45)
  (unrealized (0 1) (7 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb n-0 nb-0 text)
    (b d o d-0 o-0 b-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n-0) (nb nb-0)
    (d d-0) (o o-0) (b b-0) (del-key-locn del-key-locn-0))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (8 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (7 0)
    (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn-0
       (cat pt-7 (key-rec b-0 d-0 o-0 nb-0 n-0 (hash-dk b nb n k))))
      (send (cat b-0 nb-0 n-0 (enc "may I pass" (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 48)
  (parent 45)
  (seen 53)
  (unrealized (0 1) (8 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (hash-dk b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)) ((6 4) (7 0))
    ((7 1) (1 2)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (displaced 8 6 passer-recv-key 5)
    (hash-dk b nb n k) (7 0)
    (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k))))
  (label 49)
  (parent 46)
  (unrealized (0 1) (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (hash-dk b nb n k))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (8 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (7 0)
    (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 50)
  (parent 46)
  (seen 55)
  (unrealized (0 1) (8 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((3 4) (1 0)) ((4 1) (3 1))
    ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0)) ((6 4) (7 0))
    ((7 1) (1 2)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)) ((6 4) (7 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test
    (contracted (n-0 n) (nb-0 nb) (d-0 d) (o-0 o) (b-0 b)
      (del-key-locn-0 del-key-locn) (pt-7 pt-6)) (hash-dk b nb n k)
    (7 0) (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k)))
    (ch-msg del-key-locn
      (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b nb n (enc "may I pass" (hash-dk b nb n k))))))
  (label 51)
  (parent 47)
  (seen 56)
  (unrealized (0 1))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb n-0 nb-0 text)
    (b d o d-0 o-0 b-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n-0) (nb nb-0)
    (d d-0) (o o-0) (b b-0) (del-key-locn del-key-locn-0))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (8 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((6 4) (7 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (7 0)
    (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k)))
    (ch-msg del-key-locn
      (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn-0
       (cat pt-7 (key-rec b-0 d-0 o-0 nb-0 n-0 (hash-dk b nb n k))))
      (send (cat b-0 nb-0 n-0 (enc "may I pass" (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 52)
  (parent 47)
  (seen 58)
  (unrealized (0 1) (8 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb n-0 nb-0 text)
    (b d o d-0 o-0 b-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n-0) (nb nb-0)
    (d d-0) (o o-0) (b b-0) (del-key-locn del-key-locn-0))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (8 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4 trRl_passer-recv-key-at-3
    trRl_passer-recv-key-at-4)
  (operation nonce-test (displaced 9 2 dev-up 4) k (8 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn-0
       (cat pt-7 (key-rec b-0 d-0 o-0 nb-0 n-0 (hash-dk b nb n k))))
      (send (cat b-0 nb-0 n-0 (enc "may I pass" (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 53)
  (parent 48)
  (seen 53)
  (unrealized (0 1) (8 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (hash-dk b nb n k))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((0 0) (8 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((6 4) (7 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener (cat b nb n k))
    (hash-dk b nb n k) (7 0)
    (ch-msg to-b (delegate b d o nb n (hash-dk b nb n k)))
    (ch-msg del-key-locn
      (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 54)
  (parent 49)
  (seen 59)
  (unrealized (0 1) (8 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (hash-dk b nb n k))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (8 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4 trRl_passer-recv-key-at-3
    trRl_passer-recv-key-at-4)
  (operation nonce-test (displaced 9 2 dev-up 4) k (8 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 55)
  (parent 50)
  (seen 55)
  (unrealized (0 1) (8 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (any ign old old1 mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (to-b from-b start-ch chan) (del-key-locn lk ls locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand dev-up 6 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (precedes ((0 0) (7 0)) ((2 4) (1 0)) ((3 1) (2 1)) ((4 1) (5 1))
    ((5 0) (4 0)) ((5 4) (3 0)) ((5 4) (6 0)) ((6 1) (1 2))
    ((7 4) (2 0)) ((7 5) (0 1)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf to-b start-ch)
  (auth to-b from-b start-ch)
  (facts (same-dev ls lk))
  (leads-to ((2 4) (1 1)) ((5 4) (3 0)) ((5 4) (6 0)) ((7 3) (1 0))
    ((7 3) (2 0)) ((7 3) (2 3)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (displaced 2 8 dev-up 6) (enc "up" k)
    (0 1))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-5 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((load lk (cat pt-5 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-0 (door-state d any)))
      (load lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-2 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-1 ign))
      (stor del-key-locn
        (cat pt-2 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn
       (cat pt-2 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b nb n (enc "may I pass" (hash-dk b nb n k)))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-3 old))
      (load ls (cat pt-4 old1))
      (stor lk (cat pt-5 (dev-key-state d o k)))
      (stor ls (cat pt-6 (door-state d (closed o))))
      (send (enc "up" k))))
  (label 56)
  (parent 51)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((k k) (d d) (o o) (start-ch start-ch) (n n) (nb nb) (d-0 d)
        (o-0 o) (b b) (lk lk) (ls ls))))
  (origs (pt-5 (7 3)) (pt-6 (7 4)) (nb (5 0)) (pt-2 (5 4)) (n (4 1))
    (pt (2 4)) (k (0 0))))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (deflistener k)
  (precedes ((0 0) (2 0)) ((0 0) (8 0)) ((2 4) (3 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0))
    ((6 4) (7 0)) ((7 1) (1 2)) ((8 1) (0 1)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)) ((6 4) (7 0)))
  (rule fact-dev-pass-same-dev0 trRl_dev-open-at-2 trRl_dev-open-at-4
    trRl_dev-up-at-1 trRl_dev-up-at-2 trRl_dev-up-at-3 trRl_dev-up-at-4
    trRl_passer-recv-key-at-3 trRl_passer-recv-key-at-4)
  (operation encryption-test (added-listener k) (enc "up" k) (0 1))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b nb n (enc "may I pass" (hash-dk b nb n k)))))
    ((recv k) (send k)))
  (label 57)
  (parent 51)
  (seen 60)
  (unrealized (8 0))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb n-0 nb-0 text)
    (b d o d-0 o-0 b-0 name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pt-7 pval)
    (start-ch to-b from-b chan)
    (ls lk del-key-locn del-key-locn-0 locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n-0) (nb nb-0)
    (d d-0) (o o-0) (b b-0) (del-key-locn del-key-locn-0))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (8 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((6 4) (7 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4 trRl_passer-recv-key-at-3
    trRl_passer-recv-key-at-4)
  (operation nonce-test (displaced 9 2 dev-up 4) k (8 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn-0
       (cat pt-7 (key-rec b-0 d-0 o-0 nb-0 n-0 (hash-dk b nb n k))))
      (send (cat b-0 nb-0 n-0 (enc "may I pass" (hash-dk b nb n k)))))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 58)
  (parent 52)
  (seen 58)
  (unrealized (0 1) (8 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (deflistener (hash-dk b nb n k))
  (deflistener (cat b nb n k))
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (8 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((5 1) (8 0)) ((6 0) (5 0))
    ((6 4) (4 0)) ((6 4) (7 0)) ((7 1) (1 2)) ((8 1) (7 0)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4 trRl_passer-recv-key-at-3
    trRl_passer-recv-key-at-4)
  (operation nonce-test (displaced 9 2 dev-up 4) k (8 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((recv (hash-dk b nb n k)) (send (hash-dk b nb n k)))
    ((recv (cat b nb n k)) (send (cat b nb n k))))
  (label 59)
  (parent 54)
  (seen 59)
  (unrealized (0 1) (8 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton open-closed
  (vars (old old1 any ign mesg) (k skey) (n nb text) (b d o name)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pt-6 pval)
    (start-ch to-b from-b chan) (ls lk del-key-locn locn))
  (defstrand owner-power-dev 2 (k k) (d d) (o o) (start-ch start-ch))
  (defstrand dev-pass 4 (k k) (n n) (nb nb) (d d) (o o) (b b) (lk lk)
    (ls ls))
  (defstrand dev-up 5 (old old) (old1 old1) (k k) (d d) (o o)
    (start-ch start-ch) (lk lk) (ls ls))
  (defstrand dev-open 5 (any any) (k k) (n n) (nb nb) (d d) (o o) (b b)
    (lk lk) (ls ls))
  (defstrand passer-open 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (defstrand owner-delg-key 2 (k k) (n n) (nb nb) (d d) (o o) (b b)
    (to-b to-b) (from-b from-b))
  (defstrand passer-recv-key 5 (kp (hash-dk b nb n k)) (ign ign) (n n)
    (nb nb) (d d) (o o) (b b) (to-b to-b) (from-b from-b)
    (del-key-locn del-key-locn))
  (defstrand passer-pass 2 (kp (hash-dk b nb n k)) (n n) (nb nb) (d d)
    (o o) (b b) (del-key-locn del-key-locn))
  (deflistener k)
  (precedes ((0 0) (2 0)) ((2 4) (3 0)) ((2 4) (8 0)) ((3 4) (1 0))
    ((4 1) (3 1)) ((5 1) (6 1)) ((6 0) (5 0)) ((6 4) (4 0))
    ((6 4) (7 0)) ((7 1) (1 2)) ((8 1) (0 1)))
  (uniq-orig k n nb)
  (gen-st (dev-key-state d o k) (door-state d (opened b nb n)))
  (conf start-ch to-b)
  (auth start-ch to-b from-b)
  (facts (same-dev ls lk))
  (leads-to ((2 3) (1 0)) ((2 3) (3 0)) ((2 3) (3 3)) ((3 4) (1 1))
    ((6 4) (4 0)) ((6 4) (7 0)))
  (rule eff-dev-up-3 fact-dev-pass-same-dev0 trRl_dev-open-at-2
    trRl_dev-open-at-4 trRl_dev-up-at-1 trRl_dev-up-at-2
    trRl_dev-up-at-3 trRl_dev-up-at-4 trRl_passer-recv-key-at-3
    trRl_passer-recv-key-at-4)
  (operation nonce-test (displaced 9 2 dev-up 4) k (8 0)
    (ch-msg start-ch (cat "power-up" d o k)))
  (traces ((send start-ch (cat "power-up" d o k)) (recv (enc "up" k)))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (load ls (cat pt (door-state d (opened b nb n))))
      (recv (cat b nb n (enc "may I pass" (hash-dk b nb n k))))
      (send (enc "you may pass" n (hash-dk b nb n k))))
    ((recv start-ch (cat "power-up" d o k)) (load lk (cat pt-0 old))
      (load ls (cat pt-1 old1))
      (stor lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt-3 (door-state d (closed o)))))
    ((load lk (cat pt-2 (dev-key-state d o k)))
      (recv (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k))))
      (load ls (cat pt-4 (door-state d any)))
      (load lk (cat pt-2 (dev-key-state d o k)))
      (stor ls (cat pt (door-state d (opened b nb n)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b n (enc (open-req b d o nb n) (hash-dk b nb n k)))))
    ((recv from-b (cat "req-key" b nb))
      (send to-b (delegate b d o nb n (hash-dk b nb n k))))
    ((send from-b (cat "req-key" b nb))
      (recv to-b (delegate b d o nb n (hash-dk b nb n k)))
      (send (hash b nb n)) (load del-key-locn (cat pt-5 ign))
      (stor del-key-locn
        (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k)))))
    ((load del-key-locn
       (cat pt-6 (key-rec b d o nb n (hash-dk b nb n k))))
      (send (cat b nb n (enc "may I pass" (hash-dk b nb n k)))))
    ((recv k) (send k)))
  (label 60)
  (parent 57)
  (seen 60)
  (unrealized (8 0))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")