(herald goals)
(comment "CPSA 3.4.0")
(comment "All input read from goals.scm")

Trees: 0 2 4 6 8 17 19 21 23 26 28 33 41 45 47 49 52 54 57 62 65.

Tree 0.

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 with no role origination assumptions"))

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) (b a name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (non-orig (privk b))
  (uniq-orig n1)
  (goals
    (forall ((b name) (n1 text) (z0 node))
      (implies
        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)
          (non (privk b)) (uniq n1))
        (exists ((z1 node))
          (and (p "resp" 1 z1) (p "resp" "b" z1 b))))))
  (comment "Initiator point of view"
    "Authentication goal: agreement on name b")
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 1, Parent: 0.

(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 (realized)
(defskeleton ns
  (vars (n1 n2 n2-0 text) (b a 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 b))
  (uniq-orig n1)
  (operation nonce-test (added-strand resp 2) n1 (0 1)
    (enc n1 a (pubk b)))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))
  (origs (n1 (0 0))))

Tree 2.

3 2 
(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 with no role origination assumptions"))

Item 2, Child: 3.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (a a) (b b)) init ns 2 
(defskeleton ns
  (vars (n1 n2 text) (b a name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (non-orig (privk b))
  (uniq-orig n1)
  (goals
    (forall ((b name) (n1 text) (z0 node))
      (implies
        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)
          (non (privk b)) (uniq n1))
        (exists ((z1 node))
          (and (p "resp" 1 z1) (p "resp" "b" z1 b) (prec z1 z0))))))
  (comment "Prec example")
  (label 2)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 3, Parent: 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 3 (realized)
(defskeleton ns
  (vars (n1 n2 n2-0 text) (b a 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 b))
  (uniq-orig n1)
  (operation nonce-test (added-strand resp 2) n1 (0 1)
    (enc n1 a (pubk b)))
  (label 3)
  (parent 2)
  (unrealized)
  (shape)
  (satisfies (no (b b) (n1 n1) (z0 (0 2))))
  (maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))
  (origs (n1 (0 0))))

Tree 4.

5 4 
(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 with no role origination assumptions"))

Item 4, Child: 5.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (b b) (a a)) resp ns 4 
(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a))
  (uniq-orig n2)
  (goals
    (forall ((a b name) (n2 text) (z0 node))
      (implies
        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
          (p "resp" "b" z0 b) (non (privk a)) (uniq n2))
        (exists ((z1 node))
          (and (p "init" 1 z1) (p "init" "b" z1 b))))))
  (comment "Responder point of view"
    "Failed authentication goal: agreement on name b")
  (label 4)
  (unrealized (0 2))
  (origs (n2 (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 5, Parent: 4.

(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 5 (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))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc n1 n2 (pubk a)))
  (label 5)
  (parent 4)
  (unrealized)
  (shape)
  (satisfies (no (a a) (b b) (n2 n2) (z0 (0 2))))
  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  (origs (n2 (0 1))))

Tree 6.

7 6 
(defprotocol nsl basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 b (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 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (comment
    "Needham-Schroeder-Lowe with no role origination assumptions"))

Item 6, Child: 7.

(enc n2 (pubk b)) (enc n1 n2 b (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (b b) (a a)) resp nsl 6 
(defskeleton nsl
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a))
  (uniq-orig n2)
  (goals
    (forall ((a b name) (n2 text) (z0 node))
      (implies
        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
          (p "resp" "b" z0 b) (non (privk a)) (uniq n2))
        (exists ((z1 node))
          (and (p "init" 1 z1) (p "init" "b" z1 b))))))
  (comment "Responder point of view"
    "Authentication goal: agreement on name b")
  (label 6)
  (unrealized (0 2))
  (origs (n2 (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 7, Parent: 6.

(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) (a a) (b b)) init ((n2 n2) (n1 n1) (b b) (a a)) resp nsl 7 (realized)
(defskeleton nsl
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b 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)))
  (label 7)
  (parent 6)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  (origs (n2 (0 1))))

