(herald "Envelope Protocol, location-based version" (bound 30)
  (limit 1200))

(comment "CPSA 4.4.5")
(comment "All input read from tst/locn_envelope.scm")
(comment "Step count limited to 1200")
(comment "Strand count bounded at 30")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpm)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 0)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (precedes ((1 3) (0 0)))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpm)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 1)
  (parent 0)
  (unrealized (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id text) (k aik akey) (tpm tpm-0 chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik) (1 2))
  (strand-map 0 1)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))))
  (label 2)
  (parent 1)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (2 0))
  (strand-map 0 1 2)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))))
  (label 3)
  (parent 2)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (current-value mesg) (v n data) (pcr-id pcr-id-0 text)
    (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v) (current-value current-value)
    (pcr-id pcr-id-0) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (0 0) (enc v k))
  (strand-map 0 1 2)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 current-value aik-0))
      (load pcr (cat pt current-value)) (send v)))
  (label 4)
  (parent 3)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id text) (k aik akey) (pt pval) (tpm tpm-0 chan)
    (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 4 2 tpm-create-key 2)
    (enc "created" k pcr-id-0 current-value aik-0) (3 1))
  (strand-map 0 1 2 3)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)))
  (label 5)
  (parent 4)
  (unrealized (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pval)
    (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (3 2))
  (strand-map 0 1 2 3)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 6)
  (parent 5)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-1) (tpm tpm-2) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1))
  (strand-map 0 1 2 3 4)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm-2 (cat "extend" pcr-id-1 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 7)
  (parent 6)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id) (tpm tpm) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-1 pcr-id) (tpm-2 tpm)) n
    (5 0) (ch-msg tpm (cat "extend" pcr-id n)))
  (strand-map 0 1 2 3 4 5)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 8)
  (parent 7)
  (realized)
  (shape)
  (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))))
  (origs (pt-0 (5 2)) (pt (4 2)) (k (2 1)) (n (1 0)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 9)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (precedes ((1 3) (0 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 10)
  (parent 9)
  (unrealized (0 0) (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (1 2))
  (strand-map 0 1)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0
       (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 11)
  (parent 10)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 12)
  (parent 11)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval)
    (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-quote)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))))
  (label 13)
  (parent 12)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "refuse"))) (3 1))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse")))))
  (label 14)
  (parent 13)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 15)
  (parent 14)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n
    (5 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 16)
  (parent 15)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (tpm tpm))))
  (origs (pt-0 (5 2)) (pt (4 2)) (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 17)
  (unrealized (0 0) (1 0) (2 2))
  (preskeleton)
  (origs (v (2 3)) (n (2 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 18)
  (parent 17)
  (unrealized (0 0) (2 2))
  (origs (v (2 3)) (n (2 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (2 2))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0
       (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 19)
  (parent 18)
  (unrealized (0 0) (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 4 2 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 20)
  (parent 19)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (current-value mesg) (n v data) (pcr-id pcr-id-0 pcr-id-1 text)
    (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v) (current-value current-value)
    (pcr-id pcr-id-1) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-1 current-value aik-0))
      (load pcr (cat pt current-value)) (send v)))
  (label 21)
  (parent 20)
  (unrealized (0 0) (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval)
    (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 5 3 tpm-create-key 2)
    (enc "created" k pcr-id-1 current-value aik-0) (4 1))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)))
  (label 22)
  (parent 21)
  (unrealized (0 0) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (4 2))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 23)
  (parent 22)
  (unrealized (0 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (5 1))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 24)
  (parent 23)
  (unrealized (0 0) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n
    (6 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 25)
  (parent 24)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pval) (tpm tpm-0 tpm-1 tpm-2 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule genStV-if-hashed-tpm-quote trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))))
  (label 26)
  (parent 25)
  (unrealized (7 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pt-3 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 2) (0 0)) ((8 2) (7 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 1))
  (strand-map 0 1 2 3 4 5 6 7)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))))
  (label 27)
  (parent 26)
  (unrealized (8 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 pcr-id-3 text)
    (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpm tpm-0 tpm-1 tpm-2 tpm-3 tpm-4 chan) (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-3) (tpm tpm-4) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 1))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((recv tpm-4 (cat "extend" pcr-id-3 n)) (load pcr-0 (cat pt-4 "0"))
      (stor pcr-0 (cat pt-3 (hash "0" n)))))
  (label 28)
  (parent 27)
  (unrealized (9 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-3 pcr-id-0) (tpm-4 tpm)) n
    (9 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr-0 (cat pt-4 "0"))
      (stor pcr-0 (cat pt-3 (hash "0" n)))))
  (label 29)
  (parent 28)
  (realized)
  (shape)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (tpm tpm))))
  (origs (pt-3 (9 2)) (pt-2 (8 2)) (pt-0 (6 2)) (pt (5 2)) (k (3 1))
    (n (2 0)) (v (2 3))))

