(herald "client_cb" (bound 12))

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

(defprotocol client-and-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 "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole fulcrum
    (vars (m er mesg) (n text) (as f name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)
      (send (enc "fm" er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc "certificate" "fulcrum" f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (defrole client-yes
    (vars (answerer f ca name) (cbkey akey) (a y n text) (q data)
      (eidc eida ch-ans ch-crowbar rest1 rest2 mesg))
    (trace (send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc ch-crowbar cbkey rest1 (privk f))
          (enc "cb" eida ch-ans (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv y)))
  (defrole ans-yes
    (vars (answerer name) (y n text) (q data))
    (trace (recv (enc q y n (pubk answerer))) (send y)))
  (defrole client-no
    (vars (answerer f ca name) (cbkey akey) (a y n text) (q data)
      (eidc eida ch-ans ch-crowbar rest1 rest2 mesg))
    (trace (send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc ch-crowbar cbkey rest1 (privk f))
          (enc "cb" eida ch-ans (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n)))
  (defrole ans-no
    (vars (answerer name) (y n text) (q data))
    (trace (recv (enc q y n (pubk answerer))) (send 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))))
  (defrule cert-rule-fulcrum
    (forall ((z-ca strd) (f name) (k akey))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "k" z-ca k)
          (p "certifier" "f" z-ca f) (= k (pubk f))) (non (invk k)))))
  (defrule cert-rule-attest-server
    (forall ((z-fm strd) (as name) (n text))
      (implies
        (and (p "fulcrum" z-fm 2) (p "fulcrum" "as" z-fm as)
          (p "fulcrum" "n" z-fm n)) (and (non (privk as)) (uniq n)))))
  (defrule local-att-crowbar
    (forall ((eid chc mesg) (cbkey akey) (proc-sec skey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc)) (non (invk cbkey)))))
  (defrule crowbar-immobile
    (forall
      ((z strd) (eid chc mesg) (proc-sec proc-sec-0 skey) (cbkey akey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)
          (p "crowbar" "proc-sec" z proc-sec-0))
        (= proc-sec proc-sec-0))))
  (defrule neq-def (forall ((m mesg)) (implies (fact neq m m) (false))))
  (defrule local-att-ans
    (forall ((eida cha mesg) (k akey) (proc-sec skey))
      (implies
        (and (fact known-ans-code cha)
          (fact enclave-w-code-and-key eida cha k proc-sec))
        (non (invk k))))))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n text) (q data)
    (ca f answerer name) (cbkey akey))
  (defstrand client-yes 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (non-orig (privk ca))
  (uniq-orig a y)
  (facts (known-crowbar-code chc) (known-ans-code cha) (neq chc cha))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv y)))
  (label 0)
  (unrealized (0 1))
  (origs (y (0 2)) (a (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n text) (q data)
    (ca f answerer name) (cbkey akey))
  (defstrand client-yes 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (precedes ((1 0) (0 1)))
  (non-orig (privk ca) (privk f))
  (uniq-orig a y)
  (facts (known-crowbar-code chc) (known-ans-code cha) (neq chc cha))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc "certificate" "fulcrum" f (pubk f) (privk ca)) (0 1))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv y))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 m mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (cbkey akey))
  (defstrand client-yes 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m m) (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (f f))
  (precedes ((1 0) (0 1)) ((2 3) (0 1)))
  (non-orig (privk ca) (privk f) (privk as))
  (uniq-orig a y n-0)
  (facts (known-crowbar-code chc) (known-ans-code cha) (neq chc cha))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc "fm" eidc chc cbkey rest1 (privk f)) (0 1))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv y))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eidc chc cbkey rest1) m))
      (send (enc n-0 (cat eidc chc cbkey rest1) m (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f)))))
  (label 2)
  (parent 1)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

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

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

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

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (proc-sec skey) (cbkey k-epid akey))
  (defstrand client-yes 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest1 k-epid))
    (er (cat eidc chc cbkey rest1)) (n n-0) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec) (cbkey cbkey))
  (precedes ((0 0) (6 0)) ((1 0) (0 1)) ((2 1) (3 0)) ((2 3) (0 1))
    ((3 1) (2 2)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (0 1)))
  (non-orig proc-sec k-epid (invk cbkey) (privk ca) (privk f)
    (privk as))
  (uniq-orig a y n-0)
  (facts (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc) (known-ans-code cha)
    (neq chc cha))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey)) (0 1))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv y))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid)))
      (send
        (enc n-0 (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f))))
    ((recv
       (enc n-0 (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (send n-0))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (hash (cat eidc chc cbkey rest1) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid))))
    ((recv (cat eidc chc cbkey rest1))
      (send
        (cat (cat eidc chc cbkey rest1)
          (hash (cat eidc chc cbkey rest1) proc-sec))))
    ((recv
       (cat (cat eida cha (pubk answerer) a rest2)
         (hash (cat eida cha (pubk answerer) a rest2) proc-sec)))
      (send (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey)))))
  (label 6)
  (parent 5)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (proc-sec skey) (cbkey k-epid akey))
  (defstrand client-yes 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest1 k-epid))
    (er (cat eidc chc cbkey rest1)) (n n-0) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec) (cbkey cbkey))
  (defstrand local-quote 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec))
  (defstrand ans-yes 2 (y y) (n n) (q q) (answerer answerer))
  (precedes ((0 0) (7 0)) ((0 2) (8 0)) ((1 0) (0 1)) ((2 1) (3 0))
    ((2 3) (0 1)) ((3 1) (2 2)) ((4 1) (2 0)) ((5 1) (4 0))
    ((6 1) (0 1)) ((7 1) (6 0)) ((8 1) (0 3)))
  (non-orig proc-sec k-epid (invk cbkey) (privk ca) (privk f)
    (privk answerer) (privk as))
  (uniq-orig a y n-0)
  (facts (enclave-w-code-and-key eida cha (pubk answerer) proc-sec)
    (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc) (known-ans-code cha)
    (neq chc cha))
  (operation nonce-test (added-strand ans-yes 2) y (0 3)
    (enc q y n (pubk answerer)))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv y))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid)))
      (send
        (enc n-0 (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f))))
    ((recv
       (enc n-0 (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (send n-0))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (hash (cat eidc chc cbkey rest1) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid))))
    ((recv (cat eidc chc cbkey rest1))
      (send
        (cat (cat eidc chc cbkey rest1)
          (hash (cat eidc chc cbkey rest1) proc-sec))))
    ((recv
       (cat (cat eida cha (pubk answerer) a rest2)
         (hash (cat eida cha (pubk answerer) a rest2) proc-sec)))
      (send (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
    ((recv (cat eida cha (pubk answerer) a rest2))
      (send
        (cat (cat eida cha (pubk answerer) a rest2)
          (hash (cat eida cha (pubk answerer) a rest2) proc-sec))))
    ((recv (enc q y n (pubk answerer))) (send y)))
  (label 8)
  (parent 7)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((ca ca) (f f) (a a) (y y) (n n) (cha cha) (chc chc)
        (answerer answerer) (cbkey cbkey) (q q) (eidc eidc) (eida eida)
        (rest1 rest1) (rest2 rest2))))
  (origs (n-0 (2 1)) (y (0 2)) (a (0 0))))

