(herald reflect (algebra diffie-hellman))

(comment "CPSA 3.6.8")
(comment "All input read from tst/reflect_dh.scm")

(defprotocol reflect diffie-hellman
  (defrole init
    (vars (a b akey))
    (trace (send (enc b (invk a))) (recv (enc a (invk b)))))
  (defrole resp
    (vars (a b akey))
    (trace (recv (enc b (invk a))) (send (enc a (invk b))))))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (non-orig (invk a) (invk b))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b)))))
  (label 0)
  (unrealized (0 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (defstrand init 1 (a a) (b b))
  (precedes ((1 0) (0 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc b (invk a))
    (0 0))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((send (enc b (invk a)))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (precedes ((1 1) (0 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand resp 2) (enc b (invk a))
    (0 0))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a)))))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand init 1 (a b) (b a))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc a (invk b))
    (1 0))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((send (enc a (invk b)))))
  (label 3)
  (parent 2)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand resp 2 (a a) (b b))
  (precedes ((1 1) (0 0)) ((2 1) (1 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand resp 2) (enc a (invk b))
    (1 0))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((recv (enc b (invk a))) (send (enc a (invk b)))))
  (label 4)
  (parent 2)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand resp 2 (a a) (b b))
  (defstrand init 1 (a a) (b b))
  (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc b (invk a))
    (2 0))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((send (enc b (invk a)))))
  (label 5)
  (parent 4)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand resp 2) (enc b (invk a))
    (2 0))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a)))))
  (label 6)
  (parent 4)
  (seen 4)
  (unrealized (3 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (defstrand init 1 (a a) (b b))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk a) (invk b))
  (operation generalization deleted (1 0))
  (traces ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((send (enc b (invk a)))))
  (label 7)
  (parent 5)
  (seen 1)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol reflect diffie-hellman
  (defrole init
    (vars (a b akey))
    (trace (send (enc b (invk a))) (recv (enc a (invk b)))))
  (defrole resp
    (vars (a b akey))
    (trace (recv (enc b (invk a))) (send (enc a (invk b))))))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (non-orig (invk a) (invk b))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b)))))
  (label 8)
  (unrealized (0 1))
  (origs)
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton reflect
  (vars (b akey))
  (defstrand init 2 (a b) (b b))
  (non-orig (invk b))
  (operation encryption-test (displaced 1 0 init 1) (enc a (invk b))
    (0 1))
  (traces ((send (enc b (invk b))) (recv (enc b (invk b)))))
  (label 9)
  (parent 8)
  (unrealized)
  (shape)
  (maps ((0) ((a b) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand init 1 (a b) (b a))
  (precedes ((1 0) (0 1)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc a (invk b))
    (0 1))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((send (enc a (invk b)))))
  (label 10)
  (parent 8)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (precedes ((1 1) (0 1)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand resp 2) (enc a (invk b))
    (0 1))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b)))))
  (label 11)
  (parent 8)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (displaced 2 0 init 1) (enc b (invk a))
    (1 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b)))))
  (label 12)
  (parent 11)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (defstrand init 1 (a a) (b b))
  (precedes ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc b (invk a))
    (1 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((send (enc b (invk a)))))
  (label 13)
  (parent 11)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand resp 2) (enc b (invk a))
    (1 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a)))))
  (label 14)
  (parent 11)
  (unrealized (2 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton reflect
  (vars (b akey))
  (defstrand init 2 (a b) (b b))
  (defstrand resp 2 (a b) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (operation encryption-test (displaced 3 0 init 1) (enc a (invk b))
    (2 0))
  (traces ((send (enc b (invk b))) (recv (enc b (invk b))))
    ((recv (enc b (invk b))) (send (enc b (invk b)))))
  (label 15)
  (parent 14)
  (seen 9)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand init 1 (a b) (b a))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc a (invk b))
    (2 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((send (enc a (invk b)))))
  (label 16)
  (parent 14)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand resp 2 (a a) (b b))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand resp 2) (enc a (invk b))
    (2 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((recv (enc b (invk a))) (send (enc a (invk b)))))
  (label 17)
  (parent 14)
  (seen 14)
  (unrealized (3 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand init 1 (a b) (b a))
  (precedes ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (invk a) (invk b))
  (operation generalization deleted (1 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((send (enc a (invk b)))))
  (label 18)
  (parent 16)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")