(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")

Trees: 0 3 5 9.

Tree 0.

2 0 
(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"))

Item 0, Child: 2.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b)) init ns 0 
(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"))

Item 2, Parent: 0.

(enc n1 n2 (pubk a)) (enc n1 a (pubk b)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ((n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b)) init ns 2 (realized)
(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))))

Tree 3.

4 3 
(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"))

Item 3, Child: 4.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ns 3 
(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"))

Item 4, Parent: 3.

(enc n2 (pubk yr_resp_id)) (enc n1 n2 (pubk a)) (enc n1 a (pubk yr_resp_id)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (my_init_id a) (yr_resp_id yr_resp_id)) init ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ns 4 (realized)
(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))))

Tree 5.

8 5 
(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"))

Item 5, Child: 8.

n2 n2 (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ns 5 
(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"))

Item 8, Parent: 5.

(enc n2 (pubk yr_resp_id)) (enc n1 n2 (pubk a)) (enc n1 a (pubk yr_resp_id)) n2 n2 (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (my_init_id a) (yr_resp_id yr_resp_id)) init ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ns 8 (realized)
(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))))

Tree 9.

12 9 
(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"))

Item 9, Child: 12.

(enc n2 (pubk b1)) (enc n1 n2 (pubk a1)) (enc n1 a1 (pubk b1)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (my_init_id a1) (yr_resp_id b1)) init ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ns 9 
(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"))

Item 12, Parent: 9.

(enc n2 (pubk b1)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b1)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b1)) init ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ns 12 (realized)
(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))))