(herald "cb" (bound 12))

(comment "CPSA 4.1.1")
(comment "All input read from cb.scm")
(comment "Strand count bounded at 12")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey) (target name))
    (trace (recv (cat er target))
      (send (cat er (hash er (hash "mac" target proc-sec))))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey) (target name))
    (trace (recv (cat er (hash er (hash "mac" target proc-sec))))
      (send (cat er (enc "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole fulcrum
    (vars (m er mesg) (n text) (as f name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)
      (send (enc "fm" er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc "certificate" "fulcrum" f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (defrule as-confirms-epid-ok
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid))
        (and (fact man-made-epid k-epid) (non k-epid)))))
  (defrule epid-quote-processor-ok
    (forall ((z-iq strd) (proc-sec skey) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (p "epid-quote" "proc-sec" z-iq proc-sec)
          (fact man-made-epid k-epid)) (non proc-sec))))
  (defrule local-quote-attests-enclave
    (forall ((z-lq strd) (eid ch rest mesg) (k akey) (proc-sec skey))
      (implies
        (and (p "local-quote" z-lq 2)
          (p "local-quote" "er" z-lq (cat eid ch k rest))
          (p "local-quote" "proc-sec" z-lq proc-sec) (non proc-sec))
        (fact enclave-w-code-and-key eid ch k proc-sec))))
  (defrule cert-rule-fulcrum
    (forall ((z-ca strd) (f name) (k akey))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "k" z-ca k)
          (p "certifier" "f" z-ca f) (= k (pubk f))) (non (invk k)))))
  (defrule cert-rule-attest-server
    (forall ((z-fm strd) (as name) (n text))
      (implies
        (and (p "fulcrum" z-fm 2) (p "fulcrum" "as" z-fm as)
          (p "fulcrum" "n" z-fm n)) (and (non (privk as)) (uniq n)))))
  (defrule local-att-crowbar
    (forall ((eid chc mesg) (cbkey akey) (proc-sec skey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc)) (non (invk cbkey)))))
  (defrule crowbar-immobile
    (forall
      ((z strd) (eid chc mesg) (proc-sec proc-sec-0 skey) (cbkey akey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)
          (p "crowbar" "proc-sec" z proc-sec-0))
        (= proc-sec proc-sec-0))))
  (defrule neq-def
    (forall ((m mesg)) (implies (fact neq m m) (false)))))

