(herald "fine/sgx_minimal")

(comment "CPSA 4.1.1")
(comment "All input read from sgx_minimal.scm")

(defprotocol sgx-min 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 "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole attest-client
    (vars (m er mesg) (n text) (as name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)))
  (defrule as-confirms-epid-ok
    (forall ((z-as strd) (k-epid akey))
      (implies
        (and (p "attest-server" z-as 2)
          (p "attest-server" "k-epid" z-as k-epid))
        (and (fact man-made-epid k-epid) (non k-epid)))))
  (defrule epid-quote-processor-ok
    (forall ((z-iq strd) (proc-sec skey) (k-epid akey))
      (implies
        (and (p "epid-quote" z-iq 2)
          (p "epid-quote" "k-epid" z-iq k-epid)
          (p "epid-quote" "proc-sec" z-iq proc-sec)
          (fact man-made-epid k-epid)) (non proc-sec))))
  (defrule local-quote-attests-enclave
    (forall ((z-lq strd) (eid ch rest mesg) (k akey) (proc-sec skey))
      (implies
        (and (p "local-quote" z-lq 2)
          (p "local-quote" "er" z-lq (cat eid ch k rest))
          (p "local-quote" "proc-sec" z-lq proc-sec) (non proc-sec))
        (fact enclave-w-code-and-key eid ch k proc-sec)))))

(defskeleton sgx-min
  (vars (eid ch rest m mesg) (n text) (as name) (k akey))
  (defstrand attest-client 3 (m m) (er (cat eid ch k rest)) (n n)
    (as as))
  (non-orig (privk as))
  (uniq-orig n)
  (traces
    ((recv (cat (cat eid ch k rest) m))
      (send (enc n (cat eid ch k rest) m (pubk as))) (recv n)))
  (label 0)
  (unrealized (0 2))
  (origs (n (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton sgx-min
  (vars (eid ch rest mesg) (n text) (as name) (proc-sec skey)
    (k k-epid akey))
  (defstrand attest-client 3 (m (enc "rq" eid ch k rest k-epid))
    (er (cat eid ch k rest)) (n n) (as as))
  (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 ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 0)))
  (non-orig proc-sec k-epid (privk as))
  (uniq-orig n)
  (facts (man-made-epid k-epid))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc "rq" eid ch k rest k-epid) (0 0))
  (traces
    ((recv (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
          (pubk as))) (recv n))
    ((recv
       (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid ch k rest) (hash (cat eid ch k rest) proc-sec)))
      (send (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))))
  (label 2)
  (parent 1)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton sgx-min
  (vars (eid ch rest mesg) (n text) (as name) (proc-sec skey)
    (k k-epid akey))
  (defstrand attest-client 3 (m (enc "rq" eid ch k rest k-epid))
    (er (cat eid ch k rest)) (n n) (as as))
  (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 ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 0)) ((3 1) (2 0)))
  (non-orig proc-sec k-epid (privk as))
  (uniq-orig n)
  (facts (enclave-w-code-and-key eid ch k proc-sec)
    (man-made-epid k-epid))
  (rule local-quote-attests-enclave)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eid ch k rest) proc-sec) (2 0))
  (traces
    ((recv (cat (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)))
      (send
        (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
          (pubk as))) (recv n))
    ((recv
       (enc n (cat eid ch k rest) (enc "rq" eid ch k rest k-epid)
         (pubk as))) (send n))
    ((recv
       (cat (cat eid ch k rest) (hash (cat eid ch k rest) proc-sec)))
      (send (cat (cat eid ch k rest) (enc "rq" 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 3)
  (parent 2)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((as as) (eid eid) (ch ch) (rest rest) (k k) (n n)
        (m (enc "rq" eid ch k rest k-epid)))))
  (origs (n (0 1))))

(comment "Nothing left to do")