(comment "CPSA 2.2.11")
(comment "Extracted shapes")
(herald "Otway-Rees Protocol"
  (comment "Standard version using variables of sort mesg"))
(comment "CPSA 2.2.11")
(comment "All input read from an_or.scm")

Trees: 0 3 6 9.

Tree 0.

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

Item 0, Children: 1 2.

(defskeleton an_or
  (vars (x mesg) (nb na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (na na) (nb nb) (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 a b na)) (send (cat a b na nb))
      (recv (cat x (enc nb a b k (ltk b s)))) (send x)))
  (label 0)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

Item 1, Parent: 0.

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

Item 2, Parent: 0.

(defskeleton an_or
  (vars (x mesg) (nb na na-0 text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (na na) (nb nb) (yr_init_id a) (my_resp_id b)
    (s s) (k k))
  (defstrand serv 2 (na na-0) (nb nb) (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 (added-strand serv 2)
    (enc nb a b k (ltk b s)) (0 2))
  (traces
    ((recv (cat a b na)) (send (cat a b na nb))
      (recv (cat x (enc nb a b k (ltk b s)))) (send x))
    ((recv (cat a b na-0 nb))
      (send (cat (enc na-0 a b k (ltk a s)) (enc nb a b k (ltk b s))))))
  (label 2)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b b) (na na) (k k) (x x))))
  (origs (k (1 1)) (nb (0 1))))

Tree 3.

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

Item 3, Children: 4 5.

(defskeleton an_or
  (vars (na text) (s a b name) (k skey))
  (defstrand init 2 (na na) (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 a b na)) (recv (enc na a b k (ltk a s)))))
  (label 3)
  (unrealized (0 1))
  (origs (na (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

Item 4, Parent: 3.

(defskeleton an_or
  (vars (na nb text) (s a b name) (k skey))
  (defstrand init 2 (na na) (my_init_id a) (yr_resp_id b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (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 (added-strand serv 2)
    (enc na a b k (ltk a s)) (0 1))
  (traces ((send (cat a b na)) (recv (enc na a b k (ltk a s))))
    ((recv (cat a b na nb))
      (send (cat (enc na a b k (ltk a s)) (enc nb a b k (ltk b s))))))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((na na) (s s) (a a) (b b) (k k))))
  (origs (k (1 1)) (na (0 0))))

Item 5, Parent: 3.

(defskeleton an_or
  (vars (na na-0 text) (s a name) (k skey))
  (defstrand init 2 (na na) (my_init_id a) (yr_resp_id a) (s s) (k k))
  (defstrand serv 2 (na na-0) (nb na) (a a) (b a) (s s) (k k))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (ltk a s))
  (uniq-orig na k)
  (operation encryption-test (added-strand serv 2)
    (enc na a a k (ltk a s)) (0 1))
  (traces ((send (cat a a na)) (recv (enc na a a k (ltk a s))))
    ((recv (cat a a na-0 na))
      (send (cat (enc na-0 a a k (ltk a s)) (enc na a a k (ltk a s))))))
  (label 5)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((na na) (s s) (a a) (b a) (k k))))
  (origs (k (1 1)) (na (0 0))))

Tree 6.

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

Item 6.

(defskeleton an_or
  (vars (x mesg) (nb na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (na na) (nb nb) (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 a b na)) (send (cat a b na nb))
      (recv (cat x (enc nb a b k (ltk b s)))) (send x))
    ((recv k) (send k)))
  (label 6)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

Tree 9.

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

Item 9.

(defskeleton an_or
  (vars (na text) (s a b name) (k skey))
  (defstrand init 2 (na na) (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 a b na)) (recv (enc na a b k (ltk a s))))
    ((recv k) (send k)))
  (label 9)
  (unrealized (0 1))
  (origs (na (0 0)))
  (comment "2 in cohort - 2 not yet seen"))