(herald "Station-to-station protocol" (algebra diffie-hellman))
(comment "CPSA 3.4.0")
(comment "All input read from station.scm")

Trees: 0 67 96 127.

Tree 0.

(defprotocol station-to-station diffie-hellman
  (defrole init
    (vars (x expn) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc (exp (gen) x) h (privk a)) (exp h x))))
    (uniq-gen x))
  (defrole resp
    (vars (y expn) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc h (exp (gen) y) (privk a)) (exp h y))))
    (uniq-gen y)
    (absent (y h))))

Item 0, Children: 1 2 3.

(defskeleton station-to-station
  (vars (a b name) (h base) (x expn))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (label 0)
  (unrealized (0 1))
  (origs)
  (comment "3 in cohort - 3 not yet seen"))

Item 1, Parent: 0, Child: 4.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (1 1)) ((1 2) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (operation encryption-test (added-strand init 3)
    (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b))
      (exp (gen) (mul x x-0))) (0 1))
  (label 1)
  (parent 0)
  (unrealized (1 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 2, Parent: 0.

(defskeleton station-to-station
  (vars (a b name) (x y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation encryption-test (added-strand resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
      (exp (gen) (mul x y))) (0 1))
  (label 2)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (h (exp (gen) y)))))
  (origs))

Item 3, Parent: 0, Children: 5 6 7 8 9.

(defskeleton station-to-station
  (vars (a b name) (h base) (x expn))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation encryption-test (added-listener (exp h x))
    (enc (enc h (exp (gen) x) (privk b)) (exp h x)) (0 1))
  (label 3)
  (parent 0)
  (unrealized (0 1) (1 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 4, Parent: 1, Child: 10.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((1 0) (2 0)) ((1 2) (0 1)) ((2 1) (1 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (operation encryption-test (added-listener (exp (gen) (mul x x-0)))
    (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b-0))
      (exp (gen) (mul x x-0))) (1 1))
  (label 4)
  (parent 1)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 5, Parent: 3.

(defskeleton station-to-station
  (vars (a b name) (x expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (contracted (h (exp (gen) (rec x)))) (gen)
    (1 0))
  (label 5)
  (parent 3)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 6, Parent: 3.

(defskeleton station-to-station
  (vars (a b name) (x expn))
  (defstrand init 3 (a a) (b b) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (label 6)
  (parent 3)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 7, Parent: 3.

(defskeleton station-to-station
  (vars (a b name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (label 7)
  (parent 3)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 8, Parent: 3.

(defskeleton station-to-station
  (vars (a b b-0 name) (h base) (x y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (1 0))
  (label 8)
  (parent 3)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 9, Parent: 3, Children: 11 12 13 14.

(defskeleton station-to-station
  (vars (a b name) (h base) (x expn) (w expr))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (deflistener (cat (exp h (mul x (rec w))) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul x (rec w))) w))
    (exp h x) (1 0))
  (label 9)
  (parent 3)
  (unrealized (0 1) (2 0))
  (comment "4 in cohort - 4 not yet seen"))

Item 10, Parent: 4, Children: 15 16 17 18 19.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn) (w expr))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) (mul x x-0 (rec w))) w))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x-0 (rec w))) w))
    (exp (gen) (mul x x-0)) (2 0))
  (label 10)
  (parent 4)
  (unrealized (3 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 11, Parent: 9, Children: 20 21.

(defskeleton station-to-station
  (vars (a b name) (x expn) (w expr))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w))) (x x))
  (deflistener (exp (gen) w))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (contracted (h (exp (gen) (mul (rec x) w))))
    (gen) (2 0))
  (label 11)
  (parent 9)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 12, Parent: 9, Children: 22 23.

(defskeleton station-to-station
  (vars (a b name) (w expr) (x expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul w x)))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (label 12)
  (parent 9)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 13, Parent: 9, Children: 24 25 26.

(defskeleton station-to-station
  (vars (a b name) (x expn) (w expr) (x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w x-0)))
    (x x))
  (deflistener (exp (gen) (mul w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (label 13)
  (parent 9)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 14, Parent: 9, Children: 27 28 29.

(defskeleton station-to-station
  (vars (a b b-0 name) (h base) (x expn) (w expr) (y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w y))) (x x))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (2 0))
  (label 14)
  (parent 9)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 15, Parent: 10.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (precur (3 0))
  (operation nonce-test (contracted (x-1 x) (x-2 x-0) (w (mul x x-0)))
    (gen) (3 0))
  (label 15)
  (parent 10)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

Item 16, Parent: 10.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x)) (x x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 4 0 init 1) (exp (gen) x-1) (3 0))
  (label 16)
  (parent 10)
  (unrealized (3 0))
  (comment "empty cohort"))

Item 17, Parent: 10.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-1) (3 0))
  (label 17)
  (parent 10)
  (unrealized (3 0))
  (comment "empty cohort"))