Tree 8.

15 13 16 15 16 14 12 11 10 9 8 
(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 with no role origination assumptions"))

Item 8, Child: 9.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) n1 n1 ((n1 n1) (n2 n2) (a a) (b b)) init ns 8 
(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (deflistener n1)
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (goals
    (forall ((a b name) (n1 text) (z0 z1 node))
      (implies
        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "a" z0 a)
          (p "init" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n1)
          (non (privk a)) (non (privk b)) (uniq n1)) (false))))
  (comment "Initiator point of view"
    "Secrecy goal: nonce n1 not revealed")
  (label 8)
  (unrealized (0 0) (1 1))
  (preskeleton)
  (comment "Not a skeleton"))

Item 9, Parent: 8, Child: 10.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) n1 n1 ((n1 n1) (n2 n2) (a a) (b b)) init ns 9 
(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (deflistener n1)
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (goals
    (forall ((a b name) (n1 text) (z0 z1 node))
      (implies
        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "a" z0 a)
          (p "init" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n1)
          (non (privk a)) (non (privk b)) (uniq n1)) (false))))
  (comment "Initiator point of view"
    "Secrecy goal: nonce n1 not revealed")
  (label 9)
  (parent 8)
  (unrealized (0 0) (1 1))
  (origs (n1 (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 10, Parent: 9, Child: 11.

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

Item 11, Parent: 10, Children: 12 13.

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

Item 12, Parent: 11, Children: 14 15.

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

Item 13, Parent: 11, Seen Child: 15.

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

Item 14, Parent: 12, Child: 16.

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

Item 15, Parent: 12, Seen Child: 16.

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

Item 16, Parent: 14.

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

Tree 17.

18 17 
(defprotocol unilateral basic
  (defrole init
    (vars (a name) (n text))
    (trace (send (enc n (pubk a))) (recv n)))
  (defrole resp
    (vars (a name) (n text))
    (trace (recv (enc n (pubk a))) (send n)))
  (comment "Unilateral authentication"))

Item 17, Child: 18.

n (enc n (pubk a)) ((n n) (a a)) init unilateral 17
(defskeleton unilateral
  (vars (n text) (a name))
  (defstrand init 2 (n n) (a a))
  (non-orig (privk a))
  (uniq-orig n)
  (goals
    (forall ((a name) (n text) (z0 node))
      (implies
        (and (p "init" 1 z0) (p "init" "n" z0 n) (p "init" "a" z0 a)
          (non (privk a)) (uniq n))
        (exists ((z1 node))
          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
  (comment "Unilateral authentication goal")
  (label 17)
  (unrealized (0 1))
  (origs (n (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 18, Parent: 17.

n (enc n (pubk a)) n (enc n (pubk a)) ((n n) (a a)) resp ((n n) (a a)) init unilateral 18 (realized) 
(defskeleton unilateral
  (vars (n text) (a name))
  (defstrand init 2 (n n) (a a))
  (defstrand resp 2 (n n) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (0 1) (enc n (pubk a)))
  (label 18)
  (parent 17)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((a a) (n n))))
  (origs (n (0 0))))

Tree 19.

20 19 
(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 with no role origination assumptions"))

Item 19, Child: 20.

(enc n n2 (pubk a-0)) (enc n a-0 (pubk a)) ((n1 n) (n2 n2) (a a-0) (b a)) init ns 19 
(defskeleton ns
  (vars (n n2 text) (a a-0 name))
  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
  (non-orig (privk a))
  (uniq-orig n)
  (goals
    (forall ((a name) (n text) (z0 node))
      (implies
        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "b" z0 a)
          (non (privk a)) (uniq n))
        (exists ((z1 node))
          (and (p "resp" 1 z1) (p "resp" "b" z1 a))))))
  (comment "Initiator authentication goal"
    "Same as unilateral goal under the predicate mapping:"
    (p "init" "n") "->" (p "init" "n1") "and" (p "init" "a") "->"
    (p "init" "b") "and" (p "resp" "a") "->" (p "resp" "b"))
  (label 19)
  (unrealized (0 1))
  (origs (n (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 20, Parent: 19.

(enc n n2-0 (pubk a-0)) (enc n a-0 (pubk a)) (enc n n2 (pubk a-0)) (enc n a-0 (pubk a)) ((n2 n2-0) (n1 n) (b a) (a a-0)) resp ((n1 n) (n2 n2) (a a-0) (b a)) init ns 20 (realized)
(defskeleton ns
  (vars (n n2 n2-0 text) (a a-0 name))
  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
  (defstrand resp 2 (n2 n2-0) (n1 n) (b a) (a a-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (0 1)
    (enc n a-0 (pubk a)))
  (label 20)
  (parent 19)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((a a) (n n) (a-0 a-0) (n2 n2))))
  (origs (n (0 0))))

Tree 21.

22 21 
(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 with no role origination assumptions"))

Item 21, Child: 22.

(enc n (pubk b)) (enc n1 n (pubk a)) (enc n1 a (pubk b)) ((n2 n) (n1 n1) (b b) (a a)) resp ns 21 
(defskeleton ns
  (vars (n n1 text) (a b name))
  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
  (non-orig (privk a))
  (uniq-orig n)
  (goals
    (forall ((a name) (n text) (z0 node))
      (implies
        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
          (non (privk a)) (uniq n))
        (exists ((z1 node))
          (and (p "init" 2 z1) (p "init" "a" z1 a))))))
  (comment "Responder authentication goal"
    "Same as unilateral goal under the predicate mapping:" (p "init" 1)
    "->" (p "resp" 2) "and" (p "init" "n") "->" (p "resp" "n2") "and"
    (p "init" "a") "->" (p "resp" "a") "and" (p "resp" 1) "->"
    (p "init" 2) "and" (p "resp" "a") "->" (p "init" "a"))
  (label 21)
  (unrealized (0 2))
  (origs (n (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 22, Parent: 21.

(enc n (pubk b-0)) (enc n1 n (pubk a)) (enc n1 a (pubk b-0)) (enc n (pubk b)) (enc n1 n (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n) (a a) (b b-0)) init ((n2 n) (n1 n1) (b b) (a a)) resp ns 22 (realized)
(defskeleton ns
  (vars (n n1 text) (a b b-0 name))
  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (non-orig (privk a))
  (uniq-orig n)
  (operation nonce-test (added-strand init 3) n (0 2)
    (enc n1 n (pubk a)))
  (label 22)
  (parent 21)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((a a) (n n) (b b) (n1 n1))))
  (origs (n (0 1))))

Tree 23.

25 24 23 
(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 with no role origination assumptions"))

Item 23, Child: 24.

(enc n n2 (pubk a)) (enc n a (pubk b)) ((n1 n) (n2 n2) (a a) (b b)) init ns 23 
(defskeleton ns
  (vars (n n2 text) (a b name))
  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n)
  (goals
    (forall ((a b name) (n text) (z0 node))
      (implies
        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
        (exists ((z1 node)) (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))
    (forall ((a b name) (n text) (z0 node))
      (implies
        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
        (exists ((z1 node))
          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
  (comment "Two initiator authentication goals")
  (label 23)
  (unrealized (0 1))
  (origs (n (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 24, Parent: 23, Child: 25.

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

Item 25, Parent: 24.

(enc n n2 (pubk a)) (enc n a (pubk b)) (enc n n2 (pubk a)) (enc n a (pubk b)) ((n2 n2) (n1 n) (b b) (a a)) resp ((n1 n) (n2 n2) (a a) (b b)) init ns 25 (realized)
(defskeleton ns
  (vars (n n2 text) (a b name))
  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n)
  (operation nonce-test (contracted (n2-0 n2)) n (0 1)
    (enc n n2 (pubk a)) (enc n a (pubk b)))
  (label 25)
  (parent 24)
  (unrealized)
  (shape)
  (satisfies yes yes)
  (maps ((0) ((a a) (b b) (n n) (n2 n2))))
  (origs (n (0 0))))

Tree 26.

27 26 
(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 with no role origination assumptions"))

Item 26, Child: 27.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (a a) (b b)) init ns 26 
(defskeleton ns
  (vars (n1 n2 text) (b a name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (non-orig (privk b))
  (uniq-orig n1)
  (goals
    (forall ((n1 n2 text) (b a name) (z z-0 node))
      (implies
        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk b))
          (uniq-at n1 z))
        (exists ((n2-0 text) (z-1 z-2 z-3 node))
          (and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)
            (p "resp" "n2" z-3 n2-0) (p "resp" "n1" z-3 n1)
            (p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)
            (prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)
            (str-prec z-2 z-3))))))
  (comment "Shape analysis sentence")
  (label 26)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 27, Parent: 26.

(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 27 (realized)
(defskeleton ns
  (vars (n1 n2 n2-0 text) (b a 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 b))
  (uniq-orig n1)
  (operation nonce-test (added-strand resp 2) n1 (0 1)
    (enc n1 a (pubk b)))
  (label 27)
  (parent 26)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((n1 n1) (n2 n2) (b b) (a a))))
  (origs (n1 (0 0))))

Tree 28.

32 31 30 29 28 
(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 with no role origination assumptions"))

Item 28, Child: 29.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) n2 n2 ((n2 n2) (n1 n1) (b b) (a a)) resp ns 28 
(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (deflistener n2)
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (goals
    (forall ((a b name) (n2 text) (z0 z1 node))
      (implies
        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
          (p "resp" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n2)
          (non (privk a)) (non (privk b)) (uniq n2)) (false))))
  (comment "Responder point of view"
    "Failed secrecy goal: nonce n2 not revealed")
  (label 28)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (comment "Not a skeleton"))

Item 29, Parent: 28, Child: 30.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) n2 n2 ((n2 n2) (n1 n1) (b b) (a a)) resp ns 29 
(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (deflistener n2)
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (precedes ((1 1) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (goals
    (forall ((a b name) (n2 text) (z0 z1 node))
      (implies
        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
          (p "resp" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n2)
          (non (privk a)) (non (privk b)) (uniq n2)) (false))))
  (comment "Responder point of view"
    "Failed secrecy goal: nonce n2 not revealed")
  (label 29)
  (parent 28)
  (unrealized (0 0) (1 2))
  (origs (n2 (1 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 30, Parent: 29, Children: 31 32.

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

Item 31, Parent: 30.

(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)) n2 n2 ((n1 n1) (n2 n2) (a a) (b b-0)) init ((n2 n2) (n1 n1) (b b) (a a)) resp ns 31 (realized)
(defskeleton ns
  (vars (n2 n1 text) (a b b-0 name))
  (deflistener n2)
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
  (precedes ((1 1) (2 1)) ((2 2) (0 0)) ((2 2) (1 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (operation nonce-test (displaced 3 2 init 3) n2 (0 0)
    (enc n1 n2 (pubk a)))
  (label 31)
  (parent 30)
  (unrealized)
  (shape)
  (satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))
  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))
  (origs (n2 (1 1))))

Item 32, Parent: 30.

(enc n2 (pubk b-1)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b-1)) (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)) n2 n2 ((n1 n1) (n2 n2) (a a) (b b-1)) init ((n1 n1) (n2 n2) (a a) (b b-0)) init ((n2 n2) (n1 n1) (b b) (a a)) resp ns 32 (realized)
(defskeleton ns
  (vars (n2 n1 text) (a b b-0 b-1 name))
  (deflistener n2)
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-1))
  (precedes ((1 1) (2 1)) ((1 1) (3 1)) ((2 2) (1 2)) ((3 2) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 0)
    (enc n1 n2 (pubk a)))
  (label 32)
  (parent 30)
  (unrealized)
  (shape)
  (satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))
  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))
  (origs (n2 (1 1))))

Tree 33.

40 39 37 35 38 36 34 33 
(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 with no role origination assumptions"))

Item 33, Children: 34 35.

(enc n2-0 (pubk b)) (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1-0) (n2 n2-0) (a a) (b b)) init ((n1 n1) (n2 n2) (a a) (b b)) init ns 33 
(defskeleton ns
  (vars (n1 n1-0 n2 n2-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1 n1-0)
  (subgoals
    (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))
      (implies
        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)
          (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
          (p "init" "a" z-0 a) (p "init" "b" z-0 b)
          (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)
          (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)
          (str-prec z-1 z-2) (non (privk a)) (non (privk b))
          (uniq-at n1 z) (uniq-at n1-0 z-1)) (= z-1 z))))
  (comment "Double initiator point of view")
  (label 33)
  (unrealized (0 1) (1 1))
  (origs (n1 (0 0)) (n1-0 (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 34, Parent: 33, Child: 36.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (a a) (b b)) init ns 34 
(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)
  (operation collapsed 1 0)
  (label 34)
  (parent 33)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 35, Parent: 33, Child: 37.

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

Item 36, Parent: 34, Child: 38.

(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 36 
(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 36)
  (parent 34)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 37, Parent: 35, Child: 39.

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

Item 38, Parent: 36.

(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 38 (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 38)
  (parent 36)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))
  (origs (n1 (0 0))))

Item 39, Parent: 37, Child: 40.

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

Item 40, Parent: 39.

(enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)) (enc n1-0 n2 (pubk a)) (enc n1-0 a (pubk b)) (enc n2 (pubk b)) (enc n1-0 n2 (pubk a)) (enc n1-0 a (pubk b)) (enc n2-0 (pubk b)) (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)) ((n2 n2-0) (n1 n1) (b b) (a a)) resp ((n2 n2) (n1 n1-0) (b b) (a a)) resp ((n1 n1-0) (n2 n2) (a a) (b b)) init ((n1 n1) (n2 n2-0) (a a) (b b)) init ns 40 (realized)
(defskeleton ns
  (vars (n1 n1-0 n2 n2-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))
  (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n1-0) (b b) (a a))
  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1 n1-0)
  (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1)
    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
  (label 40)
  (parent 39)
  (unrealized)
  (shape)
  (satisfies
    (no (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2) (a a) (b b) (z (0 0))
      (z-0 (0 2)) (z-1 (1 0)) (z-2 (1 2))))
  (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2))))
  (origs (n1 (0 0)) (n1-0 (1 0))))

Tree 41.

44 43 42 41 
(defprotocol nsl-typeless basic
  (defrole init
    (vars (a b name) (n1 text) (n2 mesg))
    (trace (send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 text) (n1 mesg))
    (trace (recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (comment "Needham-Schroeder-Lowe with untyped nonces"))

Item 41, Child: 42.

(enc n1 n2 b (pubk a)) (enc a n1 (pubk b)) n2 n2 ((n1 n1) (n2 n2) (b b) (a a)) resp nsl-typeless 41
(defskeleton nsl-typeless
  (vars (n1 mesg) (n2 text) (a b name))
  (deflistener n2)
  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (goals
    (forall ((n2 text) (a b name) (z z-0 node))
      (implies
        (and (p "resp" 1 z) (p "" 0 z-0) (p "resp" "n2" z n2)
          (p "resp" "b" z b) (p "resp" "a" z a) (p "" "x" z-0 n2)
          (non (privk a)) (non (privk b)) (uniq n2)) (false))))
  (comment "Shows typeflaw in typeless NSL")
  (label 41)
  (unrealized (0 0))
  (preskeleton)
  (comment "Not a skeleton"))

Item 42, Parent: 41, Children: 43 44.

(enc n1 n2 b (pubk a)) (enc a n1 (pubk b)) n2 n2 ((n1 n1) (n2 n2) (b b) (a a)) resp nsl-typeless 42
(defskeleton nsl-typeless
  (vars (n1 mesg) (n2 text) (a b name))
  (deflistener n2)
  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
  (precedes ((1 1) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (goals
    (forall ((n2 text) (a b name) (z z-0 node))
      (implies
        (and (p "resp" 1 z) (p "" 0 z-0) (p "resp" "n2" z n2)
          (p "resp" "b" z b) (p "resp" "a" z a) (p "" "x" z-0 n2)
          (non (privk a)) (non (privk b)) (uniq n2)) (false))))
  (comment "Shows typeflaw in typeless NSL")
  (label 42)
  (parent 41)
  (unrealized (0 0))
  (origs (n2 (1 1)))
  (comment "2 in cohort - 2 not yet seen"))

Item 43, Parent: 42.

(enc n2 (pubk b)) (enc n1 n2 b (pubk a)) (enc a n1 (pubk b)) (enc n1 n2 b (pubk a)) (enc a n1 (pubk b)) n2 n2 ((n2 n2) (n1 n1) (a a) (b b)) init ((n1 n1) (n2 n2) (b b) (a a)) resp nsl-typeless 43
(defskeleton nsl-typeless
  (vars (n2 n1 text) (a b name))
  (deflistener n2)
  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
  (defstrand init 3 (n2 n2) (n1 n1) (a a) (b b))
  (precedes ((1 1) (2 1)) ((2 2) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 0)
    (enc n1 n2 b (pubk a)))
  (label 43)
  (parent 42)
  (unrealized (0 0))
  (comment "empty cohort"))

Item 44, Parent: 42.

(enc (cat n2 b) n2-0 a (pubk a-0)) (enc a-0 n2 b (pubk a)) (enc a-0 n2 b (pubk a)) (enc a a-0 (pubk b)) n2 n2 ((n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0)) resp ((n1 a-0) (n2 n2) (b b) (a a)) resp nsl-typeless 44 (realized) 
(defskeleton nsl-typeless
  (vars (n2 n2-0 text) (a b a-0 name))
  (deflistener n2)
  (defstrand resp 2 (n1 a-0) (n2 n2) (b b) (a a))
  (defstrand resp 2 (n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0))
  (precedes ((1 1) (2 0)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (operation nonce-test (added-strand resp 2) n2 (0 0)
    (enc a-0 n2 b (pubk a)))
  (label 44)
  (parent 42)
  (unrealized)
  (shape)
  (satisfies (no (n2 n2) (a a) (b b) (z (1 1)) (z-0 (0 0))))
  (maps ((0 1) ((n2 n2) (a a) (b b) (n1 a-0))))
  (origs (n2 (1 1))))

Tree 45.

46 45 
(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 with no role origination assumptions"))

Item 45, Child: 46.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (b b) (a a)) resp ns 45 
(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a))
  (uniq-orig n2)
  (subgoals
    (forall ((n1 n2 text) (a b name) (z z-0 node))
      (implies
        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
          (non (privk b)) (uniq-at n1 z))
        (exists ((z-1 z-2 z-3 node))
          (and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)
            (p "resp" "n2" z-3 n2) (p "resp" "n1" z-3 n1)
            (p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)
            (prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)
            (str-prec z-2 z-3))))))
  (comment "Responder point of view with SAS")
  (label 45)
  (unrealized (0 2))
  (origs (n2 (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 46, Parent: 45.

(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 46 (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))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc n1 n2 (pubk a)))
  (label 46)
  (parent 45)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
  (origs (n2 (0 1))))

Tree 47.

48 47 
(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 with no role origination assumptions"))

Item 47, Child: 48.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (b b) (a a)) resp ns 47 
(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a))
  (uniq-orig n2)
  (subgoals
    (forall ((n1 n2 text) (a b name) (z z-0 node))
      (implies
        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
          (non (privk b)) (uniq-at n1 z)) (false))))
  (comment "Responder point of view with false as the conclusion")
  (label 47)
  (unrealized (0 2))
  (origs (n2 (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 48, Parent: 47.

(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 48 (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))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc n1 n2 (pubk a)))
  (label 48)
  (parent 47)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
  (origs (n2 (0 1))))

Tree 49.

51 50 49 
(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 with no role origination assumptions"))

Item 49, Child: 50.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (a a) (b b)) init ns 49 
(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)
  (subgoals
    (forall ((n1 n2 text) (a b name) (z z-0 node))
      (implies
        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
          (non (privk b)) (uniq-at n1 z)) (false))))
  (comment "Initiator point of view with false as the conclusion")
  (label 49)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 50, Parent: 49, Child: 51.

(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 50 
(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 50)
  (parent 49)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 51, Parent: 50.

(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 51 (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 51)
  (parent 50)
  (unrealized)
  (shape)
  (satisfies (no (n1 n1) (n2 n2) (a a) (b b) (z (0 0)) (z-0 (0 2))))
  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  (origs (n1 (0 0))))

Tree 52.

53 52 
(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 with no role origination assumptions"))

Item 52, Child: 53.

(enc n (pubk b)) (enc n1 n (pubk a)) (enc n1 a (pubk b)) ((n2 n) (n1 n1) (b b) (a a)) resp ns 52 
(defskeleton ns
  (vars (n n1 text) (a b name))
  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
  (non-orig (privk a) (privk b))
  (uniq-orig n)
  (goals
    (forall ((a b name) (n text) (z0 node))
      (implies
        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
        (exists ((z1 node)) (and (p "init" 2 z1) (p "init" "a" z1 a)))))
    (forall ((a b name) (n text) (z0 node))
      (implies
        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
        (exists ((z1 node))
          (and (p "init" 2 z1) (p "init" "b" z1 b))))))
  (comment "Two responder authentication goals")
  (label 52)
  (unrealized (0 2))
  (origs (n (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 53, Parent: 52.

(enc n (pubk b-0)) (enc n1 n (pubk a)) (enc n1 a (pubk b-0)) (enc n (pubk b)) (enc n1 n (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n) (a a) (b b-0)) init ((n2 n) (n1 n1) (b b) (a a)) resp ns 53 (realized)
(defskeleton ns
  (vars (n n1 text) (a b b-0 name))
  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig n)
  (operation nonce-test (added-strand init 3) n (0 2)
    (enc n1 n (pubk a)))
  (label 53)
  (parent 52)
  (unrealized)
  (shape)
  (satisfies yes (no (a a) (b b) (n n) (z0 (0 2))))
  (maps ((0) ((a a) (b b) (n n) (n1 n1))))
  (origs (n (0 1))))

Tree 54.

56 55 54 
(defprotocol ns-role-origs 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))))
    (non-orig (privk b))
    (uniq-orig n1))
  (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))))
    (non-orig (privk a))
    (uniq-orig n2))
  (comment
    "Needham-Schroeder with role assumptions that are too strong"))

Item 54, Child: 55.

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

Item 55, Parent: 54, Child: 56.

(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-role-origs 55
(defskeleton ns-role-origs
  (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 n2-0)
  (operation nonce-test (added-strand resp 2) n1 (0 1)
    (enc n1 a (pubk b)))
  (label 55)
  (parent 54)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 56, Parent: 55.

(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-role-origs 56 (realized) 
(defskeleton ns-role-origs
  (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 n2)
  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
  (label 56)
  (parent 55)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  (origs (n2 (1 1)) (n1 (0 0))))

Tree 57.

59 61 60 59 58 57 
(defprotocol ns-role-origs 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))))
    (non-orig (privk b))
    (uniq-orig n1))
  (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))))
    (non-orig (privk a))
    (uniq-orig n2))
  (comment
    "Needham-Schroeder with role assumptions that are too strong"))

