(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))
    (trace (recv er) (send (cat er (hash er proc-sec)))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (cat er (enc er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc 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 er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc 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 as-confirms-non-std
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (defrule as-key-std
    (forall ((z-as strd) (as name))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "as" z-as as))
        (fact is-std-sigkey (privk as)))))
  (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 epid-quote-non-std
    (forall ((z-iq strd) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (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-non-epid
    (forall ((z-ca strd) (ca name))
      (implies (and (p "certifier" z-ca 1) (p "certifier" "ca" z-ca ca))
        (fact is-std-sigkey (privk ca)))))
  (defrule fulcrum-non-epid
    (forall ((z-fm strd) (f name))
      (implies (and (p "fulcrum" z-fm 2) (p "fulcrum" "f" z-fm f))
        (fact is-std-sigkey (privk f)))))
  (defrule trust-anchor-inverse-is-non
    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k)))))
  (defrule fulcrum-doesnt-use-trust-anchor
    (forall ((z strd) (f name))
      (implies
        (and (fact trust-anchor (pubk f)) (p "fulcrum" z 2)
          (p "fulcrum" "f" z f)) (false))))
  (defrule crowbar-doesnt-use-trust-anchor
    (forall ((z strd) (cbkey akey))
      (implies
        (and (fact trust-anchor cbkey) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)) (false))))
  (defrule crowbar-doesnt-use-fulcrum-key
    (forall ((z z-ca strd) (f name))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "f" z-ca f)
          (p "crowbar" z 2) (p "crowbar" "cbkey" z (pubk f))) (false))))
  (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-std-sig
    (forall ((z strd) (cbkey akey))
      (implies (and (p "crowbar" z 2) (p "crowbar" "cbkey" z cbkey))
        (fact is-std-sigkey (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 crowbar-code-never-ca
    (forall ((z-ca strd) (eid chc mesg) (proc-sec skey) (ca name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk ca) proc-sec)
          (fact known-crowbar-code chc) (p "certifier" z-ca 1)
          (p "certifier" "ca" z-ca ca)) (false))))
  (defrule crowbar-code-never-fulcrum
    (forall ((z-f strd) (eid chc mesg) (proc-sec skey) (f name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk f) proc-sec)
          (fact known-crowbar-code chc) (p "fulcrum" z-f 4)
          (p "fulcrum" "f" z-f f)) (false))))
  (defrule neq-def (forall ((m mesg)) (implies (fact neq m m) (false))))
  (defrule sig-keys-inverse-std
    (forall ((k akey))
      (implies (fact is-std-sigkey k) (fact is-std-sigkey (invk k))))))

(defskeleton cb-over-sgx
  (vars (f ca name))
  (deflistener (enc f (pubk f) (privk ca)))
  (facts (trust-anchor (pubk ca)) (is-std-sigkey (privk ca)))
  (traces
    ((recv (enc f (pubk f) (privk ca)))
      (send (enc f (pubk f) (privk ca)))))
  (label 0)
  (unrealized)
  (origs)
  (comment "Not in theory"))

