(herald "Station-to-station protocol unflipped"
  (algebra diffie-hellman))

(comment "CPSA 4.4.3")
(comment "All input read from tst/sts_unflip.scm")

(defprotocol station-to-station-unflip diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))
      (send (privk a)))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))
      (send (privk b)))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (x rndx))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (non-orig (privk b))
  (uniq-gen x)
  (traces
    ((send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))))
  (label 0)
  (unrealized (0 1))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-gen x y)
  (operation encryption-test (added-strand resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
      (exp (gen) (mul x y))) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 1)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (h (exp (gen) y)))))
  (origs))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (x rndx))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-gen x)
  (operation encryption-test (added-listener (exp h x))
    (enc (enc h (exp (gen) x) (privk b)) (exp h x)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x))))
    ((recv (exp h x)) (send (exp h x))))
  (label 2)
  (parent 0)
  (unrealized (0 1) (1 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx))
  (defstrand init 3 (a a) (b b) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (gen)
          (enc (enc (gen) (exp (gen) x) (privk b)) (exp (gen) x))))
      (send (enc (enc (gen) (exp (gen) x) (privk a)) (exp (gen) x))))
    ((recv (exp (gen) x)) (send (exp (gen) x))))
  (label 3)
  (parent 2)
  (unrealized (0 1))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-gen x)
  (operation nonce-test (contracted (h (exp (gen) (rec x)))) (gen)
    (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (rec x))
          (enc (enc (exp (gen) (rec x)) (exp (gen) x) (privk b))
            (gen))))
      (send
        (enc (enc (exp (gen) (rec x)) (exp (gen) x) (privk a)) (gen))))
    ((recv (gen)) (send (gen))))
  (label 4)
  (parent 2)
  (unrealized (0 1))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x x-0 rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (privk b))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) x-0))
          (enc
            (enc (exp (gen) (mul (rec x) x-0)) (exp (gen) x) (privk b))
            (exp (gen) x-0))))
      (send
        (enc (enc (exp (gen) (mul (rec x) x-0)) (exp (gen) x) (privk a))
          (exp (gen) x-0))))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((send (exp (gen) x-0))))
  (label 5)
  (parent 2)
  (unrealized (0 1))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (h base) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen x y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) y))
          (enc (enc (exp (gen) (mul (rec x) y)) (exp (gen) x) (privk b))
            (exp (gen) y))))
      (send
        (enc (enc (exp (gen) (mul (rec x) y)) (exp (gen) x) (privk a))
          (exp (gen) y)))) ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b-0)) (exp h y))))))
  (label 6)
  (parent 2)
  (unrealized (0 1))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (x rndx) (w expt))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (deflistener (cat (exp h (mul x (rec w))) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul x (rec w))) w))
    (exp h x) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x))))
    ((recv (exp h x)) (send (exp h x)))
    ((recv (cat (exp h (mul x (rec w))) w))
      (send (cat (exp h (mul x (rec w))) w))))
  (label 7)
  (parent 2)
  (unrealized (0 1) (2 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (w expt) (x rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul w x)))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) w)
          (enc (enc (exp (gen) w) (exp (gen) x) (privk b))
            (exp (gen) (mul w x)))))
      (send
        (enc (enc (exp (gen) w) (exp (gen) x) (privk a))
          (exp (gen) (mul w x)))))
    ((recv (exp (gen) (mul w x))) (send (exp (gen) (mul w x))))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 8)
  (parent 7)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx) (w expt))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w))) (x x))
  (deflistener (exp (gen) w))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (contracted (h (exp (gen) (mul (rec x) w))))
    (gen) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) w))
          (enc (enc (exp (gen) (mul (rec x) w)) (exp (gen) x) (privk b))
            (exp (gen) w))))
      (send
        (enc (enc (exp (gen) (mul (rec x) w)) (exp (gen) x) (privk a))
          (exp (gen) w)))) ((recv (exp (gen) w)) (send (exp (gen) w)))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 9)
  (parent 7)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w x-0)))
    (x x))
  (deflistener (exp (gen) (mul w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (privk b))
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) w x-0))
          (enc
            (enc (exp (gen) (mul (rec x) w x-0)) (exp (gen) x)
              (privk b)) (exp (gen) (mul w x-0)))))
      (send
        (enc
          (enc (exp (gen) (mul (rec x) w x-0)) (exp (gen) x) (privk a))
          (exp (gen) (mul w x-0)))))
    ((recv (exp (gen) (mul w x-0))) (send (exp (gen) (mul w x-0))))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0))))
  (label 10)
  (parent 7)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (h base) (x rndx) (w expt) (y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w y))) (x x))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) w y))
          (enc
            (enc (exp (gen) (mul (rec x) w y)) (exp (gen) x) (privk b))
            (exp (gen) (mul w y)))))
      (send
        (enc (enc (exp (gen) (mul (rec x) w y)) (exp (gen) x) (privk a))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b-0)) (exp h y))))))
  (label 11)
  (parent 7)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x) y))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 12)
  (parent 8)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (gen) (mul x y))) (send (cat (gen) (mul x y))))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 13)
  (parent 9)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x x-0 y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) y)))
  (defstrand init 1 (x x-0))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0))
    ((4 1) (2 0)))
  (non-orig (privk b))
  (uniq-gen x x-0 y)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) y)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) y))))
    ((send (exp (gen) x-0)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 14)
  (parent 10)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (displaced 4 3 resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b-0)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 15)
  (parent 11)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (h base) (x y y-0 rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y-0)) (x x))
  (deflistener (exp (gen) (mul x y-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) y-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y-0))
  (precedes ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (2 0)))
  (non-orig (privk b))
  (uniq-gen x y y-0)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y-0)
          (enc (enc (exp (gen) y-0) (exp (gen) x) (privk b))
            (exp (gen) (mul x y-0)))))
      (send
        (enc (enc (exp (gen) y-0) (exp (gen) x) (privk a))
          (exp (gen) (mul x y-0)))))
    ((recv (exp (gen) (mul x y-0))) (send (exp (gen) (mul x y-0))))
    ((recv (cat (exp (gen) y) (mul x (rec y) y-0)))
      (send (cat (exp (gen) y) (mul x (rec y) y-0))))
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b-0)) (exp h y)))))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y-0)
          (enc (enc (exp (gen) y-0) (exp (gen) x) (privk b))
            (exp (gen) (mul x y-0)))))))
  (label 16)
  (parent 11)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol station-to-station-unflip diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))
      (send (privk a)))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))
      (send (privk b)))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (non-orig (privk a))
  (uniq-gen y)
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))))
  (label 17)
  (unrealized (0 2))
  (origs)
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen y x)
  (operation encryption-test (added-strand init 3)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
      (exp (gen) (mul y x))) (0 2))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x))))))
  (label 18)
  (parent 17)
  (unrealized (1 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (b name) (h base) (y rndx))
  (defstrand resp 3 (a b) (b b) (h h) (y y))
  (non-orig (privk b))
  (uniq-gen y)
  (operation encryption-test (displaced 1 0 resp 2)
    (enc (enc (exp (gen) y) h (privk a)) (exp h y)) (0 2))
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk b)) (exp h y)))))
  (label 19)
  (parent 17)
  (realized)
  (shape)
  (maps ((0) ((a b) (b b) (y y) (h h))))
  (origs))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-gen y)
  (operation encryption-test (added-listener (exp h y))
    (enc (enc (exp (gen) y) h (privk a)) (exp h y)) (0 2))
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y))))
    ((recv (exp h y)) (send (exp h y))))
  (label 20)
  (parent 17)
  (unrealized (0 2) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen x y)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (1 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y))))))
  (label 21)
  (parent 18)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (y y) (h (exp (gen) x)))))
  (origs))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1)))
  (non-orig (privk a))
  (uniq-gen y x)
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (1 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 22)
  (parent 18)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (y rndx))
  (defstrand resp 3 (a a) (b b) (h (gen)) (y y))
  (deflistener (exp (gen) y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-gen y)
  (operation nonce-test (displaced 2 0 resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (gen))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
      (recv (enc (enc (exp (gen) y) (gen) (privk a)) (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y))))
  (label 23)
  (parent 20)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx) (w expt))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (deflistener (cat (exp h (mul y (rec w))) w))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-gen y)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul y (rec w))) w))
    (exp h y) (1 0))
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y))))
    ((recv (exp h y)) (send (exp h y)))
    ((recv (cat (exp h (mul y (rec w))) w))
      (send (cat (exp h (mul y (rec w))) w))))
  (label 24)
  (parent 20)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul y x)) (2 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 25)
  (parent 22)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul y x)) (2 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 26)
  (parent 22)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (b name) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (gen)) (y y))
  (deflistener (exp (gen) y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk b))
  (uniq-gen y)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc (exp (gen) y) (gen) (privk a)) (0 2))
  (traces
    ((recv (gen))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
      (recv (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y))))
  (label 27)
  (parent 23)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (w expt) (y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-gen y)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 resp 2) (exp (gen) y-0) (2 0))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk a))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 28)
  (parent 24)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (b name) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (gen)) (y y))
  (non-orig (privk b))
  (uniq-gen y)
  (operation generalization deleted (1 0))
  (traces
    ((recv (gen))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
      (recv (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y)))))
  (label 29)
  (parent 27)
  (realized)
  (shape)
  (maps ((0) ((a b) (b b) (y y) (h (gen)))))
  (origs))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) y) (exp (gen) x) (privk a)) (0 2))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x))))))
  (label 30)
  (parent 28)
  (unrealized (2 0) (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (b name) (w expt) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen y)
  (precur (2 0))
  (operation encryption-test (displaced 3 0 resp 2)
    (enc (exp (gen) y) (exp (gen) w) (privk a)) (0 2))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 31)
  (parent 28)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (displaced 4 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (3 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y))))))
  (label 32)
  (parent 30)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (3 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 33)
  (parent 30)
  (unrealized (2 0) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (b name) (w expt) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (exp (gen) w)) (y y))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk b))
  (uniq-gen y)
  (precur (1 0))
  (operation generalization deleted (1 0))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
          (exp (gen) (mul w y)))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 34)
  (parent 31)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 35)
  (parent 33)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 36)
  (parent 33)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (b name) (w expt) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (exp (gen) w)) (y y))
  (non-orig (privk b))
  (uniq-gen y)
  (operation generalization deleted (1 0))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
          (exp (gen) (mul w y))))))
  (label 37)
  (parent 34)
  (realized)
  (shape)
  (maps ((0) ((a b) (b b) (y y) (h (exp (gen) w)))))
  (origs))