Item 18, Parent: 10.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 0) (3 0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (3 0))
  (label 18)
  (parent 10)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

Item 19, Parent: 10.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x x-0 y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x x-0 (rec y))))
  (defstrand resp 2 (b b-1) (h h) (y y))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0 y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (3 0))
  (label 19)
  (parent 10)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

Item 20, Parent: 11, Child: 30.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0)
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (0 1))
  (label 20)
  (parent 11)
  (unrealized (1 0) (2 0) (3 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 21, Parent: 11.

(defskeleton station-to-station
  (vars (a b name) (x y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y)
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 21)
  (parent 11)
  (unrealized (1 0) (2 0))
  (comment "empty cohort"))

Item 22, Parent: 12, Child: 31.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0)
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (0 1))
  (label 22)
  (parent 12)
  (unrealized (2 0) (3 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 23, Parent: 12.

(defskeleton station-to-station
  (vars (a b name) (x y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x) y))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y)
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 23)
  (parent 12)
  (unrealized (2 0))
  (comment "empty cohort"))

Item 24, Parent: 13, Child: 32.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0)
  (operation encryption-test (displaced 3 4 init 3)
    (enc (exp (gen) x-1) (exp (gen) x) (privk b)) (0 1))
  (label 24)
  (parent 13)
  (unrealized (2 0) (3 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 25, Parent: 13, Child: 33.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-1)) (x x))
  (deflistener (exp (gen) (mul x x-1)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) x-1)))
  (defstrand init 1 (x x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (4 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0 x-1)
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) x-1) (exp (gen) x) (privk b)) (0 1))
  (label 25)
  (parent 13)
  (unrealized (1 0) (2 0) (4 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 26, Parent: 13.

(defskeleton station-to-station
  (vars (a b name) (x x-0 y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) y)))
  (defstrand init 1 (x x-0))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0))
    ((4 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0 y)
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 26)
  (parent 13)
  (unrealized (1 0) (2 0))
  (comment "empty cohort"))

Item 27, Parent: 14, Child: 34.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x y x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 2) (0 1)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y x-0)
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (0 1))
  (label 27)
  (parent 14)
  (unrealized (1 0) (2 0) (4 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 28, Parent: 14.

(defskeleton station-to-station
  (vars (a b name) (x y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y)
  (operation encryption-test (displaced 4 3 resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b-0)) (0 1))
  (label 28)
  (parent 14)
  (unrealized (2 0))
  (comment "empty cohort"))

Item 29, Parent: 14.

(defskeleton station-to-station
  (vars (a b b-0 name) (h base) (x y y-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y-0)) (x x))
  (deflistener (exp (gen) (mul x y-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) y-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y-0))
  (precedes ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (2 0)))
  (absent (y-0 (exp (gen) x)) (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y y-0)
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b)) (0 1))
  (label 29)
  (parent 14)
  (unrealized (1 0) (2 0))
  (comment "empty cohort"))

Item 30, Parent: 20, Child: 35.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 2) (0 1)) ((4 1) (3 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0)
  (operation encryption-test (added-listener (exp (gen) (mul x x-0)))
    (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b-0))
      (exp (gen) (mul x x-0))) (3 1))
  (label 30)
  (parent 20)
  (unrealized (1 0) (2 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 31, Parent: 22, Child: 36.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 2) (0 1)) ((4 1) (3 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0)
  (operation encryption-test (added-listener (exp (gen) (mul x x-0)))
    (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b-0))
      (exp (gen) (mul x x-0))) (3 1))
  (label 31)
  (parent 22)
  (unrealized (2 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 32, Parent: 24, Child: 37.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 2) (0 1)) ((4 1) (3 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0)
  (operation encryption-test (added-listener (exp (gen) (mul x x-0)))
    (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b-0))
      (exp (gen) (mul x x-0))) (3 1))
  (label 32)
  (parent 24)
  (unrealized (2 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 33, Parent: 25, Child: 38.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-1)) (x x))
  (deflistener (exp (gen) (mul x x-1)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) x-1)))
  (defstrand init 1 (x x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-1))
  (deflistener (exp (gen) (mul x x-1)))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 0) (5 0)) ((4 2) (0 1))
    ((5 1) (4 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x x-0 x-1)
  (operation encryption-test (added-listener (exp (gen) (mul x x-1)))
    (enc (enc (exp (gen) x) (exp (gen) x-1) (privk b-0))
      (exp (gen) (mul x x-1))) (4 1))
  (label 33)
  (parent 25)
  (unrealized (1 0) (2 0) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 34, Parent: 27, Child: 39.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x y x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 0) (5 0)) ((4 2) (0 1))
    ((5 1) (4 1)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y x-0)
  (operation encryption-test (added-listener (exp (gen) (mul x x-0)))
    (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b-1))
      (exp (gen) (mul x x-0))) (4 1))
  (label 34)
  (parent 27)
  (unrealized (1 0) (2 0) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 35, Parent: 30, Children: 40 41 42 43 44.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn) (w expr))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) (mul x x-0 (rec w))) w))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x-0 (rec w))) w))
    (exp (gen) (mul x x-0)) (4 0))
  (label 35)
  (parent 30)
  (unrealized (1 0) (2 0) (5 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 36, Parent: 31, Children: 45 46 47 48 49.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn) (w expr))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) (mul x x-0 (rec w))) w))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x-0 (rec w))) w))
    (exp (gen) (mul x x-0)) (4 0))
  (label 36)
  (parent 31)
  (unrealized (2 0) (5 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 37, Parent: 32, Children: 50 51 52 53 54.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn) (w expr))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) (mul x x-0 (rec w))) w))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x-0 (rec w))) w))
    (exp (gen) (mul x x-0)) (4 0))
  (label 37)
  (parent 32)
  (unrealized (2 0) (5 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 38, Parent: 33, Children: 55 56 57 58 59 60.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn) (w expr))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-1)) (x x))
  (deflistener (exp (gen) (mul x x-1)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) x-1)))
  (defstrand init 1 (x x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-1))
  (deflistener (exp (gen) (mul x x-1)))
  (deflistener (cat (exp (gen) (mul x x-1 (rec w))) w))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x-1 (rec w))) w))
    (exp (gen) (mul x x-1)) (5 0))
  (label 38)
  (parent 33)
  (unrealized (1 0) (2 0) (6 0))
  (comment "6 in cohort - 6 not yet seen"))

