(herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman))

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

(defprotocol dhke diffie-hellman
  (defrole init
    (vars (a b name) (x y expn))
    (trace (send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))
      (send (enc "i" a b (exp (exp (gen) x) y))))
    (uniq-orig x))
  (defrole resp
    (vars (a b name) (x y expn))
    (trace (recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))
      (recv (enc "i" a b (exp (exp (gen) x) y))))
    (uniq-orig y)))

(defskeleton dhke
  (vars (a b name) (x y expn))
  (defstrand resp 3 (a a) (b b) (x x) (y y))
  (non-orig (privk a) (privk b))
  (uniq-orig y)
  (traces
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))
      (recv (enc "i" a b (exp (exp (gen) x) y)))))
  (label 0)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dhke
  (vars (a b name) (x y expn))
  (defstrand resp 3 (a a) (b b) (x x) (y y))
  (defstrand init 3 (a a) (b b) (x x) (y y))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-strand init 3)
    (enc "i" a b (exp (exp (gen) x) y)) (0 2))
  (traces
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))
      (recv (enc "i" a b (exp (exp (gen) x) y))))
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))
      (send (enc "i" a b (exp (exp (gen) x) y)))))
  (label 2)
  (parent 1)
  (unrealized)
  (shape))

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

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

(comment "Nothing left to do")

(defprotocol dhke diffie-hellman
  (defrole init
    (vars (a b name) (x y expn))
    (trace (send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))
      (send (enc "i" a b (exp (exp (gen) x) y))))
    (uniq-orig x))
  (defrole resp
    (vars (a b name) (x y expn))
    (trace (recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))
      (recv (enc "i" a b (exp (exp (gen) x) y))))
    (uniq-orig y)))

(defskeleton dhke
  (vars (a b name) (x y expn))
  (defstrand init 2 (a a) (b b) (x x) (y y))
  (non-orig (privk a) (privk b))
  (uniq-orig x)
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))))
  (label 5)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke
  (vars (a b a-0 name) (x y x-0 expn))
  (defstrand init 2 (a a) (b b) (x x) (y y))
  (defstrand resp 2 (a a-0) (b b) (x x-0) (y y))
  (precedes ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (privk b)) (0 1))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" (exp (gen) x-0) (privk a-0)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a-0 b (exp (exp (gen) y) x-0))))))
  (label 6)
  (parent 5)
  (seen 7)
  (unrealized (0 1))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dhke
  (vars (a b name) (x y expn))
  (defstrand init 2 (a a) (b b) (x x) (y y))
  (defstrand resp 2 (a a) (b b) (x x) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-strand resp 2)
    (enc a b (exp (exp (gen) x) y)) (0 1))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))))
  (label 7)
  (parent 6)
  (unrealized)
  (shape))

(defskeleton dhke
  (vars (a b a-0 name) (x y x-0 expn))
  (defstrand init 2 (a a) (b b) (x x) (y y))
  (defstrand resp 2 (a a-0) (b b) (x x-0) (y y))
  (deflistener (exp (exp (gen) x) y))
  (precedes ((0 0) (2 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-listener (exp (exp (gen) x) y))
    (enc a b (exp (exp (gen) x) y)) (0 1))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" (exp (gen) x-0) (privk a-0)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a-0 b (exp (exp (gen) y) x-0)))))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y))))
  (label 8)
  (parent 6)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke
  (vars (a b a-0 name) (x y x-0 expn))
  (defstrand init 2 (a a) (b b) (x x) (y y))
  (defstrand resp 2 (a a-0) (b b) (x x-0) (y y))
  (deflistener (exp (exp (gen) x) y))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-listener x) (exp (exp (gen) x) y)
    (2 0))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" (exp (gen) x-0) (privk a-0)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a-0 b (exp (exp (gen) y) x-0)))))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv x) (send x)))
  (label 9)
  (parent 8)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dh-mim diffie-hellman
  (defrole init
    (vars (x y expn) (n text))
    (trace (send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (exp (gen) x) y))))
    (uniq-orig n x))
  (defrole resp
    (vars (x y expn) (n text))
    (trace (recv (exp (gen) x)) (send (exp (gen) y))
      (recv (enc n (exp (exp (gen) x) y))))
    (uniq-orig y))
  (comment "Diffie-Hellman without signatures"
    "has a man-in-the-middle attack"))

(defskeleton dh-mim
  (vars (n text) (x y expn))
  (defstrand init 3 (n n) (x x) (y y))
  (deflistener n)
  (uniq-orig n x)
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))
  (label 10)
  (unrealized (1 0)))