(comment "Nothing left to do")

(defprotocol station-to-station-unflip diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))
      (send (privk a)))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))
      (send (privk b)))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (non-orig (privk a))
  (uniq-gen y)
  (facts (neq a b))
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))))
  (label 38)
  (unrealized (0 2))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen y x)
  (facts (neq a b))
  (operation encryption-test (added-strand init 3)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
      (exp (gen) (mul y x))) (0 2))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x))))))
  (label 39)
  (parent 38)
  (unrealized (1 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-gen y)
  (facts (neq a b))
  (operation encryption-test (added-listener (exp h y))
    (enc (enc (exp (gen) y) h (privk a)) (exp h y)) (0 2))
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y))))
    ((recv (exp h y)) (send (exp h y))))
  (label 40)
  (parent 38)
  (unrealized (0 2) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen x y)
  (facts (neq a b))
  (operation encryption-test (displaced 2 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (1 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y))))))
  (label 41)
  (parent 39)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (y y) (h (exp (gen) x)))))
  (origs))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1)))
  (non-orig (privk a))
  (uniq-gen y x)
  (facts (neq a b))
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (1 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 42)
  (parent 39)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (y rndx))
  (defstrand resp 3 (a a) (b b) (h (gen)) (y y))
  (deflistener (exp (gen) y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-gen y)
  (facts (neq a b))
  (operation nonce-test (displaced 2 0 resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (gen))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
      (recv (enc (enc (exp (gen) y) (gen) (privk a)) (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y))))
  (label 43)
  (parent 40)
  (unrealized (0 2))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx) (w expt))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (deflistener (cat (exp h (mul y (rec w))) w))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-gen y)
  (precur (2 0))
  (facts (neq a b))
  (operation nonce-test (added-listener (cat (exp h (mul y (rec w))) w))
    (exp h y) (1 0))
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y))))
    ((recv (exp h y)) (send (exp h y)))
    ((recv (cat (exp h (mul y (rec w))) w))
      (send (cat (exp h (mul y (rec w))) w))))
  (label 44)
  (parent 40)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (facts (neq a b))
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul y x)) (2 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 45)
  (parent 42)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (facts (neq a b))
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul y x)) (2 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 46)
  (parent 42)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (w expt) (y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-gen y)
  (precur (2 0))
  (facts (neq a b))
  (operation nonce-test (displaced 3 0 resp 2) (exp (gen) y-0) (2 0))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk a))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 47)
  (parent 44)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (facts (neq a b))
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) y) (exp (gen) x) (privk a)) (0 2))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x))))))
  (label 48)
  (parent 47)
  (unrealized (2 0) (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)))
  (non-orig (privk a))
  (uniq-gen x y)
  (precur (2 0))
  (facts (neq a b))
  (operation encryption-test (displaced 4 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (3 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y))))))
  (label 49)
  (parent 48)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (facts (neq a b))
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (3 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 50)
  (parent 48)
  (unrealized (2 0) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (facts (neq a b))
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 51)
  (parent 50)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (non-orig (privk a))
  (uniq-gen y x)
  (precur (2 0))
  (facts (neq a b))
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 52)
  (parent 50)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol station-to-station-unflip diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))
      (send (privk a)))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))
      (send (privk b)))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (x rndx))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (traces
    ((send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x))))
    ((recv (exp h x)) (send (exp h x))))
  (label 53)
  (unrealized (0 1) (1 0))
  (preskeleton)
  (origs)
  (comment "Not a skeleton"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (x rndx))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (precedes ((0 0) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (traces
    ((send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x))))
    ((recv (exp h x)) (send (exp h x))))
  (label 54)
  (parent 53)
  (unrealized (0 1) (1 0))
  (origs)
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx))
  (defstrand init 3 (a a) (b b) (h (gen)) (x x))
  (deflistener (exp (gen) x))
  (precedes ((0 0) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (gen)
          (enc (enc (gen) (exp (gen) x) (privk b)) (exp (gen) x))))
      (send (enc (enc (gen) (exp (gen) x) (privk a)) (exp (gen) x))))
    ((recv (exp (gen) x)) (send (exp (gen) x))))
  (label 55)
  (parent 54)
  (unrealized (0 1))
  (dead)
  (origs)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (rec x))) (x x))
  (deflistener (gen))
  (precedes ((0 0) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation nonce-test (contracted (h (exp (gen) (rec x)))) (gen)
    (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (rec x))
          (enc (enc (exp (gen) (rec x)) (exp (gen) x) (privk b))
            (gen))))
      (send
        (enc (enc (exp (gen) (rec x)) (exp (gen) x) (privk a)) (gen))))
    ((recv (gen)) (send (gen))))
  (label 56)
  (parent 54)
  (unrealized (0 1))
  (dead)
  (origs)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x x-0 rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) x-0))) (x x))
  (deflistener (exp (gen) x-0))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (1 0)) ((2 0) (0 1)) ((2 0) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) x-0))
          (enc
            (enc (exp (gen) (mul (rec x) x-0)) (exp (gen) x) (privk b))
            (exp (gen) x-0))))
      (send
        (enc (enc (exp (gen) (mul (rec x) x-0)) (exp (gen) x) (privk a))
          (exp (gen) x-0))))
    ((recv (exp (gen) x-0)) (send (exp (gen) x-0)))
    ((send (exp (gen) x-0))))
  (label 57)
  (parent 54)
  (unrealized (0 1))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (h base) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) y))) (x x))
  (deflistener (exp (gen) y))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (1 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) y))
          (enc (enc (exp (gen) (mul (rec x) y)) (exp (gen) x) (privk b))
            (exp (gen) y))))
      (send
        (enc (enc (exp (gen) (mul (rec x) y)) (exp (gen) x) (privk a))
          (exp (gen) y)))) ((recv (exp (gen) y)) (send (exp (gen) y)))
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b-0)) (exp h y))))))
  (label 58)
  (parent 54)
  (unrealized (0 1))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (x rndx) (w expt))
  (defstrand init 3 (a a) (b b) (h h) (x x))
  (deflistener (exp h x))
  (deflistener (cat (exp h (mul x (rec w))) w))
  (precedes ((0 0) (2 0)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul x (rec w))) w))
    (exp h x) (1 0))
  (traces
    ((send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x))))
    ((recv (exp h x)) (send (exp h x)))
    ((recv (cat (exp h (mul x (rec w))) w))
      (send (cat (exp h (mul x (rec w))) w))))
  (label 59)
  (parent 54)
  (unrealized (0 1) (2 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (w expt) (x rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) w)) (x x))
  (deflistener (exp (gen) (mul w x)))
  (deflistener (cat (exp (gen) x) w))
  (precedes ((0 0) (2 0)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) w)
          (enc (enc (exp (gen) w) (exp (gen) x) (privk b))
            (exp (gen) (mul w x)))))
      (send
        (enc (enc (exp (gen) w) (exp (gen) x) (privk a))
          (exp (gen) (mul w x)))))
    ((recv (exp (gen) (mul w x))) (send (exp (gen) (mul w x))))
    ((recv (cat (exp (gen) x) w)) (send (cat (exp (gen) x) w))))
  (label 60)
  (parent 59)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx) (w expt))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w))) (x x))
  (deflistener (exp (gen) w))
  (deflistener (cat (gen) w))
  (precedes ((0 0) (2 0)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (2 0))
  (operation nonce-test (contracted (h (exp (gen) (mul (rec x) w))))
    (gen) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) w))
          (enc (enc (exp (gen) (mul (rec x) w)) (exp (gen) x) (privk b))
            (exp (gen) w))))
      (send
        (enc (enc (exp (gen) (mul (rec x) w)) (exp (gen) x) (privk a))
          (exp (gen) w)))) ((recv (exp (gen) w)) (send (exp (gen) w)))
    ((recv (cat (gen) w)) (send (cat (gen) w))))
  (label 61)
  (parent 59)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x rndx) (w expt) (x-0 rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w x-0)))
    (x x))
  (deflistener (exp (gen) (mul w x-0)))
  (deflistener (cat (exp (gen) x-0) w))
  (defstrand init 1 (x x-0))
  (precedes ((0 0) (2 0)) ((2 1) (1 0)) ((3 0) (0 1)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (precur (2 0))
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) w x-0))
          (enc
            (enc (exp (gen) (mul (rec x) w x-0)) (exp (gen) x)
              (privk b)) (exp (gen) (mul w x-0)))))
      (send
        (enc
          (enc (exp (gen) (mul (rec x) w x-0)) (exp (gen) x) (privk a))
          (exp (gen) (mul w x-0)))))
    ((recv (exp (gen) (mul w x-0))) (send (exp (gen) (mul w x-0))))
    ((recv (cat (exp (gen) x-0) w)) (send (cat (exp (gen) x-0) w)))
    ((send (exp (gen) x-0))))
  (label 62)
  (parent 59)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (h base) (x rndx) (w expt) (y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) (mul (rec x) w y))) (x x))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (precedes ((0 0) (2 0)) ((2 1) (1 0)) ((3 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) (mul (rec x) w y))
          (enc
            (enc (exp (gen) (mul (rec x) w y)) (exp (gen) x) (privk b))
            (exp (gen) (mul w y)))))
      (send
        (enc (enc (exp (gen) (mul (rec x) w y)) (exp (gen) x) (privk a))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w)))
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b-0)) (exp h y))))))
  (label 63)
  (parent 59)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x) y))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((2 1) (1 0)) ((3 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 64)
  (parent 60)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((2 1) (1 0)) ((3 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (gen) (mul x y))) (send (cat (gen) (mul x y))))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 65)
  (parent 61)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x x-0 y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0) y)))
  (defstrand init 1 (x x-0))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (4 0)) ((2 1) (1 0)) ((3 0) (0 1)) ((3 0) (2 0))
    ((4 1) (0 1)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0 y)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0) y)))
      (send (cat (exp (gen) x-0) (mul x (rec x-0) y))))
    ((send (exp (gen) x-0)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 66)
  (parent 62)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (3 0)) ((2 1) (1 0)) ((3 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (displaced 4 3 resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b-0)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))))
  (label 67)
  (parent 63)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (h base) (x y y-0 rndx))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y-0)) (x x))
  (deflistener (exp (gen) (mul x y-0)))
  (deflistener (cat (exp (gen) y) (mul x (rec y) y-0)))
  (defstrand resp 2 (b b-0) (h h) (y y))
  (defstrand resp 2 (b b) (h (exp (gen) x)) (y y-0))
  (precedes ((0 0) (4 0)) ((2 1) (1 0)) ((3 1) (0 1)) ((3 1) (2 0))
    ((4 1) (0 1)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y y-0)
  (precur (2 0))
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y-0) (exp (gen) x) (privk b)) (0 1))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y-0)
          (enc (enc (exp (gen) y-0) (exp (gen) x) (privk b))
            (exp (gen) (mul x y-0)))))
      (send
        (enc (enc (exp (gen) y-0) (exp (gen) x) (privk a))
          (exp (gen) (mul x y-0)))))
    ((recv (exp (gen) (mul x y-0))) (send (exp (gen) (mul x y-0))))
    ((recv (cat (exp (gen) y) (mul x (rec y) y-0)))
      (send (cat (exp (gen) y) (mul x (rec y) y-0))))
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b-0)) (exp h y)))))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y-0)
          (enc (enc (exp (gen) y-0) (exp (gen) x) (privk b))
            (exp (gen) (mul x y-0)))))))
  (label 68)
  (parent 63)
  (unrealized (1 0) (2 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol station-to-station-unflip diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))
      (send (privk a)))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))
      (send (privk b)))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y))))
    ((recv (exp h y)) (send (exp h y))))
  (label 69)
  (unrealized (0 2) (1 0))
  (preskeleton)
  (origs)
  (comment "Not a skeleton"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (precedes ((0 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y))))
    ((recv (exp h y)) (send (exp h y))))
  (label 70)
  (parent 69)
  (unrealized (0 2) (1 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (y rndx))
  (defstrand resp 3 (a a) (b b) (h (gen)) (y y))
  (deflistener (exp (gen) y))
  (precedes ((0 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (operation nonce-test (displaced 2 0 resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (gen))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
      (recv (enc (enc (exp (gen) y) (gen) (privk a)) (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y))))
  (label 71)
  (parent 70)
  (unrealized (0 2))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (h base) (y rndx) (w expt))
  (defstrand resp 3 (a a) (b b) (h h) (y y))
  (deflistener (exp h y))
  (deflistener (cat (exp h (mul y (rec w))) w))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp h (mul y (rec w))) w))
    (exp h y) (1 0))
  (traces
    ((recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y))))
    ((recv (exp h y)) (send (exp h y)))
    ((recv (cat (exp h (mul y (rec w))) w))
      (send (cat (exp h (mul y (rec w))) w))))
  (label 72)
  (parent 70)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (b name) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (gen)) (y y))
  (deflistener (exp (gen) y))
  (precedes ((0 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen y)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc (exp (gen) y) (gen) (privk a)) (0 2))
  (traces
    ((recv (gen))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
      (recv (enc (enc (exp (gen) y) (gen) (privk b)) (exp (gen) y))))
    ((recv (exp (gen) y)) (send (exp (gen) y))))
  (label 73)
  (parent 71)
  (realized)
  (shape)
  (maps ((0 1) ((a b) (b b) (y y) (h (gen)))))
  (origs))

