(herald "Otway-Rees Protocol"
  (comment "Standard version using variables of sort mesg")
  (algebra diffie-hellman))
(comment "CPSA 3.4.0")
(comment "All input read from bltk_or.scm")

Tree 0.

(defprotocol or diffie-hellman
  (defrole init
    (vars (a b s name) (na text) (k skey) (m text))
    (trace (send (cat m a b (enc na m a b (bltk a s))))
      (recv (cat m (enc na k (bltk a s))))))
  (defrole resp
    (vars (a b s name) (nb text) (k skey) (m text) (x y mesg))
    (trace (recv (cat m a b x))
      (send (cat m a b x (enc nb m a b (bltk b s))))
      (recv (cat m y (enc nb k (bltk b s)))) (send y)))
  (defrole serv
    (vars (a b s name) (na nb text) (k skey) (m text))
    (trace
      (recv
        (cat m a b (enc na m a b (bltk a s)) (enc nb m a b (bltk b s))))
      (send (cat m (enc na k (bltk a s)) (enc nb k (bltk b s)))))
    (uniq-orig k)))

Item 0, Children: 1 2 3 4.

(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) (a a) (b b) (s s) (k k))
  (non-orig (bltk s a) (bltk s b))
  (uniq-orig nb)
  (label 0)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "4 in cohort - 4 not yet seen"))

Item 1, Parent: 0, Child: 5.

(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) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m-0) (a a-0) (b s) (s b) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (0 2))
  (label 1)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 2, Parent: 0, Child: 6.

(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) (a a) (b 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 (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (0 2))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 3, Parent: 0, Child: 7.

(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) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m-0) (a s) (b b-0) (s b) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (0 2))
  (label 3)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 4, Parent: 0, Child: 8.

(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) (a a) (b 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 (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (0 2))
  (label 4)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 5, Parent: 1, Children: 9 10 11.

(defskeleton or
  (vars (x y mesg) (nb m na text) (a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk a b) (bltk b b))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 a-0 s (bltk s b)) (1 0))
  (label 5)
  (parent 1)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

Item 6, Parent: 2, Children: 12 13 14, Seen Child: 10.

(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) (a a) (b 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 (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 a-0 b (bltk s b)) (1 0))
  (label 6)
  (parent 2)
  (seen 10)
  (unrealized (1 0))
  (comment "4 in cohort - 3 not yet seen"))

Item 7, Parent: 3.

(defskeleton or
  (vars (x y mesg) (nb m nb-0 text) (a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s a) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b b) (s b) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk a a) (bltk a b))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 s b (bltk s b)) (1 0))
  (label 7)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s a) (a a) (b b) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))

Item 8, Parent: 4, Children: 15 16, Seen Child: 13.

(defskeleton or
  (vars (x y mesg) (nb m nb-0 text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 b b (bltk s b)) (1 0))
  (label 8)
  (parent 4)
  (seen 13)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

Item 9, Parent: 5, Seen Child: 12.

(defskeleton or
  (vars (x y mesg) (nb m na text) (a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (defstrand init 1 (na na) (m m) (a a) (b b) (s b))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig (bltk a b) (bltk b b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc na m a b (bltk a b)) (1 0))
  (label 9)
  (parent 5)
  (seen 12)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 10, Parent: 5.

(defskeleton or
  (vars (x y x-0 mesg) (nb m na text) (a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (defstrand resp 2 (x x-0) (nb na) (m m) (a a) (b b) (s a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (bltk a b) (bltk b b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand resp 2)
    (enc na m a b (bltk a b)) (1 0))
  (label 10)
  (parent 5)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s b) (a a) (b b) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))

Item 11, Parent: 5, Seen Child: 13.

(defskeleton or
  (vars (x y mesg) (nb m text) (a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s a) (k k))
  (defstrand serv 2 (na nb) (nb nb) (m m) (a a) (b a) (s a) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk a a))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc na m a a (bltk a a)) (1 0))
  (label 11)
  (parent 5)
  (seen 13)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 12, Parent: 6.

(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) (a a) (b 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) (a a) (b b) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc na m a b (bltk s a)) (1 0))
  (label 12)
  (parent 6)
  (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))))

Item 13, Parent: 6.

(defskeleton or
  (vars (x y mesg) (nb m text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc na m a a (bltk s a)) (1 0))
  (label 13)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))

Item 14, Parent: 6.

(defskeleton or
  (vars (x y x-0 mesg) (nb m na text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand resp 2 (x x-0) (nb na) (m m) (a a) (b a) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (added-strand resp 2)
    (enc na m a a (bltk s a)) (1 0))
  (label 14)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))

Item 15, Parent: 8.

(defskeleton or
  (vars (x y mesg) (nb m nb-0 text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  (defstrand init 1 (na nb-0) (m m) (a a) (b a) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc nb-0 m a a (bltk s a)) (1 0))
  (label 15)
  (parent 8)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))

Item 16, Parent: 8.

(defskeleton or
  (vars (x y x-0 mesg) (nb m nb-0 text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  (defstrand resp 2 (x x-0) (nb nb-0) (m m) (a a) (b a) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (added-strand resp 2)
    (enc nb-0 m a a (bltk s a)) (1 0))
  (label 16)
  (parent 8)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))