(herald "Envelope Protocol, location-based version" (check-nonces)
  (bound 30) (limit 6000))

(comment "CPSA 4.4.3")
(comment "All input read from tst/sync_locn_envelope.scm")
(comment "Step count limited to 6000")
(comment "Strand count bounded at 30")
(comment "Nonces checked first")

(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 nonce text) (pcr locn)
      (tpm chan))
    (trace (send tpm (cat "token" nonce))
      (recv tpm (cat "extend" pcr-id value (hash pcr-id value nonce)))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok"))
    (uniq-orig nonce))
  (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 nonce text) (k aik akey)
      (tpm tpmconf chan))
    (trace (recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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 tpmconf)
    (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 3))
          (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-3
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 2))))))

(defskeleton envelope
  (vars (v n data) (pcr-id nonce text) (k aik akey) (tpm tpmconf chan))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpmconf)
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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 3))
  (preskeleton)
  (origs (v (1 4)) (n (1 1)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (v n data) (pcr-id nonce text) (k aik akey) (tpm tpmconf chan))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (precedes ((1 4) (0 0)))
  (non-orig aik)
  (uniq-orig v n)
  (conf tpmconf)
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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 3))
  (origs (v (1 4)) (n (1 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id nonce text) (k aik akey)
    (tpm tpmconf tpm-0 chan))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0))
  (precedes ((1 4) (0 0)) ((2 1) (1 3)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpmconf)
  (auth tpm-0)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik) (1 3))
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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 nonce text) (k aik akey) (tpm tpmconf chan))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (precedes ((1 2) (2 0)) ((1 4) (0 0)) ((2 1) (1 3)))
  (non-orig aik (invk k))
  (uniq-orig v n k)
  (conf tpmconf)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 3)
    (ch-msg tpm-0
      (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (2 0))
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id nonce text) (k aik akey) (tpm tpmconf chan))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (tpm tpm))
  (precedes ((1 2) (2 0)) ((1 4) (0 0)) ((2 1) (1 3)) ((3 0) (1 0)))
  (non-orig aik (invk k))
  (uniq-orig v n nonce k)
  (conf tpmconf)
  (auth tpm)
  (operation channel-test (added-strand tpm-extend-enc 1)
    (ch-msg tpm (cat "token" nonce)) (1 0))
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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)))
    ((send tpm (cat "token" nonce))))
  (label 4)
  (parent 3)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (current-value mesg) (v n data) (pcr-id nonce pcr-id-0 text)
    (k aik aik-0 akey) (pt pval) (tpm tpmconf tpm-0 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 2) (2 0)) ((1 4) (4 0)) ((2 1) (1 3)) ((3 0) (1 0))
    ((4 3) (0 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig v n nonce k)
  (conf tpmconf)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (0 0) (enc v k))
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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 5)
  (parent 4)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id nonce text) (k aik akey) (pt pval)
    (tpm tpmconf tpm-0 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 2) (2 0)) ((1 4) (4 0)) ((2 1) (1 3)) ((3 0) (1 0))
    ((4 3) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig v n nonce k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 5 2 tpm-create-key 2)
    (enc "created" k pcr-id-0 current-value aik-0) (4 1))
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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 6)
  (parent 5)
  (unrealized (4 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (v n data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (pt pt-0 pval) (tpmconf tpm tpm-0 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm-0) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (precedes ((1 2) (2 0)) ((1 4) (3 0)) ((2 1) (1 3)) ((3 3) (0 0))
    ((4 0) (1 0)) ((4 3) (3 2)))
  (non-orig aik (invk k))
  (uniq-orig v n nonce k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm-0)
  (leads-to ((4 3) (3 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 3 5 tpm-extend-enc 4)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (4 2))
  (traces ((recv v) (send v))
    ((recv tpm-0 (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (send tpm-0
        (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)))
    ((recv tpm (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-0 "obtain" (hash pcr-id-0 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 7)
  (parent 6)
  (unrealized (4 1) (4 2))
  (dead)
  (comment "empty cohort"))

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

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

(defskeleton envelope
  (vars (v n data) (pcr-id nonce pcr-id-0 nonce-0 pcr-id-1 nonce-1 text)
    (k aik akey) (pt pt-0 pt-1 pval)
    (tpm tpmconf tpm-0 tpm-1 tpm-2 chan) (pcr locn))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-0) (nonce nonce-0)
    (tpm tpm-1) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-1) (nonce nonce-1) (tpm tpm-2) (pcr pcr))
  (precedes ((1 1) (6 1)) ((1 2) (2 0)) ((1 4) (4 0)) ((2 1) (1 3))
    ((3 0) (1 0)) ((4 3) (0 0)) ((5 3) (4 2)) ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig v n nonce nonce-0 nonce-1 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (5 2))
  (traces ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1
        (cat "extend" pcr-id-0 "obtain"
          (hash pcr-id-0 "obtain" nonce-0)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2 (cat "extend" pcr-id-1 n (hash pcr-id-1 n nonce-1)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 10)
  (parent 8)
  (unrealized (6 1))
  (dead)
  (comment "empty cohort"))

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

(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 nonce text) (pcr locn)
      (tpm chan))
    (trace (send tpm (cat "token" nonce))
      (recv tpm (cat "extend" pcr-id value (hash pcr-id value nonce)))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok"))
    (uniq-orig nonce))
  (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 nonce text) (k aik akey)
      (tpm tpmconf chan))
    (trace (recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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 tpmconf)
    (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 3))
          (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-3
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 2))))))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpmconf)
  (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 tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 12)
  (unrealized (0 0) (1 3))
  (preskeleton)
  (origs (v (1 4)) (n (1 1)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (precedes ((1 4) (0 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpmconf)
  (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 tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 13)
  (parent 12)
  (unrealized (0 0) (1 3))
  (origs (v (1 4)) (n (1 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (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 4) (0 0)) ((2 1) (1 3)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpmconf)
  (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 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 tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 14)
  (parent 13)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((1 2) (2 0)) ((1 4) (0 0)) ((2 1) (1 3)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpmconf)
  (auth tpm)
  (operation channel-test (displaced 3 1 alice 3)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (2 0))
  (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 tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 15)
  (parent 14)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (tpm tpm))
  (precedes ((1 2) (2 0)) ((1 4) (0 0)) ((2 1) (1 3)) ((3 0) (1 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (conf tpmconf)
  (auth tpm)
  (operation channel-test (added-strand tpm-extend-enc 1)
    (ch-msg tpm (cat "token" nonce)) (1 0))
  (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 tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce))))
  (label 16)
  (parent 15)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey) (pt pval)
    (tpm tpmconf tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 2) (2 0)) ((1 4) (4 0)) ((2 1) (1 3)) ((3 0) (1 0))
    ((4 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (gen-st (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (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))
  (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 tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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 17)
  (parent 16)
  (unrealized (4 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 nonce text) (k aik akey)
    (pt pt-0 pval) (tpmconf tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm-0) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (precedes ((1 2) (2 0)) ((1 4) (3 0)) ((2 1) (1 3)) ((3 2) (0 0))
    ((4 0) (1 0)) ((4 3) (3 1)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpm-0)
  (leads-to ((4 3) (3 1)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 3 5 tpm-extend-enc 4)
    (ch-msg pcr (cat pt (hash (hash "0" n) "refuse"))) (4 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)))
    ((recv tpm-0 (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (send tpm-0
        (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)))
    ((recv tpm (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)))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "refuse" (hash pcr-id-1 "refuse" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse")))))
  (label 18)
  (parent 17)
  (unrealized (4 1) (4 2))
  (dead)
  (comment "empty cohort"))

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

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 pcr-id-1 nonce pcr-id-2 nonce-0 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpmconf tpm tpm-0 tpm-1 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpm-1) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-1))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-2) (nonce nonce-0) (tpm tpm-1) (pcr pcr))
  (precedes ((1 1) (5 1)) ((1 2) (2 0)) ((1 4) (3 0)) ((2 1) (1 3))
    ((3 2) (0 0)) ((4 3) (3 1)) ((5 0) (1 0)) ((5 3) (4 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpm-1)
  (leads-to ((4 3) (3 1)) ((5 3) (4 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 3 6 tpm-extend-enc 4)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (5 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 tpm-1 (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpm-1
        (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-1
       (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 (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)))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "refuse" (hash pcr-id-1 "refuse" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 20)
  (parent 19)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 nonce pcr-id-1 nonce-0 pcr-id-2 nonce-1 text)
    (k aik akey) (pt pt-0 pt-1 pval)
    (tpm tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce-0)
    (tpm tpm-1) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-2) (nonce nonce-1) (tpm tpm-2) (pcr pcr))
  (precedes ((1 1) (6 1)) ((1 2) (2 0)) ((1 4) (4 0)) ((2 1) (1 3))
    ((3 0) (1 0)) ((4 2) (0 0)) ((5 3) (4 1)) ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 nonce-1 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpm)
  (leads-to ((5 3) (4 1)) ((6 3) (5 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (5 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 tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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)))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1
        (cat "extend" pcr-id-1 "refuse"
          (hash pcr-id-1 "refuse" nonce-0)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-1)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 21)
  (parent 19)
  (unrealized (6 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 nonce nonce-0 text)
    (k aik akey) (pt pt-0 pt-1 pval) (tpmconf tpm tpm-0 chan)
    (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (pcr pcr))
  (precedes ((1 1) (5 1)) ((1 2) (2 0)) ((1 4) (3 0)) ((2 1) (1 3))
    ((3 2) (0 0)) ((4 3) (3 1)) ((5 0) (1 0)) ((5 3) (4 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpmconf)
  (leads-to ((4 3) (3 1)) ((5 3) (4 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 6 1 alice 2)
    (ch-msg tpm-1 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-0)))
    (5 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)))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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)))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "refuse" (hash pcr-id-1 "refuse" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "refuse"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 22)
  (parent 20)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce-0) (tpm tpmconf) (tpmconf tpmconf))))
  (origs (n (1 1)) (nonce-0 (5 0)) (pt-0 (5 3)) (nonce (4 0)) (pt (4 3))
    (k (2 1)) (v (1 4))))

