(herald "Yahalom Protocol With Forwarding" (bound 15))

(comment "CPSA 4.4.7")
(comment "All input read from tst/yahalom-forward.scm")
(comment "Strand count bounded at 15")

(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) (rest mesg) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (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 (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)))))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (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 (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k))))
  (label 0)
  (unrealized (0 2) (0 4))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

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

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

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

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (2 1)) ((2 2) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-b)
  (operation encryption-test (added-strand init 3) (enc n-b k) (0 4))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 4)
  (parent 2)
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "3 in cohort - 3 not yet seen"))

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

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (3 1)) ((1 1) (0 2)) ((1 1) (3 1)) ((2 1) (1 0))
    ((3 2) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-b)
  (operation encryption-test (added-strand init 3) (enc n-b k) (0 4))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a 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 6)
  (parent 3)
  (unrealized (3 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (deflistener k)
  (precedes ((1 1) (0 2)) ((1 1) (3 0)) ((2 1) (1 0)) ((3 1) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-b)
  (operation encryption-test (added-listener k) (enc n-b k) (0 4))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a 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 7)
  (parent 3)
  (unrealized (0 4) (3 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (2 1)) ((2 2) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-b)
  (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)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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 8)
  (parent 4)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (origs (k (1 1)) (n-b (0 1))))

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (3 1)) ((2 2) (0 4))
    ((3 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-b)
  (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)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 9)
  (parent 4)
  (seen 8)
  (seen-ops
    (8
      (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))) (strand-map 0 1 2 2)))
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((1 1) (2 1))
    ((2 2) (0 4)) ((3 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c))))))
  (label 10)
  (parent 4)
  (seen 12)
  (seen-ops
    (12
      (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))) (strand-map 0 1 2 3)))
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "3 in cohort - 2 not yet seen"))

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

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((2 2) (0 4)) ((3 2) (2 1)) ((4 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c))))))
  (label 12)
  (parent 9)
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (3 1)) ((1 1) (4 0))
    ((2 2) (0 4)) ((3 2) (2 1)) ((4 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-b)
  (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)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 13)
  (parent 9)
  (unrealized (4 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((1 1) (2 1))
    ((2 2) (0 4)) ((3 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c))))))
  (label 14)
  (parent 10)
  (seen 8)
  (seen-ops
    (8 (operation generalization deleted (3 0)) (strand-map 0 1 2)))
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((1 1) (2 1))
    ((2 2) (0 4)) ((3 1) (4 1)) ((4 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 15)
  (parent 10)
  (seen 18)
  (seen-ops
    (18
      (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)))
      (strand-map 0 1 2 3 4)))
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1)) ((2 1) (1 0))
    ((3 2) (0 4)) ((4 1) (5 1)) ((5 2) (3 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 16)
  (parent 11)
  (unrealized (3 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((2 2) (0 4)) ((3 2) (2 1)) ((4 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((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 (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c))))))
  (label 17)
  (parent 12)
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((2 2) (0 4)) ((3 2) (2 1)) ((4 1) (5 1)) ((5 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 18)
  (parent 12)
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((1 1) (5 0)) ((2 2) (0 4)) ((3 2) (2 1)) ((4 1) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)))))
    ((recv k) (send k)))
  (label 19)
  (parent 12)
  (unrealized (5 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((1 1) (2 1))
    ((2 2) (0 4)) ((3 1) (4 1)) ((4 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 15)
  (seen 14)
  (seen-ops
    (14 (operation generalization deleted (4 0)) (strand-map 0 1 2 3)))
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (0 2))
    ((1 1) (2 1)) ((2 2) (0 4)) ((3 1) (4 1)) ((4 2) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 21)
  (parent 15)
  (seen 26)
  (seen-ops
    (26
      (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))
        (enc b k-1 n-a n-b (ltk a c))) (strand-map 0 1 2 3 4 5)))
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((1 1) (2 1))
    ((2 2) (0 4)) ((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 k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 15)
  (unrealized (2 1) (5 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((2 1) (1 0)) ((3 2) (0 4)) ((4 1) (5 1)) ((5 2) (3 1))
    ((6 1) (3 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 23)
  (parent 16)
  (unrealized (3 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (deflistener k-0)
  (precedes ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1)) ((2 1) (1 0))
    ((3 2) (0 4)) ((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 k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 24)
  (parent 16)
  (unrealized (3 1) (6 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((1 1) (2 1))
    ((2 2) (0 4)) ((3 1) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (operation generalization deleted (2 0))
  (strand-map 0 1 3 4)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c))))))
  (label 25)
  (parent 17)
  (seen 8)
  (seen-ops
    (8 (operation generalization deleted (3 0)) (strand-map 0 1 2)))
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2))
    ((1 1) (3 1)) ((2 2) (0 4)) ((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 k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 26)
  (parent 18)
  (unrealized (2 1))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((2 2) (0 4)) ((3 2) (2 1)) ((4 1) (5 1)) ((5 2) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((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 (cat (enc a k-0 (ltk b c)) (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 27)
  (parent 18)
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((1 1) (6 0)) ((2 2) (0 4)) ((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 k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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) (send k)))
  (label 28)
  (parent 18)
  (unrealized (6 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((2 2) (0 4)) ((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 k k-0 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 29)
  (parent 18)
  (unrealized (2 1) (6 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (0 2))
    ((1 1) (2 1)) ((2 2) (0 4)) ((3 1) (4 1)) ((4 2) (2 1))
    ((5 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 30)
  (parent 21)
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (0 2))
    ((1 1) (2 1)) ((2 2) (0 4)) ((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 k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c)))))
    ((recv k-0) (send k-0)))
  (label 31)
  (parent 21)
  (unrealized (2 1) (6 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k-0)
  (precedes ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2)) ((1 1) (3 1))
    ((2 1) (1 0)) ((3 2) (0 4)) ((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 k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a-0 n-b-0 (ltk a 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 (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c)))))
    ((recv k-0) (send k-0)))
  (label 32)
  (parent 23)
  (unrealized (3 1) (7 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2))
    ((1 1) (3 1)) ((2 2) (0 4)) ((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 k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((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 (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 33)
  (parent 26)
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2))
    ((1 1) (3 1)) ((1 1) (7 0)) ((2 2) (0 4)) ((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 k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c)))))
    ((recv k) (send k)))
  (label 34)
  (parent 26)
  (unrealized (7 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a n-a-0 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k-0)
  (precedes ((0 1) (1 0)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2))
    ((1 1) (3 1)) ((2 2) (0 4)) ((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 k k-0 k-1 n-b)
  (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)))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a 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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c)))))
    ((recv k-0) (send k-0)))
  (label 35)
  (parent 26)
  (unrealized (2 1) (7 0))
  (dead)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((1 1) (2 1))
    ((2 2) (0 4)) ((3 1) (4 1)) ((4 2) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 n-b)
  (operation generalization deleted (2 0))
  (strand-map 0 1 3 4 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 36)
  (parent 27)
  (seen 25)
  (seen-ops
    (25 (operation generalization deleted (4 0)) (strand-map 0 1 2 3)))
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((1 1) (2 1)) ((2 2) (0 4)) ((3 1) (2 1)) ((4 1) (2 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 k-1 n-b)
  (operation generalization deleted (4 0))
  (strand-map 0 1 2 3 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)))))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 37)
  (parent 30)
  (seen 14)
  (seen-ops
    (14 (operation generalization deleted (3 0)) (strand-map 0 1 2 4)))
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k-0) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (0 2))
    ((1 1) (2 1)) ((2 2) (0 4)) ((3 1) (4 1)) ((4 2) (0 4))
    ((5 1) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 k-1 n-b)
  (operation generalization deleted (2 0))
  (strand-map 0 1 3 4 5 6)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (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 (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 38)
  (parent 33)
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (rest mesg) (k k-0 k-1 skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k-0) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand serv 2 (k k-1) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((1 1) (2 1)) ((2 2) (0 4)) ((3 1) (0 4)) ((4 1) (0 4)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k k-0 k-1 n-b)
  (operation generalization deleted (4 0))
  (strand-map 0 1 2 3 5)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k 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)))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-0 (ltk b c)) (enc b k-0 n-a n-b (ltk a c)))))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k-1 (ltk b c)) (enc b k-1 n-a n-b (ltk a c))))))
  (label 39)
  (parent 38)
  (seen 25)
  (seen-ops
    (25 (operation generalization deleted (3 0)) (strand-map 0 1 2 4)))
  (realized)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (rest rest) (k k))))
  (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) (rest mesg) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (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 (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)))))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (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 (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k))) ((recv k) (send k)))
  (label 40)
  (unrealized (0 2) (0 4))
  (maps
    ((0 1) ((a a) (b b) (c c) (n-b n-b) (k k) (n-a n-a) (rest rest))))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton yahalom
  (vars (rest mesg) (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 5 (rest rest) (k k) (n-a n-a) (n-b n-b) (b b) (a a)
    (c c))
  (deflistener k)
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (2 0)) ((2 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-b)
  (operation encryption-test (displaced 3 0 resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c))))))
  (label 42)
  (parent 41)
  (unrealized (0 4) (1 0))
  (dead)
  (maps
    ((0 1) ((a a) (b b) (c c) (n-b n-b) (k k) (n-a n-a) (rest rest))))
  (comment "empty cohort"))

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

(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) (rest mesg) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (cat (enc a k (ltk b c)) rest)) (send rest)
      (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 (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)))))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

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

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b c name))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-a)
  (operation encryption-test (added-strand serv 2)
    (enc b k n-a n-b (ltk a c)) (0 1))
  (strand-map 0)
  (traces
    ((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 (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c))))))
  (label 45)
  (parent 44)
  (unrealized (1 0))
  (maps ((0) ((a a) (b b) (c c) (n-a n-a) (n-b n-b) (k k))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b c name))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k n-a)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a n-b (ltk b c)) (1 0))
  (strand-map 0 1)
  (traces
    ((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 (cat (enc a k (ltk b c)) (enc b k n-a n-b (ltk a c)))))
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))))
  (label 46)
  (parent 45)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (c c) (n-a n-a) (n-b n-b) (k k))))
  (origs (k (1 1)) (n-a (0 0))))

(comment "Nothing left to do")