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

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

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

(defskeleton tor
  (vars (b name) (x y expn))
  (defstrand init 2 (b b) (x x) (y y))
  (non-orig (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))))))
  (label 0)
  (unrealized (0 1))
  (origs (x (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton tor
  (vars (b name) (x y expn))
  (defstrand init 2 (b b) (x x) (y y))
  (deflistener (exp (exp (gen) x) y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig x)
  (operation encryption-test (added-listener (exp (exp (gen) x) y))
    (enc "hash" (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)))))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y))))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (b name) (x y expn))
  (defstrand init 2 (b b) (x x) (y y))
  (defstrand resp 2 (b b) (x x) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (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)))))
    ((recv (enc (exp (gen) x) (pubk b)))
      (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y))))))
  (label 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps ((0) ((b b) (x x) (y y))))
  (origs (y (1 1)) (x (0 0))))

(defskeleton tor
  (vars (b b-0 name) (x y expn))
  (defstrand init 2 (b b) (x x) (y y))
  (defstrand resp 2 (b b-0) (x x) (y y))
  (deflistener x)
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (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)))))
    ((recv (enc (exp (gen) x) (pubk b-0)))
      (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y)))))
    ((recv x) (send x)))
  (label 4)
  (parent 1)
  (unrealized (2 0))
  (comment "empty cohort"))

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

(comment "Nothing left to do")

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

(defskeleton tor
  (vars (n text) (b name) (x y expn))
  (defstrand resp 3 (n n) (b b) (x x) (y y))
  (non-orig (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))))
      (recv (enc n (exp (exp (gen) x) y)))))
  (label 6)
  (unrealized)
  (shape)
  (maps ((0) ((b b) (x x) (y y) (n n))))
  (origs (y (0 1))))

(comment "Nothing left to do")

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

(defskeleton tor
  (vars (n text) (b name) (x y expn))
  (defstrand init 3 (n n) (b b) (x x) (y y))
  (deflistener n)
  (non-orig (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))))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))
  (label 7)
  (unrealized (0 1) (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

(defskeleton tor
  (vars (n text) (b name) (x y expn))
  (defstrand init 3 (n n) (b b) (x x) (y y))
  (deflistener n)
  (precedes ((0 2) (1 0)))
  (non-orig (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))))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))
  (label 8)
  (parent 7)
  (unrealized (0 1) (1 0))
  (origs (n (0 2)) (x (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (n text) (b name) (x y expn))
  (defstrand init 3 (n n) (b b) (x x) (y y))
  (deflistener n)
  (deflistener (exp (exp (gen) x) y))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (1 0)))
  (non-orig (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))))
      (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 9)
  (parent 8)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton tor
  (vars (n text) (b name) (x y expn))
  (defstrand init 3 (n n) (b b) (x x) (y y))
  (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 (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))))
      (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 10)
  (parent 9)
  (unrealized (0 1) (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")