(defskeleton dh-mim
  (vars (n text) (x y expn))
  (defstrand init 3 (n n) (x x) (y y))
  (deflistener n)
  (precedes ((0 2) (1 0)))
  (uniq-orig n x)
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))
  (label 11)
  (parent 10)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol dhke-with-base-vars diffie-hellman
  (defrole init
    (vars (a b name) (g base) (x expn))
    (trace (send (enc "i" (exp (gen) x) (privk a)))
      (recv (cat (enc g (privk b)) (enc a b (exp g x))))
      (send (enc "i" a b (exp g x))))
    (uniq-orig x))
  (defrole resp
    (vars (a b name) (h base) (y expn))
    (trace (recv (enc "i" h (privk a)))
      (send (cat (enc (exp (gen) y) (privk b)) (enc a b (exp h y))))
      (recv (enc "i" a b (exp h y))))
    (uniq-orig y)))

(defskeleton dhke-with-base-vars
  (vars (a b name) (h base) (y expn))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (non-orig (privk a) (privk b))
  (uniq-orig y)
  (traces
    ((recv (enc "i" h (privk a)))
      (send (cat (enc (exp (gen) y) (privk b)) (enc a b (exp h y))))
      (recv (enc "i" a b (exp h y)))))
  (label 12)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke-with-base-vars
  (vars (a b name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 1 (a a) (x x))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig y x)
  (operation encryption-test (added-strand init 1)
    (enc "i" (exp (gen) x) (privk a)) (0 0))
  (traces
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) y) x))))
      (recv (enc "i" a b (exp (exp (gen) y) x))))
    ((send (enc "i" (exp (gen) x) (privk a)))))
  (label 13)
  (parent 12)
  (seen 14)
  (unrealized (0 2))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dhke-with-base-vars
  (vars (a b name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b) (g (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig y x)
  (operation encryption-test (added-strand init 3)
    (enc "i" a b (exp (exp (gen) y) x)) (0 2))
  (traces
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) y) x))))
      (recv (enc "i" a b (exp (exp (gen) y) x))))
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) y) x))))
      (send (enc "i" a b (exp (exp (gen) y) x)))))
  (label 14)
  (parent 13)
  (unrealized)
  (shape))

(defskeleton dhke-with-base-vars
  (vars (a b name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 1 (a a) (x x))
  (deflistener (exp (exp (gen) y) x))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig y x)
  (operation encryption-test (added-listener (exp (exp (gen) y) x))
    (enc "i" a b (exp (exp (gen) y) x)) (0 2))
  (traces
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) y) x))))
      (recv (enc "i" a b (exp (exp (gen) y) x))))
    ((send (enc "i" (exp (gen) x) (privk a))))
    ((recv (exp (exp (gen) y) x)) (send (exp (exp (gen) y) x))))
  (label 15)
  (parent 13)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke-with-base-vars
  (vars (a b name) (y x expn))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 1 (a a) (x x))
  (deflistener (exp (exp (gen) y) x))
  (deflistener y)
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((2 1) (0 2)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig y x)
  (operation encryption-test (added-listener y) (exp (exp (gen) y) x)
    (2 0))
  (traces
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) y) x))))
      (recv (enc "i" a b (exp (exp (gen) y) x))))
    ((send (enc "i" (exp (gen) x) (privk a))))
    ((recv (exp (exp (gen) y) x)) (send (exp (exp (gen) y) x)))
    ((recv y) (send y)))
  (label 16)
  (parent 15)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhke-with-base-vars diffie-hellman
  (defrole init
    (vars (a b name) (g base) (x expn))
    (trace (send (enc "i" (exp (gen) x) (privk a)))
      (recv (cat (enc g (privk b)) (enc a b (exp g x))))
      (send (enc "i" a b (exp g x))))
    (uniq-orig x))
  (defrole resp
    (vars (a b name) (h base) (y expn))
    (trace (recv (enc "i" h (privk a)))
      (send (cat (enc (exp (gen) y) (privk b)) (enc a b (exp h y))))
      (recv (enc "i" a b (exp h y))))
    (uniq-orig y)))

(defskeleton dhke-with-base-vars
  (vars (a b name) (g base) (x expn))
  (defstrand init 2 (a a) (b b) (g g) (x x))
  (non-orig (privk a) (privk b))
  (uniq-orig x)
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv (cat (enc g (privk b)) (enc a b (exp g x))))))
  (label 17)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke-with-base-vars
  (vars (a b a-0 name) (h base) (x y expn))
  (defstrand init 2 (a a) (b b) (g (exp (gen) y)) (x x))
  (defstrand resp 2 (a a-0) (b b) (h h) (y y))
  (precedes ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (privk b)) (0 1))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" h (privk a-0)))
      (send (cat (enc (exp (gen) y) (privk b)) (enc a-0 b (exp h y))))))
  (label 18)
  (parent 17)
  (seen 19)
  (unrealized (0 1))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dhke-with-base-vars
  (vars (a b name) (x y expn))
  (defstrand init 2 (a a) (b b) (g (exp (gen) y)) (x x))
  (defstrand resp 2 (a a) (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-strand resp 2)
    (enc a b (exp (exp (gen) x) y)) (0 1))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" (exp (gen) x) (privk a)))
      (send
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y))))))
  (label 19)
  (parent 18)
  (unrealized)
  (shape))