(defskeleton cb-over-sgx
  (vars (f ca name))
  (deflistener (enc "certificate" "fulcrum" f (pubk f) (privk ca)))
  (non-orig (privk ca))
  (traces
    ((recv (enc "certificate" "fulcrum" f (pubk f) (privk ca)))
      (send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 0)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (f ca name))
  (deflistener (enc "certificate" "fulcrum" f (pubk f) (privk ca)))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (precedes ((1 0) (0 0)))
  (non-orig (privk f) (privk ca))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc "certificate" "fulcrum" f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv (enc "certificate" "fulcrum" f (pubk f) (privk ca)))
      (send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((f f) (ca ca))))
  (origs))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey) (target name))
    (trace (recv (cat er target))
      (send (cat er (hash er (hash "mac" target proc-sec))))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey) (target name))
    (trace (recv (cat er (hash er (hash "mac" target proc-sec))))
      (send (cat er (enc "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole fulcrum
    (vars (m er mesg) (n text) (as f name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)
      (send (enc "fm" er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc "certificate" "fulcrum" f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (defrule as-confirms-epid-ok
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid))
        (and (fact man-made-epid k-epid) (non k-epid)))))
  (defrule epid-quote-processor-ok
    (forall ((z-iq strd) (proc-sec skey) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (p "epid-quote" "proc-sec" z-iq proc-sec)
          (fact man-made-epid k-epid)) (non proc-sec))))
  (defrule local-quote-attests-enclave
    (forall ((z-lq strd) (eid ch rest mesg) (k akey) (proc-sec skey))
      (implies
        (and (p "local-quote" z-lq 2)
          (p "local-quote" "er" z-lq (cat eid ch k rest))
          (p "local-quote" "proc-sec" z-lq proc-sec) (non proc-sec))
        (fact enclave-w-code-and-key eid ch k proc-sec))))
  (defrule cert-rule-fulcrum
    (forall ((z-ca strd) (f name) (k akey))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "k" z-ca k)
          (p "certifier" "f" z-ca f) (= k (pubk f))) (non (invk k)))))
  (defrule cert-rule-attest-server
    (forall ((z-fm strd) (as name) (n text))
      (implies
        (and (p "fulcrum" z-fm 2) (p "fulcrum" "as" z-fm as)
          (p "fulcrum" "n" z-fm n)) (and (non (privk as)) (uniq n)))))
  (defrule local-att-crowbar
    (forall ((eid chc mesg) (cbkey akey) (proc-sec skey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc)) (non (invk cbkey)))))
  (defrule crowbar-immobile
    (forall
      ((z strd) (eid chc mesg) (proc-sec proc-sec-0 skey) (cbkey akey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)
          (p "crowbar" "proc-sec" z proc-sec-0))
        (= proc-sec proc-sec-0))))
  (defrule neq-def
    (forall ((m mesg)) (implies (fact neq m m) (false)))))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (f ca name) (k akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid ch k rest (privk f))))
  (non-orig (privk ca))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid ch k rest (privk f))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid ch k rest (privk f))))))
  (label 2)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (f ca name) (k akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (precedes ((1 0) (0 0)))
  (non-orig (privk f) (privk ca))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc "certificate" "fulcrum" f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid ch k rest (privk f))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid ch k rest (privk f)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 3)
  (parent 2)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eid ch rest m mesg) (n text) (f ca as name) (k akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m m) (er (cat eid ch k rest)) (n n) (as as)
    (f f))
  (precedes ((1 0) (0 0)) ((2 3) (0 0)))
  (non-orig (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc "fm" eid ch k rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid ch k rest (privk f))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid ch k rest (privk f)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) m))
      (send (enc n (cat eid ch k rest) m (pubk as))) (recv n)
      (send (enc "fm" eid ch k rest (privk f)))))
  (label 4)
  (parent 3)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (n text) (f ca as name) (k k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid ch k rest k-epid))
    (er (cat eid ch k rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid ch k rest)) (n n) (as as)
    (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2)))
  (non-orig k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid))
  (rule as-confirms-epid-ok)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
      (pubk as)))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid ch k rest (privk f))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid ch k rest (privk f)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
          (pubk as))) (recv n)
      (send (enc "fm" eid ch k rest (privk f))))
    ((recv
       (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
         (pubk as))) (send n)))
  (label 5)
  (parent 4)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (k k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid ch k rest k-epid))
    (er (cat eid ch k rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid ch k rest)) (n n) (as as)
    (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eid ch k rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc "rq" eid ch k rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid ch k rest (privk f))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid ch k rest (privk f)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
          (pubk as))) (recv n)
      (send (enc "fm" eid ch k rest (privk f))))
    ((recv
       (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid ch k rest)
         (hash (cat eid ch k rest) (hash "mac" target proc-sec))))
      (send (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))))
  (label 6)
  (parent 5)
  (unrealized (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (k k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid ch k rest k-epid))
    (er (cat eid ch k rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid ch k rest)) (n n) (as as)
    (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eid ch k rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid ch k rest)) (target target)
    (proc-sec proc-sec))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eid ch k proc-sec)
    (man-made-epid k-epid))
  (rule local-quote-attests-enclave)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eid ch k rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid ch k rest (privk f))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid ch k rest (privk f)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
          (pubk as))) (recv n)
      (send (enc "fm" eid ch k rest (privk f))))
    ((recv
       (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid ch k rest)
         (hash (cat eid ch k rest) (hash "mac" target proc-sec))))
      (send (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid))))
    ((recv (cat (cat eid ch k rest) target))
      (send
        (cat (cat eid ch k rest)
          (hash (cat eid ch k rest) (hash "mac" target proc-sec))))))
  (label 7)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0) ((f f) (ca ca) (k k) (eid eid) (ch ch) (rest rest))))
  (origs (n (2 1))))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (k k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid ch k rest k-epid))
    (er (cat eid ch k rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid ch k rest)) (n n) (as as)
    (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eid ch k rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (deflistener (cat (cat eid ch k rest) (hash "mac" target proc-sec)))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid))
  (operation encryption-test
    (added-listener
      (cat (cat eid ch k rest) (hash "mac" target proc-sec)))
    (hash (cat eid ch k rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid ch k rest (privk f))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid ch k rest (privk f)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
          (pubk as))) (recv n)
      (send (enc "fm" eid ch k rest (privk f))))
    ((recv
       (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid ch k rest)
         (hash (cat eid ch k rest) (hash "mac" target proc-sec))))
      (send (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid))))
    ((recv (cat (cat eid ch k rest) (hash "mac" target proc-sec)))
      (send (cat (cat eid ch k rest) (hash "mac" target proc-sec)))))
  (label 8)
  (parent 6)
  (unrealized (5 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey) (target name))
    (trace (recv (cat er target))
      (send (cat er (hash er (hash "mac" target proc-sec))))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey) (target name))
    (trace (recv (cat er (hash er (hash "mac" target proc-sec))))
      (send (cat er (enc "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole fulcrum
    (vars (m er mesg) (n text) (as f name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)
      (send (enc "fm" er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc "certificate" "fulcrum" f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (defrule as-confirms-epid-ok
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid))
        (and (fact man-made-epid k-epid) (non k-epid)))))
  (defrule epid-quote-processor-ok
    (forall ((z-iq strd) (proc-sec skey) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (p "epid-quote" "proc-sec" z-iq proc-sec)
          (fact man-made-epid k-epid)) (non proc-sec))))
  (defrule local-quote-attests-enclave
    (forall ((z-lq strd) (eid ch rest mesg) (k akey) (proc-sec skey))
      (implies
        (and (p "local-quote" z-lq 2)
          (p "local-quote" "er" z-lq (cat eid ch k rest))
          (p "local-quote" "proc-sec" z-lq proc-sec) (non proc-sec))
        (fact enclave-w-code-and-key eid ch k proc-sec))))
  (defrule cert-rule-fulcrum
    (forall ((z-ca strd) (f name) (k akey))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "k" z-ca k)
          (p "certifier" "f" z-ca f) (= k (pubk f))) (non (invk k)))))
  (defrule cert-rule-attest-server
    (forall ((z-fm strd) (as name) (n text))
      (implies
        (and (p "fulcrum" z-fm 2) (p "fulcrum" "as" z-fm as)
          (p "fulcrum" "n" z-fm n)) (and (non (privk as)) (uniq n)))))
  (defrule local-att-crowbar
    (forall ((eid chc mesg) (cbkey akey) (proc-sec skey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc)) (non (invk cbkey)))))
  (defrule crowbar-immobile
    (forall
      ((z strd) (eid chc mesg) (proc-sec proc-sec-0 skey) (cbkey akey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)
          (p "crowbar" "proc-sec" z proc-sec-0))
        (= proc-sec proc-sec-0))))
  (defrule neq-def
    (forall ((m mesg)) (implies (fact neq m m) (false)))))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (non-orig (privk ca))
  (facts (known-crowbar-code chc))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey))))))
  (label 9)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (precedes ((1 0) (0 0)))
  (non-orig (privk f) (privk ca))
  (facts (known-crowbar-code chc))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc "certificate" "fulcrum" f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 10)
  (parent 9)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest m mesg) (n text) (f ca as name) (cbkey akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m m) (er (cat eid chc cbkey rest)) (n n) (as as)
    (f f))
  (precedes ((1 0) (0 0)) ((2 3) (0 0)))
  (non-orig (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (known-crowbar-code chc))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc "fm" eid chc cbkey rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eid chc cbkey rest) m))
      (send (enc n (cat eid chc cbkey rest) m (pubk as))) (recv n)
      (send (enc "fm" eid chc cbkey rest (privk f)))))
  (label 11)
  (parent 10)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as name)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid chc cbkey rest k-epid))
    (er (cat eid chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid chc cbkey rest)) (n n) (as as)
    (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2)))
  (non-orig k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc))
  (rule as-confirms-epid-ok)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eid chc cbkey rest) (enc "rq" eid chc cbkey rest k-epid)
      (pubk as)))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (send n)))
  (label 12)
  (parent 11)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid chc cbkey rest k-epid))
    (er (cat eid chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid chc cbkey rest)) (n n) (as as)
    (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eid chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc "rq" eid chc cbkey rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid)))))
  (label 13)
  (parent 12)
  (unrealized (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid chc cbkey rest k-epid))
    (er (cat eid chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid chc cbkey rest)) (n n) (as as)
    (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eid chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid chc cbkey rest)) (target target)
    (proc-sec proc-sec))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk f) (privk ca)
    (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eid chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc))
  (rule local-att-crowbar)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eid chc cbkey rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid))))
    ((recv (cat (cat eid chc cbkey rest) target))
      (send
        (cat (cat eid chc cbkey rest)
          (hash (cat eid chc cbkey rest)
            (hash "mac" target proc-sec))))))
  (label 14)
  (parent 13)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid chc cbkey rest k-epid))
    (er (cat eid chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid chc cbkey rest)) (n n) (as as)
    (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eid chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (deflistener
    (cat (cat eid chc cbkey rest) (hash "mac" target proc-sec)))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc))
  (operation encryption-test
    (added-listener
      (cat (cat eid chc cbkey rest) (hash "mac" target proc-sec)))
    (hash (cat eid chc cbkey rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid))))
    ((recv (cat (cat eid chc cbkey rest) (hash "mac" target proc-sec)))
      (send
        (cat (cat eid chc cbkey rest) (hash "mac" target proc-sec)))))
  (label 15)
  (parent 13)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eid chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eid chc cbkey rest k-epid))
    (er (cat eid chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eid chc cbkey rest)) (n n) (as as)
    (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eid chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid chc cbkey rest)) (target target)
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er er) (proc-sec proc-sec) (cbkey cbkey))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (0 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk f) (privk ca)
    (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eid chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc "cb" er (invk cbkey)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eid chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eid chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest)
         (enc "rq" eid chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eid chc cbkey rest)
          (enc "rq" eid chc cbkey rest k-epid))))
    ((recv (cat (cat eid chc cbkey rest) target))
      (send
        (cat (cat eid chc cbkey rest)
          (hash (cat eid chc cbkey rest)
            (hash "mac" target proc-sec)))))
    ((recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (label 16)
  (parent 14)
  (unrealized (6 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey) (target name))
    (trace (recv (cat er target))
      (send (cat er (hash er (hash "mac" target proc-sec))))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey) (target name))
    (trace (recv (cat er (hash er (hash "mac" target proc-sec))))
      (send (cat er (enc "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole fulcrum
    (vars (m er mesg) (n text) (as f name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)
      (send (enc "fm" er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc "certificate" "fulcrum" f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (defrule as-confirms-epid-ok
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid))
        (and (fact man-made-epid k-epid) (non k-epid)))))
  (defrule epid-quote-processor-ok
    (forall ((z-iq strd) (proc-sec skey) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (p "epid-quote" "proc-sec" z-iq proc-sec)
          (fact man-made-epid k-epid)) (non proc-sec))))
  (defrule local-quote-attests-enclave
    (forall ((z-lq strd) (eid ch rest mesg) (k akey) (proc-sec skey))
      (implies
        (and (p "local-quote" z-lq 2)
          (p "local-quote" "er" z-lq (cat eid ch k rest))
          (p "local-quote" "proc-sec" z-lq proc-sec) (non proc-sec))
        (fact enclave-w-code-and-key eid ch k proc-sec))))
  (defrule cert-rule-fulcrum
    (forall ((z-ca strd) (f name) (k akey))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "k" z-ca k)
          (p "certifier" "f" z-ca f) (= k (pubk f))) (non (invk k)))))
  (defrule cert-rule-attest-server
    (forall ((z-fm strd) (as name) (n text))
      (implies
        (and (p "fulcrum" z-fm 2) (p "fulcrum" "as" z-fm as)
          (p "fulcrum" "n" z-fm n)) (and (non (privk as)) (uniq n)))))
  (defrule local-att-crowbar
    (forall ((eid chc mesg) (cbkey akey) (proc-sec skey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc)) (non (invk cbkey)))))
  (defrule crowbar-immobile
    (forall
      ((z strd) (eid chc mesg) (proc-sec proc-sec-0 skey) (cbkey akey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)
          (p "crowbar" "proc-sec" z proc-sec-0))
        (= proc-sec proc-sec-0))))
  (defrule neq-def
    (forall ((m mesg)) (implies (fact neq m m) (false)))))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (non-orig (privk ca))
  (facts (known-crowbar-code chc) (neq er (cat eidc chc cbkey rest)))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey))))))
  (label 17)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (precedes ((1 0) (0 0)))
  (non-orig (privk f) (privk ca))
  (facts (known-crowbar-code chc) (neq er (cat eidc chc cbkey rest)))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc "certificate" "fulcrum" f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 18)
  (parent 17)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest m mesg) (n text) (f ca as name) (cbkey akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m m) (er (cat eidc chc cbkey rest)) (n n)
    (as as) (f f))
  (precedes ((1 0) (0 0)) ((2 3) (0 0)))
  (non-orig (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (known-crowbar-code chc) (neq er (cat eidc chc cbkey rest)))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc "fm" eidc chc cbkey rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eidc chc cbkey rest) m))
      (send (enc n (cat eidc chc cbkey rest) m (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f)))))
  (label 19)
  (parent 18)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as name)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2)))
  (non-orig k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (rule as-confirms-epid-ok)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eidc chc cbkey rest)
      (enc "rq" eidc chc cbkey rest k-epid) (pubk as)))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n)))
  (label 20)
  (parent 19)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc "rq" eidc chc cbkey rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid)))))
  (label 21)
  (parent 20)
  (unrealized (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (target target) (proc-sec proc-sec))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk f) (privk ca)
    (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (rule local-att-crowbar)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid))))
    ((recv (cat (cat eidc chc cbkey rest) target))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest)
            (hash "mac" target proc-sec))))))
  (label 22)
  (parent 21)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (deflistener
    (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (operation encryption-test
    (added-listener
      (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))
    (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid))))
    ((recv (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))))
  (label 23)
  (parent 21)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as target name)
    (proc-sec skey) (cbkey k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (target target) (proc-sec proc-sec))
  (defstrand crowbar 2 (er er) (proc-sec proc-sec) (cbkey cbkey))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (0 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk f) (privk ca)
    (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc "cb" er (invk cbkey)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" er (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" er (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid))))
    ((recv (cat (cat eidc chc cbkey rest) target))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest)
            (hash "mac" target proc-sec)))))
    ((recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (label 24)
  (parent 22)
  (unrealized (6 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey) (target name))
    (trace (recv (cat er target))
      (send (cat er (hash er (hash "mac" target proc-sec))))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey) (target name))
    (trace (recv (cat er (hash er (hash "mac" target proc-sec))))
      (send (cat er (enc "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole fulcrum
    (vars (m er mesg) (n text) (as f name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)
      (send (enc "fm" er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc "certificate" "fulcrum" f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (defrule as-confirms-epid-ok
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid))
        (and (fact man-made-epid k-epid) (non k-epid)))))
  (defrule epid-quote-processor-ok
    (forall ((z-iq strd) (proc-sec skey) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (p "epid-quote" "proc-sec" z-iq proc-sec)
          (fact man-made-epid k-epid)) (non proc-sec))))
  (defrule local-quote-attests-enclave
    (forall ((z-lq strd) (eid ch rest mesg) (k akey) (proc-sec skey))
      (implies
        (and (p "local-quote" z-lq 2)
          (p "local-quote" "er" z-lq (cat eid ch k rest))
          (p "local-quote" "proc-sec" z-lq proc-sec) (non proc-sec))
        (fact enclave-w-code-and-key eid ch k proc-sec))))
  (defrule cert-rule-fulcrum
    (forall ((z-ca strd) (f name) (k akey))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "k" z-ca k)
          (p "certifier" "f" z-ca f) (= k (pubk f))) (non (invk k)))))
  (defrule cert-rule-attest-server
    (forall ((z-fm strd) (as name) (n text))
      (implies
        (and (p "fulcrum" z-fm 2) (p "fulcrum" "as" z-fm as)
          (p "fulcrum" "n" z-fm n)) (and (non (privk as)) (uniq n)))))
  (defrule local-att-crowbar
    (forall ((eid chc mesg) (cbkey akey) (proc-sec skey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc)) (non (invk cbkey)))))
  (defrule crowbar-immobile
    (forall
      ((z strd) (eid chc mesg) (proc-sec proc-sec-0 skey) (cbkey akey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)
          (p "crowbar" "proc-sec" z proc-sec-0))
        (= proc-sec proc-sec-0))))
  (defrule neq-def
    (forall ((m mesg)) (implies (fact neq m m) (false)))))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (f ca name) (cbkey ka akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (non-orig (privk ca))
  (facts (known-crowbar-code chc) (neq chc cha))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey))))))
  (label 25)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (f ca name) (cbkey ka akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (precedes ((1 0) (0 0)))
  (non-orig (privk f) (privk ca))
  (facts (known-crowbar-code chc) (neq chc cha))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc "certificate" "fulcrum" f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 26)
  (parent 25)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta m mesg) (n text) (f ca as name)
    (cbkey ka akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m m) (er (cat eidc chc cbkey rest)) (n n)
    (as as) (f f))
  (precedes ((1 0) (0 0)) ((2 3) (0 0)))
  (non-orig (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (known-crowbar-code chc) (neq chc cha))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc "fm" eidc chc cbkey rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eidc chc cbkey rest) m))
      (send (enc n (cat eidc chc cbkey rest) m (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f)))))
  (label 27)
  (parent 26)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (n text) (f ca as name)
    (cbkey ka k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2)))
  (non-orig k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc) (neq chc cha))
  (rule as-confirms-epid-ok)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eidc chc cbkey rest)
      (enc "rq" eidc chc cbkey rest k-epid) (pubk as)))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n)))
  (label 28)
  (parent 27)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (n text)
    (f ca as target name) (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc) (neq chc cha))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc "rq" eidc chc cbkey rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid)))))
  (label 29)
  (parent 28)
  (unrealized (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (n text)
    (f ca as target name) (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (target target) (proc-sec proc-sec))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk f) (privk ca)
    (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc) (neq chc cha))
  (rule local-att-crowbar)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid))))
    ((recv (cat (cat eidc chc cbkey rest) target))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest)
            (hash "mac" target proc-sec))))))
  (label 30)
  (parent 29)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (n text)
    (f ca as target name) (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (deflistener
    (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig proc-sec k-epid (privk f) (privk ca) (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid) (known-crowbar-code chc) (neq chc cha))
  (operation encryption-test
    (added-listener
      (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))
    (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec)) (4 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid))))
    ((recv (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest) (hash "mac" target proc-sec)))))
  (label 31)
  (parent 29)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (n text)
    (f ca as target name) (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
      (enc "fm" eidc chc cbkey rest (privk f))
      (enc "cb" eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest k-epid))
    (er (cat eidc chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest)) (n n)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest)) (target target)
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (target target) (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eida cha ka resta)) (proc-sec proc-sec)
    (cbkey cbkey))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (0 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk f) (privk ca)
    (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc) (neq chc cha))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc "cb" eida cha ka resta (invk cbkey)) (0 0))
  (traces
    ((recv
       (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
         (enc "fm" eidc chc cbkey rest (privk f))
         (enc "cb" eida cha ka resta (invk cbkey))))
      (send
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest (privk f))
          (enc "cb" eida cha ka resta (invk cbkey)))))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc "fm" eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest)
         (enc "rq" eidc chc cbkey rest k-epid) (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) (hash "mac" target proc-sec))))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc "rq" eidc chc cbkey rest k-epid))))
    ((recv (cat (cat eidc chc cbkey rest) target))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest)
            (hash "mac" target proc-sec)))))
    ((recv
       (cat (cat eida cha ka resta)
         (hash (cat eida cha ka resta) proc-sec)))
      (send (enc "cb" eida cha ka resta (invk cbkey)))))
  (label 32)
  (parent 30)
  (unrealized (6 0))
  (comment "empty cohort"))

(comment "Nothing left to do")