(herald "Yahalom Protocol with Forwarding Removed"
  (algebra diffie-hellman) (bound 12))
(comment "CPSA 3.4.0")
(comment "All input read from yahalom.scm")

Trees: 0 52.

Tree 0.

13 7 38 27 47 37 26 18 12 6 3 11 5 36 25 46 35 16 45 34 30 24 16 23 20 17 8 16 14 10 22 15 33 21 44 32 43 31 50 42 49 41 28 51 48 40 30 28 39 29 20 8 28 19 14 8 9 8 4 2 1 0 
(defprotocol yahalom diffie-hellman
  (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)))

Item 0, Child: 1.

(enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 0 
(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)
  (label 0)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 1, Parent: 0, Children: 2 3.

(enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 1 
(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))
  (label 1)
  (parent 0)
  (unrealized (0 3) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 2, Parent: 1, Children: 4 5.

(enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 2 
(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))
  (label 2)
  (parent 1)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 3, Parent: 1, Children: 6 7.

(cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 3 
(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))
  (label 3)
  (parent 1)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 4, Parent: 2, Children: 8 9 10.

(enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 4 
(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))
  (label 4)
  (parent 2)
  (unrealized (2 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 5, Parent: 2, Child: 11.

k k (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 5 
(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))
  (label 5)
  (parent 2)
  (unrealized (0 3) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 6, Parent: 3, Child: 12.

(enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 6 
(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))
  (label 6)
  (parent 3)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 7, Parent: 3, Child: 13.

k k (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 7 
(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))
  (label 7)
  (parent 3)
  (unrealized (0 3) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 8, Parent: 4.

(enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 8 (realized)
(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)))
  (label 8)
  (parent 4)
  (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))))

Item 9, Parent: 4, Children: 14 15, Seen Child: 8.

(enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 9 
(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)))
  (label 9)
  (parent 4)
  (seen 8)
  (unrealized (2 1))
  (comment "3 in cohort - 2 not yet seen"))

Item 10, Parent: 4, Children: 16 17, Seen Child: 14.

(enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 10 
(defskeleton yahalom
  (vars (n-b n-a 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 (added-strand serv 2) n-b (2 1)
    (enc a n-a n-b (ltk b c)) (enc b k n-a n-b (ltk a c)))
  (label 10)
  (parent 4)
  (seen 14)
  (unrealized (2 1))
  (comment "3 in cohort - 2 not yet seen"))

Item 11, Parent: 5.

k k (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 11 
(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 (displaced 3 1 serv 3) k (2 0)
    (enc b k n-a n-b (ltk a c)))
  (label 11)
  (parent 5)
  (unrealized (0 3) (2 0))
  (comment "empty cohort"))

Item 12, Parent: 6, Child: 18.

(enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 12 
(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)))
  (label 12)
  (parent 6)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 13, Parent: 7.

k k (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 13 
(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 (displaced 4 1 serv 3) k (3 0)
    (enc b k n-a-0 n-b-0 (ltk a c)))
  (label 13)
  (parent 7)
  (unrealized (0 3) (3 0))
  (comment "empty cohort"))

Item 14, Parent: 9, Children: 19 20 21.

(enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 14 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (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) (4 0)) ((1 1) (3 1)) ((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 k-0)
  (operation nonce-test (added-strand serv 2) 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)))
  (label 14)
  (parent 9)
  (unrealized (2 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 15, Parent: 9, Child: 22.

k k (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 15 
(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)))
  (label 15)
  (parent 9)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 16, Parent: 10, Seen Child: 8.

(enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 16 (realized)
(defskeleton yahalom
  (vars (n-b n-a 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 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))
    (enc b k-0 n-a n-b (ltk a c)))
  (label 16)
  (parent 10)
  (seen 8)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 17, Parent: 10, Children: 23 24 25, Seen Child: 20.

(enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 17 
(defskeleton yahalom
  (vars (n-b n-a 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 (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))
    (enc b k-0 n-a n-b (ltk a c)))
  (label 17)
  (parent 10)
  (seen 20)
  (unrealized (2 1))
  (comment "4 in cohort - 3 not yet seen"))

Item 18, Parent: 12, Children: 26 27.

(enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 18 
(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)))
  (label 18)
  (parent 12)
  (unrealized (3 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 19, Parent: 14, Child: 28.

(enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 19 (realized)
(defskeleton yahalom
  (vars (n-b n-a 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 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) (4 0)) ((1 1) (3 1)) ((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 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 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)))
  (label 19)
  (parent 14)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 20, Parent: 14, Children: 29 30 31 32.

(enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 20 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (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) (4 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 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)
    (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)))
  (label 20)
  (parent 14)
  (unrealized (2 1))
  (comment "4 in cohort - 4 not yet seen"))

Item 21, Parent: 14, Child: 33.

k k (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 21 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (3 1)) ((1 1) (5 0))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (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) 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))
    (enc b k-0 n-a n-b (ltk a c)))
  (label 21)
  (parent 14)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 22, Parent: 15.