Item 57, Child: 58.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n2 n2) (n1 n1) (b b) (a a)) resp ns-role-origs 57
(defskeleton ns-role-origs
  (vars (n2 n1 text) (b a name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a))
  (uniq-orig n2)
  (label 57)
  (unrealized (0 2))
  (origs (n2 (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 58, Parent: 57, Children: 59 60.

(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-role-origs 58
(defskeleton ns-role-origs
  (vars (n2 n1 text) (b a 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 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b-0))
  (uniq-orig n2 n1)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc n1 n2 (pubk a)))
  (label 58)
  (parent 57)
  (unrealized (0 0) (0 2))
  (comment "2 in cohort - 2 not yet seen"))

Item 59, Parent: 58.

(enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) (enc n2 (pubk b)) (enc n1 n2 (pubk a)) (enc n1 a (pubk b)) ((n1 n1) (n2 n2) (a a) (b b)) init ((n2 n2) (n1 n1) (b b) (a a)) resp ns-role-origs 59 (realized) 
(defskeleton ns-role-origs
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2 n1)
  (operation nonce-test (contracted (b-0 b)) n1 (0 0)
    (enc n1 a (pubk b)))
  (label 59)
  (parent 58)
  (unrealized)
  (shape)
  (maps ((0) ((b b) (a a) (n2 n2) (n1 n1))))
  (origs (n1 (1 0)) (n2 (0 1))))

Item 60, Parent: 58, Child: 61.

(enc n1 n2-0 (pubk a)) (enc n1 a (pubk b-0)) (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)) ((n2 n2-0) (n1 n1) (b b-0) (a a)) resp ((n1 n1) (n2 n2) (a a) (b b-0)) init ((n2 n2) (n1 n1) (b b) (a a)) resp ns-role-origs 60
(defskeleton ns-role-origs
  (vars (n2 n1 n2-0 text) (b a 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))
  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b-0) (a a))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b-0))
  (uniq-orig n2 n1 n2-0)
  (operation nonce-test (added-strand resp 2) n1 (0 0)
    (enc n1 a (pubk b-0)))
  (label 60)
  (parent 58)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