(defskeleton cb-over-sgx
  (vars (f ca name))
  (deflistener (enc f (pubk f) (privk ca)))
  (non-orig (privk ca))
  (facts (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)))
  (rule sig-keys-inverse-std)
  (traces
    ((recv (enc f (pubk f) (privk ca)))
      (send (enc f (pubk f) (privk ca)))))
  (label 1)
  (parent 0)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (f ca name))
  (deflistener (enc 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))
  (facts (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv (enc f (pubk f) (privk ca)))
      (send (enc f (pubk f) (privk ca))))
    ((send (enc f (pubk f) (privk ca)))))
  (label 2)
  (parent 1)
  (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))
    (trace (recv er) (send (cat er (hash er proc-sec)))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (cat er (enc er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc 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 er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc 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 as-confirms-non-std
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (defrule as-key-std
    (forall ((z-as strd) (as name))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "as" z-as as))
        (fact is-std-sigkey (privk as)))))
  (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 epid-quote-non-std
    (forall ((z-iq strd) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (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-non-epid
    (forall ((z-ca strd) (ca name))
      (implies (and (p "certifier" z-ca 1) (p "certifier" "ca" z-ca ca))
        (fact is-std-sigkey (privk ca)))))
  (defrule fulcrum-non-epid
    (forall ((z-fm strd) (f name))
      (implies (and (p "fulcrum" z-fm 2) (p "fulcrum" "f" z-fm f))
        (fact is-std-sigkey (privk f)))))
  (defrule trust-anchor-inverse-is-non
    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k)))))
  (defrule fulcrum-doesnt-use-trust-anchor
    (forall ((z strd) (f name))
      (implies
        (and (fact trust-anchor (pubk f)) (p "fulcrum" z 2)
          (p "fulcrum" "f" z f)) (false))))
  (defrule crowbar-doesnt-use-trust-anchor
    (forall ((z strd) (cbkey akey))
      (implies
        (and (fact trust-anchor cbkey) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)) (false))))
  (defrule crowbar-doesnt-use-fulcrum-key
    (forall ((z z-ca strd) (f name))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "f" z-ca f)
          (p "crowbar" z 2) (p "crowbar" "cbkey" z (pubk f))) (false))))
  (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-std-sig
    (forall ((z strd) (cbkey akey))
      (implies (and (p "crowbar" z 2) (p "crowbar" "cbkey" z cbkey))
        (fact is-std-sigkey (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 crowbar-code-never-ca
    (forall ((z-ca strd) (eid chc mesg) (proc-sec skey) (ca name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk ca) proc-sec)
          (fact known-crowbar-code chc) (p "certifier" z-ca 1)
          (p "certifier" "ca" z-ca ca)) (false))))
  (defrule crowbar-code-never-fulcrum
    (forall ((z-f strd) (eid chc mesg) (proc-sec skey) (f name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk f) proc-sec)
          (fact known-crowbar-code chc) (p "fulcrum" z-f 4)
          (p "fulcrum" "f" z-f f)) (false))))
  (defrule neq-def (forall ((m mesg)) (implies (fact neq m m) (false))))
  (defrule sig-keys-inverse-std
    (forall ((k akey))
      (implies (fact is-std-sigkey k) (fact is-std-sigkey (invk k))))))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (f ca name) (k akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
  (facts (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid ch k rest (privk f))))))
  (label 3)
  (unrealized)
  (origs)
  (comment "Not in theory"))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (f ca name) (k akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
  (non-orig (privk ca))
  (facts (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)))
  (rule sig-keys-inverse-std)
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid ch k rest (privk f))))))
  (label 4)
  (parent 3)
  (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 f (pubk f) (privk ca)) (enc 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))
  (facts (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid ch k rest (privk f)))))
    ((send (enc f (pubk f) (privk ca)))))
  (label 5)
  (parent 4)
  (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 f (pubk f) (privk ca)) (enc 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)
  (facts (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc eid ch k rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid ch k rest (privk f)))))
    ((send (enc 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 eid ch k rest (privk f)))))
  (label 6)
  (parent 5)
  (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 f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f)))
  (rule sig-keys-inverse-std)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eid ch k rest) (enc eid ch k rest k-epid) (pubk as)))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid ch k rest (privk f)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) (enc eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc eid ch k rest k-epid)
          (pubk as))) (recv n) (send (enc eid ch k rest (privk f))))
    ((recv
       (enc n (cat eid ch k rest) (enc eid ch k rest k-epid) (pubk as)))
      (send n)))
  (label 7)
  (parent 6)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (n text) (f ca as name) (proc-sec skey)
    (k k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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)) (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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f)))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc eid ch k rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid ch k rest (privk f)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) (enc eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc eid ch k rest k-epid)
          (pubk as))) (recv n) (send (enc eid ch k rest (privk f))))
    ((recv
       (enc n (cat eid ch k rest) (enc eid ch k rest k-epid) (pubk as)))
      (send n))
    ((recv
       (cat (cat eid ch k rest) (hash (cat eid ch k rest) proc-sec)))
      (send (cat (cat eid ch k rest) (enc eid ch k rest k-epid)))))
  (label 8)
  (parent 7)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (ch rest mesg) (n n-0 text) (f ca as as-0 name) (k akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc n-0 ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc n-0 ch k rest (pubk as-0)))
    (er (cat n-0 ch k rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat n-0 ch k rest)) (n n) (as as)
    (k-epid (pubk as-0)))
  (defstrand fulcrum 2 (m (cat k rest)) (er ch) (n n-0) (as as-0))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig (privk f) (privk ca) (privk as) (privk as-0) (pubk as-0))
  (uniq-orig n n-0)
  (facts (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid (pubk as-0)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f)))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 2)
    (enc n-0 ch k rest (pubk as-0)) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc n-0 ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc n-0 ch k rest (privk f)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv (cat (cat n-0 ch k rest) (enc n-0 ch k rest (pubk as-0))))
      (send
        (enc n (cat n-0 ch k rest) (enc n-0 ch k rest (pubk as-0))
          (pubk as))) (recv n) (send (enc n-0 ch k rest (privk f))))
    ((recv
       (enc n (cat n-0 ch k rest) (enc n-0 ch k rest (pubk as-0))
         (pubk as))) (send n))
    ((recv (cat ch k rest)) (send (enc n-0 ch k rest (pubk as-0)))))
  (label 9)
  (parent 7)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton cb-over-sgx
  (vars (eid ch rest mesg) (n text) (f ca as name) (proc-sec skey)
    (k k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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)) (proc-sec proc-sec)
    (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid ch k rest)) (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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f)))
  (rule local-quote-attests-enclave)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eid ch k rest) proc-sec) (4 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca)) (enc eid ch k rest (privk f))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid ch k rest (privk f)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv (cat (cat eid ch k rest) (enc eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc eid ch k rest k-epid)
          (pubk as))) (recv n) (send (enc eid ch k rest (privk f))))
    ((recv
       (enc n (cat eid ch k rest) (enc eid ch k rest k-epid) (pubk as)))
      (send n))
    ((recv
       (cat (cat eid ch k rest) (hash (cat eid ch k rest) proc-sec)))
      (send (cat (cat eid ch k rest) (enc eid ch k rest k-epid))))
    ((recv (cat eid ch k rest))
      (send
        (cat (cat eid ch k rest) (hash (cat eid ch k rest) proc-sec)))))
  (label 10)
  (parent 8)
  (unrealized)
  (shape)
  (maps ((0) ((f f) (ca ca) (k k) (eid eid) (ch ch) (rest rest))))
  (origs (n (2 1))))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey))
    (trace (recv er) (send (cat er (hash er proc-sec)))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (cat er (enc er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc 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 er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc 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 as-confirms-non-std
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (defrule as-key-std
    (forall ((z-as strd) (as name))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "as" z-as as))
        (fact is-std-sigkey (privk as)))))
  (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 epid-quote-non-std
    (forall ((z-iq strd) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (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-non-epid
    (forall ((z-ca strd) (ca name))
      (implies (and (p "certifier" z-ca 1) (p "certifier" "ca" z-ca ca))
        (fact is-std-sigkey (privk ca)))))
  (defrule fulcrum-non-epid
    (forall ((z-fm strd) (f name))
      (implies (and (p "fulcrum" z-fm 2) (p "fulcrum" "f" z-fm f))
        (fact is-std-sigkey (privk f)))))
  (defrule trust-anchor-inverse-is-non
    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k)))))
  (defrule fulcrum-doesnt-use-trust-anchor
    (forall ((z strd) (f name))
      (implies
        (and (fact trust-anchor (pubk f)) (p "fulcrum" z 2)
          (p "fulcrum" "f" z f)) (false))))
  (defrule crowbar-doesnt-use-trust-anchor
    (forall ((z strd) (cbkey akey))
      (implies
        (and (fact trust-anchor cbkey) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)) (false))))
  (defrule crowbar-doesnt-use-fulcrum-key
    (forall ((z z-ca strd) (f name))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "f" z-ca f)
          (p "crowbar" z 2) (p "crowbar" "cbkey" z (pubk f))) (false))))
  (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-std-sig
    (forall ((z strd) (cbkey akey))
      (implies (and (p "crowbar" z 2) (p "crowbar" "cbkey" z cbkey))
        (fact is-std-sigkey (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 crowbar-code-never-ca
    (forall ((z-ca strd) (eid chc mesg) (proc-sec skey) (ca name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk ca) proc-sec)
          (fact known-crowbar-code chc) (p "certifier" z-ca 1)
          (p "certifier" "ca" z-ca ca)) (false))))
  (defrule crowbar-code-never-fulcrum
    (forall ((z-f strd) (eid chc mesg) (proc-sec skey) (f name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk f) proc-sec)
          (fact known-crowbar-code chc) (p "fulcrum" z-f 4)
          (p "fulcrum" "f" z-f f)) (false))))
  (defrule neq-def (forall ((m mesg)) (implies (fact neq m m) (false))))
  (defrule sig-keys-inverse-std
    (forall ((k akey))
      (implies (fact is-std-sigkey k) (fact is-std-sigkey (invk k))))))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (facts (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))))
  (label 11)
  (unrealized)
  (origs)
  (comment "Not in theory"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (non-orig (privk ca))
  (facts (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc)
    (neq (privk f) (invk cbkey)))
  (rule sig-keys-inverse-std)
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))))
  (label 12)
  (parent 11)
  (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 f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc 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 (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc)
    (neq (privk f) (invk cbkey)))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca)))))
  (label 13)
  (parent 12)
  (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 f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc 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 (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc)
    (neq (privk f) (invk cbkey)))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc eid chc cbkey rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc 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 eid chc cbkey rest (privk f)))))
  (label 14)
  (parent 13)
  (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 f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (rule sig-keys-inverse-std)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
      (pubk as)))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
          (pubk as))) (recv n)
      (send (enc eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
         (pubk as))) (send n)))
  (label 15)
  (parent 14)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc eid chc cbkey rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
          (pubk as))) (recv n)
      (send (enc eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) proc-sec)))
      (send
        (cat (cat eid chc cbkey rest)
          (enc eid chc cbkey rest k-epid)))))
  (label 16)
  (parent 15)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (er chc rest mesg) (n n-0 text) (f ca as as-0 name)
    (cbkey akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc n-0 chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc n-0 chc cbkey rest (pubk as-0)))
    (er (cat n-0 chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat n-0 chc cbkey rest)) (n n) (as as)
    (k-epid (pubk as-0)))
  (defstrand fulcrum 2 (m (cat cbkey rest)) (er chc) (n n-0) (as as-0))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig (privk f) (privk ca) (privk as) (privk as-0) (pubk as-0))
  (uniq-orig n n-0)
  (facts (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid (pubk as-0)) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 2)
    (enc n-0 chc cbkey rest (pubk as-0)) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc n-0 chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc n-0 chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat n-0 chc cbkey rest)
         (enc n-0 chc cbkey rest (pubk as-0))))
      (send
        (enc n (cat n-0 chc cbkey rest)
          (enc n-0 chc cbkey rest (pubk as-0)) (pubk as))) (recv n)
      (send (enc n-0 chc cbkey rest (privk f))))
    ((recv
       (enc n (cat n-0 chc cbkey rest)
         (enc n-0 chc cbkey rest (pubk as-0)) (pubk as))) (send n))
    ((recv (cat chc cbkey rest))
      (send (enc n-0 chc cbkey rest (pubk as-0)))))
  (label 17)
  (parent 15)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid chc cbkey rest))
    (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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (rule local-att-crowbar)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eid chc cbkey rest) proc-sec) (4 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
          (pubk as))) (recv n)
      (send (enc eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) proc-sec)))
      (send
        (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid))))
    ((recv (cat eid chc cbkey rest))
      (send
        (cat (cat eid chc cbkey rest)
          (hash (cat eid chc cbkey rest) proc-sec)))))
  (label 18)
  (parent 16)
  (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 name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid chc cbkey rest))
    (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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc er (invk cbkey)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
          (pubk as))) (recv n)
      (send (enc eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) proc-sec)))
      (send
        (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid))))
    ((recv (cat eid chc cbkey rest))
      (send
        (cat (cat eid chc cbkey rest)
          (hash (cat eid chc cbkey rest) proc-sec))))
    ((recv (cat er (hash er proc-sec))) (send (enc er (invk cbkey)))))
  (label 19)
  (parent 18)
  (unrealized (6 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eid chc rest mesg) (n text) (f ca as name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc eid chc cbkey rest (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid chc cbkey rest))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eid chc cbkey rest)) (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)) ((5 1) (6 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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (operation encryption-test (displaced 7 5 local-quote 2)
    (hash er proc-sec) (6 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f))
         (enc eid chc cbkey rest (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f))
          (enc eid chc cbkey rest (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
          (pubk as))) (recv n)
      (send (enc eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) proc-sec)))
      (send
        (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid))))
    ((recv (cat eid chc cbkey rest))
      (send
        (cat (cat eid chc cbkey rest)
          (hash (cat eid chc cbkey rest) proc-sec))))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) proc-sec)))
      (send (enc eid chc cbkey rest (invk cbkey)))))
  (label 20)
  (parent 19)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((f f) (ca ca) (cbkey cbkey) (er (cat eid chc cbkey rest))
        (eid eid) (chc chc) (rest rest))))
  (origs (n (2 1))))