k k (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 22 
(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 (displaced 5 1 serv 3) k (4 0)
    (enc b k n-a n-b (ltk a c)))
  (label 22)
  (parent 15)
  (unrealized (4 0))
  (comment "empty cohort"))

Item 23, Parent: 17, Seen Child: 16.

(enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 23 (realized)
(defskeleton yahalom
  (vars (n-b n-a 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)))
  (label 23)
  (parent 17)
  (seen 16)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 24, Parent: 17, Children: 34 35, Seen Child: 30.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 24 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (2 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation nonce-test (added-strand serv 2) 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)))
  (label 24)
  (parent 17)
  (seen 30)
  (unrealized (2 1))
  (comment "3 in cohort - 2 not yet seen"))

Item 25, Parent: 17, Child: 36.

k-0 k-0 (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 25 
(defskeleton yahalom
  (vars (n-b n-a 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)))
  (label 25)
  (parent 17)
  (unrealized (2 1) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 26, Parent: 18, Child: 37.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 26 
(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 k-1 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))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (4 0)) ((0 1) (6 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))
    ((6 1) (3 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation nonce-test (added-strand serv 2) 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)))
  (label 26)
  (parent 18)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 27, Parent: 18, Child: 38.

k-0 k-0 (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 27 
(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)))
  (label 27)
  (parent 18)
  (unrealized (3 1) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 28, Parent: 19, Seen Child: 8.

(enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 28 (realized)
(defskeleton yahalom
  (vars (n-b n-a 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) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation generalization deleted (2 0))
  (label 28)
  (parent 19)
  (seen 8)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 29, Parent: 20, Child: 39.

(enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 29 (realized)
(defskeleton yahalom
  (vars (n-b n-a 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 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) (4 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 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)))
  (label 29)
  (parent 20)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 30, Parent: 20, Children: 40 41 42.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 30 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (3 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 1))
    ((5 2) (2 1)) ((6 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation nonce-test (added-strand serv 2) 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)))
  (label 30)
  (parent 20)
  (unrealized (2 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 31, Parent: 20, Child: 43.

k k (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 31 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (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)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (3 1)) ((1 1) (6 0))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 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)))
  (label 31)
  (parent 20)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 32, Parent: 20, Child: 44.

k-0 k-0 (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 32 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (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) (4 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 1)) ((4 1) (6 0))
    ((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)))
  (label 32)
  (parent 20)
  (unrealized (2 1) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 33, Parent: 21.

k k (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 33 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((1 2) (5 0)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation nonce-test (displaced 6 1 serv 3) k (5 0)
    (enc b k n-a n-b (ltk a c)))
  (label 33)
  (parent 21)
  (unrealized (5 0))
  (comment "empty cohort"))

Item 34, Parent: 24, Child: 45.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 34 (realized)
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k k-0 k-1 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (2 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (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))
    (enc b k-1 n-a n-b (ltk a c)))
  (label 34)
  (parent 24)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 35, Parent: 24, Child: 46.

