(comment "CPSA 2.2.11") (comment "Extracted shapes") (herald "Needham-Schroeder Public-Key Protocol" (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe.")) (comment "CPSA 2.2.11") (comment "All input read from ns.scm") (defprotocol ns basic (defrole init (vars (my_init_id yr_resp_id name) (n1 n2 text)) (trace (send (enc n1 my_init_id (pubk yr_resp_id))) (recv (enc n1 n2 (pubk my_init_id))) (send (enc n2 (pubk yr_resp_id))))) (defrole resp (vars (my_resp_id yr_init_id name) (n2 n1 text)) (trace (recv (enc n1 yr_init_id (pubk my_resp_id))) (send (enc n1 n2 (pubk yr_init_id))) (recv (enc n2 (pubk my_resp_id))))) (comment "Needham-Schroeder")) (defskeleton ns (vars (n1 n2 text) (a b name)) (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b)) (non-orig (privk a) (privk b)) (uniq-orig n1) (comment "Initiator point-of-view") (traces ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b))))) (label 0) (unrealized (0 1)) (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns (vars (n1 n2 text) (a b name)) (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b)) (defstrand resp 2 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) (precedes ((0 0) (1 0)) ((1 1) (0 1))) (non-orig (privk a) (privk b)) (uniq-orig n1) (operation nonce-test (contracted (n2-0 n2)) n1 (0 1) (enc n1 n2 (pubk a)) (enc n1 a (pubk b))) (traces ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))) (label 2) (parent 0) (unrealized) (shape) (maps ((0) ((a a) (b b) (n1 n1) (n2 n2)))) (origs (n1 (0 0)))) (comment "Nothing left to do") (defprotocol ns basic (defrole init (vars (my_init_id yr_resp_id name) (n1 n2 text)) (trace (send (enc n1 my_init_id (pubk yr_resp_id))) (recv (enc n1 n2 (pubk my_init_id))) (send (enc n2 (pubk yr_resp_id))))) (defrole resp (vars (my_resp_id yr_init_id name) (n2 n1 text)) (trace (recv (enc n1 yr_init_id (pubk my_resp_id))) (send (enc n1 n2 (pubk yr_init_id))) (recv (enc n2 (pubk my_resp_id))))) (comment "Needham-Schroeder")) (defskeleton ns (vars (n2 n1 text) (a b name)) (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) (non-orig (privk a)) (uniq-orig n2) (comment "Responder point-of-view") (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b))))) (label 3) (unrealized (0 2)) (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns (vars (n2 n1 text) (a b yr_resp_id name)) (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id yr_resp_id)) (precedes ((0 1) (1 1)) ((1 2) (0 2))) (non-orig (privk a)) (uniq-orig n2) (operation nonce-test (added-strand init 3) n2 (0 2) (enc n1 n2 (pubk a))) (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b)))) ((send (enc n1 a (pubk yr_resp_id))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk yr_resp_id))))) (label 4) (parent 3) (unrealized) (shape) (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) (origs (n2 (0 1)))) (comment "Nothing left to do") (defprotocol ns basic (defrole init (vars (my_init_id yr_resp_id name) (n1 n2 text)) (trace (send (enc n1 my_init_id (pubk yr_resp_id))) (recv (enc n1 n2 (pubk my_init_id))) (send (enc n2 (pubk yr_resp_id))))) (defrole resp (vars (my_resp_id yr_init_id name) (n2 n1 text)) (trace (recv (enc n1 yr_init_id (pubk my_resp_id))) (send (enc n1 n2 (pubk yr_init_id))) (recv (enc n2 (pubk my_resp_id))))) (comment "Needham-Schroeder")) (defskeleton ns (vars (n1 n2 text) (a b name)) (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) (deflistener n2) (non-orig (privk a) (privk b)) (uniq-orig n1 n2) (comment "Responder point-of-view, secrecy?") (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b)))) ((recv n2) (send n2))) (label 5) (unrealized (0 2) (1 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton ns (vars (n1 n2 text) (a b yr_resp_id name)) (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) (deflistener n2) (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id yr_resp_id)) (precedes ((0 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)) ((2 2) (1 0))) (non-orig (privk a) (privk b)) (uniq-orig n1 n2) (operation nonce-test (displaced 3 2 init 3) n2 (0 2) (enc n1 n2 (pubk a))) (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b)))) ((recv n2) (send n2)) ((send (enc n1 a (pubk yr_resp_id))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk yr_resp_id))))) (label 8) (parent 5) (unrealized) (shape) (maps ((0 1) ((a a) (b b) (n1 n1) (n2 n2)))) (origs (n1 (2 0)) (n2 (0 1)))) (comment "Nothing left to do") (defprotocol ns basic (defrole init (vars (my_init_id yr_resp_id name) (n1 n2 text)) (trace (send (enc n1 my_init_id (pubk yr_resp_id))) (recv (enc n1 n2 (pubk my_init_id))) (send (enc n2 (pubk yr_resp_id))))) (defrole resp (vars (my_resp_id yr_init_id name) (n2 n1 text)) (trace (recv (enc n1 yr_init_id (pubk my_resp_id))) (send (enc n1 n2 (pubk yr_init_id))) (recv (enc n2 (pubk my_resp_id))))) (comment "Needham-Schroeder")) (defskeleton ns (vars (n1 n2 text) (a b a1 b1 name)) (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a1) (yr_resp_id b1)) (non-orig (privk a) (privk b)) (uniq-orig n1 n2) (comment "Implicit auth, both nonces u.o.") (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b)))) ((send (enc n1 a1 (pubk b1))) (recv (enc n1 n2 (pubk a1))) (send (enc n2 (pubk b1))))) (label 9) (unrealized (0 0) (0 2) (1 1)) (preskeleton) (comment "Not a skeleton")) (defskeleton ns (vars (n1 n2 text) (a b b1 name)) (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b1)) (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2))) (non-orig (privk a) (privk b)) (uniq-orig n1 n2) (operation nonce-test (displaced 2 1 init 3) n2 (0 2) (enc n1 n2 (pubk a))) (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b)))) ((send (enc n1 a (pubk b1))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b1))))) (label 12) (parent 9) (unrealized) (shape) (maps ((0 1) ((a a) (b b) (a1 a) (b1 b1) (n1 n1) (n2 n2)))) (origs (n1 (1 0)) (n2 (0 1)))) (comment "Nothing left to do")