(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") (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))) (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")) (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)))) (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)))) (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 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))) (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")) (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)))) (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)))) (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 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))) (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")) (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)) (deflistener k) (defstrand serv 2 (na nb) (nb nb-0) (a b) (b b) (s s) (k k)) (precedes ((0 1) (2 0)) ((2 1) (0 2)) ((2 1) (1 0))) (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 k) (send k)) ((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 7) (parent 6) (unrealized (1 0)) (comment "empty cohort")) (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)) (deflistener k) (defstrand serv 2 (na na-0) (nb nb) (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 (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 k) (send k)) ((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 8) (parent 6) (unrealized (1 0)) (comment "empty cohort")) (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 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))) (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")) (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)) (deflistener k) (defstrand serv 2 (na na) (nb nb) (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 (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 k) (send k)) ((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 10) (parent 9) (unrealized (1 0)) (comment "empty cohort")) (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)) (deflistener k) (defstrand serv 2 (na na-0) (nb na) (a a) (b a) (s s) (k k)) (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0))) (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 k) (send k)) ((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 11) (parent 9) (unrealized (1 0)) (comment "empty cohort")) (comment "Nothing left to do")