Item 39, Parent: 34, Children: 61 62 63 64 65 66.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x y x-0 expn) (w expr))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) (mul x x-0 (rec w))) w))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x y x-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x-0 (rec w))) w))
    (exp (gen) (mul x x-0)) (5 0))
  (label 39)
  (parent 34)
  (unrealized (1 0) (2 0) (6 0))
  (comment "6 in cohort - 6 not yet seen"))

Item 40, Parent: 35.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (contracted (x-1 x) (x-2 x-0) (w (mul x x-0)))
    (gen) (5 0))
  (label 40)
  (parent 35)
  (unrealized (1 0) (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 41, Parent: 35.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 6 0 init 1) (exp (gen) x-1) (5 0))
  (label 41)
  (parent 35)
  (unrealized (1 0) (2 0) (5 0))
  (comment "empty cohort"))

Item 42, Parent: 35.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 6 3 init 1) (exp (gen) x-1) (5 0))
  (label 42)
  (parent 35)
  (unrealized (1 0) (2 0) (5 0))
  (comment "empty cohort"))

Item 43, Parent: 35.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 0) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (5 0))
  (label 43)
  (parent 35)
  (unrealized (1 0) (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 44, Parent: 35.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x x-0 y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x x-0 (rec y))))
  (defstrand resp 2 (b b-1) (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0 y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (5 0))
  (label 44)
  (parent 35)
  (unrealized (1 0) (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 45, Parent: 36.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (contracted (x-1 x) (x-2 x-0) (w (mul x x-0)))
    (gen) (5 0))
  (label 45)
  (parent 36)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 46, Parent: 36.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 6 0 init 1) (exp (gen) x-1) (5 0))
  (label 46)
  (parent 36)
  (unrealized (2 0) (5 0))
  (comment "empty cohort"))

Item 47, Parent: 36.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 6 3 init 1) (exp (gen) x-1) (5 0))
  (label 47)
  (parent 36)
  (unrealized (2 0) (5 0))
  (comment "empty cohort"))

Item 48, Parent: 36.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 0) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (5 0))
  (label 48)
  (parent 36)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 49, Parent: 36.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x x-0 y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x x-0 (rec y))))
  (defstrand resp 2 (b b-1) (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0 y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (5 0))
  (label 49)
  (parent 36)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 50, Parent: 37.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (contracted (x-1 x) (x-2 x-0) (w (mul x x-0)))
    (gen) (5 0))
  (label 50)
  (parent 37)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 51, Parent: 37.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 6 0 init 1) (exp (gen) x-1) (5 0))
  (label 51)
  (parent 37)
  (unrealized (2 0) (5 0))
  (comment "empty cohort"))

Item 52, Parent: 37.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 6 3 init 1) (exp (gen) x-1) (5 0))
  (label 52)
  (parent 37)
  (unrealized (2 0) (5 0))
  (comment "empty cohort"))

Item 53, Parent: 37.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 0) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (5 0))
  (label 53)
  (parent 37)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 54, Parent: 37.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x x-0 y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x x-0 (rec y))))
  (defstrand resp 2 (b b-1) (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (5 0)) ((3 2) (0 1)) ((4 1) (3 1))
    ((5 1) (4 0)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x x-0 y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (5 0))
  (label 54)
  (parent 37)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 55, Parent: 38.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-1)) (x x-0))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x) (mul (rec x) x-0 x-1)))
  (defstrand init 1 (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x-1))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (gen) (mul x-0 x-1)))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test
    (contracted (x-2 x-0) (x-3 x-1) (w (mul x-0 x-1))) (gen) (6 0))
  (label 55)
  (parent 38)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Item 56, Parent: 38.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x-1))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x) (mul (rec x) x-0 x-1)))
  (defstrand init 1 (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-1)) (x x-0))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x-1) x-0))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (displaced 7 0 init 1) (exp (gen) x-2) (6 0))
  (label 56)
  (parent 38)
  (unrealized (1 0) (2 0) (6 0))
  (comment "empty cohort"))

