(herald "A Tagged version of Otway-Rees Protocol"
  (comment "using variables of sort mesg"))

(comment "CPSA 2.2.11")
(comment "All input read from tagged_or.scm")

(defprotocol or basic
  (defrole init
    (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
    (trace
      (send
        (cat m my_init_id yr_resp_id
          (enc "init_req" na m my_init_id yr_resp_id
            (ltk my_init_id s))))
      (recv (cat m (enc na k (ltk my_init_id s))))))
  (defrole resp
    (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
      (x y mesg))
    (trace (recv (cat m yr_init_id my_resp_id x))
      (send
        (cat m yr_init_id my_resp_id x
          (enc "resp_req" nb m yr_init_id my_resp_id
            (ltk my_resp_id s))))
      (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  (defrole serv
    (vars (a b s name) (na nb text) (k skey) (m text))
    (trace
      (recv
        (cat m a b (enc "init_req" na m a b (ltk a s))
          (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    (uniq-orig k)))

(defskeleton or
  (vars (x y mesg) (nb m text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb)
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y)))
  (label 0)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton or
  (vars (x y mesg) (nb m nb-0 m-0 text) (s a b b-0 name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m-0) (a b) (b b-0) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (ltk b s))
    (0 2))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv
       (cat m-0 b b-0 (enc "init_req" nb m-0 b b-0 (ltk b s))
         (enc "resp_req" nb-0 m-0 b b-0 (ltk b-0 s))))
      (send (cat m-0 (enc nb k (ltk b s)) (enc nb-0 k (ltk b-0 s))))))
  (label 1)
  (parent 0)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton or
  (vars (x y mesg) (nb m na m-0 text) (s a b a-0 name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m-0) (a a-0) (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 nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (ltk b s))
    (0 2))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv
       (cat m-0 a-0 b (enc "init_req" na m-0 a-0 b (ltk a-0 s))
         (enc "resp_req" nb m-0 a-0 b (ltk b s))))
      (send (cat m-0 (enc na k (ltk a-0 s)) (enc nb k (ltk b s))))))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (x y mesg) (nb m na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (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 nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc "resp_req" nb m-0 a-0 b (ltk b s)) (1 0))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s))))))
  (label 3)
  (parent 2)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (x y mesg) (nb m na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand init 1 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc "init_req" na m a b (ltk a s)) (1 0))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b b) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))

(comment "Nothing left to do")

(defprotocol or basic
  (defrole init
    (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
    (trace
      (send
        (cat m my_init_id yr_resp_id
          (enc "init_req" na m my_init_id yr_resp_id
            (ltk my_init_id s))))
      (recv (cat m (enc na k (ltk my_init_id s))))))
  (defrole resp
    (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
      (x y mesg))
    (trace (recv (cat m yr_init_id my_resp_id x))
      (send
        (cat m yr_init_id my_resp_id x
          (enc "resp_req" nb m yr_init_id my_resp_id
            (ltk my_resp_id s))))
      (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  (defrole serv
    (vars (a b s name) (na nb text) (k skey) (m text))
    (trace
      (recv
        (cat m a b (enc "init_req" na m a b (ltk a s))
          (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    (uniq-orig k)))

(defskeleton or
  (vars (na m text) (s a b name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na)
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s))))))
  (label 5)
  (unrealized (0 1))
  (origs (na (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton or
  (vars (na m nb m-0 text) (s a b b-0 name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (defstrand serv 2 (na na) (nb nb) (m m-0) (a a) (b b-0) (s s) (k k))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na k)
  (operation encryption-test (added-strand serv 2) (enc na k (ltk a s))
    (0 1))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s)))))
    ((recv
       (cat m-0 a b-0 (enc "init_req" na m-0 a b-0 (ltk a s))
         (enc "resp_req" nb m-0 a b-0 (ltk b-0 s))))
      (send (cat m-0 (enc na k (ltk a s)) (enc nb k (ltk b-0 s))))))
  (label 6)
  (parent 5)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (na m na-0 m-0 text) (s a b a-0 name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (defstrand serv 2 (na na-0) (nb na) (m m-0) (a a-0) (b a) (s s) (k k))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na k)
  (operation encryption-test (added-strand serv 2) (enc na k (ltk a s))
    (0 1))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s)))))
    ((recv
       (cat m-0 a-0 a (enc "init_req" na-0 m-0 a-0 a (ltk a-0 s))
         (enc "resp_req" na m-0 a-0 a (ltk a s))))
      (send (cat m-0 (enc na-0 k (ltk a-0 s)) (enc na k (ltk a s))))))
  (label 7)
  (parent 5)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton or
  (vars (na m nb text) (s a b name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (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 na k)
  (operation encryption-test (displaced 2 0 init 1)
    (enc "init_req" na m-0 a b-0 (ltk a s)) (1 0))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s)))))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s))))))
  (label 8)
  (parent 6)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (x mesg) (na m nb text) (s a b name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand resp 2 (x x) (nb nb) (m m) (yr_init_id a) (my_resp_id b)
    (s s))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na k)
  (operation encryption-test (added-strand resp 2)
    (enc "resp_req" nb m a b (ltk b s)) (1 0))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s)))))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))))
  (label 9)
  (parent 8)
  (unrealized)
  (shape)
  (maps ((0) ((na na) (s s) (a a) (b b) (k k) (m m))))
  (origs (k (1 1)) (na (0 0))))

