(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"))

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

(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))
  (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) (n-a n-b text) (a b s name) (k skey))
  (defstrand init 3 (blob blob) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k))
  (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))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (blob mesg) (n-a n-b text) (a b s name) (k skey))
  (defstrand init 3 (blob blob) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b k)
  (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) (n-a n-b text) (a b s name) (k skey))
  (defstrand init 3 (blob blob) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (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 n-a n-b k)
  (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)
  (unrealized)
  (shape))

(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))
  (comment "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (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))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 n-b-0 text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (deflistener k)
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (precedes ((2 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b k)
  (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 (n-a n-b n-a-0 n-b-0 text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (deflistener k)
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (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 n-a n-b k)
  (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 5)
  (parent 4)
  (unrealized (0 2) (1 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (deflistener k)
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (precedes ((0 1) (2 0)) ((2 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b k)
  (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 6)
  (parent 4)
  (unrealized (0 2) (1 0))
  (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))
  (comment "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k 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)))))
  (label 7)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 n-b-0 text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (precedes ((1 1) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b k)
  (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 (n-a n-b n-a-0 n-b-0 text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (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 n-a n-b k)
  (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 9)
  (parent 8)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b k)
  (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 10)
  (parent 8)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (blob mesg) (n-a n-b n-a-0 n-b-0 n-a-1 text)
    (a b s a-0 b-0 s-0 name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s))
  (defstrand init 3 (blob blob) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (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 n-a n-b k)
  (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 11)
  (parent 9)
  (seen 13)
  (unrealized (3 1))
  (comment "3 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b n-a-0 n-b-0 text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (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 n-a n-b k)
  (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 12)
  (parent 9)
  (unrealized (0 2) (3 0))
  (comment "empty cohort"))

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

(defskeleton yahalom
  (vars (n-a n-b text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (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 n-a n-b k)
  (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 14)
  (parent 10)
  (unrealized (0 2) (2 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (blob mesg) (n-a n-b n-a-0 n-b-0 n-a-1 text)
    (a b s a-0 b-0 s-0 name) (k k-0 skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s))
  (defstrand init 3 (blob blob) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k-0))
  (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 n-a n-b k k-0)
  (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 15)
  (parent 11)
  (seen 16)
  (unrealized (3 1))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (blob mesg) (n-a n-b text) (a b s name) (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand init 3 (blob blob) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k))
  (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 n-a n-b k)
  (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 16)
  (parent 13)
  (unrealized)
  (shape))

(defskeleton yahalom
  (vars (blob blob-0 mesg) (n-a n-b n-a-0 text) (a b s a-0 b-0 s-0 name)
    (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand init 3 (blob blob) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (defstrand init 3 (blob blob-0) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k))
  (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 n-a n-b k)
  (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 17)
  (parent 13)
  (unrealized (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (blob blob-0 mesg) (n-a n-b n-a-0 n-b-0 n-a-1 text)
    (a b s a-0 b-0 s-0 name) (k k-0 skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s))
  (defstrand init 3 (blob blob) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k-0))
  (defstrand init 3 (blob blob-0) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k-0))
  (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 n-a n-b k k-0)
  (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 18)
  (parent 15)
  (seen 20)
  (unrealized (3 1))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (blob blob-0 mesg) (n-a n-b n-a-0 text) (a b s a-0 b-0 s-0 name)
    (k skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand init 3 (blob blob) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (defstrand init 3 (blob blob-0) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k))
  (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 n-a n-b k)
  (operation nonce-test (added-listener k) n-b (2 1) (enc n-b k)
    (enc a n-a n-b (ltk b 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 19)
  (parent 17)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (blob blob-0 mesg) (n-a n-b n-a-0 text) (a b s a-0 b-0 s-0 name)
    (k k-0 skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand init 3 (blob blob) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k-0))
  (defstrand init 3 (blob blob-0) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k-0))
  (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 n-a n-b k k-0)
  (operation nonce-test (displaced 6 2 resp 2) n-b-0 (3 1)
    (enc n-b-0 k-0) (enc a n-a n-b-0 (ltk b s))
    (enc b k-0 n-a n-b-0 (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 20)
  (parent 18)
  (unrealized (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (blob blob-0 mesg) (n-a n-b n-a-0 n-b-0 n-a-1 text)
    (a b s a-0 b-0 s-0 name) (k k-0 skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (a a) (b b) (s s))
  (defstrand init 3 (blob blob) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k-0))
  (defstrand init 3 (blob blob-0) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k-0))
  (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 n-a n-b k k-0)
  (operation nonce-test (added-listener k-0) n-b (3 1) (enc n-b k-0)
    (enc a n-a n-b (ltk b 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 21)
  (parent 18)
  (unrealized (3 1) (6 0))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (blob blob-0 mesg) (n-a n-b n-a-0 text) (a b s a-0 b-0 s-0 name)
    (k k-0 skey))
  (defstrand resp 3 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (defstrand init 3 (blob blob) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0)
    (s s-0) (k k))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k-0))
  (defstrand init 3 (blob blob-0) (n-a n-a) (n-b n-b) (a a) (b b) (s s)
    (k k-0))
  (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 n-a n-b k k-0)
  (operation nonce-test (added-listener k-0) n-b (2 1) (enc n-b k-0)
    (enc a n-a n-b (ltk b 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 22)
  (parent 20)
  (unrealized (2 1) (5 0))
  (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))
  (comment "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b s name) (k skey))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b k)
  (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 23)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (n-a n-b text) (a b s name) (k skey))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s) (k k))
  (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 n-a n-b k)
  (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 24)
  (parent 23)
  (unrealized)
  (shape))

(comment "Nothing left to do")