Item 57, Parent: 38.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 0) (6 0)) ((4 0) (2 0)) ((4 0) (6 0))
    ((4 2) (0 1)) ((5 1) (4 1)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (displaced 7 3 init 1) (exp (gen) x-2) (6 0))
  (label 57)
  (parent 38)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Item 58, Parent: 38.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-1)) (x x-0))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x) (mul (rec x) x-0 x-1)))
  (defstrand init 1 (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x-1))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x-1) x-0))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (displaced 7 4 init 1) (exp (gen) x-2) (6 0))
  (label 58)
  (parent 38)
  (unrealized (1 0) (2 0) (6 0))
  (comment "empty cohort"))

Item 59, Parent: 38.

(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 x-2 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-1)) (x x-0))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x) (mul (rec x) x-0 x-1)))
  (defstrand init 1 (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x-1))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x-2) (mul x-0 x-1 (rec x-2))))
  (defstrand init 1 (x x-2))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)) ((7 0) (6 0)))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 x-1 x-2)
  (operation nonce-test (added-strand init 1) (exp (gen) x-2) (6 0))
  (label 59)
  (parent 38)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Item 60, Parent: 38.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x x-0 x-1 y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-1)) (x x-0))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) x) (mul (rec x) x-0 x-1)))
  (defstrand init 1 (x x))
  (defstrand init 3 (a b) (b b-0) (h (exp (gen) x-0)) (x x-1))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) y) (mul x-0 x-1 (rec y))))
  (defstrand resp 2 (b b-1) (h h) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)) ((7 1) (6 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 x-1 y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (6 0))
  (label 60)
  (parent 38)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Item 61, Parent: 39.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (y x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul (rec y) x x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen y x x-0)
  (operation nonce-test (contracted (x-1 x) (x-2 x-0) (w (mul x x-0)))
    (gen) (6 0))
  (label 61)
  (parent 39)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Item 62, Parent: 39.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (y x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul (rec y) x x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen y x x-0)
  (operation nonce-test (displaced 7 0 init 1) (exp (gen) x-1) (6 0))
  (label 62)
  (parent 39)
  (unrealized (1 0) (2 0) (6 0))
  (comment "empty cohort"))

Item 63, Parent: 39.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (y x x-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul (rec y) x x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen y x x-0)
  (operation nonce-test (displaced 7 4 init 1) (exp (gen) x-1) (6 0))
  (label 63)
  (parent 39)
  (unrealized (1 0) (2 0) (6 0))
  (comment "empty cohort"))

Item 64, Parent: 39.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (y x x-0 x-1 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul (rec y) x x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)) ((7 0) (6 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen y x x-0 x-1)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (6 0))
  (label 64)
  (parent 39)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Item 65, Parent: 39.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (x x-0 y expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x x-0 (rec y))))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x x-0 (rec y))))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (6 0)) ((4 0) (2 0)) ((4 0) (6 0))
    ((4 2) (0 1)) ((5 1) (4 1)) ((6 1) (5 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen x x-0 y)
  (operation nonce-test (displaced 7 3 resp 2) (exp (gen) y-0) (6 0))
  (label 65)
  (parent 39)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Item 66, Parent: 39.

(defskeleton station-to-station
  (vars (a b b-0 b-1 b-2 name) (h h-0 base) (y x x-0 y-0 expn))
  (defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul (rec y) x x-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y-0) (mul x x-0 (rec y-0))))
  (defstrand resp 2 (b b-2) (h h-0) (y y-0))
  (precedes ((0 0) (2 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 0) (2 0)) ((4 0) (6 0)) ((4 2) (0 1))
    ((5 1) (4 1)) ((6 1) (5 0)) ((7 1) (6 0)))
  (absent (y-0 h-0) (y h))
  (non-orig (privk a) (privk b))
  (precur (6 0) (2 0))
  (uniq-gen y x x-0 y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (6 0))
  (label 66)
  (parent 39)
  (unrealized (1 0) (2 0) (5 0) (6 0))
  (comment "empty cohort"))

Tree 67.

(defprotocol station-to-station diffie-hellman
  (defrole init
    (vars (x expn) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc (exp (gen) x) h (privk a)) (exp h x))))
    (uniq-gen x))
  (defrole resp
    (vars (y expn) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc h (exp (gen) y) (privk a)) (exp h y))))
    (uniq-gen y)
    (absent (y h))))

Item 67, Children: 68 69.

