(herald "Diffie-Hellman protocol, man-in-the-middle attack"
  (algebra diffie-hellman))

(comment "CPSA 3.2.2")
(comment "All input read from dh_mim2.scm")

(defprotocol dh_mim diffie-hellman
  (defrole init
    (vars (x expn) (h base) (n text))
    (trace (send (exp (gen) x)) (recv h) (send (enc n (exp h x))))
    (uniq-orig n)
    (uniq-gen x)
    (neq (h (gen))))
  (defrole resp
    (vars (y expn) (h base) (n text))
    (trace (recv h) (send (exp (gen) y)) (recv (enc n (exp h y))))
    (uniq-gen y)
    (neq (h (gen)))
    (ind-zero-in (y h)))
  (comment "Diffie-hellman key exchange followed by an encryption"))

(defskeleton dh_mim
  (vars (n text) (hx hy base) (x y expn))
  (defstrand init 3 (n n) (h hy) (x x))
  (defstrand resp 3 (n n) (h hx) (y y))
  (precedes ((0 2) (1 2)))
  (ind-zero-in (y hx))
  (neq (hx (gen)) (hy (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (comment "Agreement on the encrypted text only")
  (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 0)
  (unrealized (1 2))
  (origs (n (0 2)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (hy base) (y x expn))
  (defstrand init 3 (n n) (h (exp hy y)) (x x))
  (defstrand resp 3 (n n) (h (exp hy x)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)))
  (ind-zero-in (y (exp hy x)))
  (neq ((exp hy y) (gen)) ((exp hy x) (gen)))
  (pen-non-orig y x)
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (displaced 2 0 init 3) (enc n (exp hx y-0))
    (1 2))
  (traces
    ((send (exp (gen) x)) (recv (exp hy y))
      (send (enc n (exp hy (mul y x)))))
    ((recv (exp hy x)) (send (exp (gen) y))
      (recv (enc n (exp hy (mul y x))))))
  (label 1)
  (parent 0)
  (unrealized (0 1) (1 0))
  (origs (n (0 2)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (hx hy base) (x y expn))
  (defstrand init 3 (n n) (h hy) (x x))
  (defstrand resp 3 (n n) (h hx) (y y))
  (deflistener (exp hx y))
  (precedes ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2)))
  (ind-zero-in (y hx))
  (neq (hx (gen)) (hy (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (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 2)
  (parent 0)
  (unrealized (1 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (y x expn) (x-0 expr))
  (defstrand init 3 (n n) (h (exp (gen) (mul y x-0))) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) (mul x x-0))) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)))
  (ind-zero-in (y (exp (gen) (mul x x-0))))
  (neq ((exp (gen) (mul y x-0)) (gen)) ((exp (gen) (mul x x-0)) (gen)))
  (pen-non-orig y x)
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (algebra-contracted (hy (exp (gen) x-0)))
    (exp (gen) (mul x x-0)) (1 0) (exp (gen) x))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y x-0)))
      (send (enc n (exp (gen) (mul y x x-0)))))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x x-0))))))
  (label 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((n n) (hx (exp (gen) (mul x x-0))) (hy (exp (gen) (mul y x-0)))
        (x x) (y y))))
  (origs (n (0 2))))

