(herald
  "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function"
  (bound 12))
(comment "CPSA 3.4.0")
(comment "All input read from fnof_yahalom.scm")

Trees: 0 4 10 15.

Tree 0.

3 2 1 0 
(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (ltkac k skey))
    (trace (init (cat c ltkac)) (send (cat a n-a))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k)))
    (fn-of ("ltk" (ltkac (cat a c))) ("ltk-inv" ((cat a c) ltkac))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init (cat c ltkac)) (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc))) (recv (enc a k ltkbc))
      (recv (enc n-b k)))
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))
      ("ltk-inv" ((cat a c) ltkac) ((cat b c) ltkbc))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init c) (recv (cat b (enc a n-a n-b ltkbc)))
      (send (enc b k n-a n-b ltkac)) (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))
      ("ltk-inv" ((cat a c) ltkac) ((cat b c) ltkbc)))))

Item 0, Child: 1.

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

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

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

Item 2, Parent: 1.

(enc a k ltkbc) (enc b k n-a n-b ltkac) (cat b (enc a n-a n-b ltkbc)) c (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc)) (cat a n-a) (cat c ltkac) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom 2 (realized)
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 4 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (precedes ((0 2) (1 1)) ((1 3) (0 3)))
  (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))
    ("ltk-inv" ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 2 0 resp 3)
    (enc a n-a-0 n-b-0 ltkbc) (1 1))
  (label 2)
  (parent 1)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k (1 2)) (n-b (0 2))))

Item 3, Parent: 1.

(cat b (enc a n-a-0 n-b-0 ltkbc)) (cat a n-a-0) (cat c ltkac) (enc a k ltkbc) (enc b k n-a-0 n-b-0 ltkac) (cat b (enc a n-a-0 n-b-0 ltkbc)) c (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc)) (cat a n-a) (cat c ltkac) ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom 3 (realized)
(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 4 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b)
    (ltkac ltkac) (ltkbc ltkbc) (k k))
  (defstrand resp 3 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)
    (ltkac ltkac) (ltkbc ltkbc))
  (precedes ((1 3) (0 3)) ((2 2) (1 1)))
  (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))
    ("ltk-inv" ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 3)
    (enc a n-a-0 n-b-0 ltkbc) (1 1))
  (label 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k (1 2)) (n-b (0 2))))

Tree 4.

9 7 8 6 5 4 
(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (ltkac k skey))
    (trace (init (cat c ltkac)) (send (cat a n-a))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k)))
    (fn-of ("ltk" (ltkac (cat a c))) ("ltk-inv" ((cat a c) ltkac))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init (cat c ltkac)) (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc))) (recv (enc a k ltkbc))
      (recv (enc n-b k)))
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))
      ("ltk-inv" ((cat a c) ltkac) ((cat b c) ltkbc))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init c) (recv (cat b (enc a n-a n-b ltkbc)))
      (send (enc b k n-a n-b ltkac)) (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))
      ("ltk-inv" ((cat a c) ltkac) ((cat b c) ltkbc)))))

Item 4, Child: 5.

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

Item 5, Parent: 4, Children: 6 7.

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

Item 6, Parent: 5, Child: 8.

(enc a k ltkbc) (enc b k n-a n-b ltkac) (cat b (enc a n-a n-b ltkbc)) c k k (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc)) (cat a n-a) (cat c ltkac) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom 6 
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (precedes ((0 2) (2 1)) ((2 2) (1 0)) ((2 3) (0 3)))
  (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))
    ("ltk-inv" ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 3 0 resp 3)
    (enc a n-a-0 n-b-0 ltkbc) (2 1))
  (label 6)
  (parent 5)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 7, Parent: 5, Child: 9.

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

Item 8, Parent: 6.

(enc a k ltkbc) (enc b k n-a n-b ltkac) (cat b (enc a n-a n-b ltkbc)) c k k (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc)) (cat a n-a) (cat c ltkac) ((n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom 8 
(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (precedes ((0 2) (2 1)) ((2 3) (0 3)) ((2 3) (1 0)))
  (fn-of ("ltk" (ltkbc (cat b c)) (ltkac (cat a c)))
    ("ltk-inv" ((cat b c) ltkbc) ((cat a c) ltkac)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation nonce-test (displaced 3 2 serv 4) k (1 0)
    (enc b k n-a n-b ltkac))
  (label 8)
  (parent 6)
  (unrealized (1 0))
  (comment "empty cohort"))

Item 9, Parent: 7.

(cat b (enc a n-a-0 n-b-0 ltkbc)) (cat a n-a-0) (cat c ltkac) (enc a k ltkbc) (enc b k n-a-0 n-b-0 ltkac) (cat b (enc a n-a-0 n-b-0 ltkbc)) c k k (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc)) (cat a n-a) (cat c ltkac) ((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc)) resp ((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom 9 
(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b)
    (ltkac ltkac) (ltkbc ltkbc) (k k))
  (defstrand resp 3 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)
    (ltkac ltkac) (ltkbc ltkbc))
  (precedes ((2 3) (0 3)) ((2 3) (1 0)) ((3 2) (2 1)))
  (fn-of ("ltk" (ltkbc (cat b c)) (ltkac (cat a c)))
    ("ltk-inv" ((cat b c) ltkbc) ((cat a c) ltkac)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation nonce-test (displaced 4 2 serv 4) k (1 0)
    (enc b k n-a-0 n-b-0 ltkac))
  (label 9)
  (parent 7)
  (unrealized (1 0))
  (comment "empty cohort"))

Tree 10.

14 13 12 11 10 
(defprotocol yahalom2 basic
  (defrole init
    (vars (a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (send (cat a n-a (hash ltkbc)))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc) (hash c ltkac)))
      (recv (enc a k ltkbc)) (recv (enc n-b k)))
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat b (enc a n-a n-b ltkbc)))
      (send (cat (hash c) (enc b k n-a n-b ltkac)))
      (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c))))))