(defskeleton station-to-station
  (vars (a b name) (h base) (y expn))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (label 67)
  (unrealized (0 2))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

Item 68, Parent: 67, Children: 70 71.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (operation encryption-test (added-strand init 3)
    (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
      (exp (gen) (mul y x))) (0 2))
  (label 68)
  (parent 67)
  (unrealized (1 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 69, Parent: 67, Children: 72 73.

(defskeleton station-to-station
  (vars (a b name) (h base) (y expn))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (operation encryption-test (added-listener (exp h y))
    (enc (enc h (exp (gen) y) (privk a)) (exp h y)) (0 2))
  (label 69)
  (parent 67)
  (unrealized (0 2) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 70, Parent: 68.

(defskeleton station-to-station
  (vars (a b name) (x y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (1 1))
  (label 70)
  (parent 68)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (y y) (h (exp (gen) x)))))
  (origs))

Item 71, Parent: 68, Child: 74.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (1 1))
  (label 71)
  (parent 68)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 72, Parent: 69.

(defskeleton station-to-station
  (vars (a b name) (y expn))
  (defstrand resp 3 (a a) (b b) (h (gen)) (y y))
  (deflistener (exp (gen) y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y (gen)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (operation nonce-test (displaced 2 0 resp 2) (exp (gen) y-0) (1 0))
  (label 72)
  (parent 69)
  (unrealized (0 2))
  (comment "empty cohort"))

Item 73, Parent: 69, Children: 75 76 77 78.

(defskeleton station-to-station
  (vars (a b name) (h base) (y expn) (w expr))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (deflistener (cat (exp h (mul y (rec w))) w))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul y (rec w))) w))
    (exp h y) (1 0))
  (label 73)
  (parent 69)
  (unrealized (0 2) (2 0))
  (comment "4 in cohort - 4 not yet seen"))

Item 74, Parent: 71, Children: 79 80 81 82 83.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn) (w expr))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) (mul y x (rec w))) w))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec w))) w))
    (exp (gen) (mul y x)) (2 0))
  (label 74)
  (parent 71)
  (unrealized (3 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 75, Parent: 73, Child: 84.

(defskeleton station-to-station
  (vars (a b name) (w expr) (y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (gen) (mul w y)))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (absent (y (exp (gen) w)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (precur (2 0))
  (operation nonce-test
    (contracted (y-0 y) (h (exp (gen) w)) (w (mul w y))) (gen) (2 0))
  (label 75)
  (parent 73)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 76, Parent: 73, Child: 85.

(defskeleton station-to-station
  (vars (a b name) (w expr) (x y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) (mul w x))) (y y))
  (deflistener (exp (gen) (mul w x y)))
  (deflistener (cat (exp (gen) x) (mul w y)))
  (defstrand init 1 (x x))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)) ((3 0) (0 0)))
  (absent (y (exp (gen) (mul w x))))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y)
  (operation nonce-test (added-strand init 1) (exp (gen) x) (2 0))
  (label 76)
  (parent 73)
  (unrealized (0 2) (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 77, Parent: 73, Child: 86.

(defskeleton station-to-station
  (vars (a b name) (w expr) (y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (absent (y (exp (gen) w)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y)
  (operation nonce-test (displaced 3 0 resp 2) (exp (gen) y-0) (2 0))
  (label 77)
  (parent 73)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

Item 78, Parent: 73, Child: 87.

(defskeleton station-to-station
  (vars (a b b-0 name) (h base) (w expr) (y y-0 expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) (mul w y))) (y y-0))
  (deflistener (exp (gen) (mul w y y-0)))
  (deflistener (cat (exp (gen) y) (mul w y-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)) ((3 1) (0 0)))
  (absent (y h) (y-0 (exp (gen) (mul w y))))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (2 0))
  (label 78)
  (parent 73)
  (unrealized (0 2) (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 79, Parent: 74.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (gen) (mul y x)))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (precur (3 0))
  (operation nonce-test (contracted (y-0 y) (x-0 x) (w (mul y x))) (gen)
    (3 0))
  (label 79)
  (parent 74)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

Item 80, Parent: 74.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-0) (3 0))
  (label 80)
  (parent 74)
  (unrealized (3 0))
  (comment "empty cohort"))

Item 81, Parent: 74.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x x-0 expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 0) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (3 0))
  (label 81)
  (parent 74)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

Item 82, Parent: 74.