Item 61, Parent: 60, Seen Child: 59.

(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)) (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 ((n2 n2) (n1 n1) (b b) (a a)) resp ns-role-origs 61 (realized) 
(defskeleton ns-role-origs
  (vars (n2 n1 n2-0 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (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 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2 n1 n2-0)
  (operation nonce-test (contracted (b-0 b)) n1 (0 0)
    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
  (label 61)
  (parent 60)
  (seen 59)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Tree 62.

64 63 62 
(defprotocol ns2 basic
  (defrole init
    (vars (a b name) (n1 n2 n3 text))
    (trace (send (enc n1 n3 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 n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
      (recv (enc n2 (pubk b))))
    (note doubled nonce in the first message))
  (note that this protocol is derived from Needham-Schroeder))

Item 62, Child: 63.

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

Item 63, Parent: 62, Child: 64.

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

Item 64, Parent: 63.

(enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)) (enc n2 (pubk b)) (enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)) ((n2 n2) (n1 n3) (b b) (a a)) resp ((n1 n3) (n2 n2) (n3 n3) (a a) (b b)) init ns2 64 (realized)
(defskeleton ns2
  (vars (n3 n2 text) (a b name))
  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n3) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n3)
  (operation nonce-test (contracted (n2-0 n2)) n3 (0 1)
    (enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)))
  (label 64)
  (parent 63)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3))))
  (origs (n3 (0 0))))

Tree 65.

65 
(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 with no role origination assumptions"))

Item 65.

(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 65 (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)
  (label 65)
  (unrealized)
  (shape)
  (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b))))
  (origs (n1 (0 0))))