(comment "CPSA 2.2.11")
(comment "Extracted shapes")
(herald "Needham-Schroeder Lowe Public-Key Protocol"
  (comment "This protocol eliminates the man-in-the-middle"
    "attack discovered by Gavin Lowe."))
(comment "CPSA 2.2.11")
(comment "All input read from nsl.scm")

Trees: 0 3 5 8.

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 yr_resp_id (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 my_resp_id (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 b (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 b (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 b (pubk a)) (enc n1 a (pubk b)) (enc n2 (pubk b)) (enc n1 n2 b (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 a (pubk b)) (enc n1 n2 b (pubk a)))
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (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 yr_resp_id (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 my_resp_id (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 b (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 b (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 b)) (enc n1 n2 b (pubk a)) (enc n1 a (pubk b)) (enc n2 (pubk b)) (enc n1 n2 b (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b)) 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 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 b))
  (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 b (pubk a)))
  (traces
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b))))
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  (origs (n2 (0 1))))

Tree 5.

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 yr_resp_id (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 my_resp_id (pubk yr_init_id)))
      (recv (enc n2 (pubk my_resp_id)))))
  (comment "Needham-Schroeder"))

Item 5.

n2 n2 (enc n2 (pubk b)) (enc n1 n2 b (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 b (pubk a)))
      (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))
  (label 5)
  (unrealized (0 2) (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

Tree 8.

11 8 
(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 yr_resp_id (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 my_resp_id (pubk yr_init_id)))
      (recv (enc n2 (pubk my_resp_id)))))
  (comment "Needham-Schroeder"))

Item 8, Child: 11.

(enc n2 (pubk b1)) (enc n1 n2 b1 (pubk a1)) (enc n1 a1 (pubk b1)) (enc n2 (pubk b)) (enc n1 n2 b (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 8 
(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 b (pubk a)))
      (recv (enc n2 (pubk b))))
    ((send (enc n1 a1 (pubk b1))) (recv (enc n1 n2 b1 (pubk a1)))
      (send (enc n2 (pubk b1)))))
  (label 8)
  (unrealized (0 0) (0 2) (1 1))
  (preskeleton)
  (comment "Not a skeleton"))

Item 11, Parent: 8.

(enc n2 (pubk b)) (enc n1 n2 b (pubk a)) (enc n1 a (pubk b)) (enc n2 (pubk b)) (enc n1 n2 b (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b)) init ((n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a)) resp ns 11 (realized)
(defskeleton ns
  (vars (n1 n2 text) (a b 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 b))
  (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 b (pubk a)))
  (traces
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b))))
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))))
  (label 11)
  (parent 8)
  (unrealized)
  (shape)
  (maps ((0 1) ((a a) (b b) (a1 a) (b1 b) (n1 n1) (n2 n2))))
  (origs (n1 (1 0)) (n2 (0 1))))