(defskeleton station-to-station-unflip
  (vars (a b name) (w expt) (y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (precur (2 0))
  (operation nonce-test (displaced 3 0 resp 2) (exp (gen) y-0) (2 0))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk a))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 74)
  (parent 72)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((2 1) (1 0)) ((3 0) (0 0))
    ((3 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (precur (2 0))
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) y) (exp (gen) x) (privk a)) (0 2))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x))))))
  (label 75)
  (parent 74)
  (unrealized (2 0) (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (b name) (w expt) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (deflistener (cat (exp (gen) y) w))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen y)
  (precur (2 0))
  (operation encryption-test (displaced 3 0 resp 2)
    (enc (exp (gen) y) (exp (gen) w) (privk a)) (0 2))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y))))
    ((recv (cat (exp (gen) y) w)) (send (cat (exp (gen) y) w))))
  (label 76)
  (parent 74)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
  (precedes ((0 1) (2 0)) ((0 1) (3 1)) ((2 1) (1 0)) ((3 0) (0 0))
    ((3 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (2 0))
  (operation encryption-test (displaced 4 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (3 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y))))))
  (label 77)
  (parent 75)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((2 1) (1 0)) ((3 0) (0 0))
    ((3 2) (0 2)) ((4 1) (3 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (precur (2 0))
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (3 1))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 78)
  (parent 75)
  (unrealized (2 0) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (b name) (w expt) (y rndx))
  (defstrand resp 3 (a b) (b b) (h (exp (gen) w)) (y y))
  (deflistener (exp (gen) (mul w y)))
  (precedes ((0 1) (1 0)))
  (non-orig (privk b))
  (uniq-gen y)
  (operation generalization deleted (2 0))
  (traces
    ((recv (exp (gen) w))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
            (exp (gen) (mul w y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) w) (privk b))
          (exp (gen) (mul w y)))))
    ((recv (exp (gen) (mul w y))) (send (exp (gen) (mul w y)))))
  (label 79)
  (parent 76)
  (realized)
  (shape)
  (maps ((0 1) ((a b) (b b) (y y) (h (exp (gen) w)))))
  (origs))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((2 1) (1 0)) ((3 0) (0 0))
    ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 80)
  (parent 78)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (2 0)) ((0 1) (5 0)) ((2 1) (1 0)) ((3 0) (0 0))
    ((3 2) (0 2)) ((4 1) (3 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (precur (2 0))
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x)))
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 81)
  (parent 78)
  (unrealized (2 0) (5 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol station-to-station-unflip diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))
      (send (privk a)))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))
      (send (privk b)))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b))))
  (label 82)
  (unrealized (1 2))
  (origs ((privk b) (1 3)) ((privk a) (0 3)))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b name) (y x rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a) (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen y x)
  (operation encryption-test (displaced 2 0 init 3)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
      (exp (gen) (mul y x))) (1 2))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul y x)))) (send (privk b))))
  (label 83)
  (parent 82)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (b b) (x x) (y y) (a-0 a))))
  (origs ((privk b) (1 3)) ((privk a) (0 3))))

