(herald "Needham-Schroeder Public-Key Protocol"
  (comment "This protocol contains a man-in-the-middle"
    "attack discovered by Galvin Lowe."))
(comment "CPSA 3.4.0")
(comment "All input read from ns.scm")

Trees: 0 3.

Tree 0.

2 1 0 
(defprotocol ns basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
      (recv (enc n2 (pubk b)))))
  (comment "Needham-Schroeder"))

Item 0, Child: 1.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (a a) (b b)) init ns 0 
(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (comment "Initiator point-of-view")
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 1, Parent: 0, Child: 2.

(enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2-0) (n1 n1) (b b) (a a)) resp ((n1 n1) (n2 n2) (a a) (b b)) init ns 1 
(defskeleton ns
  (vars (n1 n2 n2-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (operation nonce-test (added-strand resp 2) n1 (0 1)
    (enc n1 a (pubk b)))
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 2, Parent: 1.

(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) (b b) (a a)) resp ((n1 n1) (n2 n2) (a a) (b b)) init ns 2 (realized)
(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a 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)))
  (label 2)
  (parent 1)
  (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 (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
      (recv (enc n2 (pubk b)))))
  (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) (b b) (a a)) resp ns 3 
(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (comment "Responder point-of-view")
  (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-0)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b-0)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (a a) (b b-0)) init ((n2 n2) (n1 n1) (b b) (a a)) resp ns 4 (realized)
(defskeleton ns
  (vars (n2 n1 text) (a b b-0 name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc n1 n2 (pubk a)))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  (origs (n2 (0 1))))