(comment "CPSA 4.1.1")
(comment "Extracted shapes")

(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)))
  (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 0)
  (unrealized)
  (shape)
  (maps ((0) ((f f) (ca ca))))
  (origs))

(comment "Nothing left to do")

(defprotocol cb-over-sgx basic
  (defrole local-quote
    (vars (er mesg) (proc-sec skey))
    (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) (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 3)
  (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 (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 11)
  (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 11)
  (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) (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 22)
  (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) (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 32)
  (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")