(defskeleton station-to-station
  (vars (a b b-0 name) (x y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y)
  (operation nonce-test (displaced 4 0 resp 2) (exp (gen) y-0) (3 0))
  (label 82)
  (parent 74)
  (unrealized (3 0))
  (comment "empty cohort"))

Item 83, Parent: 74.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (y x y-0 expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y-0) (mul y x (rec y-0))))
  (defstrand resp 2 (b b-1) (h h) (y y-0))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y-0 h) (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (label 83)
  (parent 74)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

Item 84, Parent: 75.

(defskeleton station-to-station
  (vars (a b name) (w expr) (y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (gen) (mul w y)))
  (deflistener y)
  (precedes ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0)))
  (absent (y (exp (gen) w)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (precur (2 0))
  (operation nonce-test (added-listener y) (mul w y) (2 0))
  (label 84)
  (parent 75)
  (unrealized (0 2) (3 0))
  (comment "empty cohort"))

Item 85, Parent: 76.

(defskeleton station-to-station
  (vars (a b name) (w expr) (x y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) (mul w x))) (y y))
  (deflistener (exp (gen) (mul w x y)))
  (deflistener (cat (exp (gen) x) (mul w y)))
  (defstrand init 1 (x x))
  (deflistener y)
  (precedes ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (1 0)) ((3 0) (0 0))
    ((4 1) (2 0)))
  (absent (y (exp (gen) (mul w x))))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y)
  (operation nonce-test (added-listener y) (mul w y) (2 0))
  (label 85)
  (parent 76)
  (unrealized (0 2) (4 0))
  (comment "empty cohort"))

Item 86, Parent: 77, Children: 88 89.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y x)
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) x) (exp (gen) y) (privk a)) (0 2))
  (label 86)
  (parent 77)
  (unrealized (2 0) (3 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 87, Parent: 78.

(defskeleton station-to-station
  (vars (a b b-0 name) (h base) (w expr) (y y-0 expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) (mul w y))) (y y-0))
  (deflistener (exp (gen) (mul w y y-0)))
  (deflistener (cat (exp (gen) y) (mul w y-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (deflistener y-0)
  (precedes ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (1 0)) ((3 1) (0 0))
    ((4 1) (2 0)))
  (absent (y h) (y-0 (exp (gen) (mul w y))))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y y-0)
  (operation nonce-test (added-listener y-0) (mul w y-0) (2 0))
  (label 87)
  (parent 78)
  (unrealized (0 2) (4 0))
  (comment "empty cohort"))

Item 88, Parent: 86.

(defskeleton station-to-station
  (vars (a b name) (x y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y)
  (operation encryption-test (displaced 4 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (3 1))
  (label 88)
  (parent 86)
  (unrealized (2 0))
  (comment "empty cohort"))

Item 89, Parent: 86, Child: 90.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y x)
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (3 1))
  (label 89)
  (parent 86)
  (unrealized (2 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 90, Parent: 89, Children: 91 92 93 94 95.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn) (w expr))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) (mul y x (rec w))) w))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen y x)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec w))) w))
    (exp (gen) (mul y x)) (4 0))
  (label 90)
  (parent 89)
  (unrealized (2 0) (5 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 91, Parent: 90.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen y x)
  (operation nonce-test (contracted (y-0 y) (x-0 x) (w (mul y x))) (gen)
    (5 0))
  (label 91)
  (parent 90)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 92, Parent: 90.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen y x)
  (operation nonce-test (displaced 6 3 init 1) (exp (gen) x-0) (5 0))
  (label 92)
  (parent 90)
  (unrealized (2 0) (5 0))
  (comment "empty cohort"))

Item 93, Parent: 90.

(defskeleton station-to-station
  (vars (a b b-0 name) (y x x-0 expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0))
    ((6 0) (5 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen y x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (5 0))
  (label 93)
  (parent 90)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Item 94, Parent: 90.

(defskeleton station-to-station
  (vars (a b b-0 name) (x y expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen x y)
  (operation nonce-test (displaced 6 0 resp 2) (exp (gen) y-0) (5 0))
  (label 94)
  (parent 90)
  (unrealized (2 0) (5 0))
  (comment "empty cohort"))

Item 95, Parent: 90.

(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (h base) (y x y-0 expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y-0) (mul y x (rec y-0))))
  (defstrand resp 2 (b b-1) (h h) (y y-0))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0))
    ((6 1) (5 0)))
  (absent (y-0 h) (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (5 0) (2 0))
  (uniq-gen y x y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (5 0))
  (label 95)
  (parent 90)
  (unrealized (2 0) (4 0) (5 0))
  (comment "empty cohort"))

Tree 96.

(defprotocol station-weak diffie-hellman
  (defrole weak-init
    (vars (x expn) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc (exp (gen) x) h (privk a)) (exp h x)))))
  (defrole weak-resp
    (vars (y expn) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc h (exp (gen) y) (privk a)) (exp h y))))
    (absent (y h))))

Item 96, Children: 97 98 99.

(defskeleton station-weak
  (vars (a b name) (h base) (x expn))
  (defstrand weak-init 3 (a a) (b b) (h h) (x x))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (label 96)
  (unrealized (0 1))
  (origs)
  (comment "3 in cohort - 3 not yet seen"))

Item 97, Parent: 96.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (1 1)) ((1 2) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-init 3)
    (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b))
      (exp (gen) (mul x x-0))) (0 1))
  (label 97)
  (parent 96)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (h (exp (gen) x-0)))))
  (origs))

Item 98, Parent: 96.

