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

(defprotocol yahalom-6:3:6 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-6:3:6
  (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-6:3:6
  (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-6:3:6
  (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-6:3:6 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-6:3:6
  (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-6:3:6
  (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 "1 in cohort - 1 not yet seen"))

(defskeleton yahalom-6:3:6
  (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"))

(comment "Nothing left to do")

(defprotocol yahalom-6:3:6 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-6:3:6
  (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 6)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom-6:3:6
  (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 7)
  (parent 6)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom-6:3:6
  (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 8)
  (parent 7)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom-6:3:6
  (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 9)
  (parent 8)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom-6:3:6
  (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 10)
  (parent 8)
  (unrealized (0 2) (3 0))
  (comment "empty cohort"))

(defskeleton yahalom-6:3:6
  (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 11)
  (parent 9)
  (unrealized (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom-6:3:6
  (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 (n-a-0 n-a) (n-b-0 n-b) (k-0 k) (a-0 a) (b-0 b) (s-0 s)
      (n-a-1 n-a)) n-b (3 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 12)
  (parent 11)
  (unrealized)
  (shape))

(defskeleton yahalom-6:3:6
  (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 13)
  (parent 11)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom-6:3:6
  (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 14)
  (parent 13)
  (unrealized (3 1) (6 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol yahalom-6:3:6 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-6:3:6
  (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 15)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom-6:3:6
  (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 16)
  (parent 15)
  (unrealized)
  (shape))

(comment "Nothing left to do")