(defskeleton dhke-with-base-vars
  (vars (a b a-0 name) (h base) (x y expn))
  (defstrand init 2 (a a) (b b) (g (exp (gen) y)) (x x))
  (defstrand resp 2 (a a-0) (b b) (h h) (y y))
  (deflistener (exp (exp (gen) x) y))
  (precedes ((0 0) (2 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-listener (exp (exp (gen) x) y))
    (enc a b (exp (exp (gen) x) y)) (0 1))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" h (privk a-0)))
      (send (cat (enc (exp (gen) y) (privk b)) (enc a-0 b (exp h y)))))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y))))
  (label 20)
  (parent 18)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke-with-base-vars
  (vars (a b a-0 name) (h base) (x y expn))
  (defstrand init 2 (a a) (b b) (g (exp (gen) y)) (x x))
  (defstrand resp 2 (a a-0) (b b) (h h) (y y))
  (deflistener (exp (exp (gen) x) y))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig x y)
  (operation encryption-test (added-listener x) (exp (exp (gen) x) y)
    (2 0))
  (traces
    ((send (enc "i" (exp (gen) x) (privk a)))
      (recv
        (cat (enc (exp (gen) y) (privk b))
          (enc a b (exp (exp (gen) x) y)))))
    ((recv (enc "i" h (privk a-0)))
      (send (cat (enc (exp (gen) y) (privk b)) (enc a-0 b (exp h y)))))
    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))
    ((recv x) (send x)))
  (label 21)
  (parent 20)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dh-mim-with-base-vars diffie-hellman
  (defrole init
    (vars (x expn) (hy base) (n text))
    (trace (send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    (uniq-orig n x))
  (defrole resp
    (vars (y expn) (hx base) (n text))
    (trace (recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y))))
    (uniq-orig y))
  (comment "Diffie-Hellman without signatures"
    "has a man-in-the-middle attack"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy hx base) (x y expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (defstrand resp 3 (n n) (hx hx) (y y))
  (uniq-orig n x y)
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y)))))
  (label 22)
  (unrealized (1 2)))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy hx base) (x y expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (defstrand resp 3 (n n) (hx hx) (y y))
  (precedes ((0 2) (1 2)))
  (uniq-orig n x y)
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y)))))
  (label 23)
  (parent 22)
  (seen 24)
  (unrealized (1 2))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (x y expn))
  (defstrand init 3 (n n) (hy (exp (gen) y)) (x x))
  (defstrand resp 3 (n n) (hx (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)))
  (uniq-orig n x y)
  (operation encryption-test (added-strand init 3)
    (enc n (exp (exp (gen) x) y)) (1 2))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (exp (gen) x) y))))
    ((recv (exp (gen) x)) (send (exp (gen) y))
      (recv (enc n (exp (exp (gen) x) y)))))
  (label 24)
  (parent 23)
  (unrealized)
  (shape))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy hx base) (x y expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (defstrand resp 3 (n n) (hx hx) (y y))
  (deflistener (exp hx y))
  (precedes ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2)))
  (uniq-orig n x y)
  (operation encryption-test (added-listener (exp hx y))
    (enc n (exp hx y)) (1 2))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y))))
    ((recv (exp hx y)) (send (exp hx y))))
  (label 25)
  (parent 23)
  (seen 26)
  (unrealized (1 2) (2 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy base) (x y expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (defstrand resp 3 (n n) (hx (gen)) (y y))
  (deflistener (exp (gen) y))
  (precedes ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2)))
  (uniq-orig n x y)
  (operation encryption-test (added-strand resp 2) (exp (gen) y) (2 0))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y))))
  (label 26)
  (parent 25)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy hx base) (x y expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (defstrand resp 3 (n n) (hx hx) (y y))
  (deflistener (exp hx y))
  (deflistener y)
  (precedes ((0 2) (1 2)) ((1 1) (3 0)) ((2 1) (1 2)) ((3 1) (2 0)))
  (uniq-orig n x y)
  (operation encryption-test (added-listener y) (exp hx y) (2 0))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y))))
    ((recv (exp hx y)) (send (exp hx y))) ((recv y) (send y)))
  (label 27)
  (parent 25)
  (unrealized (1 2) (3 0))
  (comment "empty cohort"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy base) (x y expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (defstrand resp 3 (n n) (hx (gen)) (y y))
  (deflistener (exp (gen) y))
  (deflistener (exp hy x))
  (precedes ((0 0) (3 0)) ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2))
    ((3 1) (1 2)))
  (uniq-orig n x y)
  (operation nonce-test (added-listener (exp hy x)) n (1 2)
    (enc n (exp hy x)))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (exp hy x)) (send (exp hy x))))
  (label 28)
  (parent 26)
  (seen 29)
  (unrealized (3 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (x y expn))
  (defstrand init 3 (n n) (hy (gen)) (x x))
  (defstrand resp 3 (n n) (hx (gen)) (y y))
  (deflistener (exp (gen) y))
  (deflistener (exp (gen) x))
  (precedes ((0 0) (3 0)) ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2))
    ((3 1) (1 2)))
  (uniq-orig n x y)
  (operation encryption-test (added-strand init 1) (exp (gen) x) (3 0))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (exp (gen) x)) (send (exp (gen) x))))
  (label 29)
  (parent 28)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy base) (x y expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (defstrand resp 3 (n n) (hx (gen)) (y y))
  (deflistener (exp (gen) y))
  (deflistener (exp hy x))
  (deflistener x)
  (precedes ((0 0) (4 0)) ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2))
    ((3 1) (1 2)) ((4 1) (3 0)))
  (uniq-orig n x y)
  (operation encryption-test (added-listener x) (exp hy x) (3 0))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv (exp hy x)) (send (exp hy x))) ((recv x) (send x)))
  (label 30)
  (parent 28)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (x y expn))
  (defstrand init 3 (n n) (hy (gen)) (x x))
  (defstrand resp 3 (n n) (hx (gen)) (y y))
  (deflistener (exp (gen) x))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((2 1) (1 2)))
  (uniq-orig n x y)
  (operation generalization deleted (2 0))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))
    ((recv (exp (gen) x)) (send (exp (gen) x))))
  (label 31)
  (parent 29)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (x y expn))
  (defstrand init 3 (n n) (hy (gen)) (x x))
  (defstrand resp 3 (n n) (hx (gen)) (y y))
  (precedes ((0 2) (1 2)))
  (uniq-orig n x y)
  (operation generalization deleted (2 0))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))
    ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y)))))
  (label 32)
  (parent 31)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol dh-mim-with-base-vars diffie-hellman
  (defrole init
    (vars (x expn) (hy base) (n text))
    (trace (send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    (uniq-orig n x))
  (defrole resp
    (vars (y expn) (hx base) (n text))
    (trace (recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y))))
    (uniq-orig y))
  (comment "Diffie-Hellman without signatures"
    "has a man-in-the-middle attack"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy base) (x expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (deflistener n)
  (uniq-orig n x)
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv n) (send n)))
  (label 33)
  (unrealized (1 0)))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy base) (x expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (deflistener n)
  (precedes ((0 2) (1 0)))
  (uniq-orig n x)
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv n) (send n)))
  (label 34)
  (parent 33)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy base) (x expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (deflistener n)
  (deflistener (exp hy x))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (1 0)))
  (uniq-orig n x)
  (operation nonce-test (added-listener (exp hy x)) n (1 0)
    (enc n (exp hy x)))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv n) (send n)) ((recv (exp hy x)) (send (exp hy x))))
  (label 35)
  (parent 34)
  (seen 36)
  (unrealized (2 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (x expn))
  (defstrand init 3 (n n) (hy (gen)) (x x))
  (deflistener n)
  (deflistener (exp (gen) x))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (1 0)))
  (uniq-orig n x)
  (operation encryption-test (added-strand init 1) (exp (gen) x) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))
    ((recv n) (send n)) ((recv (exp (gen) x)) (send (exp (gen) x))))
  (label 36)
  (parent 35)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (hy base) (x expn))
  (defstrand init 3 (n n) (hy hy) (x x))
  (deflistener n)
  (deflistener (exp hy x))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0)))
  (uniq-orig n x)
  (operation encryption-test (added-listener x) (exp hy x) (2 0))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv n) (send n)) ((recv (exp hy x)) (send (exp hy x)))
    ((recv x) (send x)))
  (label 37)
  (parent 35)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dh-mim-with-base-vars
  (vars (n text) (x expn))
  (defstrand init 3 (n n) (hy (gen)) (x x))
  (deflistener n)
  (precedes ((0 2) (1 0)))
  (uniq-orig n x)
  (operation generalization deleted (2 0))
  (traces
    ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))
    ((recv n) (send n)))
  (label 38)
  (parent 36)
  (unrealized)
  (shape))

(comment "Nothing left to do")