(defskeleton station-weak
  (vars (a b name) (x y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
      (exp (gen) (mul x y))) (0 1))
  (label 98)
  (parent 96)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (h (exp (gen) y)))))
  (origs))

Item 99, Parent: 96, Children: 100 101 102 103 104.

(defskeleton station-weak
  (vars (a b name) (h base) (x expn))
  (defstrand weak-init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation encryption-test (added-listener (exp h x))
    (enc (enc h (exp (gen) x) (privk b)) (exp h x)) (0 1))
  (label 99)
  (parent 96)
  (unrealized (0 1) (1 0))
  (comment "5 in cohort - 5 not yet seen"))

Item 100, Parent: 99.

(defskeleton station-weak
  (vars (a b name) (x expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (contracted (h (exp (gen) (rec x)))) (gen)
    (1 0))
  (label 100)
  (parent 99)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 101, Parent: 99.

(defskeleton station-weak
  (vars (a b name) (x expn))
  (defstrand weak-init 3 (a a) (b b) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 weak-init 1) (exp (gen) x-0)
    (1 0))
  (label 101)
  (parent 99)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 102, Parent: 99.

(defskeleton station-weak
  (vars (a b name) (x x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) (mul (rec x) x-0)))
    (x x))
  (deflistener (exp (gen) x-0))
  (defstrand weak-init 1 (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (added-strand weak-init 1) (exp (gen) x-0)
    (1 0))
  (label 102)
  (parent 99)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 103, Parent: 99.

(defskeleton station-weak
  (vars (a b b-0 name) (h base) (x y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) (mul (rec x) y)))
    (x x))
  (deflistener (exp (gen) y))
  (defstrand weak-resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (added-strand weak-resp 2) (exp (gen) y) (1 0))
  (label 103)
  (parent 99)
  (unrealized (0 1))
  (comment "empty cohort"))

Item 104, Parent: 99, Children: 105 106 107 108.

(defskeleton station-weak
  (vars (a b name) (h base) (x expn) (w expr))
  (defstrand weak-init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (deflistener (cat (exp h (mul x (rec w))) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul x (rec w))) w))
    (exp h x) (1 0))
  (label 104)
  (parent 99)
  (unrealized (0 1) (2 0))
  (comment "4 in cohort - 4 not yet seen"))

Item 105, Parent: 104, Children: 109 110.

(defskeleton station-weak
  (vars (a b name) (x expn) (w expr))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w)))
    (x x))
  (deflistener (exp (gen) w))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (contracted (h (exp (gen) (mul (rec x) w))))
    (gen) (2 0))
  (label 105)
  (parent 104)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 106, Parent: 104, Children: 111 112.

(defskeleton station-weak
  (vars (a b name) (w expr) (x expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul w x)))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (displaced 3 0 weak-init 1) (exp (gen) x-0)
    (2 0))
  (label 106)
  (parent 104)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 107, Parent: 104, Children: 113 114 115.

(defskeleton station-weak
  (vars (a b name) (x expn) (w expr) (x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w x-0)))
    (x x))
  (deflistener (exp (gen) (mul w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand weak-init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-strand weak-init 1) (exp (gen) x-0)
    (2 0))
  (label 107)
  (parent 104)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 108, Parent: 104, Children: 116 117 118.

(defskeleton station-weak
  (vars (a b b-0 name) (h base) (x expn) (w expr) (y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w y)))
    (x x))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (defstrand weak-resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-strand weak-resp 2) (exp (gen) y) (2 0))
  (label 108)
  (parent 104)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 109, Parent: 105, Child: 119.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-init 3)
    (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (0 1))
  (label 109)
  (parent 105)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 110, Parent: 105, Child: 120.

(defskeleton station-weak
  (vars (a b name) (x y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 110)
  (parent 105)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 111, Parent: 106, Child: 121.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-init 3)
    (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (0 1))
  (label 111)
  (parent 106)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 112, Parent: 106, Child: 122.

(defskeleton station-weak
  (vars (a b name) (x y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x) y))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 112)
  (parent 106)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 113, Parent: 107.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (3 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((3 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (displaced 3 4 weak-init 3)
    (enc (exp (gen) x-1) (exp (gen) x) (privk b)) (0 1))
  (label 113)
  (parent 107)
  (unrealized (2 0))
  (comment "empty cohort"))

Item 114, Parent: 107, Child: 123.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-1)) (x x))
  (deflistener (exp (gen) (mul x x-1)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) x-1)))
  (defstrand weak-init 1 (x x-0))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-1))
  (precedes ((0 0) (2 0)) ((0 0) (4 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-init 3)
    (enc (exp (gen) x-1) (exp (gen) x) (privk b)) (0 1))
  (label 114)
  (parent 107)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 115, Parent: 107, Child: 124.

(defskeleton station-weak
  (vars (a b name) (x x-0 y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) y)))
  (defstrand weak-init 1 (x x-0))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 115)
  (parent 107)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 116, Parent: 108, Child: 125.