(comment "Nothing left to do")

(defprotocol or basic
  (defrole init
    (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
    (trace
      (send
        (cat m my_init_id yr_resp_id
          (enc "init_req" na m my_init_id yr_resp_id
            (ltk my_init_id s))))
      (recv (cat m (enc na k (ltk my_init_id s))))))
  (defrole resp
    (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
      (x y mesg))
    (trace (recv (cat m yr_init_id my_resp_id x))
      (send
        (cat m yr_init_id my_resp_id x
          (enc "resp_req" nb m yr_init_id my_resp_id
            (ltk my_resp_id s))))
      (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  (defrole serv
    (vars (a b s name) (na nb text) (k skey) (m text))
    (trace
      (recv
        (cat m a b (enc "init_req" na m a b (ltk a s))
          (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    (uniq-orig k)))

(defskeleton or
  (vars (x y mesg) (nb m text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (deflistener k)
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb)
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv k) (send k)))
  (label 10)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton or
  (vars (x y mesg) (nb m nb-0 m-0 text) (s a b b-0 name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (deflistener k)
  (defstrand serv 2 (na nb) (nb nb-0) (m m-0) (a b) (b b-0) (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 nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (ltk b s))
    (0 2))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv k) (send k))
    ((recv
       (cat m-0 b b-0 (enc "init_req" nb m-0 b b-0 (ltk b s))
         (enc "resp_req" nb-0 m-0 b b-0 (ltk b-0 s))))
      (send (cat m-0 (enc nb k (ltk b s)) (enc nb-0 k (ltk b-0 s))))))
  (label 11)
  (parent 10)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton or
  (vars (x y mesg) (nb m na m-0 text) (s a b a-0 name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (deflistener k)
  (defstrand serv 2 (na na) (nb nb) (m m-0) (a a-0) (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 nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (ltk b s))
    (0 2))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv k) (send k))
    ((recv
       (cat m-0 a-0 b (enc "init_req" na m-0 a-0 b (ltk a-0 s))
         (enc "resp_req" nb m-0 a-0 b (ltk b s))))
      (send (cat m-0 (enc na k (ltk a-0 s)) (enc nb k (ltk b s))))))
  (label 12)
  (parent 10)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (x y mesg) (nb m na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (deflistener k)
  (defstrand serv 2 (na na) (nb nb) (m m) (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 nb k)
  (operation encryption-test (displaced 3 0 resp 2)
    (enc "resp_req" nb m-0 a-0 b (ltk b s)) (2 0))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv k) (send k))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s))))))
  (label 13)
  (parent 12)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (x y mesg) (nb m na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
    (my_resp_id b) (s s) (k k))
  (deflistener k)
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand init 1 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s))
  (precedes ((0 1) (2 0)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc "init_req" na m a b (ltk a s)) (2 0))
  (traces
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y))
    ((recv k) (send k))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))))
  (label 14)
  (parent 13)
  (unrealized (1 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol or basic
  (defrole init
    (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
    (trace
      (send
        (cat m my_init_id yr_resp_id
          (enc "init_req" na m my_init_id yr_resp_id
            (ltk my_init_id s))))
      (recv (cat m (enc na k (ltk my_init_id s))))))
  (defrole resp
    (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
      (x y mesg))
    (trace (recv (cat m yr_init_id my_resp_id x))
      (send
        (cat m yr_init_id my_resp_id x
          (enc "resp_req" nb m yr_init_id my_resp_id
            (ltk my_resp_id s))))
      (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  (defrole serv
    (vars (a b s name) (na nb text) (k skey) (m text))
    (trace
      (recv
        (cat m a b (enc "init_req" na m a b (ltk a s))
          (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    (uniq-orig k)))

(defskeleton or
  (vars (na m text) (s a b name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (deflistener k)
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na)
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s))))) ((recv k) (send k)))
  (label 15)
  (unrealized (0 1))
  (origs (na (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton or
  (vars (na m nb m-0 text) (s a b b-0 name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (deflistener k)
  (defstrand serv 2 (na na) (nb nb) (m m-0) (a a) (b b-0) (s s) (k k))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na k)
  (operation encryption-test (added-strand serv 2) (enc na k (ltk a s))
    (0 1))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s))))) ((recv k) (send k))
    ((recv
       (cat m-0 a b-0 (enc "init_req" na m-0 a b-0 (ltk a s))
         (enc "resp_req" nb m-0 a b-0 (ltk b-0 s))))
      (send (cat m-0 (enc na k (ltk a s)) (enc nb k (ltk b-0 s))))))
  (label 16)
  (parent 15)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (na m na-0 m-0 text) (s a b a-0 name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (deflistener k)
  (defstrand serv 2 (na na-0) (nb na) (m m-0) (a a-0) (b a) (s s) (k k))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na k)
  (operation encryption-test (added-strand serv 2) (enc na k (ltk a s))
    (0 1))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s))))) ((recv k) (send k))
    ((recv
       (cat m-0 a-0 a (enc "init_req" na-0 m-0 a-0 a (ltk a-0 s))
         (enc "resp_req" na m-0 a-0 a (ltk a s))))
      (send (cat m-0 (enc na-0 k (ltk a-0 s)) (enc na k (ltk a s))))))
  (label 17)
  (parent 15)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton or
  (vars (na m nb text) (s a b name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (deflistener k)
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na k)
  (operation encryption-test (displaced 3 0 init 1)
    (enc "init_req" na m-0 a b-0 (ltk a s)) (2 0))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s))))) ((recv k) (send k))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s))))))
  (label 18)
  (parent 16)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton or
  (vars (x mesg) (na m nb text) (s a b name) (k skey))
  (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
    (k k))
  (deflistener k)
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand resp 2 (x x) (nb nb) (m m) (yr_init_id a) (my_resp_id b)
    (s s))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig na k)
  (operation encryption-test (added-strand resp 2)
    (enc "resp_req" nb m a b (ltk b s)) (2 0))
  (traces
    ((send (cat m a b (enc "init_req" na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s))))) ((recv k) (send k))
    ((recv
       (cat m a b (enc "init_req" na m a b (ltk a s))
         (enc "resp_req" nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    ((recv (cat m a b x))
      (send (cat m a b x (enc "resp_req" nb m a b (ltk b s))))))
  (label 19)
  (parent 18)
  (unrealized (1 0))
  (comment "empty cohort"))

(comment "Nothing left to do")