(herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman)
  (comment "Achieves unilateral authentication"))

(comment "CPSA 2.2.0")
(comment "All input read")

(defprotocol tor diffie-hellman
  (defrole init
    (vars (x y expn) (b name) (n text) (kh akey))
    (trace (send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y))))
    (non-orig (invk kh))
    (uniq-orig n x))
  (defrole resp
    (vars (x y expn) (b name) (n text) (kh akey))
    (trace (recv (enc (exp (gen) x) (pubk b)))
      (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (recv (enc n (exp (exp (gen) x) y))))
    (non-orig (invk kh))
    (uniq-orig y)))

(defskeleton tor
  (vars (b name) (x y expn) (kh akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (non-orig (invk kh) (privk b))
  (uniq-orig x)
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))))
  (label 0)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton tor
  (vars (b b-0 name) (x y expn) (kh kh-0 akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-strand resp 2) (exp (exp (gen) x) y)
    (0 1))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv (enc (exp (gen) x) (pubk b-0)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))
  (label 1)
  (parent 0)
  (unrealized (0 1) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton tor
  (vars (b name) (x y expn) (kh akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (deflistener x)
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk kh) (privk b))
  (uniq-orig x)
  (operation encryption-test (added-listener x) (exp (exp (gen) x) y)
    (0 1))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv x) (send x)))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (b name) (x y expn) (kh kh-0 akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig x y)
  (operation encryption-test (contracted (b-0 b)) (exp (gen) x) (1 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))
  (label 3)
  (parent 1)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton tor
  (vars (b b-0 name) (x y expn) (kh kh-0 akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-listener x) (exp (gen) x) (1 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv (enc (exp (gen) x) (pubk b-0)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv x) (send x)))
  (label 4)
  (parent 1)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (b name) (x y y-0 expn) (kh kh-0 akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (deflistener x)
  (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig x y-0)
  (operation nonce-test (added-strand resp 2) x (1 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv x) (send x))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y-0)
          (enc "hash" (exp (exp (gen) x) y-0) kh-0)))))
  (label 5)
  (parent 2)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton tor
  (vars (b name) (x y expn) (kh akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk kh) (privk b))
  (uniq-orig x y)
  (operation encryption-test (contracted (kh-0 kh))
    (exp (exp (gen) x) y) (0 1) (enc "hash" (exp (exp (gen) x) y) kh))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))))
  (label 6)
  (parent 3)
  (unrealized)
  (shape))