(defskeleton cb-over-sgx
  (vars (er eid chc rest mesg) (n text) (f ca as name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eid chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eid chc cbkey rest))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er er) (proc-sec proc-sec) (cbkey cbkey))
  (defstrand local-quote 2 (er er) (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)) ((6 1) (0 0)) ((7 1) (6 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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq (privk f) (invk cbkey)))
  (operation encryption-test (added-strand local-quote 2)
    (hash er proc-sec) (6 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eid chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)))
      (send
        (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
          (pubk as))) (recv n)
      (send (enc eid chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid chc cbkey rest)
         (hash (cat eid chc cbkey rest) proc-sec)))
      (send
        (cat (cat eid chc cbkey rest) (enc eid chc cbkey rest k-epid))))
    ((recv (cat eid chc cbkey rest))
      (send
        (cat (cat eid chc cbkey rest)
          (hash (cat eid chc cbkey rest) proc-sec))))
    ((recv (cat er (hash er proc-sec))) (send (enc er (invk cbkey))))
    ((recv er) (send (cat er (hash er proc-sec)))))
  (label 21)
  (parent 19)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((f f) (ca ca) (cbkey cbkey) (er er) (eid eid) (chc chc)
        (rest rest))))
  (origs (n (2 1))))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey))
    (trace (recv er) (send (cat er (hash er proc-sec)))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (cat er (enc er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc 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 er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc 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 as-confirms-non-std
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (defrule as-key-std
    (forall ((z-as strd) (as name))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "as" z-as as))
        (fact is-std-sigkey (privk as)))))
  (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 epid-quote-non-std
    (forall ((z-iq strd) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (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-non-epid
    (forall ((z-ca strd) (ca name))
      (implies (and (p "certifier" z-ca 1) (p "certifier" "ca" z-ca ca))
        (fact is-std-sigkey (privk ca)))))
  (defrule fulcrum-non-epid
    (forall ((z-fm strd) (f name))
      (implies (and (p "fulcrum" z-fm 2) (p "fulcrum" "f" z-fm f))
        (fact is-std-sigkey (privk f)))))
  (defrule trust-anchor-inverse-is-non
    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k)))))
  (defrule fulcrum-doesnt-use-trust-anchor
    (forall ((z strd) (f name))
      (implies
        (and (fact trust-anchor (pubk f)) (p "fulcrum" z 2)
          (p "fulcrum" "f" z f)) (false))))
  (defrule crowbar-doesnt-use-trust-anchor
    (forall ((z strd) (cbkey akey))
      (implies
        (and (fact trust-anchor cbkey) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)) (false))))
  (defrule crowbar-doesnt-use-fulcrum-key
    (forall ((z z-ca strd) (f name))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "f" z-ca f)
          (p "crowbar" z 2) (p "crowbar" "cbkey" z (pubk f))) (false))))
  (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-std-sig
    (forall ((z strd) (cbkey akey))
      (implies (and (p "crowbar" z 2) (p "crowbar" "cbkey" z cbkey))
        (fact is-std-sigkey (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 crowbar-code-never-ca
    (forall ((z-ca strd) (eid chc mesg) (proc-sec skey) (ca name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk ca) proc-sec)
          (fact known-crowbar-code chc) (p "certifier" z-ca 1)
          (p "certifier" "ca" z-ca ca)) (false))))
  (defrule crowbar-code-never-fulcrum
    (forall ((z-f strd) (eid chc mesg) (proc-sec skey) (f name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk f) proc-sec)
          (fact known-crowbar-code chc) (p "fulcrum" z-f 4)
          (p "fulcrum" "f" z-f f)) (false))))
  (defrule neq-def (forall ((m mesg)) (implies (fact neq m m) (false))))
  (defrule sig-keys-inverse-std
    (forall ((k akey))
      (implies (fact is-std-sigkey k) (fact is-std-sigkey (invk k))))))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (facts (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq er (cat eidc chc cbkey rest)))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))))
  (label 22)
  (unrealized)
  (origs)
  (comment "Not in theory"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (f ca name) (cbkey akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (non-orig (privk ca))
  (facts (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (rule sig-keys-inverse-std)
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))))
  (label 23)
  (parent 22)
  (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 f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc 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 (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca)))))
  (label 24)
  (parent 23)
  (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 f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc 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 (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc)
    (neq er (cat eidc chc cbkey rest)))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc eidc chc cbkey rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc 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 eidc chc cbkey rest (privk f)))))
  (label 25)
  (parent 24)
  (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 f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq er (cat eidc chc cbkey rest)))
  (rule sig-keys-inverse-std)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
      (pubk as)))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n)))
  (label 26)
  (parent 25)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (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 eidc chc cbkey rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid)))))
  (label 27)
  (parent 26)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (chc er rest mesg) (n n-0 text) (f ca as as-0 name)
    (cbkey akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc n-0 chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc n-0 chc cbkey rest (pubk as-0)))
    (er (cat n-0 chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat n-0 chc cbkey rest)) (n n) (as as)
    (k-epid (pubk as-0)))
  (defstrand fulcrum 2 (m (cat cbkey rest)) (er chc) (n n-0) (as as-0))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig (privk f) (privk ca) (privk as) (privk as-0) (pubk as-0))
  (uniq-orig n n-0)
  (facts (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid (pubk as-0)) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq er (cat n-0 chc cbkey rest)))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 2)
    (enc n-0 chc cbkey rest (pubk as-0)) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc n-0 chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc n-0 chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat n-0 chc cbkey rest)
         (enc n-0 chc cbkey rest (pubk as-0))))
      (send
        (enc n (cat n-0 chc cbkey rest)
          (enc n-0 chc cbkey rest (pubk as-0)) (pubk as))) (recv n)
      (send (enc n-0 chc cbkey rest (privk f))))
    ((recv
       (enc n (cat n-0 chc cbkey rest)
         (enc n-0 chc cbkey rest (pubk as-0)) (pubk as))) (send n))
    ((recv (cat chc cbkey rest))
      (send (enc n-0 chc cbkey rest (pubk as-0)))))
  (label 28)
  (parent 26)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (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) proc-sec) (4 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid))))
    ((recv (cat eidc chc cbkey rest))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest) proc-sec)))))
  (label 29)
  (parent 27)
  (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 name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq er (cat eidc chc cbkey rest)))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc er (invk cbkey)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid))))
    ((recv (cat eidc chc cbkey rest))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest) proc-sec))))
    ((recv (cat er (hash er proc-sec))) (send (enc er (invk cbkey)))))
  (label 30)
  (parent 29)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eidc chc er rest mesg) (n text) (f ca as name) (proc-sec skey)
    (cbkey k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc er (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er er) (proc-sec proc-sec) (cbkey cbkey))
  (defstrand local-quote 2 (er er) (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)) ((6 1) (0 0)) ((7 1) (6 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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq er (cat eidc chc cbkey rest)))
  (operation encryption-test (added-strand local-quote 2)
    (hash er proc-sec) (6 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f)) (enc er (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid))))
    ((recv (cat eidc chc cbkey rest))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest) proc-sec))))
    ((recv (cat er (hash er proc-sec))) (send (enc er (invk cbkey))))
    ((recv er) (send (cat er (hash er proc-sec)))))
  (label 31)
  (parent 30)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((f f) (ca ca) (cbkey cbkey) (eidc eidc) (chc chc) (er er)
        (rest rest))))
  (origs (n (2 1))))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey))
    (trace (recv er) (send (cat er (hash er proc-sec)))))
  (defrole epid-quote
    (vars (er mesg) (k-epid akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (cat er (enc er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc 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 er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc 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 as-confirms-non-std
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (defrule as-key-std
    (forall ((z-as strd) (as name))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "as" z-as as))
        (fact is-std-sigkey (privk as)))))
  (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 epid-quote-non-std
    (forall ((z-iq strd) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (fact is-std-sigkey k-epid)) (false))))
  (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-non-epid
    (forall ((z-ca strd) (ca name))
      (implies (and (p "certifier" z-ca 1) (p "certifier" "ca" z-ca ca))
        (fact is-std-sigkey (privk ca)))))
  (defrule fulcrum-non-epid
    (forall ((z-fm strd) (f name))
      (implies (and (p "fulcrum" z-fm 2) (p "fulcrum" "f" z-fm f))
        (fact is-std-sigkey (privk f)))))
  (defrule trust-anchor-inverse-is-non
    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k)))))
  (defrule fulcrum-doesnt-use-trust-anchor
    (forall ((z strd) (f name))
      (implies
        (and (fact trust-anchor (pubk f)) (p "fulcrum" z 2)
          (p "fulcrum" "f" z f)) (false))))
  (defrule crowbar-doesnt-use-trust-anchor
    (forall ((z strd) (cbkey akey))
      (implies
        (and (fact trust-anchor cbkey) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)) (false))))
  (defrule crowbar-doesnt-use-fulcrum-key
    (forall ((z z-ca strd) (f name))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "f" z-ca f)
          (p "crowbar" z 2) (p "crowbar" "cbkey" z (pubk f))) (false))))
  (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-std-sig
    (forall ((z strd) (cbkey akey))
      (implies (and (p "crowbar" z 2) (p "crowbar" "cbkey" z cbkey))
        (fact is-std-sigkey (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 crowbar-code-never-ca
    (forall ((z-ca strd) (eid chc mesg) (proc-sec skey) (ca name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk ca) proc-sec)
          (fact known-crowbar-code chc) (p "certifier" z-ca 1)
          (p "certifier" "ca" z-ca ca)) (false))))
  (defrule crowbar-code-never-fulcrum
    (forall ((z-f strd) (eid chc mesg) (proc-sec skey) (f name))
      (implies
        (and (fact enclave-w-code-and-key eid chc (pubk f) proc-sec)
          (fact known-crowbar-code chc) (p "fulcrum" z-f 4)
          (p "fulcrum" "f" z-f f)) (false))))
  (defrule neq-def (forall ((m mesg)) (implies (fact neq m m) (false))))
  (defrule sig-keys-inverse-std
    (forall ((k akey))
      (implies (fact is-std-sigkey k) (fact is-std-sigkey (invk k))))))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (f ca name) (cbkey ka akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (facts (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq chc cha))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey))))))
  (label 32)
  (unrealized)
  (origs)
  (comment "Not in theory"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (f ca name) (cbkey ka akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (non-orig (privk ca))
  (facts (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc) (neq chc cha))
  (rule sig-keys-inverse-std)
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey))))))
  (label 33)
  (parent 32)
  (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 f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc 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 (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc) (neq chc cha))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc f (pubk f) (privk ca)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca)))))
  (label 34)
  (parent 33)
  (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 f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc 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 (is-std-sigkey (invk cbkey)) (is-std-sigkey (pubk f))
    (is-std-sigkey (pubk ca)) (trust-anchor (pubk ca))
    (is-std-sigkey (privk ca)) (is-std-sigkey (privk f))
    (is-std-sigkey cbkey) (known-crowbar-code chc) (neq chc cha))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc eidc chc cbkey rest (privk f)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc 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 eidc chc cbkey rest (privk f)))))
  (label 35)
  (parent 34)
  (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 f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq chc cha))
  (rule sig-keys-inverse-std)
  (operation nonce-test (added-strand attest-server 2) n (2 2)
    (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
      (pubk as)))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n)))
  (label 36)
  (parent 35)
  (unrealized (2 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 name)
    (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (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 (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq chc cha))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc eidc chc cbkey rest k-epid) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid)))))
  (label 37)
  (parent 36)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton cb-over-sgx
  (vars (eida chc cha rest resta mesg) (n n-0 text) (f ca as as-0 name)
    (cbkey ka akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc n-0 chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc n-0 chc cbkey rest (pubk as-0)))
    (er (cat n-0 chc cbkey rest)) (n n) (as as) (f f))
  (defstrand attest-server 2 (er (cat n-0 chc cbkey rest)) (n n) (as as)
    (k-epid (pubk as-0)))
  (defstrand fulcrum 2 (m (cat cbkey rest)) (er chc) (n n-0) (as as-0))
  (precedes ((1 0) (0 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig (privk f) (privk ca) (privk as) (privk as-0) (pubk as-0))
  (uniq-orig n n-0)
  (facts (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid (pubk as-0)) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq chc cha))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 2)
    (enc n-0 chc cbkey rest (pubk as-0)) (2 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc n-0 chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc n-0 chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat n-0 chc cbkey rest)
         (enc n-0 chc cbkey rest (pubk as-0))))
      (send
        (enc n (cat n-0 chc cbkey rest)
          (enc n-0 chc cbkey rest (pubk as-0)) (pubk as))) (recv n)
      (send (enc n-0 chc cbkey rest (privk f))))
    ((recv
       (enc n (cat n-0 chc cbkey rest)
         (enc n-0 chc cbkey rest (pubk as-0)) (pubk as))) (send n))
    ((recv (cat chc cbkey rest))
      (send (enc n-0 chc cbkey rest (pubk as-0)))))
  (label 38)
  (parent 36)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton cb-over-sgx
  (vars (eidc eida chc cha rest resta mesg) (n text) (f ca as name)
    (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (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) proc-sec) (4 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid))))
    ((recv (cat eidc chc cbkey rest))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest) proc-sec)))))
  (label 39)
  (parent 37)
  (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 name)
    (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (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)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq chc cha))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc eida cha ka resta (invk cbkey)) (0 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid))))
    ((recv (cat eidc chc cbkey rest))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest) proc-sec))))
    ((recv
       (cat (cat eida cha ka resta)
         (hash (cat eida cha ka resta) proc-sec)))
      (send (enc eida cha ka resta (invk cbkey)))))
  (label 40)
  (parent 39)
  (unrealized (6 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 name)
    (proc-sec skey) (cbkey ka k-epid akey))
  (deflistener
    (cat (enc f (pubk f) (privk ca)) (enc eidc chc cbkey rest (privk f))
      (enc eida cha ka resta (invk cbkey))))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc 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))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eida cha ka resta)) (proc-sec proc-sec)
    (cbkey cbkey))
  (defstrand local-quote 2 (er (cat eida cha ka resta))
    (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)) ((6 1) (0 0)) ((7 1) (6 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk f) (privk ca)
    (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eida cha ka proc-sec)
    (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (is-std-sigkey (pubk as)) (is-std-sigkey (privk as))
    (man-made-epid k-epid) (is-std-sigkey (invk cbkey))
    (is-std-sigkey (pubk f)) (is-std-sigkey (pubk ca))
    (trust-anchor (pubk ca)) (is-std-sigkey (privk ca))
    (is-std-sigkey (privk f)) (is-std-sigkey cbkey)
    (known-crowbar-code chc) (neq chc cha))
  (rule local-quote-attests-enclave)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eida cha ka resta) proc-sec) (6 0))
  (traces
    ((recv
       (cat (enc f (pubk f) (privk ca))
         (enc eidc chc cbkey rest (privk f))
         (enc eida cha ka resta (invk cbkey))))
      (send
        (cat (enc f (pubk f) (privk ca))
          (enc eidc chc cbkey rest (privk f))
          (enc eida cha ka resta (invk cbkey)))))
    ((send (enc f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)))
      (send
        (enc n (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid) (pubk as))) (recv n)
      (send (enc eidc chc cbkey rest (privk f))))
    ((recv
       (enc n (cat eidc chc cbkey rest) (enc eidc chc cbkey rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eidc chc cbkey rest)
         (hash (cat eidc chc cbkey rest) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest)
          (enc eidc chc cbkey rest k-epid))))
    ((recv (cat eidc chc cbkey rest))
      (send
        (cat (cat eidc chc cbkey rest)
          (hash (cat eidc chc cbkey rest) proc-sec))))
    ((recv
       (cat (cat eida cha ka resta)
         (hash (cat eida cha ka resta) proc-sec)))
      (send (enc eida cha ka resta (invk cbkey))))
    ((recv (cat eida cha ka resta))
      (send
        (cat (cat eida cha ka resta)
          (hash (cat eida cha ka resta) proc-sec)))))
  (label 41)
  (parent 40)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((f f) (ca ca) (cbkey cbkey) (ka ka) (eidc eidc) (eida eida)
        (chc chc) (cha cha) (rest rest) (resta resta))))
  (origs (n (2 1))))

(comment "Nothing left to do")