(herald "Yahalom Protocol Without Forwarding")

(comment "CPSA 2.2.8")
(comment "All input read")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    (uniq-orig k)))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))))
  (label 0)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (precedes ((1 2) (0 2)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 3) (enc a k (ltk b c))
    (0 2))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c)))
      (send (enc a k (ltk b c)))))
  (label 1)
  (parent 0)
  (unrealized (0 3) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((1 2) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (1 0))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c))))))
  (label 2)
  (parent 1)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (precedes ((0 1) (1 0)) ((1 2) (0 2)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (1 0))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 3)
  (parent 1)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 n-a-1 text) (a b c a-0 b-0 c-0 name)
    (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (precedes ((0 1) (3 1)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 1) (1 0))
    ((3 2) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-strand init 3) (enc n-b k) (0 3))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c)))))
    ((send (cat a-0 n-a-1)) (recv (enc b-0 k n-a-1 n-b (ltk a-0 c-0)))
      (send (enc n-b k))))
  (label 4)
  (parent 2)
  (seen 6)
  (unrealized (3 1))
  (comment "3 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (deflistener k)
  (precedes ((1 1) (3 0)) ((1 2) (0 2)) ((2 1) (1 0)) ((3 1) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-listener k) (enc n-b k) (0 3))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c)))))
    ((recv k) (send k)))
  (label 5)
  (parent 2)
  (seen 9)
  (unrealized (0 3) (3 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-strand init 3) (enc n-b k) (0 3))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k))))
  (label 6)
  (parent 3)
  (unrealized (2 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (2 0)) ((1 2) (0 2)) ((2 1) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-listener k) (enc n-b k) (0 3))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((recv k) (send k)))
  (label 7)
  (parent 3)
  (seen 12)
  (unrealized (0 3) (2 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 n-a-1 text) (a b c a-0 b-0 c-0 name)
    (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (precedes ((0 1) (4 0)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 1) (1 0))
    ((3 2) (0 3)) ((4 1) (3 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 2) n-b (3 1)
    (enc a n-a n-b (ltk b c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c)))))
    ((send (cat a-0 n-a-1)) (recv (enc b-0 k n-a-1 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c)))))
  (label 8)
  (parent 4)
  (seen 10 14)
  (unrealized (3 1))
  (comment "4 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (deflistener k)
  (precedes ((1 2) (0 2)) ((1 2) (3 0)) ((2 1) (1 0)) ((3 1) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (added-strand serv 3) k (3 0)
    (enc b k n-a-0 n-b-0 (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c)))))
    ((recv k) (send k)))
  (label 9)
  (parent 5)
  (unrealized (0 3) (3 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (n-a-0 n-a))
    n-b (2 1) (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (label 10)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (k k))))
  (origs (k (1 1)) (n-b (0 1))))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 2) (0 3))
    ((3 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (added-strand init 3) n-b (2 1)
    (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (label 11)
  (parent 6)
  (unrealized (2 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 0)) ((2 1) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (added-strand serv 3) k (2 0)
    (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((recv k) (send k)))
  (label 12)
  (parent 7)
  (unrealized (0 3) (2 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 n-a-1 text) (a b c a-0 b-0 c-0 name)
    (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (precedes ((0 1) (4 0)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 1) (1 0))
    ((3 2) (0 3)) ((4 1) (5 1)) ((5 2) (3 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand init 3) n-b (3 1)
    (enc a n-a n-b (ltk b c)) (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c)))))
    ((send (cat a-0 n-a-1)) (recv (enc b-0 k n-a-1 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0))))
  (label 13)
  (parent 8)
  (seen 15 17)
  (unrealized (3 1))
  (comment "4 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (2 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (displaced 5 2 resp 2) n-b-0 (3 1)
    (enc a n-a n-b-0 (ltk b c)) (enc b k-0 n-a n-b-0 (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c)))))
  (label 14)
  (parent 8)
  (seen 10 11 17)
  (unrealized (2 1))
  (comment "3 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 2) (0 3))
    ((3 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (n-a-0 n-a))
    n-b (2 1) (enc n-b k) (enc a n-a n-b (ltk b c))
    (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (label 15)
  (parent 11)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (3 1)) ((1 1) (4 0)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (added-listener k) n-b (2 1) (enc n-b k)
    (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))) ((recv k) (send k)))
  (label 16)
  (parent 11)
  (seen 19)
  (unrealized (4 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (2 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (displaced 6 2 resp 2) n-b-0 (3 1)
    (enc n-b-0 k-0) (enc a n-a n-b-0 (ltk b c))
    (enc b k-0 n-a n-b-0 (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0))))
  (label 17)
  (parent 13)
  (unrealized (2 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 n-a-1 text) (a b c a-0 b-0 c-0 name)
    (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (deflistener k-0)
  (precedes ((0 1) (4 0)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 1) (1 0))
    ((3 2) (0 3)) ((4 1) (5 1)) ((4 1) (6 0)) ((5 2) (3 1))
    ((6 1) (3 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-listener k-0) n-b (3 1) (enc n-b k-0)
    (enc a n-a n-b (ltk b c)) (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c)))))
    ((send (cat a-0 n-a-1)) (recv (enc b-0 k n-a-1 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0))) ((recv k-0) (send k-0)))
  (label 18)
  (parent 13)
  (seen 19 23)
  (unrealized (3 1) (6 0))
  (comment "3 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (3 1)) ((1 2) (0 2)) ((1 2) (4 0))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (added-strand serv 3) k (4 0)
    (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))) ((recv k) (send k)))
  (label 19)
  (parent 16)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b c name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (2 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (n-a-0 n-a))
    n-b (2 1) (enc n-b k-0) (enc a n-a n-b (ltk b c))
    (enc b k n-a n-b (ltk a c)) (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0))))
  (label 20)
  (parent 17)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (5 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1)) ((5 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand init 3) n-b (2 1) (enc n-b k-0)
    (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c))
    (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (label 21)
  (parent 17)
  (unrealized (2 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (2 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (4 1)) ((3 1) (5 0)) ((4 2) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-listener k-0) n-b (2 1) (enc n-b k-0)
    (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c))
    (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0))) ((recv k-0) (send k-0)))
  (label 22)
  (parent 17)
  (seen 19 28)
  (unrealized (2 1) (5 0))
  (comment "3 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 n-a-1 text) (a b c a-0 b-0 c-0 name)
    (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (deflistener k-0)
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (precedes ((0 1) (6 0)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 1) (1 0))
    ((3 2) (0 3)) ((4 2) (3 1)) ((5 1) (3 1)) ((6 1) (4 1))
    ((6 2) (5 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 3) k-0 (6 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c)))))
    ((send (cat a-0 n-a-1)) (recv (enc b-0 k n-a-1 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0))) ((recv k-0) (send k-0))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c)))
      (send (enc a k-0 (ltk b c)))))
  (label 23)
  (parent 18)
  (unrealized (3 1) (5 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b c name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (2 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation generalization deleted (4 0))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c)))))
  (label 24)
  (parent 20)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b c name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (5 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1)) ((5 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (n-a-0 n-a))
    n-b (2 1) (enc n-b k) (enc n-b k-0) (enc a n-a n-b (ltk b c))
    (enc b k n-a n-b (ltk a c)) (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (label 25)
  (parent 21)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (5 1)) ((1 1) (6 0))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1))
    ((5 2) (2 1)) ((6 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-listener k) n-b (2 1) (enc n-b k)
    (enc n-b k-0) (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c))
    (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))) ((recv k) (send k)))
  (label 26)
  (parent 21)
  (seen 30)
  (unrealized (6 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (5 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 1) (4 1)) ((3 1) (6 0)) ((4 2) (2 1))
    ((5 2) (2 1)) ((6 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-listener k-0) n-b (2 1) (enc n-b k)
    (enc n-b k-0) (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c))
    (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))) ((recv k-0) (send k-0)))
  (label 27)
  (parent 21)
  (seen 31 32)
  (unrealized (2 1) (6 0))
  (comment "3 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (deflistener k-0)
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (precedes ((0 1) (1 0)) ((0 1) (5 0)) ((1 1) (2 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (2 1)) ((5 1) (3 1))
    ((5 2) (4 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 3) k-0 (5 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0))) ((recv k-0) (send k-0))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c)))
      (send (enc a k-0 (ltk b c)))))
  (label 28)
  (parent 22)
  (unrealized (2 1) (4 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b c name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (4 1)) ((1 2) (0 2))
    ((2 1) (3 1)) ((3 2) (0 3)) ((4 2) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation generalization deleted (2 0))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (label 29)
  (parent 25)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (5 1)) ((1 2) (0 2))
    ((1 2) (6 0)) ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1))
    ((5 2) (2 1)) ((6 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 3) k (6 0)
    (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))) ((recv k) (send k)))
  (label 30)
  (parent 26)
  (unrealized (6 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (3 1)) ((1 1) (4 1)) ((1 2) (0 2))
    ((1 2) (5 0)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 2) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (displaced 3 7 serv 3) k (6 0)
    (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))) ((recv k) (send k)))
  (label 31)
  (parent 26)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand init 3 (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (deflistener k-0)
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (precedes ((0 1) (1 0)) ((0 1) (6 0)) ((1 1) (4 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 2) (2 1)) ((5 1) (2 1))
    ((6 1) (3 1)) ((6 2) (5 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 3) k-0 (6 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((send (cat a-0 n-a-0)) (recv (enc b-0 k n-a-0 n-b (ltk a-0 c-0)))
      (send (enc n-b k)))
    ((send (cat a n-a)) (recv (enc b k-0 n-a n-b (ltk a c)))
      (send (enc n-b k-0)))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))) ((recv k-0) (send k-0))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c)))
      (send (enc a k-0 (ltk b c)))))
  (label 32)
  (parent 27)
  (unrealized (2 1) (5 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b c name) (k k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (defstrand init 3 (n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((2 1) (0 3)) ((3 2) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation generalization deleted (3 0))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k-0 n-a n-b (ltk a c))))
    ((send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (label 33)
  (parent 29)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    (uniq-orig k)))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (deflistener k)
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k)))
    ((recv k) (send k)))
  (label 34)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 3) (enc a k (ltk b c))
    (0 2))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c)))
      (send (enc a k (ltk b c)))))
  (label 35)
  (parent 34)
  (unrealized (0 3) (1 0) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)) ((3 1) (2 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (2 0))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c))))))
  (label 36)
  (parent 35)
  (seen 38)
  (unrealized (0 3) (1 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)) ((2 2) (0 2)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation encryption-test (displaced 3 0 resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (2 0))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 37)
  (parent 35)
  (seen 39)
  (unrealized (0 3) (1 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((2 2) (0 2)) ((2 2) (1 0)) ((3 1) (2 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (added-strand serv 3) k (1 0)
    (enc b k n-a-0 n-b-0 (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c))))))
  (label 38)
  (parent 36)
  (unrealized (0 3) (1 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k))
  (precedes ((0 1) (2 0)) ((2 2) (0 2)) ((2 2) (1 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k)
  (operation nonce-test (added-strand serv 3) k (1 0)
    (enc b k n-a n-b (ltk a c)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 39)
  (parent 37)
  (unrealized (0 3) (1 0))
  (comment "empty cohort"))

(comment "Nothing left to do")