(comment "Nothing left to do")

(defprotocol client-and-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 "rq" er k-epid)))))
  (defrole attest-server
    (vars (er mesg) (n text) (k-epid akey) (as name))
    (trace (recv (enc n er (enc "rq" er k-epid) (pubk as))) (send n)))
  (defrole fulcrum
    (vars (m er mesg) (n text) (as f name))
    (trace (recv (cat er m)) (send (enc n er m (pubk as))) (recv n)
      (send (enc "fm" er (privk f)))))
  (defrole certifier
    (vars (ca f name) (k akey))
    (trace (send (enc "certificate" "fulcrum" f k (privk ca)))))
  (defrole crowbar
    (vars (er mesg) (cbkey akey) (proc-sec skey))
    (trace (recv (cat er (hash er proc-sec)))
      (send (enc "cb" er (invk cbkey)))))
  (defrole client-yes
    (vars (answerer f ca name) (cbkey akey) (a y n text) (q data)
      (eidc eida ch-ans ch-crowbar rest1 rest2 mesg))
    (trace (send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc ch-crowbar cbkey rest1 (privk f))
          (enc "cb" eida ch-ans (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv y)))
  (defrole ans-yes
    (vars (answerer name) (y n text) (q data))
    (trace (recv (enc q y n (pubk answerer))) (send y)))
  (defrole client-no
    (vars (answerer f ca name) (cbkey akey) (a y n text) (q data)
      (eidc eida ch-ans ch-crowbar rest1 rest2 mesg))
    (trace (send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc ch-crowbar cbkey rest1 (privk f))
          (enc "cb" eida ch-ans (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n)))
  (defrole ans-no
    (vars (answerer name) (y n text) (q data))
    (trace (recv (enc q y n (pubk answerer))) (send 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))))
  (defrule cert-rule-fulcrum
    (forall ((z-ca strd) (f name) (k akey))
      (implies
        (and (p "certifier" z-ca 1) (p "certifier" "k" z-ca k)
          (p "certifier" "f" z-ca f) (= k (pubk f))) (non (invk k)))))
  (defrule cert-rule-attest-server
    (forall ((z-fm strd) (as name) (n text))
      (implies
        (and (p "fulcrum" z-fm 2) (p "fulcrum" "as" z-fm as)
          (p "fulcrum" "n" z-fm n)) (and (non (privk as)) (uniq n)))))
  (defrule local-att-crowbar
    (forall ((eid chc mesg) (cbkey akey) (proc-sec skey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc)) (non (invk cbkey)))))
  (defrule crowbar-immobile
    (forall
      ((z strd) (eid chc mesg) (proc-sec proc-sec-0 skey) (cbkey akey))
      (implies
        (and (fact enclave-w-code-and-key eid chc cbkey proc-sec)
          (fact known-crowbar-code chc) (p "crowbar" z 2)
          (p "crowbar" "cbkey" z cbkey)
          (p "crowbar" "proc-sec" z proc-sec-0))
        (= proc-sec proc-sec-0))))
  (defrule neq-def (forall ((m mesg)) (implies (fact neq m m) (false))))
  (defrule local-att-ans
    (forall ((eida cha mesg) (k akey) (proc-sec skey))
      (implies
        (and (fact known-ans-code cha)
          (fact enclave-w-code-and-key eida cha k proc-sec))
        (non (invk k))))))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n text) (q data)
    (ca f answerer name) (cbkey akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (non-orig (privk ca))
  (uniq-orig a n)
  (facts (known-crowbar-code chc) (known-ans-code cha) (neq chc cha))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n)))
  (label 9)
  (unrealized (0 1))
  (origs (n (0 2)) (a (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n text) (q data)
    (ca f answerer name) (cbkey akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (precedes ((1 0) (0 1)))
  (non-orig (privk ca) (privk f))
  (uniq-orig a n)
  (facts (known-crowbar-code chc) (known-ans-code cha) (neq chc cha))
  (rule cert-rule-fulcrum)
  (operation encryption-test (added-strand certifier 1)
    (enc "certificate" "fulcrum" f (pubk f) (privk ca)) (0 1))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca)))))
  (label 10)
  (parent 9)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 m mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (cbkey akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m m) (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (f f))
  (precedes ((1 0) (0 1)) ((2 3) (0 1)))
  (non-orig (privk ca) (privk f) (privk as))
  (uniq-orig a n n-0)
  (facts (known-crowbar-code chc) (known-ans-code cha) (neq chc cha))
  (rule cert-rule-attest-server)
  (operation encryption-test (added-strand fulcrum 4)
    (enc "fm" eidc chc cbkey rest1 (privk f)) (0 1))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv (cat (cat eidc chc cbkey rest1) m))
      (send (enc n-0 (cat eidc chc cbkey rest1) m (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f)))))
  (label 11)
  (parent 10)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (cbkey k-epid akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest1 k-epid))
    (er (cat eidc chc cbkey rest1)) (n n-0) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (k-epid k-epid))
  (precedes ((1 0) (0 1)) ((2 1) (3 0)) ((2 3) (0 1)) ((3 1) (2 2)))
  (non-orig k-epid (privk ca) (privk f) (privk as))
  (uniq-orig a n n-0)
  (facts (man-made-epid k-epid) (known-crowbar-code chc)
    (known-ans-code cha) (neq chc cha))
  (rule as-confirms-epid-ok)
  (operation nonce-test (added-strand attest-server 2) n-0 (2 2)
    (enc n-0 (cat eidc chc cbkey rest1)
      (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as)))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid)))
      (send
        (enc n-0 (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f))))
    ((recv
       (enc n-0 (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (send n-0)))
  (label 12)
  (parent 11)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (proc-sec skey) (cbkey k-epid akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest1 k-epid))
    (er (cat eidc chc cbkey rest1)) (n n-0) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec) (k-epid k-epid))
  (precedes ((1 0) (0 1)) ((2 1) (3 0)) ((2 3) (0 1)) ((3 1) (2 2))
    ((4 1) (2 0)))
  (non-orig proc-sec k-epid (privk ca) (privk f) (privk as))
  (uniq-orig a n n-0)
  (facts (man-made-epid k-epid) (known-crowbar-code chc)
    (known-ans-code cha) (neq chc cha))
  (rule epid-quote-processor-ok)
  (operation encryption-test (added-strand epid-quote 2)
    (enc "rq" eidc chc cbkey rest1 k-epid) (2 0))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid)))
      (send
        (enc n-0 (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f))))
    ((recv
       (enc n-0 (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (send n-0))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (hash (cat eidc chc cbkey rest1) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid)))))
  (label 13)
  (parent 12)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (proc-sec skey) (cbkey k-epid akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest1 k-epid))
    (er (cat eidc chc cbkey rest1)) (n n-0) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec) (cbkey cbkey))
  (precedes ((0 0) (6 0)) ((1 0) (0 1)) ((2 1) (3 0)) ((2 3) (0 1))
    ((3 1) (2 2)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (0 1)))
  (non-orig proc-sec k-epid (invk cbkey) (privk ca) (privk f)
    (privk as))
  (uniq-orig a n n-0)
  (facts (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc) (known-ans-code cha)
    (neq chc cha))
  (rule crowbar-immobile)
  (operation encryption-test (added-strand crowbar 2)
    (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey)) (0 1))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid)))
      (send
        (enc n-0 (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f))))
    ((recv
       (enc n-0 (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (send n-0))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (hash (cat eidc chc cbkey rest1) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid))))
    ((recv (cat eidc chc cbkey rest1))
      (send
        (cat (cat eidc chc cbkey rest1)
          (hash (cat eidc chc cbkey rest1) proc-sec))))
    ((recv
       (cat (cat eida cha (pubk answerer) a rest2)
         (hash (cat eida cha (pubk answerer) a rest2) proc-sec)))
      (send (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey)))))
  (label 15)
  (parent 14)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (proc-sec skey) (cbkey k-epid akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest1 k-epid))
    (er (cat eidc chc cbkey rest1)) (n n-0) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec) (cbkey cbkey))
  (defstrand local-quote 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec))
  (precedes ((0 0) (7 0)) ((1 0) (0 1)) ((2 1) (3 0)) ((2 3) (0 1))
    ((3 1) (2 2)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (0 1))
    ((7 1) (6 0)))
  (non-orig proc-sec k-epid (invk cbkey) (privk ca) (privk f)
    (privk answerer) (privk as))
  (uniq-orig a n n-0)
  (facts (enclave-w-code-and-key eida cha (pubk answerer) proc-sec)
    (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc) (known-ans-code cha)
    (neq chc cha))
  (rule local-att-ans)
  (operation encryption-test (added-strand local-quote 2)
    (hash (cat eida cha (pubk answerer) a rest2) proc-sec) (6 0))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid)))
      (send
        (enc n-0 (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f))))
    ((recv
       (enc n-0 (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (send n-0))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (hash (cat eidc chc cbkey rest1) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid))))
    ((recv (cat eidc chc cbkey rest1))
      (send
        (cat (cat eidc chc cbkey rest1)
          (hash (cat eidc chc cbkey rest1) proc-sec))))
    ((recv
       (cat (cat eida cha (pubk answerer) a rest2)
         (hash (cat eida cha (pubk answerer) a rest2) proc-sec)))
      (send (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
    ((recv (cat eida cha (pubk answerer) a rest2))
      (send
        (cat (cat eida cha (pubk answerer) a rest2)
          (hash (cat eida cha (pubk answerer) a rest2) proc-sec)))))
  (label 16)
  (parent 15)
  (unrealized (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton client-and-cb-over-sgx
  (vars (cha chc eidc eida rest1 rest2 mesg) (a y n n-0 text) (q data)
    (ca f answerer as name) (proc-sec skey) (cbkey k-epid akey))
  (defstrand client-no 4 (eidc eidc) (eida eida) (ch-ans cha)
    (ch-crowbar chc) (rest1 rest1) (rest2 rest2) (a a) (y y) (n n) (q q)
    (answerer answerer) (f f) (ca ca) (cbkey cbkey))
  (defstrand certifier 1 (ca ca) (f f) (k (pubk f)))
  (defstrand fulcrum 4 (m (enc "rq" eidc chc cbkey rest1 k-epid))
    (er (cat eidc chc cbkey rest1)) (n n-0) (as as) (f f))
  (defstrand attest-server 2 (er (cat eidc chc cbkey rest1)) (n n-0)
    (as as) (k-epid k-epid))
  (defstrand epid-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec) (k-epid k-epid))
  (defstrand local-quote 2 (er (cat eidc chc cbkey rest1))
    (proc-sec proc-sec))
  (defstrand crowbar 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec) (cbkey cbkey))
  (defstrand local-quote 2 (er (cat eida cha (pubk answerer) a rest2))
    (proc-sec proc-sec))
  (defstrand ans-no 2 (y y) (n n) (q q) (answerer answerer))
  (precedes ((0 0) (7 0)) ((0 2) (8 0)) ((1 0) (0 1)) ((2 1) (3 0))
    ((2 3) (0 1)) ((3 1) (2 2)) ((4 1) (2 0)) ((5 1) (4 0))
    ((6 1) (0 1)) ((7 1) (6 0)) ((8 1) (0 3)))
  (non-orig proc-sec k-epid (invk cbkey) (privk ca) (privk f)
    (privk answerer) (privk as))
  (uniq-orig a n n-0)
  (facts (enclave-w-code-and-key eida cha (pubk answerer) proc-sec)
    (enclave-w-code-and-key eidc chc cbkey proc-sec)
    (man-made-epid k-epid) (known-crowbar-code chc) (known-ans-code cha)
    (neq chc cha))
  (operation nonce-test (added-strand ans-no 2) n (0 3)
    (enc q y n (pubk answerer)))
  (traces
    ((send a)
      (recv
        (cat (enc "certificate" "fulcrum" f (pubk f) (privk ca))
          (enc "fm" eidc chc cbkey rest1 (privk f))
          (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
      (send (enc q y n (pubk answerer))) (recv n))
    ((send (enc "certificate" "fulcrum" f (pubk f) (privk ca))))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid)))
      (send
        (enc n-0 (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (recv n-0)
      (send (enc "fm" eidc chc cbkey rest1 (privk f))))
    ((recv
       (enc n-0 (cat eidc chc cbkey rest1)
         (enc "rq" eidc chc cbkey rest1 k-epid) (pubk as))) (send n-0))
    ((recv
       (cat (cat eidc chc cbkey rest1)
         (hash (cat eidc chc cbkey rest1) proc-sec)))
      (send
        (cat (cat eidc chc cbkey rest1)
          (enc "rq" eidc chc cbkey rest1 k-epid))))
    ((recv (cat eidc chc cbkey rest1))
      (send
        (cat (cat eidc chc cbkey rest1)
          (hash (cat eidc chc cbkey rest1) proc-sec))))
    ((recv
       (cat (cat eida cha (pubk answerer) a rest2)
         (hash (cat eida cha (pubk answerer) a rest2) proc-sec)))
      (send (enc "cb" eida cha (pubk answerer) a rest2 (invk cbkey))))
    ((recv (cat eida cha (pubk answerer) a rest2))
      (send
        (cat (cat eida cha (pubk answerer) a rest2)
          (hash (cat eida cha (pubk answerer) a rest2) proc-sec))))
    ((recv (enc q y n (pubk answerer))) (send n)))
  (label 17)
  (parent 16)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((ca ca) (f f) (a a) (y y) (n n) (cha cha) (chc chc)
        (answerer answerer) (cbkey cbkey) (q q) (eidc eidc) (eida eida)
        (rest1 rest1) (rest2 rest2))))
  (origs (n-0 (2 1)) (n (0 2)) (a (0 0))))

(comment "Nothing left to do")