(defskeleton dh_mim
  (vars (n text) (hy base) (x y expn) (y-0 expr))
  (defstrand init 3 (n n) (h hy) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) y-0)) (y y))
  (deflistener (exp (gen) (mul y y-0)))
  (precedes ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2)))
  (ind-zero-in (y (exp (gen) y-0)))
  (neq ((exp (gen) y-0) (gen)) (hy (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (algebra-contracted (hx (exp (gen) y-0)))
    (exp (gen) (mul y y-0)) (2 0) (exp (gen) y))
  (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0)))))
  (label 4)
  (parent 2)
  (unrealized (1 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (x y expn) (y-0 expr))
  (defstrand init 3 (n n) (h (exp (gen) (mul (rec x) y y-0))) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) y-0)) (y y))
  (deflistener (exp (gen) (mul y y-0)))
  (precedes ((0 2) (1 2)) ((1 1) (0 1)) ((1 1) (2 0)) ((2 1) (1 2)))
  (ind-zero-in (y (exp (gen) y-0)))
  (neq ((exp (gen) y-0) (gen)) ((exp (gen) (mul (rec x) y y-0)) (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test
    (contracted (hy (exp (gen) (mul (rec x) y y-0)))) n (1 2)
    (enc n (exp (gen) (mul y y-0))))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul (rec x) y y-0)))
      (send (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0)))))
  (label 5)
  (parent 4)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (hy base) (x y expn) (y-0 expr))
  (defstrand init 3 (n n) (h hy) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) y-0)) (y y))
  (deflistener (exp (gen) (mul y y-0)))
  (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)))
  (ind-zero-in (y (exp (gen) y-0)))
  (neq ((exp (gen) y-0) (gen)) (hy (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (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 (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (exp hy x)) (send (exp hy x))))
  (label 6)
  (parent 4)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (y x expn) (y-0 expr))
  (defstrand init 3 (n n) (h (exp (gen) (mul y y-0))) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) (mul x y-0))) (y y))
  (deflistener (exp (gen) (mul y x y-0)))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 1) (2 0))
    ((2 1) (1 2)))
  (ind-zero-in (y (exp (gen) (mul x y-0))))
  (neq ((exp (gen) (mul x y-0)) (gen)) ((exp (gen) (mul y y-0)) (gen)))
  (pen-non-orig y x)
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test
    (algebra-contracted (x-0 x) (y-1 (mul x y-0)) (y-2 y-0))
    (exp (gen) (mul y y-0)) (0 1))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y y-0)))
      (send (enc n (exp (gen) (mul y x y-0)))))
    ((recv (exp (gen) (mul x y-0))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x y-0)))))
    ((recv (exp (gen) (mul y x y-0))) (send (exp (gen) (mul y x y-0)))))
  (label 7)
  (parent 5)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (x y expn) (y-0 x-0 expr))
  (defstrand init 3 (n n) (h (exp (gen) x-0)) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) y-0)) (y y))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (3 0)) ((0 2) (1 2)) ((1 1) (2 0)) ((2 1) (1 2))
    ((3 1) (1 2)))
  (ind-zero-in (y (exp (gen) y-0)))
  (neq ((exp (gen) y-0) (gen)) ((exp (gen) x-0) (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (algebra-contracted (hy (exp (gen) x-0)))
    (exp (gen) (mul x x-0)) (3 0) (exp (gen) x))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) (mul x x-0)))))
  (label 8)
  (parent 6)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (y x expn) (y-0 expr))
  (defstrand init 3 (n n) (h (exp (gen) (mul y (rec x) y-0))) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) y-0)) (y y))
  (deflistener (exp (gen) (mul y y-0)))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 1) (2 0))
    ((2 1) (1 2)))
  (ind-zero-in (y (exp (gen) y-0)))
  (neq ((exp (gen) y-0) (gen)) ((exp (gen) (mul y (rec x) y-0)) (gen)))
  (pen-non-orig y x)
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test
    (algebra-contracted (x-0 x) (y-1 (mul (rec x) y-0)) (y-2 y-0))
    (exp (gen) (mul y y-0)) (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y (rec x) y-0)))
      (send (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0)))))
  (label 9)
  (parent 7)
  (seen 7)
  (unrealized (0 1))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (x y expn) (y-0 x-0 expr))
  (defstrand init 3 (n n) (h (exp (gen) x-0)) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) y-0)) (y y))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((0 2) (1 2)) ((2 1) (1 2)))
  (ind-zero-in (y (exp (gen) y-0)))
  (neq ((exp (gen) y-0) (gen)) ((exp (gen) x-0) (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (operation generalization deleted (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0)))))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) (mul x x-0)))))
  (label 10)
  (parent 8)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_mim
  (vars (n text) (x y expn) (y-0 x-0 expr))
  (defstrand init 3 (n n) (h (exp (gen) x-0)) (x x))
  (defstrand resp 3 (n n) (h (exp (gen) y-0)) (y y))
  (precedes ((0 2) (1 2)))
  (ind-zero-in (y (exp (gen) y-0)))
  (neq ((exp (gen) y-0) (gen)) ((exp (gen) x-0) (gen)))
  (pen-non-orig x y)
  (uniq-gen x y)
  (uniq-orig n)
  (operation generalization deleted (2 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))))
    ((recv (exp (gen) y-0)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y y-0))))))
  (label 11)
  (parent 10)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((n n) (hx (exp (gen) y-0)) (hy (exp (gen) x-0)) (x x) (y y))))
  (origs (n (0 2))))

(comment "Nothing left to do")