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

(comment "CPSA 3.6.0")
(comment "All input read from dh_test.scm")
(comment "Strand count bounded at 20")

(defprotocol foo3 diffie-hellman
  (defrole resp (vars (h base)) (trace (recv h)))
  (defrole init (vars (x rndx)) (trace (send (exp (gen) x)))))

(defskeleton foo3
  (vars (x rndx))
  (defstrand resp 1 (h (exp (gen) x)))
  (non-orig x)
  (traces ((recv (exp (gen) x))))
  (label 0)
  (unrealized (0 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton foo3
  (vars (x rndx))
  (defstrand resp 1 (h (exp (gen) x)))
  (defstrand init 1 (x x))
  (precedes ((1 0) (0 0)))
  (non-orig x)
  (operation nonce-test (added-strand init 1) (exp (gen) x) (0 0))
  (traces ((recv (exp (gen) x))) ((send (exp (gen) x))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((x x))))
  (origs))

(defskeleton foo3
  (vars (x rndx) (w expt))
  (defstrand resp 1 (h (exp (gen) x)))
  (deflistener (cat (exp (gen) (mul x (rec w))) w))
  (precedes ((1 1) (0 0)))
  (non-orig x)
  (precur (1 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x (rec w))) w)) (exp (gen) x)
    (0 0))
  (traces ((recv (exp (gen) x)))
    ((recv (cat (exp (gen) (mul x (rec w))) w))
      (send (cat (exp (gen) (mul x (rec w))) w))))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton foo3
  (vars (x x-0 rndx))
  (defstrand resp 1 (h (exp (gen) x)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig x)
  (precur (1 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces ((recv (exp (gen) x)))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (exp (gen) x-0))))
  (label 3)
  (parent 2)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton foo3
  (vars (x rndx))
  (defstrand resp 1 (h (exp (gen) x)))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand init 1 (x x))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig x)
  (precur (1 0))
  (operation nonce-test (contracted (x-0 x) (x-1 x)) (one) (1 0))
  (traces ((recv (exp (gen) x)))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((send (exp (gen) x))))
  (label 4)
  (parent 3)
  (seen 1)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")