(defskeleton tor
  (vars (b name) (x y expn) (kh kh-0 akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))
  (deflistener y)
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-listener y) (exp (exp (gen) x) y)
    (0 1) (enc "hash" (exp (exp (gen) x) y) kh-0))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv y) (send y)))
  (label 7)
  (parent 3)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (b b-0 name) (x y y-0 expn) (kh kh-0 kh-1 akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))
  (deflistener x)
  (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-1))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))
  (uniq-orig x y y-0)
  (operation nonce-test (added-strand resp 2) x (2 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv (enc (exp (gen) x) (pubk b-0)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv x) (send x))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y-0)
          (enc "hash" (exp (exp (gen) x) y-0) kh-1)))))
  (label 8)
  (parent 4)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton tor
  (vars (b b-0 name) (x y y-0 expn) (kh kh-0 kh-1 akey))
  (defstrand init 2 (b b) (x x) (y y) (kh kh))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))
  (deflistener y)
  (defstrand resp 2 (b b-0) (x y) (y y-0) (kh kh-1))
  (precedes ((0 0) (1 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))
  (uniq-orig x y y-0)
  (operation nonce-test (added-strand resp 2) y (2 0) (exp (gen) y)
    (enc "hash" (exp (exp (gen) x) y) kh-0))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv y) (send y))
    ((recv (enc (exp (gen) y) (pubk b-0)))
      (send
        (cat (exp (gen) y-0)
          (enc "hash" (exp (exp (gen) y) y-0) kh-1)))))
  (label 9)
  (parent 7)
  (unrealized (0 1) (2 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol tor diffie-hellman
  (defrole init
    (vars (x y expn) (b name) (n text) (kh akey))
    (trace (send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y))))
    (non-orig (invk kh))
    (uniq-orig n x))
  (defrole resp
    (vars (x y expn) (b name) (n text) (kh akey))
    (trace (recv (enc (exp (gen) x) (pubk b)))
      (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (recv (enc n (exp (exp (gen) x) y))))
    (non-orig (invk kh))
    (uniq-orig y)))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh akey))
  (defstrand resp 3 (n n) (b b) (x x) (y y) (kh kh))
  (non-orig (invk kh) (privk b))
  (uniq-orig y)
  (traces
    ((recv (enc (exp (gen) x) (pubk b)))
      (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (recv (enc n (exp (exp (gen) x) y)))))
  (label 10)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol tor diffie-hellman
  (defrole init
    (vars (x y expn) (b name) (n text) (kh akey))
    (trace (send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y))))
    (non-orig (invk kh))
    (uniq-orig n x))
  (defrole resp
    (vars (x y expn) (b name) (n text) (kh akey))
    (trace (recv (enc (exp (gen) x) (pubk b)))
      (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (recv (enc n (exp (exp (gen) x) y))))
    (non-orig (invk kh))
    (uniq-orig y)))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (non-orig (invk kh) (privk b))
  (uniq-orig n x)
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))
  (label 11)
  (unrealized (0 1) (1 0)))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (precedes ((0 2) (1 0)))
  (non-orig (invk kh) (privk b))
  (uniq-orig n x)
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))
  (label 12)
  (parent 11)
  (unrealized (0 1) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (1 0)))
  (non-orig (invk kh) (privk b))
  (uniq-orig n x)
  (operation nonce-test (added-listener (exp (exp (gen) x) y)) n (1 0)
    (enc n (exp (exp (gen) x) y)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y))))
  (label 13)
  (parent 12)
  (seen 14)
  (unrealized (0 1) (2 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton tor
  (vars (n text) (b b-0 name) (x y expn) (kh kh-0 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))
  (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig n x y)
  (operation encryption-test (added-strand resp 2) (exp (exp (gen) x) y)
    (2 0))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv (enc (exp (gen) x) (pubk b-0)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))
  (label 14)
  (parent 13)
  (seen 16)
  (unrealized (0 1) (2 0) (3 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (invk kh) (privk b))
  (uniq-orig n x)
  (operation encryption-test (added-listener x) (exp (exp (gen) x) y)
    (2 0))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv x) (send x)))
  (label 15)
  (parent 13)
  (seen 18)
  (unrealized (0 1) (3 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh kh-0 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))
  (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig n x y)
  (operation encryption-test (contracted (b-0 b)) (exp (gen) x) (3 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))
  (label 16)
  (parent 14)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (n text) (b b-0 name) (x y expn) (kh kh-0 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))
  (deflistener x)
  (precedes ((0 0) (4 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig n x y)
  (operation encryption-test (added-listener x) (exp (gen) x) (3 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv (enc (exp (gen) x) (pubk b-0)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv x) (send x)))
  (label 17)
  (parent 14)
  (seen 20)
  (unrealized (4 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (n text) (b name) (x y y-0 expn) (kh kh-0 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (deflistener x)
  (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-0))
  (precedes ((0 0) (4 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig n x y-0)
  (operation nonce-test (added-strand resp 2) x (3 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv x) (send x))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y-0)
          (enc "hash" (exp (exp (gen) x) y-0) kh-0)))))
  (label 18)
  (parent 15)
  (unrealized (0 1) (3 0))
  (comment "empty cohort"))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh kh-0 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((0 2) (1 0)) ((2 1) (1 0))
    ((3 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig n x y)
  (operation encryption-test (added-listener x) (exp (exp (gen) x) y)
    (2 0) (enc "hash" (exp (exp (gen) x) y) kh-0))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv x) (send x)))
  (label 19)
  (parent 16)
  (seen 21 22)
  (unrealized (0 1) (4 0))
  (comment "6 in cohort - 2 not yet seen"))

(defskeleton tor
  (vars (n text) (b b-0 name) (x y y-0 expn) (kh kh-0 kh-1 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))
  (deflistener x)
  (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-1))
  (precedes ((0 0) (5 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (4 0)))
  (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))
  (uniq-orig n x y y-0)
  (operation nonce-test (added-strand resp 2) x (4 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv (enc (exp (gen) x) (pubk b-0)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv x) (send x))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y-0)
          (enc "hash" (exp (exp (gen) x) y-0) kh-1)))))
  (label 20)
  (parent 17)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton tor
  (vars (n text) (b name) (x y y-0 expn) (kh kh-0 kh-1 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))
  (deflistener x)
  (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-1))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 2) (1 0)) ((2 1) (1 0))
    ((3 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))
  (uniq-orig n x y y-0)
  (operation nonce-test (added-strand resp 2) x (4 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv x) (send x))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y-0)
          (enc "hash" (exp (exp (gen) x) y-0) kh-1)))))
  (label 21)
  (parent 19)
  (unrealized (0 1) (4 0))
  (comment "empty cohort"))

(defskeleton tor
  (vars (n text) (b name) (x y expn) (kh kh-0 akey))
  (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))
    ((3 1) (4 0)) ((4 1) (2 0)))
  (non-orig (invk kh) (invk kh-0) (privk b))
  (uniq-orig n x y)
  (operation nonce-test (displaced 5 3 resp 2) x (4 0)
    (enc (exp (gen) x) (pubk b)))
  (traces
    ((send (enc (exp (gen) x) (pubk b)))
      (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send
        (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))
    ((recv x) (send x)))
  (label 22)
  (parent 19)
  (unrealized (0 1) (4 0))
  (comment "empty cohort"))

(comment "Nothing left to do")