(comment "Nothing left to do")

(defprotocol envelope-plus basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule ordered-extends
    (forall ((y z strd) (pcr locn))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "pcr" y pcr)
          (p "tpm-extend-enc" "pcr" z pcr))
        (or
          (= y z)
          (prec y (idx 2) z (idx 1))
          (prec z (idx 2) y (idx 1))))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpm)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 30)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (precedes ((1 3) (0 0)))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpm)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 31)
  (parent 30)
  (unrealized (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id text) (k aik akey) (tpm tpm-0 chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik) (1 2))
  (strand-map 0 1)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))))
  (label 32)
  (parent 31)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (2 0))
  (strand-map 0 1 2)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))))
  (label 33)
  (parent 32)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (current-value mesg) (v n data) (pcr-id pcr-id-0 text)
    (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v) (current-value current-value)
    (pcr-id pcr-id-0) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (0 0) (enc v k))
  (strand-map 0 1 2)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 current-value aik-0))
      (load pcr (cat pt current-value)) (send v)))
  (label 34)
  (parent 33)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id text) (k aik akey) (pt pval) (tpm tpm-0 chan)
    (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 4 2 tpm-create-key 2)
    (enc "created" k pcr-id-0 current-value aik-0) (3 1))
  (strand-map 0 1 2 3)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)))
  (label 35)
  (parent 34)
  (unrealized (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pval)
    (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (3 2))
  (strand-map 0 1 2 3)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 36)
  (parent 35)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-1) (tpm tpm-2) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1))
  (strand-map 0 1 2 3 4)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm-2 (cat "extend" pcr-id-1 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 37)
  (parent 36)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id) (tpm tpm) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-1 pcr-id) (tpm-2 tpm)) n
    (5 0) (ch-msg tpm (cat "extend" pcr-id n)))
  (strand-map 0 1 2 3 4 5)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 38)
  (parent 37)
  (realized)
  (shape)
  (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))))
  (origs (pt-0 (5 2)) (pt (4 2)) (k (2 1)) (n (1 0)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope-plus basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule ordered-extends
    (forall ((y z strd) (pcr locn))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "pcr" y pcr)
          (p "tpm-extend-enc" "pcr" z pcr))
        (or
          (= y z)
          (prec y (idx 2) z (idx 1))
          (prec z (idx 2) y (idx 1))))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 39)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (precedes ((1 3) (0 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 40)
  (parent 39)
  (unrealized (0 0) (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (1 2))
  (strand-map 0 1)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0
       (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 41)
  (parent 40)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 42)
  (parent 41)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval)
    (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-quote)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))))
  (label 43)
  (parent 42)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "refuse"))) (3 1))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse")))))
  (label 44)
  (parent 43)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 45)
  (parent 44)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n
    (5 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 46)
  (parent 45)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (tpm tpm))))
  (origs (pt-0 (5 2)) (pt (4 2)) (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope-plus basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule ordered-extends
    (forall ((y z strd) (pcr locn))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "pcr" y pcr)
          (p "tpm-extend-enc" "pcr" z pcr))
        (or
          (= y z)
          (prec y (idx 2) z (idx 1))
          (prec z (idx 2) y (idx 1))))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 47)
  (unrealized (0 0) (1 0) (2 2))
  (preskeleton)
  (origs (v (2 3)) (n (2 0)))
  (comment "Not a skeleton"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 48)
  (parent 47)
  (unrealized (0 0) (2 2))
  (origs (v (2 3)) (n (2 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (2 2))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0
       (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 49)
  (parent 48)
  (unrealized (0 0) (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 4 2 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 50)
  (parent 49)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (current-value mesg) (n v data) (pcr-id pcr-id-0 pcr-id-1 text)
    (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v) (current-value current-value)
    (pcr-id pcr-id-1) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-1 current-value aik-0))
      (load pcr (cat pt current-value)) (send v)))
  (label 51)
  (parent 50)
  (unrealized (0 0) (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval)
    (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 5 3 tpm-create-key 2)
    (enc "created" k pcr-id-1 current-value aik-0) (4 1))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)))
  (label 52)
  (parent 51)
  (unrealized (0 0) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (4 2))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 53)
  (parent 52)
  (unrealized (0 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (5 1))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 54)
  (parent 53)
  (unrealized (0 0) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n
    (6 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 55)
  (parent 54)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pval) (tpm tpm-0 tpm-1 tpm-2 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule genStV-if-hashed-tpm-quote trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))))
  (label 56)
  (parent 55)
  (unrealized (7 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pt-3 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 2) (0 0)) ((8 2) (7 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 1))
  (strand-map 0 1 2 3 4 5 6 7)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))))
  (label 57)
  (parent 56)
  (unrealized (8 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 pcr-id-3 text)
    (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpm tpm-0 tpm-1 tpm-2 tpm-3 tpm-4 chan) (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-3) (tpm tpm-4) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 1))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((recv tpm-4 (cat "extend" pcr-id-3 n)) (load pcr-0 (cat pt-4 "0"))
      (stor pcr-0 (cat pt-3 (hash "0" n)))))
  (label 58)
  (parent 57)
  (unrealized (9 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-3 pcr-id-0) (tpm-4 tpm)) n
    (9 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr-0 (cat pt-4 "0"))
      (stor pcr-0 (cat pt-3 (hash "0" n)))))
  (label 59)
  (parent 58)
  (realized)
  (shape)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (tpm tpm))))
  (origs (pt-3 (9 2)) (pt-2 (8 2)) (pt-0 (6 2)) (pt (5 2)) (k (3 1))
    (n (2 0)) (v (2 3))))

