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

(defprotocol dhke 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
  (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 0)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke
  (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 1)
  (parent 0)
  (seen 2)
  (unrealized (0 2))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dhke
  (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 2)
  (parent 1)
  (unrealized)
  (shape))

(defskeleton dhke
  (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 3)
  (parent 1)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke
  (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 4)
  (parent 3)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhke 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
  (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 5)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke
  (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 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) (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 7)
  (parent 6)
  (unrealized)
  (shape))

(defskeleton dhke
  (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 8)
  (parent 6)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhke
  (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 9)
  (parent 8)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dh-mim 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
  (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 10)
  (unrealized (1 2)))

(defskeleton dh-mim
  (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 11)
  (parent 10)
  (seen 12)
  (unrealized (1 2))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim
  (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 12)
  (parent 11)
  (unrealized)
  (shape))

(defskeleton dh-mim
  (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 13)
  (parent 11)
  (seen 14)
  (unrealized (1 2) (2 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim
  (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 14)
  (parent 13)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim
  (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 15)
  (parent 13)
  (unrealized (1 2) (3 0))
  (comment "empty cohort"))

(defskeleton dh-mim
  (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 16)
  (parent 14)
  (seen 17)
  (unrealized (3 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim
  (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 17)
  (parent 16)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim
  (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 18)
  (parent 16)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dh-mim
  (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 19)
  (parent 17)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim
  (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 20)
  (parent 19)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol dh-mim 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
  (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 21)
  (unrealized (1 0)))

(defskeleton dh-mim
  (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 22)
  (parent 21)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim
  (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 23)
  (parent 22)
  (seen 24)
  (unrealized (2 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dh-mim
  (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 24)
  (parent 23)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh-mim
  (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 25)
  (parent 23)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dh-mim
  (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 26)
  (parent 24)
  (unrealized)
  (shape))

(comment "Nothing left to do")