(herald dhstatic-state (algebra diffie-hellman) (bound 16))

(comment "CPSA 4.4.3")
(comment "All input read from tst/dhstatic-state.scm")
(comment "Strand count bounded at 16")

(defprotocol dhstatic-state diffie-hellman
  (defrole cert
    (vars (subj ca name) (serial data) (galpha mesg))
    (trace (recv (sig (cert-req subj galpha ca) (privk "sig" subj)))
      (send (sig (cert subj galpha ca serial) (privk "sig" ca))))
    (uniq-orig serial)
    (comment "Certificate Authority"))
  (defrole get-cert
    (vars (self ca name) (serial data) (ra rndx) (static-key locn)
      (ignore mesg))
    (trace
      (send (sig (cert-req self (exp (gen) ra) ca) (privk "sig" self)))
      (recv (sig (cert self (exp (gen) ra) ca serial) (privk "sig" ca)))
      (load static-key ignore)
      (stor static-key (cat "privkey" self ra serial ca)))
    (uniq-gen ra)
    (comment "Get certified"))
  (defrole init
    (vars (a b ca name) (ra rndx) (serial-a serial-b data) (galpha base)
      (n text) (static-key locn))
    (trace (load static-key (cat "privkey" a ra serial-a ca))
      (recv (sig (cert b galpha ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp galpha ra))) (recv n))
    (uniq-orig n)
    (gen-st (cat "privkey" a ra serial-a ca))
    (facts (neq a b))
    (comment "Initiator is A"))
  (defrole resp
    (vars (a b ca name) (rb rndx) (serial-b serial-a data) (galpha base)
      (n text) (static-key locn))
    (trace (load static-key (cat "privkey" b rb serial-b ca))
      (recv (sig (cert a galpha ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp galpha rb))) (send n))
    (facts (neq a b))
    (gen-st (cat "privkey" b rb serial-b ca))
    (comment "Responder is B"))
  (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))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule fact-init-neq0
    (forall ((z strd) (b a name))
      (implies
        (and (p "init" z (idx 2)) (p "init" "a" z a) (p "init" "b" z b))
        (fact neq a b))))
  (defgenrule fact-resp-neq0
    (forall ((z strd) (b a name))
      (implies
        (and (p "resp" z (idx 2)) (p "resp" "a" z a) (p "resp" "b" z b))
        (fact neq a b))))
  (defgenrule trRl_get-cert-at-3
    (forall ((z strd))
      (implies (p "get-cert" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_get-cert-at-2
    (forall ((z strd))
      (implies (p "get-cert" z (idx 4)) (trans z (idx 2)))))
  (defgenrule gen-st-init-0
    (forall ((z strd) (a name) (ra rndx) (serial-a data) (ca name))
      (implies
        (and (p "init" z (idx 1)) (p "init" "ca" z ca)
          (p "init" "serial-a" z serial-a) (p "init" "ra" z ra)
          (p "init" "a" z a))
        (gen-st (cat "privkey" a ra serial-a ca)))))
  (defgenrule gen-st-resp-0
    (forall ((z strd) (b name) (rb rndx) (serial-b data) (ca name))
      (implies
        (and (p "resp" z (idx 1)) (p "resp" "ca" z ca)
          (p "resp" "serial-b" z serial-b) (p "resp" "rb" z rb)
          (p "resp" "b" z b))
        (gen-st (cat "privkey" b rb serial-b ca)))))
  (lang (cert-req (tupl 3)) (cert (tupl 4)) (sig sign)))

(defskeleton dhstatic-state
  (vars (serial-a serial-b data) (n text) (ca b a name) (pt pval)
    (galpha base) (static-key locn) (ra rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (ra ra))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig n)
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv (sig (cert b galpha ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp galpha ra))) (recv n)))
  (label 0)
  (unrealized (0 1))
  (origs (n (0 2)))
  (comment "Not closed under rules"))