(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 nonce text) (pcr locn)
      (tpm chan))
    (trace (send tpm (cat "token" nonce))
      (recv tpm (cat "extend" pcr-id value (hash pcr-id value nonce)))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok"))
    (uniq-orig nonce))
  (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 nonce text) (k aik akey)
      (tpm tpmconf chan))
    (trace (recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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 tpmconf)
    (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 3))
          (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-3
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 2))))))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpmconf)
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 23)
  (unrealized (0 0) (1 0) (2 3))
  (preskeleton)
  (origs (v (2 4)) (n (2 1)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (precedes ((2 4) (0 0)) ((2 4) (1 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpmconf)
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 24)
  (parent 23)
  (unrealized (0 0) (2 3))
  (origs (v (2 4)) (n (2 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (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 4) (0 0)) ((2 4) (1 0)) ((3 1) (2 3)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpmconf)
  (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 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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 25)
  (parent 24)
  (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 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (1 0)) ((3 1) (2 3)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpmconf)
  (auth tpm)
  (operation channel-test (displaced 4 2 alice 3)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 26)
  (parent 25)
  (unrealized (0 0) (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (tpm tpm))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (1 0)) ((3 1) (2 3))
    ((4 0) (2 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (conf tpmconf)
  (auth tpm)
  (operation channel-test (added-strand tpm-extend-enc 1)
    (ch-msg tpm (cat "token" nonce)) (2 0))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce))))
  (label 27)
  (parent 26)
  (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 nonce pcr-id-1 text) (k aik aik-0 akey) (pt pval)
    (tpm tpmconf tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0)) ((3 1) (2 3))
    ((4 0) (2 0)) ((5 3) (1 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig n v nonce k)
  (conf tpmconf)
  (auth tpm)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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 28)
  (parent 27)
  (unrealized (0 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey) (pt pval)
    (tpm tpmconf tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0)) ((3 1) (2 3))
    ((4 0) (2 0)) ((5 3) (1 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 6 3 tpm-create-key 2)
    (enc "created" k pcr-id-1 current-value aik-0) (5 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))) ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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 29)
  (parent 28)
  (unrealized (0 0) (5 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 nonce text) (k aik akey)
    (pt pt-0 pval) (tpmconf tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm-0) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (4 0)) ((3 1) (2 3))
    ((4 3) (1 0)) ((5 0) (2 0)) ((5 3) (4 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm-0)
  (leads-to ((5 3) (4 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 4 6 tpm-extend-enc 4)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (5 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))
    ((recv tpm-0 (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (send tpm-0
        (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)))
    ((recv tpm (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 30)
  (parent 29)
  (unrealized (0 0) (5 1) (5 2))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce pcr-id-1 nonce-0 text)
    (k aik akey) (pt pt-0 pval) (tpm tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce-0)
    (tpm tpm-1) (pcr pcr))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0)) ((3 1) (2 3))
    ((4 0) (2 0)) ((5 3) (1 0)) ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (leads-to ((6 3) (5 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (5 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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1
        (cat "extend" pcr-id-1 "obtain"
          (hash pcr-id-1 "obtain" nonce-0)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 31)
  (parent 29)
  (unrealized (0 0) (6 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 pcr-id-1 nonce pcr-id-2 nonce-0 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpm-1) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-1))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-2) (nonce nonce-0) (tpm tpm-1) (pcr pcr))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (4 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm-1)
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 4 7 tpm-extend-enc 4)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (6 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))
    ((recv tpm-1 (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpm-1
        (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-1
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 32)
  (parent 31)
  (unrealized (0 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 nonce pcr-id-1 nonce-0 pcr-id-2 nonce-1 text)
    (k aik akey) (pt pt-0 pt-1 pval)
    (tpm tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce-0)
    (tpm tpm-1) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-2) (nonce nonce-1) (tpm tpm-2) (pcr pcr))
  (precedes ((2 1) (7 1)) ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0))
    ((3 1) (2 3)) ((4 0) (2 0)) ((5 3) (1 0)) ((6 3) (5 2))
    ((7 3) (6 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 nonce-1 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (leads-to ((6 3) (5 2)) ((7 3) (6 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (6 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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1
        (cat "extend" pcr-id-1 "obtain"
          (hash pcr-id-1 "obtain" nonce-0)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-1)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 33)
  (parent 31)
  (unrealized (0 0) (7 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 nonce nonce-0 text)
    (k aik akey) (pt pt-0 pt-1 pval) (tpmconf tpm tpm-0 chan)
    (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (pcr pcr))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (4 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpmconf)
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 7 2 alice 2)
    (ch-msg tpm-1 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-0)))
    (6 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))) ((recv v) (send v))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 34)
  (parent 32)
  (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 nonce nonce-0 text)
    (k aik akey) (pt pt-0 pt-1 pt-2 pval) (tpmconf tpm tpm-0 tpm-1 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (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-1) (pcr pcr-0))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (4 0)) ((2 4) (7 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)) ((7 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpmconf)
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)))
  (rule genStV-if-hashed-tpm-quote trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (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))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-1 (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 35)
  (parent 34)
  (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 nonce nonce-0 pcr-id-2 nonce-1 text)
    (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pval)
    (tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (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-1) (pcr pcr-0))
  (defstrand tpm-extend-enc 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (nonce nonce-1)
    (tpm tpm-2) (pcr pcr-0))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (4 0)) ((2 4) (7 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)) ((7 2) (0 0)) ((8 3) (7 1)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 nonce-1 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpmconf)
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)) ((8 3) (7 1)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 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))) ((recv v) (send v))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-1 (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)))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2
        (cat "extend" pcr-id-2 "refuse"
          (hash pcr-id-2 "refuse" nonce-1)))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))))
  (label 36)
  (parent 35)
  (unrealized (8 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 pcr-id-1 nonce nonce-0 pcr-id-2 nonce-1 pcr-id-3
      nonce-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (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-1) (pcr pcr-0))
  (defstrand tpm-extend-enc 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (nonce nonce-1)
    (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-3) (nonce nonce-2) (tpm tpm-3) (pcr pcr-0))
  (precedes ((2 1) (6 1)) ((2 1) (9 1)) ((2 2) (3 0)) ((2 4) (4 0))
    ((2 4) (7 0)) ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 0) (2 0)) ((6 3) (5 2)) ((7 2) (0 0)) ((8 3) (7 1))
    ((9 3) (8 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 nonce-1 nonce-2 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpmconf)
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)) ((8 3) (7 1)) ((9 3) (8 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 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))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-1 (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)))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2
        (cat "extend" pcr-id-2 "refuse"
          (hash pcr-id-2 "refuse" nonce-1)))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((send tpm-3 (cat "token" nonce-2))
      (recv tpm-3 (cat "extend" pcr-id-3 n (hash pcr-id-3 n nonce-2)))
      (load pcr-0 (cat pt-4 "0")) (stor pcr-0 (cat pt-3 (hash "0" n)))))
  (label 37)
  (parent 36)
  (unrealized (9 1))
  (dead)
  (comment "empty cohort"))

