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

(comment "CPSA 4.4.7")
(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 discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (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 discreteBefore
    (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)))))
  (defgenrule eff-tpm-quote-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule eff-tpm-decrypt-3
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i)))))))

(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)
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 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-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))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 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))))
  (label 3)
  (parent 2)
  (unrealized (0 0) (1 0))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 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))))
  (label 4)
  (parent 3)
  (unrealized (0 0))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 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 (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))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 4 3)
  (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)
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm-0) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 5 3 4)
  (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))
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce-0) (k k) (aik aik)
        (tpm tpm-1) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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)
  (maps
    ((0 1)
      ((v v) (n n) (pcr-id pcr-id) (nonce nonce) (k k) (aik aik)
        (tpm tpm) (tpmconf tpmconf))))
  (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)))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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 discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (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 discreteBefore
    (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)))))
  (defgenrule eff-tpm-quote-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule eff-tpm-decrypt-3
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i)))))))

(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)
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((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))
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv 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))
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv 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))
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv 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))
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 4 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-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)
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm-0) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv 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))
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 5 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv 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))
  (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 tpm-1) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv 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)
  (maps
    ((0 1)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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)))
  (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))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik)))
    ((recv 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 discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (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 discreteBefore
    (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)))))
  (defgenrule eff-tpm-quote-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule eff-tpm-decrypt-3
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i)))))))

(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)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 5 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm-0) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 6 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce-0) (tpm tpm-1) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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)))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((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))))
  (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)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((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))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((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))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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)
  (maps
    ((0 1 2)
      ((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))))
  (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 discreteAfter
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (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 discreteBefore
    (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)))))
  (defgenrule eff-tpm-quote-2
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i))
        (or (= z z1)
          (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i))))))
  (defgenrule eff-tpm-decrypt-3
    (forall ((i indx) (z1 z strd))
      (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i))
        (or (= z z1)
          (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i)))))))

(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)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 5 4)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm-0) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 6 4 5)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce-0) (tpm tpm-1) (tpmconf tpmconf))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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)
  (maps
    ((0 1 2)
      ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0)
        (nonce nonce) (tpm tpm) (tpmconf tpmconf))))
  (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)))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((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))))
  (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)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)
    (0 0))
  (strand-map 0 1 2 3 4 5 6)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((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))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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))
  (maps
    ((0 1 2)
      ((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))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (traces
    ((recv
       (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))
      (send
        (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k)
          aik))) ((recv v) (send v))
    ((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)
  (maps
    ((0 1 2)
      ((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))))
  (comment "empty cohort"))

(comment "Nothing left to do")