(defskeleton dhstatic-state
  (vars (serial-a serial-b data) (n text) (ca b a name) (pt pval)
    (galpha base) (static-key locn) (ra rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (ra ra))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig n)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (rule fact-init-neq0 fact-resp-neq0 gen-st-resp-0)
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv (sig (cert b galpha ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp galpha ra))) (recv n)))
  (label 1)
  (parent 0)
  (unrealized (0 0) (0 1))
  (origs (n (0 2)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (galpha base) (static-key locn) (ra rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (precedes ((1 3) (0 0)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig n)
  (uniq-gen ra)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation channel-test (added-strand get-cert 4)
    (ch-msg static-key (cat pt "privkey" a ra serial-a ca)) (0 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv (sig (cert b galpha ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp galpha ra))) (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca))))
  (label 2)
  (parent 1)
  (unrealized (0 1) (0 3) (1 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (galpha base) (static-key locn) (ra rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a n)
  (uniq-gen ra)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)) (1 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv (sig (cert b galpha ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp galpha ra))) (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))))
  (label 3)
  (parent 2)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (galpha base) (static-key locn) (ra rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha galpha) (serial serial-b) (subj b) (ca ca))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)) ((3 1) (0 1)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert b galpha ca serial-b) (privk "sig" ca)) (0 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv (sig (cert b galpha ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp galpha ra))) (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b galpha ca) (privk "sig" b)))
      (send (sig (cert b galpha ca serial-b) (privk "sig" ca)))))
  (label 4)
  (parent 3)
  (unrealized (0 3) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)) ((3 1) (0 1))
    ((4 0) (3 0)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand get-cert 1)
    (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)) (3 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))))
  (label 5)
  (parent 4)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text)
    (ca b a ca-0 name) (pt pt-0 pt-1 pval)
    (static-key static-key-0 locn) (ra ra-0 rb rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec rb))))
    (static-key static-key-0) (rb rb))
  (precedes ((0 2) (5 2)) ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (5 0)) ((4 0) (3 0))
    ((5 3) (0 3)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b rb serial-b ca-0)
    (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-resp-neq0 gen-st-resp-0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (added-strand resp 4) n (0 3)
    (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((load static-key-0 (cat pt-1 "privkey" b rb serial-b ca-0))
      (recv
        (sig (cert a (exp (gen) (mul ra ra-0 (rec rb))) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n)))
  (label 6)
  (parent 5)
  (unrealized (5 0) (5 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (deflistener (exp (gen) (mul ra ra-0)))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (5 0)) ((5 1) (0 3)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (added-listener (exp (gen) (mul ra ra-0))) n
    (0 3) (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0)))))
  (label 7)
  (parent 5)
  (unrealized (5 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (b a ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra)) (static-key static-key-0)
    (rb ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self b)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (precedes ((0 2) (4 2)) ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (4 1)) ((3 1) (0 1)) ((3 1) (5 1)) ((4 3) (0 3))
    ((5 0) (3 0)) ((5 3) (4 0)))
  (non-orig (privk "sig" b) (privk "sig" ca))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra-0 serial-b ca)
    (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation channel-test (displaced 4 6 get-cert 4)
    (ch-msg static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca)) (5 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((load static-key-0 (cat pt-1 "privkey" b ra-0 serial-b ca))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" b ra-0 serial-b ca))))
  (label 8)
  (parent 6)
  (realized)
  (shape)
  (maps
    ((0)
      ((ca ca) (b b) (a a) (ra ra) (serial-a serial-a)
        (serial-b serial-b) (galpha (exp (gen) ra-0)) (n n)
        (static-key static-key))))
  (origs (pt-1 (5 3)) (serial-b (3 1)) (serial-a (2 1)) (pt (1 3))
    (n (0 2))))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (ca b a ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (rb ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (precedes ((0 2) (5 2)) ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0))
    ((5 3) (0 3)) ((6 3) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra-1 serial-b ca-0)
    (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation channel-test (added-strand get-cert 4)
    (ch-msg static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0))
    (5 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((load static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0))
      (recv
        (sig (cert a (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-1) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0))))
  (label 9)
  (parent 6)
  (unrealized (5 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (precedes ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (6 0)) ((5 1) (0 3))
    ((6 1) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (added-listener (cat (exp (gen) ra) ra-0))
    (exp (gen) (mul ra ra-0)) (5 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0))))
  (label 10)
  (parent 7)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra-0) ra))
  (precedes ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (6 0)) ((5 1) (0 3))
    ((6 1) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (added-listener (cat (exp (gen) ra-0) ra))
    (exp (gen) (mul ra ra-0)) (5 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra-0) ra)) (send (cat (exp (gen) ra-0) ra))))
  (label 11)
  (parent 7)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (ca b a ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (rb ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra ra-0)) ra-1))
  (precedes ((0 2) (5 2)) ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0))
    ((2 1) (1 1)) ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1))
    ((4 0) (3 0)) ((4 0) (7 0)) ((5 3) (0 3)) ((6 0) (7 0))
    ((6 3) (5 0)) ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra-1 serial-b ca-0)
    (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul ra ra-0)) ra-1))
    (exp (gen) (mul ra ra-0 (rec ra-1))) (5 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((load static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0))
      (recv
        (sig (cert a (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-1) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0)))
    ((recv (cat (exp (gen) (mul ra ra-0)) ra-1))
      (send (cat (exp (gen) (mul ra ra-0)) ra-1))))
  (label 12)
  (parent 9)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (ca b a ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (rb ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra (rec ra-1))) ra-0))
  (precedes ((0 2) (5 2)) ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0))
    ((2 1) (1 1)) ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1))
    ((4 0) (3 0)) ((4 0) (7 0)) ((5 3) (0 3)) ((6 0) (7 0))
    ((6 3) (5 0)) ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra-1 serial-b ca-0)
    (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul ra (rec ra-1))) ra-0))
    (exp (gen) (mul ra ra-0 (rec ra-1))) (5 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((load static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0))
      (recv
        (sig (cert a (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-1) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0)))
    ((recv (cat (exp (gen) (mul ra (rec ra-1))) ra-0))
      (send (cat (exp (gen) (mul ra (rec ra-1))) ra-0))))
  (label 13)
  (parent 9)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (ca b a ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (rb ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))
  (precedes ((0 2) (5 2)) ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0))
    ((2 1) (1 1)) ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1))
    ((4 0) (3 0)) ((4 0) (7 0)) ((5 3) (0 3)) ((6 0) (7 0))
    ((6 3) (5 0)) ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra-1 serial-b ca-0)
    (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))
    (exp (gen) (mul ra ra-0 (rec ra-1))) (5 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((load static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0))
      (recv
        (sig (cert a (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-1) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0)))
    ((recv (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))
      (send (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))))
  (label 14)
  (parent 9)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b serial data) (n text)
    (a self ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b self) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b)
    (subj self) (ca ca))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 1) (0 3)) ((5 1) (4 0)) ((6 0) (3 0))
    ((6 3) (5 0)))
  (non-orig (privk "sig" self) (privk "sig" ca))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a self) (neq self a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (displaced 4 7 get-cert 4) ra-0 (6 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a self serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial-b)
          (privk "sig" ca))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0)))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)))
      (load static-key-0 (cat pt-1 ignore-0))
      (stor static-key-0 (cat pt-2 "privkey" self ra-0 serial ca))))
  (label 15)
  (parent 10)
  (unrealized (5 0) (6 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-a serial-b data) (n text) (ca b a name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra)) (static-key static-key)
    (ra ra-0))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra-0))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((1 3) (6 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (6 0)) ((5 1) (0 3))
    ((6 1) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra-0 serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (displaced 7 1 get-cert 4) ra-0 (6 0))
  (traces
    ((load static-key (cat pt "privkey" a ra-0 serial-a ca))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra-0 serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0))))
  (label 16)
  (parent 11)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (ca b a ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (rb ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra ra-0)) ra-1))
  (precedes ((0 2) (5 2)) ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0))
    ((2 1) (1 1)) ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1))
    ((4 0) (3 0)) ((5 3) (0 3)) ((6 3) (5 0)) ((6 3) (7 0))
    ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra-1 serial-b ca-0)
    (cat "privkey" a ra serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test (displaced 8 6 get-cert 4) ra-1 (7 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b))))
    ((load static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0))
      (recv
        (sig (cert a (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-1) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" b ra-1 serial-b ca-0)))
    ((recv (cat (exp (gen) (mul ra ra-0)) ra-1))
      (send (cat (exp (gen) (mul ra ra-0)) ra-1))))
  (label 17)
  (parent 12)
  (unrealized (7 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 ignore-1 mesg) (serial-a serial-b serial data)
    (n text) (a ca self ca-0 name) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (static-key static-key-0 static-key-1 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b self) (ca ca-0) (galpha (exp (gen) ra-1)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca-0))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-b)
    (subj self) (ca ca-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b self) (ca ca) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (rb ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (defstrand get-cert 4 (ignore ignore-1) (serial serial) (self self)
    (ca ca-0) (static-key static-key-1) (ra ra-1))
  (precedes ((0 2) (4 2)) ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0))
    ((2 1) (1 1)) ((2 1) (4 1)) ((3 1) (0 1)) ((3 1) (5 1))
    ((4 3) (0 3)) ((5 0) (6 0)) ((5 3) (4 0)) ((6 1) (4 1))
    ((7 0) (3 0)) ((7 3) (6 0)))
  (non-orig (privk "sig" self) (privk "sig" ca-0))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra serial-a ca-0)
    (cat "privkey" self ra-0 serial-b ca))
  (facts (neq a self) (neq self a))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test (displaced 4 8 get-cert 4) ra-1 (7 0))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca-0))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a self serial-a serial-b (exp (gen) (mul ra ra-1))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra) ca-0 serial-a) (privk "sig" ca-0)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca-0)))
    ((recv (sig (cert-req a (exp (gen) ra) ca-0) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra) ca-0 serial-a) (privk "sig" ca-0))))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))))
    ((load static-key-0 (cat pt-1 "privkey" self ra-0 serial-b ca))
      (recv
        (sig (cert a (exp (gen) (mul ra (rec ra-0) ra-1)) ca serial-a)
          (privk "sig" ca)))
      (recv (enc n a self serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" self ra-0 serial-b ca)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1)))
    ((send
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial)
          (privk "sig" ca-0))) (load static-key-1 (cat pt-3 ignore-1))
      (stor static-key-1 (cat pt-4 "privkey" self ra-1 serial ca-0))))
  (label 18)
  (parent 13)
  (unrealized (6 0) (7 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (ca b a ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra)) (static-key static-key)
    (ra ra-1))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra-1))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand get-cert 1 (self b) (ca ca) (ra ra))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (rb ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (precedes ((0 2) (5 2)) ((1 0) (2 0)) ((1 3) (0 0)) ((1 3) (7 0))
    ((2 1) (1 1)) ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0))
    ((4 0) (7 0)) ((5 3) (0 3)) ((6 0) (7 0)) ((6 3) (5 0))
    ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" b))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra-0 serial-b ca-0)
    (cat "privkey" a ra-1 serial-a ca))
  (facts (neq a b) (neq b a))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test (displaced 8 1 get-cert 4) ra-1 (7 0))
  (traces
    ((load static-key (cat pt "privkey" a ra-1 serial-a ca))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-1))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra-1) ca) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-1) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra-1 serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra-1) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-1) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b))))
    ((load static-key-0 (cat pt-1 "privkey" b ra-0 serial-b ca-0))
      (recv
        (sig (cert a (exp (gen) (mul ra (rec ra-0) ra-1)) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-0) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-0) ca-0 serial-b)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" b ra-0 serial-b ca-0)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1))))
  (label 19)
  (parent 14)
  (unrealized (7 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b data) (n text)
    (a self ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b self) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b)
    (subj self) (ca ca))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((3 1) (6 1)) ((4 1) (0 3)) ((5 1) (4 0))
    ((6 0) (3 0)) ((6 3) (5 0)))
  (non-orig (privk "sig" self) (privk "sig" ca))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a self) (neq self a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (displaced 7 3 cert 2)
    (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)) (6 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a self serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial-b)
          (privk "sig" ca))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0)))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (load static-key-0 (cat pt-1 ignore-0))
      (stor static-key-0 (cat pt-2 "privkey" self ra-0 serial-b ca))))
  (label 20)
  (parent 15)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-a serial-b serial data) (n text)
    (a self ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b self) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b)
    (subj self) (ca ca))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial)
    (subj self) (ca ca))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 1) (0 3)) ((5 1) (4 0)) ((6 0) (3 0))
    ((6 0) (7 0)) ((6 3) (5 0)) ((7 1) (6 1)))
  (non-orig (privk "sig" self) (privk "sig" ca))
  (uniq-orig serial-a serial-b serial n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra serial-a ca))
  (facts (neq a self) (neq self a))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)) (6 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (send (enc n a self serial-a serial-b (exp (gen) (mul ra ra-0))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca)))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial-b)
          (privk "sig" ca))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0)))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)))
      (load static-key-0 (cat pt-1 ignore-0))
      (stor static-key-0 (cat pt-2 "privkey" self ra-0 serial ca)))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)))))
  (label 21)
  (parent 15)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 ignore-1 mesg) (serial-a serial-b data)
    (n text) (a ca self ca-0 name) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (static-key static-key-0 static-key-1 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b self) (ca ca-0) (galpha (exp (gen) ra-1)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca-0))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-b)
    (subj self) (ca ca-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b self) (ca ca) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (rb ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (defstrand get-cert 4 (ignore ignore-1) (serial serial-b) (self self)
    (ca ca-0) (static-key static-key-1) (ra ra-1))
  (precedes ((0 2) (4 2)) ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0))
    ((2 1) (1 1)) ((2 1) (4 1)) ((3 1) (0 1)) ((3 1) (5 1))
    ((3 1) (7 1)) ((4 3) (0 3)) ((5 0) (6 0)) ((5 3) (4 0))
    ((6 1) (4 1)) ((7 0) (3 0)) ((7 3) (6 0)))
  (non-orig (privk "sig" self) (privk "sig" ca-0))
  (uniq-orig serial-a serial-b n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra serial-a ca-0)
    (cat "privkey" self ra-0 serial-b ca))
  (facts (neq a self) (neq self a))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation encryption-test (displaced 8 3 cert 2)
    (sig (cert self (exp (gen) ra-1) ca-0 serial) (privk "sig" ca-0))
    (7 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca-0))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a self serial-a serial-b (exp (gen) (mul ra ra-1))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra) ca-0 serial-a) (privk "sig" ca-0)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca-0)))
    ((recv (sig (cert-req a (exp (gen) ra) ca-0) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra) ca-0 serial-a) (privk "sig" ca-0))))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))))
    ((load static-key-0 (cat pt-1 "privkey" self ra-0 serial-b ca))
      (recv
        (sig (cert a (exp (gen) (mul ra (rec ra-0) ra-1)) ca serial-a)
          (privk "sig" ca)))
      (recv (enc n a self serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" self ra-0 serial-b ca)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1)))
    ((send
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))) (load static-key-1 (cat pt-3 ignore-1))
      (stor static-key-1 (cat pt-4 "privkey" self ra-1 serial-b ca-0))))
  (label 22)
  (parent 18)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 ignore-1 mesg) (serial-a serial-b serial data)
    (n text) (a ca self ca-0 name) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (static-key static-key-0 static-key-1 locn) (ra ra-0 ra-1 rndx))
  (defstrand init 4 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b self) (ca ca-0) (galpha (exp (gen) ra-1)) (static-key static-key)
    (ra ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca-0))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-b)
    (subj self) (ca ca-0))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b self) (ca ca) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (rb ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-b) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (defstrand get-cert 4 (ignore ignore-1) (serial serial) (self self)
    (ca ca-0) (static-key static-key-1) (ra ra-1))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial)
    (subj self) (ca ca-0))
  (precedes ((0 2) (4 2)) ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0))
    ((2 1) (1 1)) ((2 1) (4 1)) ((3 1) (0 1)) ((3 1) (5 1))
    ((4 3) (0 3)) ((5 0) (6 0)) ((5 3) (4 0)) ((6 1) (4 1))
    ((7 0) (3 0)) ((7 0) (8 0)) ((7 3) (6 0)) ((8 1) (7 1)))
  (non-orig (privk "sig" self) (privk "sig" ca-0))
  (uniq-orig serial-a serial-b serial n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra serial-a ca-0)
    (cat "privkey" self ra-0 serial-b ca))
  (facts (neq a self) (neq self a))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert self (exp (gen) ra-1) ca-0 serial) (privk "sig" ca-0))
    (7 1))
  (traces
    ((load static-key (cat pt "privkey" a ra serial-a ca-0))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a self serial-a serial-b (exp (gen) (mul ra ra-1))))
      (recv n))
    ((send (sig (cert-req a (exp (gen) ra) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra) ca-0 serial-a) (privk "sig" ca-0)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" a ra serial-a ca-0)))
    ((recv (sig (cert-req a (exp (gen) ra) ca-0) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra) ca-0 serial-a) (privk "sig" ca-0))))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial-b)
          (privk "sig" ca-0))))
    ((load static-key-0 (cat pt-1 "privkey" self ra-0 serial-b ca))
      (recv
        (sig (cert a (exp (gen) (mul ra (rec ra-0) ra-1)) ca serial-a)
          (privk "sig" ca)))
      (recv (enc n a self serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" self ra-0 serial-b ca)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1)))
    ((send
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial)
          (privk "sig" ca-0))) (load static-key-1 (cat pt-3 ignore-1))
      (stor static-key-1 (cat pt-4 "privkey" self ra-1 serial ca-0)))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial)
          (privk "sig" ca-0)))))
  (label 23)
  (parent 18)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhstatic-state diffie-hellman
  (defrole cert
    (vars (subj ca name) (serial data) (galpha mesg))
    (trace (recv (sig (cert-req subj galpha ca) (privk "sig" subj)))
      (send (sig (cert subj galpha ca serial) (privk "sig" ca))))
    (uniq-orig serial)
    (comment "Certificate Authority"))
  (defrole get-cert
    (vars (self ca name) (serial data) (ra rndx) (static-key locn)
      (ignore mesg))
    (trace
      (send (sig (cert-req self (exp (gen) ra) ca) (privk "sig" self)))
      (recv (sig (cert self (exp (gen) ra) ca serial) (privk "sig" ca)))
      (load static-key ignore)
      (stor static-key (cat "privkey" self ra serial ca)))
    (uniq-gen ra)
    (comment "Get certified"))
  (defrole init
    (vars (a b ca name) (ra rndx) (serial-a serial-b data) (galpha base)
      (n text) (static-key locn))
    (trace (load static-key (cat "privkey" a ra serial-a ca))
      (recv (sig (cert b galpha ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp galpha ra))) (recv n))
    (uniq-orig n)
    (gen-st (cat "privkey" a ra serial-a ca))
    (facts (neq a b))
    (comment "Initiator is A"))
  (defrole resp
    (vars (a b ca name) (rb rndx) (serial-b serial-a data) (galpha base)
      (n text) (static-key locn))
    (trace (load static-key (cat "privkey" b rb serial-b ca))
      (recv (sig (cert a galpha ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp galpha rb))) (send n))
    (facts (neq a b))
    (gen-st (cat "privkey" b rb serial-b ca))
    (comment "Responder is B"))
  (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))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule fact-init-neq0
    (forall ((z strd) (b a name))
      (implies
        (and (p "init" z (idx 2)) (p "init" "a" z a) (p "init" "b" z b))
        (fact neq a b))))
  (defgenrule fact-resp-neq0
    (forall ((z strd) (b a name))
      (implies
        (and (p "resp" z (idx 2)) (p "resp" "a" z a) (p "resp" "b" z b))
        (fact neq a b))))
  (defgenrule trRl_get-cert-at-3
    (forall ((z strd))
      (implies (p "get-cert" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_get-cert-at-2
    (forall ((z strd))
      (implies (p "get-cert" z (idx 4)) (trans z (idx 2)))))
  (defgenrule gen-st-init-0
    (forall ((z strd) (a name) (ra rndx) (serial-a data) (ca name))
      (implies
        (and (p "init" z (idx 1)) (p "init" "ca" z ca)
          (p "init" "serial-a" z serial-a) (p "init" "ra" z ra)
          (p "init" "a" z a))
        (gen-st (cat "privkey" a ra serial-a ca)))))
  (defgenrule gen-st-resp-0
    (forall ((z strd) (b name) (rb rndx) (serial-b data) (ca name))
      (implies
        (and (p "resp" z (idx 1)) (p "resp" "ca" z ca)
          (p "resp" "serial-b" z serial-b) (p "resp" "rb" z rb)
          (p "resp" "b" z b))
        (gen-st (cat "privkey" b rb serial-b ca)))))
  (lang (cert-req (tupl 3)) (cert (tupl 4)) (sig sign)))

(defskeleton dhstatic-state
  (vars (serial-b serial-a data) (n text) (ca a b name) (pt pval)
    (galpha base) (static-key locn) (rb rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (rb rb))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (traces
    ((load static-key (cat pt "privkey" b rb serial-b ca))
      (recv (sig (cert a galpha ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp galpha rb))) (send n)))
  (label 24)
  (unrealized (0 1))
  (origs)
  (comment "Not closed under rules"))

(defskeleton dhstatic-state
  (vars (serial-b serial-a data) (n text) (ca a b name) (pt pval)
    (galpha base) (static-key locn) (rb rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (rb rb))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (gen-st (cat "privkey" b rb serial-b ca))
  (facts (neq b a) (neq a b))
  (rule fact-init-neq0 fact-resp-neq0 gen-st-resp-0)
  (traces
    ((load static-key (cat pt "privkey" b rb serial-b ca))
      (recv (sig (cert a galpha ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp galpha rb))) (send n)))
  (label 25)
  (parent 24)
  (unrealized (0 0) (0 1))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (galpha base) (static-key locn) (ra rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (precedes ((1 3) (0 0)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-gen ra)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation channel-test (added-strand get-cert 4)
    (ch-msg static-key (cat pt "privkey" b ra serial-b ca)) (0 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv (sig (cert a galpha ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp galpha ra))) (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca))))
  (label 26)
  (parent 25)
  (unrealized (0 1) (0 2) (1 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (galpha base) (static-key locn) (ra rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b)
  (uniq-gen ra)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)) (1 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv (sig (cert a galpha ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp galpha ra))) (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))))
  (label 27)
  (parent 26)
  (unrealized (0 1) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (galpha base) (static-key locn) (ra rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha galpha) (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha galpha) (serial serial-a) (subj a) (ca ca))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)) ((3 1) (0 1)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert a galpha ca serial-a) (privk "sig" ca)) (0 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv (sig (cert a galpha ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp galpha ra))) (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a galpha ca) (privk "sig" a)))
      (send (sig (cert a galpha ca serial-a) (privk "sig" ca)))))
  (label 28)
  (parent 27)
  (unrealized (0 2) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)) ((3 1) (0 1))
    ((4 0) (3 0)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand get-cert 1)
    (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)) (3 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))))
  (label 29)
  (parent 28)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text)
    (ca a b ca-0 name) (pt pt-0 pt-1 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (ra ra-1))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)) ((2 1) (5 1))
    ((3 1) (0 1)) ((3 1) (5 0)) ((4 0) (3 0)) ((5 2) (0 2)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra-1 serial-a ca-0)
    (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-resp-neq0 gen-st-resp-0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand init 3)
    (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))) (0 2))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))
      (recv
        (sig (cert b (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))))
  (label 30)
  (parent 29)
  (unrealized (5 0) (5 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (deflistener (exp (gen) (mul ra ra-0)))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (5 0)) ((5 1) (0 2)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-listener (exp (gen) (mul ra ra-0)))
    (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))) (0 2))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0)))))
  (label 31)
  (parent 29)
  (unrealized (5 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (a b ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra)) (static-key static-key-0)
    (ra ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self a)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)) ((2 1) (4 1))
    ((3 1) (0 1)) ((3 1) (5 1)) ((4 2) (0 2)) ((5 0) (3 0))
    ((5 3) (4 0)))
  (non-orig (privk "sig" a) (privk "sig" ca))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" a ra-0 serial-a ca)
    (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation channel-test (displaced 4 6 get-cert 4)
    (ch-msg static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca)) (5 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-0 serial-a ca))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0)))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" a ra-0 serial-a ca))))
  (label 32)
  (parent 30)
  (realized)
  (shape)
  (maps
    ((0)
      ((ca ca) (a a) (b b) (rb ra) (serial-b serial-b)
        (serial-a serial-a) (galpha (exp (gen) ra-0)) (n n)
        (static-key static-key))))
  (origs (pt-1 (5 3)) (n (4 2)) (serial-a (3 1)) (serial-b (2 1))
    (pt (1 3))))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (ca a b ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (ra ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((2 1) (1 1)) ((2 1) (5 1))
    ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0)) ((5 2) (0 2))
    ((6 3) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra-1 serial-a ca-0)
    (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation channel-test (added-strand get-cert 4)
    (ch-msg static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))
    (5 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))
      (recv
        (sig (cert b (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0)))))
    ((send (sig (cert-req a (exp (gen) ra-1) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))))
  (label 33)
  (parent 30)
  (unrealized (5 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (precedes ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (6 0)) ((5 1) (0 2))
    ((6 1) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (added-listener (cat (exp (gen) ra) ra-0))
    (exp (gen) (mul ra ra-0)) (5 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0))))
  (label 34)
  (parent 31)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra-0) ra))
  (precedes ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (6 0)) ((5 1) (0 2))
    ((6 1) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (added-listener (cat (exp (gen) ra-0) ra))
    (exp (gen) (mul ra ra-0)) (5 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra-0) ra)) (send (cat (exp (gen) ra-0) ra))))
  (label 35)
  (parent 31)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (ca a b ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (ra ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra ra-0)) ra-1))
  (precedes ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0))
    ((4 0) (7 0)) ((5 2) (0 2)) ((6 0) (7 0)) ((6 3) (5 0))
    ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra-1 serial-a ca-0)
    (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul ra ra-0)) ra-1))
    (exp (gen) (mul ra ra-0 (rec ra-1))) (5 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))
      (recv
        (sig (cert b (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0)))))
    ((send (sig (cert-req a (exp (gen) ra-1) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0)))
    ((recv (cat (exp (gen) (mul ra ra-0)) ra-1))
      (send (cat (exp (gen) (mul ra ra-0)) ra-1))))
  (label 36)
  (parent 33)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (ca a b ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (ra ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra (rec ra-1))) ra-0))
  (precedes ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0))
    ((4 0) (7 0)) ((5 2) (0 2)) ((6 0) (7 0)) ((6 3) (5 0))
    ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra-1 serial-a ca-0)
    (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul ra (rec ra-1))) ra-0))
    (exp (gen) (mul ra ra-0 (rec ra-1))) (5 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))
      (recv
        (sig (cert b (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0)))))
    ((send (sig (cert-req a (exp (gen) ra-1) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0)))
    ((recv (cat (exp (gen) (mul ra (rec ra-1))) ra-0))
      (send (cat (exp (gen) (mul ra (rec ra-1))) ra-0))))
  (label 37)
  (parent 33)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (ca a b ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (ra ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))
  (precedes ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0))
    ((4 0) (7 0)) ((5 2) (0 2)) ((6 0) (7 0)) ((6 3) (5 0))
    ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra-1 serial-a ca-0)
    (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))
    (exp (gen) (mul ra ra-0 (rec ra-1))) (5 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))
      (recv
        (sig (cert b (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0)))))
    ((send (sig (cert-req a (exp (gen) ra-1) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0)))
    ((recv (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))
      (send (cat (exp (gen) (mul ra-0 (rec ra-1))) ra))))
  (label 38)
  (parent 33)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a serial data) (n text)
    (b self ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n)
    (a self) (b b) (ca ca) (galpha (exp (gen) ra-0))
    (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a)
    (subj self) (ca ca))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 1) (0 2)) ((5 1) (4 0)) ((6 0) (3 0))
    ((6 3) (5 0)))
  (non-orig (privk "sig" self) (privk "sig" ca))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b self) (neq self b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (displaced 4 7 get-cert 4) ra-0 (6 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n self b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial-a)
          (privk "sig" ca))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0)))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)))
      (load static-key-0 (cat pt-1 ignore-0))
      (stor static-key-0 (cat pt-2 "privkey" self ra-0 serial ca))))
  (label 39)
  (parent 34)
  (unrealized (5 0) (6 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore mesg) (serial-b serial-a data) (n text) (ca a b name)
    (pt pt-0 pval) (static-key locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra)) (static-key static-key)
    (rb ra-0))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra-0))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((1 3) (6 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 0) (3 0)) ((4 0) (6 0)) ((5 1) (0 2))
    ((6 1) (5 0)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra-0 serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation nonce-test (displaced 7 1 get-cert 4) ra-0 (6 0))
  (traces
    ((load static-key (cat pt "privkey" b ra-0 serial-b ca))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra-0 serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra-0) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-0) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0))))
  (label 40)
  (parent 35)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (ca a b ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra-0)) (static-key static-key)
    (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra ra-0 (rec ra-1))))
    (static-key static-key-0) (ra ra-1))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key-0) (ra ra-1))
  (deflistener (cat (exp (gen) (mul ra ra-0)) ra-1))
  (precedes ((1 0) (2 0)) ((1 0) (7 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (5 1)) ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0))
    ((5 2) (0 2)) ((6 3) (5 0)) ((6 3) (7 0)) ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra-1 serial-a ca-0)
    (cat "privkey" b ra serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test (displaced 8 6 get-cert 4) ra-1 (7 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a)))
      (send
        (sig (cert a (exp (gen) ra-0) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca) (privk "sig" a))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0))
      (recv
        (sig (cert b (exp (gen) (mul ra ra-0 (rec ra-1))) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-0)))))
    ((send (sig (cert-req a (exp (gen) ra-1) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" a ra-1 serial-a ca-0)))
    ((recv (cat (exp (gen) (mul ra ra-0)) ra-1))
      (send (cat (exp (gen) (mul ra ra-0)) ra-1))))
  (label 41)
  (parent 36)
  (unrealized (7 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 ignore-1 mesg) (serial-b serial-a serial data)
    (n text) (b ca self ca-0 name) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (static-key static-key-0 static-key-1 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n)
    (a self) (b b) (ca ca-0) (galpha (exp (gen) ra-1))
    (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca-0))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-a)
    (subj self) (ca ca-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n)
    (a self) (b b) (ca ca) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (ra ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (defstrand get-cert 4 (ignore ignore-1) (serial serial) (self self)
    (ca ca-0) (static-key static-key-1) (ra ra-1))
  (precedes ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (4 1)) ((3 1) (0 1)) ((3 1) (5 1)) ((4 2) (0 2))
    ((5 0) (6 0)) ((5 3) (4 0)) ((6 1) (4 1)) ((7 0) (3 0))
    ((7 3) (6 0)))
  (non-orig (privk "sig" self) (privk "sig" ca-0))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra serial-b ca-0)
    (cat "privkey" self ra-0 serial-a ca))
  (facts (neq b self) (neq self b))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test (displaced 4 8 get-cert 4) ra-1 (7 0))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca-0))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n self b serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra) ca-0 serial-b) (privk "sig" ca-0)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca-0)))
    ((recv (sig (cert-req b (exp (gen) ra) ca-0) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra) ca-0 serial-b) (privk "sig" ca-0))))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))))
    ((load static-key-0 (cat pt-1 "privkey" self ra-0 serial-a ca))
      (recv
        (sig (cert b (exp (gen) (mul ra (rec ra-0) ra-1)) ca serial-b)
          (privk "sig" ca)))
      (send (enc n self b serial-a serial-b (exp (gen) (mul ra ra-1)))))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" self ra-0 serial-a ca)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1)))
    ((send
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial)
          (privk "sig" ca-0))) (load static-key-1 (cat pt-3 ignore-1))
      (stor static-key-1 (cat pt-4 "privkey" self ra-1 serial ca-0))))
  (label 42)
  (parent 37)
  (unrealized (6 0) (7 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (ca a b ca-0 name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n) (a a)
    (b b) (ca ca) (galpha (exp (gen) ra)) (static-key static-key)
    (rb ra-1))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra-1))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-a) (subj a)
    (ca ca))
  (defstrand get-cert 1 (self a) (ca ca) (ra ra))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n) (a a)
    (b b) (ca ca-0) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (ra ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self a)
    (ca ca-0) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (precedes ((1 0) (2 0)) ((1 3) (0 0)) ((1 3) (7 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((3 1) (6 1)) ((4 0) (3 0)) ((4 0) (7 0))
    ((5 2) (0 2)) ((6 0) (7 0)) ((6 3) (5 0)) ((7 1) (5 1)))
  (non-orig (privk "sig" ca) (privk "sig" a))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" a ra-0 serial-a ca-0)
    (cat "privkey" b ra-1 serial-b ca))
  (facts (neq b a) (neq a b))
  (leads-to ((1 3) (0 0)) ((6 3) (5 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation nonce-test (displaced 8 1 get-cert 4) ra-1 (7 0))
  (traces
    ((load static-key (cat pt "privkey" b ra-1 serial-b ca))
      (recv (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca)))
      (recv (enc n a b serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra-1) ca) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra-1) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra-1 serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra-1) ca) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra-1) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a)))
      (send (sig (cert a (exp (gen) ra) ca serial-a) (privk "sig" ca))))
    ((send (sig (cert-req a (exp (gen) ra) ca) (privk "sig" a))))
    ((load static-key-0 (cat pt-1 "privkey" a ra-0 serial-a ca-0))
      (recv
        (sig (cert b (exp (gen) (mul ra (rec ra-0) ra-1)) ca-0 serial-b)
          (privk "sig" ca-0)))
      (send (enc n a b serial-a serial-b (exp (gen) (mul ra ra-1)))))
    ((send (sig (cert-req a (exp (gen) ra-0) ca-0) (privk "sig" a)))
      (recv
        (sig (cert a (exp (gen) ra-0) ca-0 serial-a)
          (privk "sig" ca-0))) (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" a ra-0 serial-a ca-0)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1))))
  (label 43)
  (parent 38)
  (unrealized (7 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a data) (n text)
    (b self ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n)
    (a self) (b b) (ca ca) (galpha (exp (gen) ra-0))
    (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a)
    (subj self) (ca ca))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((3 1) (6 1)) ((4 1) (0 2)) ((5 1) (4 0))
    ((6 0) (3 0)) ((6 3) (5 0)))
  (non-orig (privk "sig" self) (privk "sig" ca))
  (uniq-orig serial-b serial-a)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b self) (neq self b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (displaced 7 3 cert 2)
    (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)) (6 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n self b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial-a)
          (privk "sig" ca))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0)))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (load static-key-0 (cat pt-1 ignore-0))
      (stor static-key-0 (cat pt-2 "privkey" self ra-0 serial-a ca))))
  (label 44)
  (parent 39)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 mesg) (serial-b serial-a serial data) (n text)
    (b self ca name) (pt pt-0 pt-1 pt-2 pval)
    (static-key static-key-0 locn) (ra ra-0 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n)
    (a self) (b b) (ca ca) (galpha (exp (gen) ra-0))
    (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial-a)
    (subj self) (ca ca))
  (deflistener (exp (gen) (mul ra ra-0)))
  (deflistener (cat (exp (gen) ra) ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (defstrand cert 2 (galpha (exp (gen) ra-0)) (serial serial)
    (subj self) (ca ca))
  (precedes ((1 0) (2 0)) ((1 0) (5 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((3 1) (0 1)) ((4 1) (0 2)) ((5 1) (4 0)) ((6 0) (3 0))
    ((6 0) (7 0)) ((6 3) (5 0)) ((7 1) (6 1)))
  (non-orig (privk "sig" self) (privk "sig" ca))
  (uniq-orig serial-b serial-a serial)
  (uniq-gen ra ra-0)
  (gen-st (cat "privkey" b ra serial-b ca))
  (facts (neq b self) (neq self b))
  (leads-to ((1 3) (0 0)))
  (rule fact-init-neq0 fact-resp-neq0 trRl_get-cert-at-2
    trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)) (6 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (recv (enc n self b serial-a serial-b (exp (gen) (mul ra ra-0))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (recv (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca)))
    ((recv (sig (cert-req b (exp (gen) ra) ca) (privk "sig" b)))
      (send (sig (cert b (exp (gen) ra) ca serial-b) (privk "sig" ca))))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial-a)
          (privk "sig" ca))))
    ((recv (exp (gen) (mul ra ra-0))) (send (exp (gen) (mul ra ra-0))))
    ((recv (cat (exp (gen) ra) ra-0)) (send (cat (exp (gen) ra) ra-0)))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)))
      (load static-key-0 (cat pt-1 ignore-0))
      (stor static-key-0 (cat pt-2 "privkey" self ra-0 serial ca)))
    ((recv (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-0) ca serial) (privk "sig" ca)))))
  (label 45)
  (parent 39)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 ignore-1 mesg) (serial-b serial-a data)
    (n text) (b ca self ca-0 name) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (static-key static-key-0 static-key-1 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n)
    (a self) (b b) (ca ca-0) (galpha (exp (gen) ra-1))
    (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca-0))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-a)
    (subj self) (ca ca-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n)
    (a self) (b b) (ca ca) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (ra ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (defstrand get-cert 4 (ignore ignore-1) (serial serial-a) (self self)
    (ca ca-0) (static-key static-key-1) (ra ra-1))
  (precedes ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (4 1)) ((3 1) (0 1)) ((3 1) (5 1)) ((3 1) (7 1))
    ((4 2) (0 2)) ((5 0) (6 0)) ((5 3) (4 0)) ((6 1) (4 1))
    ((7 0) (3 0)) ((7 3) (6 0)))
  (non-orig (privk "sig" self) (privk "sig" ca-0))
  (uniq-orig serial-b serial-a n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra serial-b ca-0)
    (cat "privkey" self ra-0 serial-a ca))
  (facts (neq b self) (neq self b))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation encryption-test (displaced 8 3 cert 2)
    (sig (cert self (exp (gen) ra-1) ca-0 serial) (privk "sig" ca-0))
    (7 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca-0))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n self b serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra) ca-0 serial-b) (privk "sig" ca-0)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca-0)))
    ((recv (sig (cert-req b (exp (gen) ra) ca-0) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra) ca-0 serial-b) (privk "sig" ca-0))))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))))
    ((load static-key-0 (cat pt-1 "privkey" self ra-0 serial-a ca))
      (recv
        (sig (cert b (exp (gen) (mul ra (rec ra-0) ra-1)) ca serial-b)
          (privk "sig" ca)))
      (send (enc n self b serial-a serial-b (exp (gen) (mul ra ra-1)))))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" self ra-0 serial-a ca)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1)))
    ((send
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))) (load static-key-1 (cat pt-3 ignore-1))
      (stor static-key-1 (cat pt-4 "privkey" self ra-1 serial-a ca-0))))
  (label 46)
  (parent 42)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhstatic-state
  (vars (ignore ignore-0 ignore-1 mesg) (serial-b serial-a serial data)
    (n text) (b ca self ca-0 name) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (static-key static-key-0 static-key-1 locn) (ra ra-0 ra-1 rndx))
  (defstrand resp 4 (serial-b serial-b) (serial-a serial-a) (n n)
    (a self) (b b) (ca ca-0) (galpha (exp (gen) ra-1))
    (static-key static-key) (rb ra))
  (defstrand get-cert 4 (ignore ignore) (serial serial-b) (self b)
    (ca ca-0) (static-key static-key) (ra ra))
  (defstrand cert 2 (galpha (exp (gen) ra)) (serial serial-b) (subj b)
    (ca ca-0))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial-a)
    (subj self) (ca ca-0))
  (defstrand init 3 (serial-a serial-a) (serial-b serial-b) (n n)
    (a self) (b b) (ca ca) (galpha (exp (gen) (mul ra (rec ra-0) ra-1)))
    (static-key static-key-0) (ra ra-0))
  (defstrand get-cert 4 (ignore ignore-0) (serial serial-a) (self self)
    (ca ca) (static-key static-key-0) (ra ra-0))
  (deflistener (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
  (defstrand get-cert 4 (ignore ignore-1) (serial serial) (self self)
    (ca ca-0) (static-key static-key-1) (ra ra-1))
  (defstrand cert 2 (galpha (exp (gen) ra-1)) (serial serial)
    (subj self) (ca ca-0))
  (precedes ((1 0) (2 0)) ((1 0) (6 0)) ((1 3) (0 0)) ((2 1) (1 1))
    ((2 1) (4 1)) ((3 1) (0 1)) ((3 1) (5 1)) ((4 2) (0 2))
    ((5 0) (6 0)) ((5 3) (4 0)) ((6 1) (4 1)) ((7 0) (3 0))
    ((7 0) (8 0)) ((7 3) (6 0)) ((8 1) (7 1)))
  (non-orig (privk "sig" self) (privk "sig" ca-0))
  (uniq-orig serial-b serial-a serial n)
  (uniq-gen ra ra-0 ra-1)
  (gen-st (cat "privkey" b ra serial-b ca-0)
    (cat "privkey" self ra-0 serial-a ca))
  (facts (neq b self) (neq self b))
  (leads-to ((1 3) (0 0)) ((5 3) (4 0)))
  (rule fact-resp-neq0 trRl_get-cert-at-2 trRl_get-cert-at-3)
  (operation encryption-test (added-strand cert 2)
    (sig (cert self (exp (gen) ra-1) ca-0 serial) (privk "sig" ca-0))
    (7 1))
  (traces
    ((load static-key (cat pt "privkey" b ra serial-b ca-0))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0)))
      (recv (enc n self b serial-a serial-b (exp (gen) (mul ra ra-1))))
      (send n))
    ((send (sig (cert-req b (exp (gen) ra) ca-0) (privk "sig" b)))
      (recv
        (sig (cert b (exp (gen) ra) ca-0 serial-b) (privk "sig" ca-0)))
      (load static-key (cat pt-0 ignore))
      (stor static-key (cat pt "privkey" b ra serial-b ca-0)))
    ((recv (sig (cert-req b (exp (gen) ra) ca-0) (privk "sig" b)))
      (send
        (sig (cert b (exp (gen) ra) ca-0 serial-b) (privk "sig" ca-0))))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial-a)
          (privk "sig" ca-0))))
    ((load static-key-0 (cat pt-1 "privkey" self ra-0 serial-a ca))
      (recv
        (sig (cert b (exp (gen) (mul ra (rec ra-0) ra-1)) ca serial-b)
          (privk "sig" ca)))
      (send (enc n self b serial-a serial-b (exp (gen) (mul ra ra-1)))))
    ((send (sig (cert-req self (exp (gen) ra-0) ca) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-0) ca serial-a) (privk "sig" ca)))
      (load static-key-0 (cat pt-2 ignore-0))
      (stor static-key-0 (cat pt-1 "privkey" self ra-0 serial-a ca)))
    ((recv (cat (exp (gen) (mul ra (rec ra-0))) ra-1))
      (send (cat (exp (gen) (mul ra (rec ra-0))) ra-1)))
    ((send
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (recv
        (sig (cert self (exp (gen) ra-1) ca-0 serial)
          (privk "sig" ca-0))) (load static-key-1 (cat pt-3 ignore-1))
      (stor static-key-1 (cat pt-4 "privkey" self ra-1 serial ca-0)))
    ((recv
       (sig (cert-req self (exp (gen) ra-1) ca-0) (privk "sig" self)))
      (send
        (sig (cert self (exp (gen) ra-1) ca-0 serial)
          (privk "sig" ca-0)))))
  (label 47)
  (parent 42)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")