(herald "Yahalom Protocol"
  (comment "A Survey of Authentication Protocol Literature:"
    "Version 1.0, John Clark and Jeremy Jacob,"
    "Yahalom Protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")
  (bound 15))

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

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (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))))
  (comment "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

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

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

(defskeleton yahalom
  (vars (blob mesg) (k skey) (n-a n-b text) (a b s name))
  (defstrand init 3 (blob blob) (k k) (n-a n-a) (n-b n-b) (a a) (b b)
    (s s))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a n-b (ltk b s)) (1 0))
  (traces
    ((send (cat a n-a)) (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k))))
    ((recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))))
  (label 2)
  (parent 1)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k) (blob blob))))
  (origs (k (1 1)) (n-a (0 0)) (n-b (2 1))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (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))))
  (comment "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

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

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

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

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

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (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))))
  (comment "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

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

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

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

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

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

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

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

(defskeleton yahalom
  (vars (k skey) (n-a n-b n-a-0 n-b-0 text) (a b s name))
  (defstrand resp 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand serv 2 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s))
  (deflistener k)
  (precedes ((1 1) (3 0)) ((2 1) (1 0)) ((3 1) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (operation encryption-test (added-listener k) (enc n-b k) (0 2))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k))))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b s))))
      (send (cat (enc b k n-a-0 n-b-0 (ltk a s)) (enc a k (ltk b s)))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b s)))))
    ((recv k) (send k)))
  (label 14)
  (parent 10)
  (unrealized (0 2) (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (blob mesg) (k skey) (n-a n-b text) (a b s name))
  (defstrand resp 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand init 3 (blob blob) (k k) (n-a n-a) (n-b n-b) (a a) (b b)
    (s s))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (s-0 s) (n-a-0 n-a))
    n-b (2 1) (enc a n-a n-b (ltk b s)) (enc b k n-a n-b (ltk a s)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k))))
    ((recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    ((send (cat a n-a)) (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (label 15)
  (parent 11)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k))))
  (origs (k (1 1)) (n-a (2 0)) (n-b (0 1))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (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))))
  (comment "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

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

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b s name))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (precedes ((1 1) (0 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a n-b (ltk b s)) (0 0))
  (traces
    ((recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))))
  (label 32)
  (parent 31)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k))))
  (origs (k (0 1)) (n-b (1 1))))

(comment "Nothing left to do")