k-0 k-0 (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 35 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (2 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 1) (4 1)) ((3 1) (6 0))
    ((4 2) (2 1)) ((5 1) (2 1)) ((6 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (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)) (enc b k-1 n-a n-b (ltk a c)))
  (label 35)
  (parent 24)
  (unrealized (2 1) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 36, Parent: 25.

(enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k-0 k-0 (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 36 
(defskeleton yahalom
  (vars (n-b n-a 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 (displaced 3 6 serv 3) k-0 (5 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (label 36)
  (parent 25)
  (unrealized (2 1) (4 0))
  (comment "empty cohort"))

Item 37, Parent: 26, Child: 47.

k-0 k-0 (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 37 
(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 k-1 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))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (deflistener k-0)
  (precedes ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((2 1) (1 0)) ((3 2) (0 3)) ((4 1) (5 1)) ((4 1) (7 0))
    ((5 2) (3 1)) ((6 1) (3 1)) ((7 1) (3 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (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))
    (enc b k-1 n-a n-b (ltk a c)))
  (label 37)
  (parent 26)
  (unrealized (3 1) (7 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 38, Parent: 27.

(enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k-0 k-0 (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 38 
(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 (displaced 4 7 serv 3) k-0 (6 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (label 38)
  (parent 27)
  (unrealized (3 1) (5 0))
  (comment "empty cohort"))

Item 39, Parent: 29, Seen Child: 28.

(enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 39 (realized)
(defskeleton yahalom
  (vars (n-b n-a 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) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0)
  (operation generalization deleted (2 0))
  (label 39)
  (parent 29)
  (seen 28)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 40, Parent: 30, Child: 48.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 40 (realized)
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k k-0 k-1 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))
  (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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (3 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 1))
    ((5 2) (2 1)) ((6 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (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))
    (enc b k-1 n-a n-b (ltk a c)))
  (label 40)
  (parent 30)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 41, Parent: 30, Child: 49.

k k (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 41 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (3 1))
    ((1 1) (7 0)) ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1))
    ((4 1) (5 1)) ((5 2) (2 1)) ((6 1) (2 1)) ((7 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (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)) (enc b k-1 n-a n-b (ltk a c)))
  (label 41)
  (parent 30)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 42, Parent: 30, Child: 50.

k-0 k-0 (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 42 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (3 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 1))
    ((4 1) (7 0)) ((5 2) (2 1)) ((6 1) (2 1)) ((7 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (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)) (enc b k-1 n-a n-b (ltk a c)))
  (label 42)
  (parent 30)
  (unrealized (2 1) (7 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 43, Parent: 31.

k k (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 43 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (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)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((1 2) (6 0)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (5 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 (displaced 7 1 serv 3) k (6 0)
    (enc b k n-a n-b (ltk a c)))
  (label 43)
  (parent 31)
  (unrealized (6 0))
  (comment "empty cohort"))

Item 44, Parent: 32.

(enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k-0 k-0 (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 44 
(defskeleton yahalom
  (vars (n-b n-a 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))
  (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) (6 0)) ((1 1) (3 1)) ((1 2) (0 2))
    ((2 2) (0 3)) ((3 2) (2 1)) ((4 2) (2 1)) ((5 1) (2 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 (displaced 4 7 serv 3) k-0 (6 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (label 44)
  (parent 32)
  (unrealized (2 1) (5 0))
  (comment "empty cohort"))

Item 45, Parent: 34, Seen Child: 16.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 45 (realized)
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k k-0 k-1 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (4 0)) ((1 1) (2 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 1) (2 1)) ((4 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation generalization deleted (4 0))
  (label 45)
  (parent 34)
  (seen 16)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 46, Parent: 35.

(enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k-0 k-0 (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 46 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (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) (4 0)) ((0 1) (6 0)) ((1 1) (2 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 1) (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 k-1)
  (operation nonce-test (displaced 3 7 serv 3) k-0 (6 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (label 46)
  (parent 35)
  (unrealized (2 1) (5 0))
  (comment "empty cohort"))

Item 47, Parent: 37.

(enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k-0 k-0 (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-1 n-b (ltk a-0 c-0)) (cat a-0 n-a-1) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 47 
(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 k-1 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))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (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) (5 0)) ((0 1) (7 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) (3 1)) ((7 1) (4 1)) ((7 2) (6 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation nonce-test (displaced 4 8 serv 3) k-0 (7 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (label 47)
  (parent 37)
  (unrealized (3 1) (6 0))
  (comment "empty cohort"))

Item 48, Parent: 40, Child: 51.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 48 (realized)
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k k-0 k-1 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (2 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 1) (4 1)) ((4 2) (0 3))
    ((5 1) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation generalization deleted (2 0))
  (label 48)
  (parent 40)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 49, Parent: 41.

k k (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 49 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (3 1))
    ((1 2) (0 2)) ((1 2) (7 0)) ((2 2) (0 3)) ((3 2) (2 1))
    ((4 1) (5 1)) ((5 2) (2 1)) ((6 1) (2 1)) ((7 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation nonce-test (displaced 8 1 serv 3) k (7 0)
    (enc b k n-a n-b (ltk a c)))
  (label 49)
  (parent 41)
  (unrealized (7 0))
  (comment "empty cohort"))

Item 50, Parent: 42.

(enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k-0 k-0 (enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k-0) (enc b k-0 n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc n-b k) (enc b-0 k n-a-0 n-b (ltk a-0 c-0)) (cat a-0 n-a-0) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k-0)) init ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 50 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k k-0 k-1 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-0))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (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)) ((0 1) (7 0)) ((1 1) (3 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 2) (2 1)) ((4 2) (2 1))
    ((5 1) (2 1)) ((6 1) (2 1)) ((7 1) (4 1)) ((7 2) (6 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation nonce-test (displaced 4 8 serv 3) k-0 (7 0)
    (enc b k-0 n-a n-b (ltk a c)))
  (label 50)
  (parent 42)
  (unrealized (2 1) (6 0))
  (comment "empty cohort"))

Item 51, Parent: 48, Seen Child: 28.

(enc b k-1 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc b k-0 n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc b k n-a n-b (ltk a c)) (cat a n-a) (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1)) serv ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-0)) serv ((n-a n-a) (n-b n-b) (a a) (b b) (c c) (k k)) init ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 51 (realized)
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (k k-0 k-1 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 serv 2 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k-1))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (4 0)) ((1 1) (2 1))
    ((1 2) (0 2)) ((2 2) (0 3)) ((3 1) (0 3)) ((4 1) (0 3)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig n-b k k-0 k-1)
  (operation generalization deleted (4 0))
  (label 51)
  (parent 48)
  (seen 28)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Tree 52.

57 55 56 54 53 52 
(defprotocol yahalom diffie-hellman
  (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)))

Item 52, Child: 53.

k k (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 52 
(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)
  (label 52)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 53, Parent: 52, Children: 54 55.

(enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) k k (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 53 
(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))
  (label 53)
  (parent 52)
  (unrealized (0 3) (1 0) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 54, Parent: 53, Child: 56.

(enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k k (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 54 
(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))
  (label 54)
  (parent 53)
  (unrealized (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 55, Parent: 53, Child: 57.

(cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) k k (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 55 
(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))
  (label 55)
  (parent 53)
  (unrealized (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 56, Parent: 54.

(enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)) (cat b (enc a n-a n-b (ltk b c))) k k (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 56 
(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 (displaced 3 2 serv 3) k (1 0)
    (enc b k n-a n-b (ltk a c)))
  (label 56)
  (parent 54)
  (unrealized (0 3) (1 0))
  (comment "empty cohort"))

Item 57, Parent: 55.

(cat b (enc a n-a-0 n-b-0 (ltk b c))) (cat a n-a-0) (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a c)) (cat b (enc a n-a-0 n-b-0 (ltk b c))) k k (enc n-b k) (enc a k (ltk b c)) (cat b (enc a n-a n-b (ltk b c))) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (k k)) resp yahalom 57 
(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 (displaced 4 2 serv 3) k (1 0)
    (enc b k n-a-0 n-b-0 (ltk a c)))
  (label 57)
  (parent 55)
  (unrealized (0 3) (1 0))
  (comment "empty cohort"))