(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 tagged_an_or.scm")

(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 "to_init" 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 "to_resp" 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 "to_init" na a b k (ltk a s))
          (enc "to_resp" nb a b k (ltk b s)))))
    (uniq-orig k)))

(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 "to_resp" nb a b k (ltk b s)))) (send x)))
  (label 0)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(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 "to_resp" 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 "to_resp" nb a b k (ltk b s)))) (send x))
    ((recv (cat a b na-0 nb))
      (send
        (cat (enc "to_init" na-0 a b k (ltk a s))
          (enc "to_resp" nb a b k (ltk b s))))))
  (label 1)
  (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))))

(comment "Nothing left to do")

(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 "to_init" 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 "to_resp" 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 "to_init" na a b k (ltk a s))
          (enc "to_resp" nb a b k (ltk b s)))))
    (uniq-orig k)))

(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 "to_init" na a b k (ltk a s)))))
  (label 2)
  (unrealized (0 1))
  (origs (na (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(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 "to_init" na a b k (ltk a s)) (0 1))
  (traces
    ((send (cat a b na)) (recv (enc "to_init" na a b k (ltk a s))))
    ((recv (cat a b na nb))
      (send
        (cat (enc "to_init" na a b k (ltk a s))
          (enc "to_resp" nb a b k (ltk b s))))))
  (label 3)
  (parent 2)
  (unrealized)
  (shape)
  (maps ((0) ((na na) (s s) (a a) (b b) (k k))))
  (origs (k (1 1)) (na (0 0))))

(comment "Nothing left to do")

(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 "to_init" 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 "to_resp" 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 "to_init" na a b k (ltk a s))
          (enc "to_resp" nb a b k (ltk b s)))))
    (uniq-orig k)))

(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 "to_resp" nb a b k (ltk b s)))) (send x))
    ((recv k) (send k)))
  (label 4)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(comment "Nothing left to do")

(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 "to_init" 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 "to_resp" 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 "to_init" na a b k (ltk a s))
          (enc "to_resp" nb a b k (ltk b s)))))
    (uniq-orig k)))

(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 "to_init" na a b k (ltk a s))))
    ((recv k) (send k)))
  (label 6)
  (unrealized (0 1))
  (origs (na (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(comment "Nothing left to do")