(defskeleton station-weak
  (vars (a b b-0 b-1 name) (h base) (x y x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) x-0)))
  (defstrand weak-resp 2 (b b-0) (h h) (y y))
  (defstrand weak-init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 1)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 2) (0 1)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-init 3)
    (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (0 1))
  (label 116)
  (parent 108)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 117, Parent: 108.

(defskeleton station-weak
  (vars (a b name) (x y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (displaced 4 3 weak-resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b-0)) (0 1))
  (label 117)
  (parent 108)
  (unrealized (2 0))
  (comment "empty cohort"))

Item 118, Parent: 108, Child: 126.

(defskeleton station-weak
  (vars (a b b-0 name) (h base) (x y y-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y-0)) (x x))
  (deflistener (exp (gen) (mul x y-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) y-0)))
  (defstrand weak-resp 2 (b b-0) (h h) (y y))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y-0))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (0 1)))
  (absent (y-0 (exp (gen) x)) (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b)) (0 1))
  (label 118)
  (parent 108)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 119, Parent: 109.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (deflistener x)
  (precedes ((0 0) (3 1)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 2) (0 1)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x x-0) (2 0))
  (label 119)
  (parent 109)
  (unrealized (4 0))
  (comment "empty cohort"))

Item 120, Parent: 110.

(defskeleton station-weak
  (vars (a b name) (x y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x y) (2 0))
  (label 120)
  (parent 110)
  (unrealized (4 0))
  (comment "empty cohort"))

Item 121, Parent: 111, Seen Child: 97.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (cat (exp (gen) x) x-0))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 1)) ((1 1) (0 1)) ((2 2) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x)
  (operation generalization deleted (1 0))
  (label 121)
  (parent 111)
  (seen 97)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 122, Parent: 112, Seen Child: 98.

(defskeleton station-weak
  (vars (a b name) (x y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (cat (exp (gen) x) y))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x)
  (operation generalization deleted (1 0))
  (label 122)
  (parent 112)
  (seen 98)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

Item 123, Parent: 114.

(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 x-1 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-1)) (x x))
  (deflistener (exp (gen) (mul x x-1)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) x-1)))
  (defstrand weak-init 1 (x x-0))
  (defstrand weak-init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-1))
  (deflistener x)
  (precedes ((0 0) (4 1)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 2) (0 1)) ((5 1) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec x-0) x-1) (2 0))
  (label 123)
  (parent 114)
  (unrealized (5 0))
  (comment "empty cohort"))

Item 124, Parent: 115.

(defskeleton station-weak
  (vars (a b name) (x x-0 y expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) y)))
  (defstrand weak-init 1 (x x-0))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y))
  (deflistener x)
  (precedes ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 0) (2 0)) ((4 1) (0 1)) ((5 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec x-0) y) (2 0))
  (label 124)
  (parent 115)
  (unrealized (5 0))
  (comment "empty cohort"))

Item 125, Parent: 116.

(defskeleton station-weak
  (vars (a b b-0 b-1 name) (h base) (x y x-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) x-0)))
  (defstrand weak-resp 2 (b b-0) (h h) (y y))
  (defstrand weak-init 3 (a b) (b b-1) (h (exp (gen) x)) (x x-0))
  (deflistener x)
  (precedes ((0 0) (4 1)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 2) (0 1)) ((5 1) (2 0)))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec y) x-0) (2 0))
  (label 125)
  (parent 116)
  (unrealized (5 0))
  (comment "empty cohort"))

Item 126, Parent: 118.

(defskeleton station-weak
  (vars (a b b-0 name) (h base) (x y y-0 expn))
  (defstrand weak-init 3 (a a) (b b) (h (exp (gen) y-0)) (x x))
  (deflistener (exp (gen) (mul x y-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) y-0)))
  (defstrand weak-resp 2 (b b-0) (h h) (y y))
  (defstrand weak-resp 2 (b b) (h (exp (gen) x)) (y y-0))
  (deflistener x)
  (precedes ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (0 1)) ((5 1) (2 0)))
  (absent (y-0 (exp (gen) x)) (y h))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec y) y-0) (2 0))
  (label 126)
  (parent 118)
  (unrealized (5 0))
  (comment "empty cohort"))

Tree 127.

(defprotocol station-weak diffie-hellman
  (defrole weak-init
    (vars (x expn) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc (exp (gen) x) h (privk a)) (exp h x)))))
  (defrole weak-resp
    (vars (y expn) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc h (exp (gen) y) (privk a)) (exp h y))))
    (absent (y h))))

Item 127, Children: 128 129 130.

(defskeleton station-weak
  (vars (a b name) (h base) (y expn))
  (defstrand weak-resp 3 (a a) (b b) (h h) (y y))
  (absent (y h))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (label 127)
  (unrealized (0 2))
  (origs)
  (comment "3 in cohort - 3 not yet seen"))

Item 128, Parent: 127.