Item 10, Child: 11.

(enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 10 
(defskeleton yahalom2
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b)
  (label 10)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 11, Parent: 10, Children: 12 13.

(enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0)) (cat b-0 (enc a n-a-0 n-b-0 ltkbc)) (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 11 
(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((1 2) (0 2)))
  (fn-of
    ("ltk" (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 3) (enc a k ltkbc)
    (0 2))
  (label 11)
  (parent 10)
  (unrealized (0 3) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 12, Parent: 11.

(enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a n-b ltkac-0)) (cat b-0 (enc a n-a n-b ltkbc)) (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 12 (realized) 
(defskeleton yahalom2
  (vars (n-b n-a text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((0 1) (1 0)) ((1 2) (0 2)))
  (fn-of
    ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (1 0))
  (label 12)
  (parent 11)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k (1 1)) (n-b (0 1))))

Item 13, Parent: 11, Child: 14.

(cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1)) (cat a n-a-0) (enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0)) (cat b-0 (enc a n-a-0 n-b-0 ltkbc)) (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc)) resp ((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 13
(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (precedes ((1 2) (0 2)) ((2 1) (1 0)))
  (fn-of
    ("ltk" (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1))
      (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (1 0))
  (label 13)
  (parent 11)
  (unrealized (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 14, Parent: 13.

(cat (hash c-2) (enc b-2 k-0 n-a n-b ltkac-2)) (cat b-2 (enc a n-a n-b ltkbc)) (cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1)) (cat a n-a-0) (enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0)) (cat b-0 (enc a n-a-0 n-b-0 ltkbc)) (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2) (ltkac ltkac-2) (ltkbc ltkbc) (k k-0)) serv ((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc)) resp ((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 14 (realized) 
(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 c-2 b-2 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 ltkac-2 k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2)
    (ltkac ltkac-2) (ltkbc ltkbc) (k k-0))
  (precedes ((0 1) (3 0)) ((1 2) (0 2)) ((2 1) (1 0)) ((3 1) (0 3)))
  (fn-of
    ("ltk" (ltkac-2 (cat a c-2)) (ltkbc (cat b-2 c-2))
      (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0)) (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 2) n-b (0 3)
    (enc a n-a n-b ltkbc))
  (label 14)
  (parent 13)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k-0 (3 1)) (k (1 1)) (n-b (0 1))))

Tree 15.

19 18 17 16 15 
(defprotocol yahalom2 basic
  (defrole init
    (vars (a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (send (cat a n-a (hash ltkbc)))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc) (hash c ltkac)))
      (recv (enc a k ltkbc)) (recv (enc n-b k)))
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat b (enc a n-a n-b ltkbc)))
      (send (cat (hash c) (enc b k n-a n-b ltkac)))
      (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c))))))

Item 15, Child: 16.

k k (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 15 
(defskeleton yahalom2
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (fn-of ("ltk" (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b)
  (label 15)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 16, Parent: 15, Children: 17 18.

(enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0)) (cat b-0 (enc a n-a-0 n-b-0 ltkbc)) k k (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 16
(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)))
  (fn-of
    ("ltk" (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 3) (enc a k ltkbc)
    (0 2))
  (label 16)
  (parent 15)
  (unrealized (0 3) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 17, Parent: 16.

(enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a n-b ltkac-0)) (cat b-0 (enc a n-a n-b ltkbc)) k k (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 17 (realized) 
(defskeleton yahalom2
  (vars (n-b n-a text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)) ((2 2) (0 2)))
  (fn-of
    ("ltk" (ltkac (cat a c)) (ltkbc (cat b c)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 3 0 resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (2 0))
  (label 17)
  (parent 16)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (k k)
        (n-a n-a))))
  (origs (k (2 1)) (n-b (0 1))))

Item 18, Parent: 16, Child: 19.

(cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1)) (cat a n-a-0) (enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0)) (cat b-0 (enc a n-a-0 n-b-0 ltkbc)) k k (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc)) resp ((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 18
(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)) ((3 1) (2 0)))
  (fn-of
    ("ltk" (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1))
      (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (2 0))
  (label 18)
  (parent 16)
  (unrealized (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 19, Parent: 18.

(cat (hash c-2) (enc b-2 k-0 n-a n-b ltkac-2)) (cat b-2 (enc a n-a n-b ltkbc)) (cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1)) (cat a n-a-0) (enc a k ltkbc) (cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0)) (cat b-0 (enc a n-a-0 n-b-0 ltkbc)) k k (enc n-b k) (enc a k ltkbc) (cat b (enc a n-a n-b ltkbc) (hash c ltkac)) (cat a n-a) ((n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2) (ltkac ltkac-2) (ltkbc ltkbc) (k k-0)) serv ((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc)) resp ((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k)) serv ((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k)) resp yahalom2 19 (realized) 
(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 c-2 b-2 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 ltkac-2 k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2)
    (ltkac ltkac-2) (ltkbc ltkbc) (k k-0))
  (precedes ((0 1) (4 0)) ((2 1) (1 0)) ((2 2) (0 2)) ((3 1) (2 0))
    ((4 1) (0 3)))
  (fn-of
    ("ltk" (ltkac-2 (cat a c-2)) (ltkbc (cat b-2 c-2))
      (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0)) (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 2) n-b (0 3)
    (enc a n-a n-b ltkbc))
  (label 19)
  (parent 18)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (k k)
        (n-a n-a))))
  (origs (k-0 (4 1)) (k (2 1)) (n-b (0 1))))