(defskeleton station-to-station-unflip
  (vars (a b name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a b) (b b) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation encryption-test (displaced 2 1 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
      (exp (gen) (mul x y))) (1 2))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
          (exp (gen) (mul x y)))) (send (privk b))))
  (label 84)
  (parent 82)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (b b) (x x) (y y) (a-0 b))))
  (origs ((privk b) (1 3)) ((privk a) (0 3))))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((2 1) (1 2)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation encryption-test (added-listener (exp (gen) (mul x y)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
      (exp (gen) (mul x y))) (1 2))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b)))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
  (label 85)
  (parent 82)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (1 2))
    ((3 1) (2 0)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul x y)) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b)))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 86)
  (parent 85)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (1 2))
    ((3 1) (2 0)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul x y)) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b)))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 87)
  (parent 85)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol station-to-station-unflip diffie-hellman
  (defrole init
    (vars (x rndx) (h base) (a b name))
    (trace (send (exp (gen) x))
      (recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
      (send (enc (enc h (exp (gen) x) (privk a)) (exp h x)))
      (send (privk a)))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (h base) (a b name))
    (trace (recv h)
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) h (privk b)) (exp h y))))
      (recv (enc (enc (exp (gen) y) h (privk a)) (exp h y)))
      (send (privk b)))
    (uniq-gen y))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b)))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
  (label 88)
  (unrealized (1 2) (2 0))
  (preskeleton)
  (origs ((privk b) (1 3)) ((privk a) (0 3)))
  (comment "Not a skeleton"))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b)))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
  (label 89)
  (parent 88)
  (unrealized (1 2) (2 0))
  (origs ((privk b) (1 3)) ((privk a) (0 3)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((3 1) (2 0)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul x y)) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b)))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 90)
  (parent 89)
  (unrealized (1 2) (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton station-to-station-unflip
  (vars (a b a-0 name) (x y rndx))
  (defstrand init 4 (a a) (b b) (h (exp (gen) y)) (x x))
  (defstrand resp 4 (a a-0) (b b) (h (exp (gen) x)) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((3 1) (2 0)))
  (uniq-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul x y)) (2 0))
  (traces
    ((send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a))
          (exp (gen) (mul x y)))) (send (privk a)))
    ((recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (recv
        (enc (enc (exp (gen) y) (exp (gen) x) (privk a-0))
          (exp (gen) (mul x y)))) (send (privk b)))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 91)
  (parent 89)
  (unrealized (1 2) (3 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")