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

(comment "CPSA 2.2.10")
(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))
  (origs (y (0 1)))
  (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)
  (unrealized (0 2))
  (comment "2 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 (displaced 1 2 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)
  (maps ((0) ((a a) (b b) (x x) (y y))))
  (origs (x (1 0)) (y (0 1))))

(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 "2 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 1 (a a) (x x))
  (deflistener (exp (exp (gen) x) y))
  (deflistener x)
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 1) (0 2))
    ((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
    ((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 x) (send x)))
  (label 4)
  (parent 3)
  (unrealized (3 0))
  (comment "empty cohort"))

(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 5)
  (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 6)
  (unrealized (0 1))
  (origs (x (0 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))
  (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 7)
  (parent 6)
  (unrealized (0 1))
  (comment "2 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 (displaced 2 1 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 8)
  (parent 7)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (y y))))
  (origs (y (1 1)) (x (0 0))))

(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 9)
  (parent 7)
  (unrealized (2 0))
  (comment "2 in cohort - 2 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 10)
  (parent 9)
  (unrealized (3 0))
  (comment "empty cohort"))

(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 y)
  (precedes ((0 0) (2 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((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
    ((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 y) (send y)))
  (label 11)
  (parent 9)
  (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 12)
  (unrealized (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

(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 13)
  (parent 12)
  (unrealized)
  (shape)
  (maps ((0 1) ((n n) (x x) (y y))))
  (origs (x (0 0)) (n (0 2))))

(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 14)
  (unrealized (0 0) (0 2))
  (origs (y (0 1)))
  (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 15)
  (parent 14)
  (unrealized (0 2))
  (comment "2 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 (displaced 1 2 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 16)
  (parent 15)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (h (exp (gen) x)) (y y))))
  (origs (x (1 0)) (y (0 1))))

(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 17)
  (parent 15)
  (unrealized (2 0))
  (comment "2 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 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 18)
  (parent 17)
  (unrealized (3 0))
  (comment "empty cohort"))

(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 x)
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 1) (0 2))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig y x)
  (operation encryption-test (added-listener x) (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 x) (send x)))
  (label 19)
  (parent 17)
  (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 20)
  (unrealized (0 1))
  (origs (x (0 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))
  (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 21)
  (parent 20)
  (unrealized (0 1))
  (comment "2 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 (displaced 2 1 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 22)
  (parent 21)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (g (exp (gen) y)) (x x))))
  (origs (y (1 1)) (x (0 0))))

(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 23)
  (parent 21)
  (unrealized (2 0))
  (comment "2 in cohort - 2 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 24)
  (parent 23)
  (unrealized (3 0))
  (comment "empty cohort"))

(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 y)
  (precedes ((0 0) (2 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((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
    ((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 y) (send y)))
  (label 25)
  (parent 23)
  (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 26)
  (unrealized (1 2))
  (preskeleton)
  (comment "Not a skeleton"))

(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 27)
  (parent 26)
  (unrealized (1 2))
  (origs (y (1 1)) (x (0 0)) (n (0 2)))
  (comment "2 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 (displaced 2 0 init 3)
    (enc n (exp (exp (gen) y) x-0)) (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 28)
  (parent 27)
  (unrealized)
  (shape)
  (maps
    ((0 1) ((n n) (x x) (hy (exp (gen) y)) (y y) (hx (exp (gen) x)))))
  (origs (n (0 2)) (x (0 0)) (y (1 1))))

(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 29)
  (parent 27)
  (unrealized (1 2) (2 0))
  (comment "2 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 (displaced 3 1 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 30)
  (parent 29)
  (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 31)
  (parent 29)
  (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 32)
  (parent 30)
  (unrealized (3 0))
  (comment "2 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 (displaced 4 0 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 33)
  (parent 32)
  (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 34)
  (parent 32)
  (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 35)
  (parent 33)
  (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 36)
  (parent 35)
  (unrealized)
  (shape)
  (maps ((0 1) ((n n) (x x) (hy (gen)) (y y) (hx (gen)))))
  (origs (x (0 0)) (y (1 1)) (n (0 2))))

(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 37)
  (unrealized (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

(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 38)
  (parent 37)
  (unrealized (1 0))
  (origs (x (0 0)) (n (0 2)))
  (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 39)
  (parent 38)
  (unrealized (2 0))
  (comment "2 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 (displaced 3 0 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 40)
  (parent 39)
  (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 41)
  (parent 39)
  (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 42)
  (parent 40)
  (unrealized)
  (shape)
  (maps ((0 1) ((n n) (x x) (hy (gen)))))
  (origs (x (0 0)) (n (0 2))))

(comment "Nothing left to do")