(comment "Nothing left to do")

(defprotocol envelope-plus-2 basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule pcr-id-identifies-pcr
    (forall ((y z strd) (pcr-id text) (pcr pcr-0 locn))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "pcr-id" y pcr-id)
          (p "tpm-extend-enc" "pcr-id" z pcr-id)
          (p "tpm-extend-enc" "pcr" y pcr)
          (p "tpm-extend-enc" "pcr" z pcr-0))
        (= pcr pcr-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpm)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 60)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (precedes ((1 3) (0 0)))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpm)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 61)
  (parent 60)
  (unrealized (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id text) (k aik akey) (tpm tpm-0 chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik) (1 2))
  (strand-map 0 1)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))))
  (label 62)
  (parent 61)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id text) (k aik akey) (tpm chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (2 0))
  (strand-map 0 1 2)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))))
  (label 63)
  (parent 62)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (current-value mesg) (v n data) (pcr-id pcr-id-0 text)
    (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v) (current-value current-value)
    (pcr-id pcr-id-0) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig v n k)
  (conf tpm)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (0 0) (enc v k))
  (strand-map 0 1 2)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 current-value aik-0))
      (load pcr (cat pt current-value)) (send v)))
  (label 64)
  (parent 63)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id text) (k aik akey) (pt pval) (tpm tpm-0 chan)
    (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 4 2 tpm-create-key 2)
    (enc "created" k pcr-id-0 current-value aik-0) (3 1))
  (strand-map 0 1 2 3)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)))
  (label 65)
  (parent 64)
  (unrealized (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pval)
    (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (3 2))
  (strand-map 0 1 2 3)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 66)
  (parent 65)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-1) (tpm tpm-2) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1))
  (strand-map 0 1 2 3 4)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm-2 (cat "extend" pcr-id-1 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 67)
  (parent 66)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id) (tpm tpm) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 2)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-1 pcr-id) (tpm-2 tpm)) n
    (5 0) (ch-msg tpm (cat "extend" pcr-id n)))
  (strand-map 0 1 2 3 4 5)
  (traces ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-0 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 68)
  (parent 67)
  (realized)
  (shape)
  (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))))
  (origs (pt-0 (5 2)) (pt (4 2)) (k (2 1)) (n (1 0)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope-plus-2 basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule pcr-id-identifies-pcr
    (forall ((y z strd) (pcr-id text) (pcr pcr-0 locn))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "pcr-id" y pcr-id)
          (p "tpm-extend-enc" "pcr-id" z pcr-id)
          (p "tpm-extend-enc" "pcr" y pcr)
          (p "tpm-extend-enc" "pcr" z pcr-0))
        (= pcr pcr-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 69)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (precedes ((1 3) (0 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 70)
  (parent 69)
  (unrealized (0 0) (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (1 2))
  (strand-map 0 1)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0
       (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 71)
  (parent 70)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 72)
  (parent 71)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval)
    (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-quote)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))))
  (label 73)
  (parent 72)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "refuse"))) (3 1))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse")))))
  (label 74)
  (parent 73)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 75)
  (parent 74)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((4 2) (3 1)) ((5 2) (4 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n
    (5 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-1 (cat "extend" pcr-id-1 "refuse"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 76)
  (parent 75)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (tpm tpm))))
  (origs (pt-0 (5 2)) (pt (4 2)) (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope-plus-2 basic
  (defrole tpm-power-on
    (vars (current-value mesg) (pcr locn) (tpm chan))
    (trace (recv tpm "power on") (load pcr current-value)
      (stor pcr "0")))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (pcr-id text) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "extend" pcr-id value))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok")))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "quote" pcr-id nonce))
      (load pcr current-value)
      (send (enc "quote" pcr-id current-value nonce aik))))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan))
    (trace (recv tpm (cat "create-req" pcr-id pcrval))
      (send (enc "created" k pcr-id pcrval aik)))
    (non-orig (invk k))
    (uniq-orig k)
    (auth tpm))
  (defrole tpm-decrypt
    (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn)
      (tpm chan))
    (trace (recv tpm (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr-id current-value aik))
      (load pcr current-value) (send m))
    (non-orig aik))
  (defrole alice
    (vars (n v data) (pcr-id text) (k aik akey) (tpm chan))
    (trace (send tpm (cat "extend" pcr-id n))
      (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig aik)
    (uniq-orig n v)
    (conf tpm)
    (neq (k aik)))
  (defrule genStV-if-hashed-tpm-power-on
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-power-on" z (idx 2))
          (p "tpm-power-on" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-extend-enc
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-extend-enc" z (idx 2))
          (p "tpm-extend-enc" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-decrypt
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-decrypt" z (idx 3))
          (p "tpm-decrypt" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule genStV-if-hashed-tpm-quote
    (forall ((z strd) (v1 v2 mesg))
      (implies
        (and (p "tpm-quote" z (idx 2))
          (p "tpm-quote" "current-value" z (hash v1 v2)))
        (gen-st (hash v1 v2)))))
  (defrule pcr-id-identifies-pcr
    (forall ((y z strd) (pcr-id text) (pcr pcr-0 locn))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "pcr-id" y pcr-id)
          (p "tpm-extend-enc" "pcr-id" z pcr-id)
          (p "tpm-extend-enc" "pcr" y pcr)
          (p "tpm-extend-enc" "pcr" z pcr-0))
        (= pcr pcr-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defgenrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defgenrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false))))
  (defgenrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule trRl_tpm-power-on-at-2
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-power-on-at-1
    (forall ((z strd))
      (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2)))))
  (defgenrule trRl_tpm-extend-enc-at-1
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 77)
  (unrealized (0 0) (1 0) (2 2))
  (preskeleton)
  (origs (v (2 3)) (n (2 0)))
  (comment "Not a skeleton"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpm)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 78)
  (parent 77)
  (unrealized (0 0) (2 2))
  (origs (v (2 3)) (n (2 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (2 2))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm-0
       (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 79)
  (parent 78)
  (unrealized (0 0) (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation channel-test (displaced 4 2 alice 2)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))))
  (label 80)
  (parent 79)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (current-value mesg) (n v data) (pcr-id pcr-id-0 pcr-id-1 text)
    (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v) (current-value current-value)
    (pcr-id pcr-id-1) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig n v k)
  (conf tpm)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-1 current-value aik-0))
      (load pcr (cat pt current-value)) (send v)))
  (label 81)
  (parent 80)
  (unrealized (0 0) (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval)
    (tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 5 3 tpm-create-key 2)
    (enc "created" k pcr-id-1 current-value aik-0) (4 1))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)))
  (label 82)
  (parent 81)
  (unrealized (0 0) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (4 2))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 83)
  (parent 82)
  (unrealized (0 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (5 1))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 84)
  (parent 83)
  (unrealized (0 0) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n
    (6 0) (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n)))))
  (label 85)
  (parent 84)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pval) (tpm tpm-0 tpm-1 tpm-2 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)))
  (rule genStV-if-hashed-tpm-quote trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))))
  (label 86)
  (parent 85)
  (unrealized (7 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pt-3 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 2) (0 0)) ((8 2) (7 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 1))
  (strand-map 0 1 2 3 4 5 6 7)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))))
  (label 87)
  (parent 86)
  (unrealized (8 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 pcr-id-3 text)
    (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpm tpm-0 tpm-1 tpm-2 tpm-3 tpm-4 chan) (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-3) (tpm tpm-4) (pcr pcr-0))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1)))
  (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 1))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((recv tpm-4 (cat "extend" pcr-id-3 n)) (load pcr-0 (cat pt-4 "0"))
      (stor pcr-0 (cat pt-3 (hash "0" n)))))
  (label 88)
  (parent 87)
  (unrealized (9 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope-plus-2
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey)
    (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik)
    (tpm tpm))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm-2) (pcr pcr))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3)
    (pcr pcr))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0")
    (pcr-id pcr-id-0) (tpm tpm) (pcr pcr))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpm)
  (auth tpm)
  (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1)))
  (rule pcr-id-identifies-pcr trRl_tpm-extend-enc-at-1
    trRl_tpm-extend-enc-at-2)
  (operation nonce-test
    (contracted (pcr-0 pcr) (pcr-id-3 pcr-id-0) (tpm-4 tpm)) n (9 0)
    (ch-msg tpm (cat "extend" pcr-id-0 n)))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((send tpm (cat "extend" pcr-id-0 n))
      (send tpm
        (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain")))
      (send
        (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))
    ((recv tpm-0 (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))
      (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))
    ((recv tpm-1 (cat "extend" pcr-id-1 "obtain"))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0"))
      (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-2 (cat "quote" pcr-id (enc v k)))
      (load pcr (cat pt-2 (hash (hash "0" n) "refuse")))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv tpm-3 (cat "extend" pcr-id-2 "refuse"))
      (load pcr (cat pt-3 (hash "0" n)))
      (stor pcr (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-4 "0"))
      (stor pcr (cat pt-3 (hash "0" n)))))
  (label 89)
  (parent 88)
  (realized)
  (shape)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (tpm tpm))))
  (origs (pt-3 (9 2)) (pt-2 (8 2)) (pt-0 (6 2)) (pt (5 2)) (k (3 1))
    (n (2 0)) (v (2 3))))

(comment "Nothing left to do")