(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 nonce text) (pcr locn)
      (tpm chan))
    (trace (send tpm (cat "token" nonce))
      (recv tpm (cat "extend" pcr-id value (hash pcr-id value nonce)))
      (load pcr current-value) (stor pcr (hash current-value value))
      (send "ext ok"))
    (uniq-orig nonce))
  (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 nonce text) (k aik akey)
      (tpm tpmconf chan))
    (trace (recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id n (hash pcr-id n nonce)))
      (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 tpmconf)
    (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 3))
          (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-3
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 3)))))
  (defgenrule trRl_tpm-extend-enc-at-2
    (forall ((z strd))
      (implies (p "tpm-extend-enc" z (idx 4)) (trans z (idx 2))))))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpmconf)
  (facts (no-state-split))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 38)
  (unrealized (0 0) (1 0) (2 3))
  (preskeleton)
  (origs (v (2 4)) (n (2 1)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (precedes ((2 4) (0 0)) ((2 4) (1 0)))
  (non-orig aik)
  (uniq-orig n v)
  (conf tpmconf)
  (facts (no-state-split))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)
  (parent 38)
  (unrealized (0 0) (2 3))
  (origs (v (2 4)) (n (2 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf tpm-0 chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (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 4) (0 0)) ((2 4) (1 0)) ((3 1) (2 3)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpmconf)
  (auth tpm-0)
  (facts (no-state-split))
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 40)
  (parent 39)
  (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 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (1 0)) ((3 1) (2 3)))
  (non-orig aik (invk k))
  (uniq-orig n v k)
  (conf tpmconf)
  (auth tpm)
  (facts (no-state-split))
  (operation channel-test (displaced 4 2 alice 3)
    (ch-msg tpm-0
      (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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 41)
  (parent 40)
  (unrealized (0 0) (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey)
    (tpm tpmconf chan))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (tpm tpm))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (1 0)) ((3 1) (2 3))
    ((4 0) (2 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (conf tpmconf)
  (auth tpm)
  (facts (no-state-split))
  (operation channel-test (added-strand tpm-extend-enc 1)
    (ch-msg tpm (cat "token" nonce)) (2 0))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce))))
  (label 42)
  (parent 41)
  (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 nonce pcr-id-1 text) (k aik aik-0 akey) (pt pval)
    (tpm tpmconf tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0)) ((3 1) (2 3))
    ((4 0) (2 0)) ((5 3) (1 0)))
  (non-orig aik aik-0 (invk k))
  (uniq-orig n v nonce k)
  (conf tpmconf)
  (auth tpm)
  (facts (no-state-split))
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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 43)
  (parent 42)
  (unrealized (0 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce text) (k aik akey) (pt pval)
    (tpm tpmconf tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0)) ((3 1) (2 3))
    ((4 0) (2 0)) ((5 3) (1 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (gen-st (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (facts (no-state-split))
  (rule genStV-if-hashed-tpm-decrypt)
  (operation encryption-test (displaced 6 3 tpm-create-key 2)
    (enc "created" k pcr-id-1 current-value aik-0) (5 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))) ((recv v) (send v))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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 44)
  (parent 43)
  (unrealized (0 0) (5 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 nonce text) (k aik akey)
    (pt pt-0 pval) (tpmconf tpm tpm-0 chan) (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm-0) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (4 0)) ((3 1) (2 3))
    ((4 3) (1 0)) ((5 0) (2 0)) ((5 3) (4 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm-0)
  (facts (no-state-split))
  (leads-to ((5 3) (4 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 4 6 tpm-extend-enc 4)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (5 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))
    ((recv tpm-0 (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (send tpm-0
        (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)))
    ((recv tpm (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 45)
  (parent 44)
  (unrealized (0 0) (5 1) (5 2))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 nonce pcr-id-1 nonce-0 text)
    (k aik akey) (pt pt-0 pval) (tpm tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce-0)
    (tpm tpm-1) (pcr pcr))
  (precedes ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0)) ((3 1) (2 3))
    ((4 0) (2 0)) ((5 3) (1 0)) ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (facts (no-state-split))
  (leads-to ((6 3) (5 2)))
  (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (5 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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1
        (cat "extend" pcr-id-1 "obtain"
          (hash pcr-id-1 "obtain" nonce-0)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain")))))
  (label 46)
  (parent 44)
  (unrealized (0 0) (6 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 pcr-id-1 nonce pcr-id-2 nonce-0 text) (k aik akey)
    (pt pt-0 pt-1 pval) (tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpm-1) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-1))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-2) (nonce nonce-0) (tpm tpm-1) (pcr pcr))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (4 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm-1)
  (facts (no-state-split))
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 4 7 tpm-extend-enc 4)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (6 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))
    ((recv tpm-1 (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpm-1
        (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-1
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 47)
  (parent 46)
  (unrealized (0 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 nonce pcr-id-1 nonce-0 pcr-id-2 nonce-1 text)
    (k aik akey) (pt pt-0 pt-1 pval)
    (tpm tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce) (k k)
    (aik aik) (tpm tpm) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm))
  (defstrand tpm-extend-enc 1 (nonce nonce) (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 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce-0)
    (tpm tpm-1) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-2) (nonce nonce-1) (tpm tpm-2) (pcr pcr))
  (precedes ((2 1) (7 1)) ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (5 0))
    ((3 1) (2 3)) ((4 0) (2 0)) ((5 3) (1 0)) ((6 3) (5 2))
    ((7 3) (6 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 nonce-1 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpm)
  (facts (no-state-split))
  (leads-to ((6 3) (5 2)) ((7 3) (6 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr (cat pt-0 (hash "0" n))) (6 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))
    ((recv tpm (cat "token" nonce))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce)))
      (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)))
    ((send tpm (cat "token" nonce)))
    ((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))
    ((send tpm-1 (cat "token" nonce-0))
      (recv tpm-1
        (cat "extend" pcr-id-1 "obtain"
          (hash pcr-id-1 "obtain" nonce-0)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-1)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 48)
  (parent 46)
  (unrealized (0 0) (7 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 nonce nonce-0 text)
    (k aik akey) (pt pt-0 pt-1 pval) (tpmconf tpm tpm-0 chan)
    (pcr locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (pcr pcr))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (0 0)) ((2 4) (4 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain"))
  (conf tpmconf)
  (auth tpmconf)
  (facts (no-state-split))
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (displaced 7 2 alice 2)
    (ch-msg tpm-1 (cat "extend" pcr-id-2 n (hash pcr-id-2 n nonce-0)))
    (6 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))) ((recv v) (send v))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))))
  (label 49)
  (parent 47)
  (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 nonce nonce-0 text)
    (k aik akey) (pt pt-0 pt-1 pt-2 pval) (tpmconf tpm tpm-0 tpm-1 chan)
    (pcr pcr-0 locn))
  (deflistener
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (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-1) (pcr pcr-0))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (4 0)) ((2 4) (7 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)) ((7 2) (0 0)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpmconf)
  (facts (no-state-split))
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)))
  (rule genStV-if-hashed-tpm-quote trRl_tpm-extend-enc-at-2
    trRl_tpm-extend-enc-at-3)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (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))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-1 (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 50)
  (parent 49)
  (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 nonce nonce-0 pcr-id-2 nonce-1 text)
    (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pval)
    (tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (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-1) (pcr pcr-0))
  (defstrand tpm-extend-enc 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (nonce nonce-1)
    (tpm tpm-2) (pcr pcr-0))
  (precedes ((2 1) (6 1)) ((2 2) (3 0)) ((2 4) (4 0)) ((2 4) (7 0))
    ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 0) (2 0))
    ((6 3) (5 2)) ((7 2) (0 0)) ((8 3) (7 1)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 nonce-1 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpmconf)
  (facts (no-state-split))
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)) ((8 3) (7 1)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 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))) ((recv v) (send v))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-1 (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)))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2
        (cat "extend" pcr-id-2 "refuse"
          (hash pcr-id-2 "refuse" nonce-1)))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))))
  (label 51)
  (parent 50)
  (unrealized (8 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data)
    (pcr-id pcr-id-0 pcr-id-1 nonce nonce-0 pcr-id-2 nonce-1 pcr-id-3
      nonce-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval)
    (tpmconf 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 5 (n n) (v v) (pcr-id pcr-id-0) (nonce nonce-0) (k k)
    (aik aik) (tpm tpmconf) (tpmconf tpmconf))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpmconf))
  (defstrand tpm-decrypt 4 (m v)
    (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k)
    (aik aik) (tpm tpm) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value "obtain")
    (current-value (hash "0" n)) (pcr-id pcr-id-1) (nonce nonce)
    (tpm tpm-0) (pcr pcr))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-0) (nonce nonce-0) (tpm tpmconf) (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-1) (pcr pcr-0))
  (defstrand tpm-extend-enc 4 (value "refuse")
    (current-value (hash "0" n)) (pcr-id pcr-id-2) (nonce nonce-1)
    (tpm tpm-2) (pcr pcr-0))
  (defstrand tpm-extend-enc 4 (value n) (current-value "0")
    (pcr-id pcr-id-3) (nonce nonce-2) (tpm tpm-3) (pcr pcr-0))
  (precedes ((2 1) (6 1)) ((2 1) (9 1)) ((2 2) (3 0)) ((2 4) (4 0))
    ((2 4) (7 0)) ((3 1) (2 3)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 0) (2 0)) ((6 3) (5 2)) ((7 2) (0 0)) ((8 3) (7 1))
    ((9 3) (8 2)))
  (non-orig aik (invk k))
  (uniq-orig n v nonce nonce-0 nonce-1 nonce-2 k)
  (gen-st (hash "0" n) (hash (hash "0" n) "obtain")
    (hash (hash "0" n) "refuse"))
  (conf tpmconf)
  (auth tpmconf)
  (facts (no-state-split))
  (leads-to ((5 3) (4 2)) ((6 3) (5 2)) ((8 3) (7 1)) ((9 3) (8 2)))
  (rule trRl_tpm-extend-enc-at-2 trRl_tpm-extend-enc-at-3)
  (operation channel-test (added-strand tpm-extend-enc 4)
    (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 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))
    ((recv tpmconf (cat "token" nonce-0))
      (send tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (send tpmconf
        (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 tpmconf
       (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 (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))
    ((send tpm-0 (cat "token" nonce))
      (recv tpm-0
        (cat "extend" pcr-id-1 "obtain" (hash pcr-id-1 "obtain" nonce)))
      (load pcr (cat pt-0 (hash "0" n)))
      (stor pcr (cat pt (hash (hash "0" n) "obtain"))))
    ((send tpmconf (cat "token" nonce-0))
      (recv tpmconf (cat "extend" pcr-id-0 n (hash pcr-id-0 n nonce-0)))
      (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))
    ((recv tpm-1 (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)))
    ((send tpm-2 (cat "token" nonce-1))
      (recv tpm-2
        (cat "extend" pcr-id-2 "refuse"
          (hash pcr-id-2 "refuse" nonce-1)))
      (load pcr-0 (cat pt-3 (hash "0" n)))
      (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))
    ((send tpm-3 (cat "token" nonce-2))
      (recv tpm-3 (cat "extend" pcr-id-3 n (hash pcr-id-3 n nonce-2)))
      (load pcr-0 (cat pt-4 "0")) (stor pcr-0 (cat pt-3 (hash "0" n)))))
  (label 52)
  (parent 51)
  (unrealized (9 1))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")