(herald "Envelope Protocol With Channels" (bound 15))

(comment "CPSA 4.4.3")
(comment "All input read from tst/chan-envelope.scm")
(comment "Strand count bounded at 15")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (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)))))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig v n)
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 0)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

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

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

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (operation encryption-test (displaced 3 1 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (2 0))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 3)
  (parent 2)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (pcrvals mesg) (v n data) (esk skey) (k aik aik-0 akey)
    (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals pcrvals) (k k) (aik aik-0)
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig esk aik aik-0 (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation nonce-test (added-strand tpm-decrypt 4) v (0 0) (enc v k))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcrvals aik-0)) (recv c pcrvals) (send v)))
  (label 4)
  (parent 3)
  (unrealized (3 1) (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 4 2 tpm-create-key 2)
    (enc "created" k pcrvals aik-0) (3 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v)))
  (label 5)
  (parent 4)
  (unrealized (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (3 2))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 6)
  (parent 5)
  (unrealized (4 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (3 2))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (enc "extend" "obtain" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 7)
  (parent 5)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend 3 (value n) (current-value "0") (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (cat "extend" n)) (recv c "0") (send c (hash "0" n))))
  (label 8)
  (parent 6)
  (unrealized (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (v n data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 9)
  (parent 6)
  (unrealized (5 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 6 1 alice 1)
    (enc "extend" n esk-0) (5 0))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 10)
  (parent 9)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (5 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 11)
  (parent 10)
  (realized)
  (shape)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (origs (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (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)))))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 12)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((1 3) (0 0)))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 13)
  (parent 12)
  (unrealized (0 0) (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk-0) (k k) (aik aik))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k (hash (hash "0" n) "obtain") aik) (1 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 14)
  (parent 13)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (displaced 3 1 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (2 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 15)
  (parent 14)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik) (0 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))))
  (label 16)
  (parent 15)
  (unrealized (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "refuse")) (3 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse"))))
  (label 17)
  (parent 16)
  (unrealized (4 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "refuse")) (3 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (enc "extend" "refuse" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse"))))
  (label 18)
  (parent 16)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend 3 (value n) (current-value "0") (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (cat "extend" n)) (recv c "0") (send c (hash "0" n))))
  (label 19)
  (parent 17)
  (unrealized (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 20)
  (parent 17)
  (unrealized (5 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 6 1 alice 1)
    (enc "extend" n esk-0) (5 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 21)
  (parent 20)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (5 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 22)
  (parent 21)
  (realized)
  (shape)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (origs (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (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)))))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 23)
  (unrealized (0 0) (1 0) (2 2))
  (preskeleton)
  (origs (v (2 3)) (n (2 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 24)
  (parent 23)
  (unrealized (0 0) (2 2))
  (origs (v (2 3)) (n (2 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk-0) (k k) (aik aik))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k (hash (hash "0" n) "obtain") aik) (2 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 25)
  (parent 24)
  (unrealized (0 0) (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (displaced 4 2 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (3 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 26)
  (parent 25)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (pcrvals mesg) (n v data) (esk skey) (k aik aik-0 akey)
    (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals pcrvals) (k k) (aik aik-0)
    (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig esk aik aik-0 (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcrvals aik-0)) (recv c pcrvals) (send v)))
  (label 27)
  (parent 26)
  (unrealized (0 0) (4 1) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 5 3 tpm-create-key 2)
    (enc "created" k pcrvals aik-0) (4 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v)))
  (label 28)
  (parent 27)
  (unrealized (0 0) (4 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (4 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 29)
  (parent 28)
  (unrealized (0 0) (5 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (4 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (enc "extend" "obtain" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 30)
  (parent 28)
  (unrealized (0 0) (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend 3 (value n) (current-value "0") (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash "0" n)) (5 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (cat "extend" n)) (recv c "0") (send c (hash "0" n))))
  (label 31)
  (parent 29)
  (unrealized (0 0) (6 0) (6 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (5 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 32)
  (parent 29)
  (unrealized (0 0) (6 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 7 2 alice 1)
    (enc "extend" n esk-0) (6 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 33)
  (parent 32)
  (unrealized (0 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (6 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 34)
  (parent 33)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik) (0 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))))
  (label 35)
  (parent 34)
  (unrealized (8 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c-0 (hash (hash "0" n) "refuse")) (8 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse"))))
  (label 36)
  (parent 35)
  (unrealized (9 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (esk esk-0) (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c-0 (hash (hash "0" n) "refuse")) (8 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (enc "extend" "refuse" esk-0)) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse"))))
  (label 37)
  (parent 35)
  (unrealized (9 0) (9 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend 3 (value n) (current-value "0") (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c-0 (hash "0" n)) (9 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (cat "extend" n)) (recv c-0 "0") (send c-0 (hash "0" n))))
  (label 38)
  (parent 36)
  (unrealized (10 0) (10 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((6 2) (9 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (displaced 10 6 tpm-extend-enc 3)
    (ch-msg c-0 (hash "0" n)) (9 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse"))))
  (label 39)
  (parent 36)
  (realized)
  (shape)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (origs (n (2 0)) (k (3 1)) (v (2 3))))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c-0 (hash "0" n)) (9 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk-0)) (recv c-0 "0")
      (send c-0 (hash "0" n))))
  (label 40)
  (parent 36)
  (unrealized (10 0) (10 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation encryption-test (displaced 11 2 alice 1)
    (enc "extend" n esk-0) (10 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c-0 "0")
      (send c-0 (hash "0" n))))
  (label 41)
  (parent 40)
  (unrealized (10 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((7 1) (10 1)) ((8 2) (0 0))
    ((9 2) (8 1)) ((10 2) (9 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (displaced 11 7 tpm-power-on 2)
    (ch-msg c-0 "0") (10 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 42)
  (parent 41)
  (realized)
  (shape)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (origs (n (2 0)) (k (3 1)) (v (2 3))))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c-0))
  (defstrand tpm-power-on 2 (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)) ((11 1) (10 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c-0 "0")
    (10 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c-0 "0") (send c-0 (hash "0" n)))
    ((recv "power on") (send c-0 "0")))
  (label 43)
  (parent 41)
  (realized)
  (shape)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (origs (n (2 0)) (k (3 1)) (v (2 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (defrule ordered-extends
    (forall ((y z strd) (c chan))
      (implies
        (and (p "tpm-extend" y (idx 3)) (p "tpm-extend" z (idx 3))
          (p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
        (or
          (= y z)
          (prec y (idx 2) z (idx 3))
          (prec z (idx 2) y (idx 3))))))
  (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)))))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig v n)
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 44)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((1 3) (0 0)))
  (non-orig esk aik)
  (uniq-orig v n)
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 45)
  (parent 44)
  (unrealized (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (operation encryption-test (displaced 3 1 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (2 0))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 47)
  (parent 46)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (pcrvals mesg) (v n data) (esk skey) (k aik aik-0 akey)
    (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals pcrvals) (k k) (aik aik-0)
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig esk aik aik-0 (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation nonce-test (added-strand tpm-decrypt 4) v (0 0) (enc v k))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcrvals aik-0)) (recv c pcrvals) (send v)))
  (label 48)
  (parent 47)
  (unrealized (3 1) (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 4 2 tpm-create-key 2)
    (enc "created" k pcrvals aik-0) (3 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v)))
  (label 49)
  (parent 48)
  (unrealized (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (3 2))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 50)
  (parent 49)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (3 2))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (enc "extend" "obtain" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 51)
  (parent 49)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (v n data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 52)
  (parent 50)
  (unrealized (5 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 6 1 alice 1)
    (enc "extend" n esk-0) (5 0))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 53)
  (parent 52)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (5 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 54)
  (parent 53)
  (realized)
  (shape)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (origs (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (defrule ordered-extends
    (forall ((y z strd) (c chan))
      (implies
        (and (p "tpm-extend" y (idx 3)) (p "tpm-extend" z (idx 3))
          (p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
        (or
          (= y z)
          (prec y (idx 2) z (idx 3))
          (prec z (idx 2) y (idx 3))))))
  (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)))))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 55)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((1 3) (0 0)))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 56)
  (parent 55)
  (unrealized (0 0) (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk-0) (k k) (aik aik))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k (hash (hash "0" n) "obtain") aik) (1 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 57)
  (parent 56)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (displaced 3 1 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (2 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 58)
  (parent 57)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik) (0 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))))
  (label 59)
  (parent 58)
  (unrealized (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "refuse")) (3 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse"))))
  (label 60)
  (parent 59)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "refuse")) (3 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (enc "extend" "refuse" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse"))))
  (label 61)
  (parent 59)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 62)
  (parent 60)
  (unrealized (5 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 6 1 alice 1)
    (enc "extend" n esk-0) (5 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 63)
  (parent 62)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (5 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 64)
  (parent 63)
  (realized)
  (shape)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (origs (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (defrule ordered-extends
    (forall ((y z strd) (c chan))
      (implies
        (and (p "tpm-extend" y (idx 3)) (p "tpm-extend" z (idx 3))
          (p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
        (or
          (= y z)
          (prec y (idx 2) z (idx 3))
          (prec z (idx 2) y (idx 3))))))
  (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)))))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 65)
  (unrealized (0 0) (1 0) (2 2))
  (preskeleton)
  (origs (v (2 3)) (n (2 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 66)
  (parent 65)
  (unrealized (0 0) (2 2))
  (origs (v (2 3)) (n (2 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk-0) (k k) (aik aik))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k (hash (hash "0" n) "obtain") aik) (2 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 67)
  (parent 66)
  (unrealized (0 0) (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (displaced 4 2 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (3 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 68)
  (parent 67)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (pcrvals mesg) (n v data) (esk skey) (k aik aik-0 akey)
    (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals pcrvals) (k k) (aik aik-0)
    (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig esk aik aik-0 (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcrvals aik-0)) (recv c pcrvals) (send v)))
  (label 69)
  (parent 68)
  (unrealized (0 0) (4 1) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 5 3 tpm-create-key 2)
    (enc "created" k pcrvals aik-0) (4 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v)))
  (label 70)
  (parent 69)
  (unrealized (0 0) (4 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (4 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 71)
  (parent 70)
  (unrealized (0 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (4 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (enc "extend" "obtain" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 72)
  (parent 70)
  (unrealized (0 0) (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (5 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 73)
  (parent 71)
  (unrealized (0 0) (6 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 7 2 alice 1)
    (enc "extend" n esk-0) (6 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 74)
  (parent 73)
  (unrealized (0 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (6 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 75)
  (parent 74)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik) (0 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))))
  (label 76)
  (parent 75)
  (unrealized (8 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c-0 (hash (hash "0" n) "refuse")) (8 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse"))))
  (label 77)
  (parent 76)
  (unrealized (9 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (esk esk-0) (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c-0 (hash (hash "0" n) "refuse")) (8 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (enc "extend" "refuse" esk-0)) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse"))))
  (label 78)
  (parent 76)
  (unrealized (9 0) (9 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c-0 (hash "0" n)) (9 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk-0)) (recv c-0 "0")
      (send c-0 (hash "0" n))))
  (label 79)
  (parent 77)
  (unrealized (10 0) (10 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation encryption-test (displaced 11 2 alice 1)
    (enc "extend" n esk-0) (10 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c-0 "0")
      (send c-0 (hash "0" n))))
  (label 80)
  (parent 79)
  (unrealized (10 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c-0))
  (defstrand tpm-power-on 2 (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)) ((11 1) (10 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c-0 "0")
    (10 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c-0 "0") (send c-0 (hash "0" n)))
    ((recv "power on") (send c-0 "0")))
  (label 81)
  (parent 80)
  (realized)
  (shape)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (origs (n (2 0)) (k (3 1)) (v (2 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (defrule ordered-extends
    (forall ((y z strd) (c chan))
      (implies
        (and (p "tpm-extend" y (idx 3)) (p "tpm-extend" z (idx 3))
          (p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
        (or
          (= y z)
          (prec y (idx 2) z (idx 3))
          (prec z (idx 2) y (idx 3))))))
  (defrule esk-same-as-chan
    (forall ((y z strd) (esk skey) (c c-0 chan))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "esk" y esk)
          (p "tpm-extend-enc" "esk" z esk) (p "tpm-extend-enc" "c" y c)
          (p "tpm-extend-enc" "c" z c-0))
        (= c c-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig v n)
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 82)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((1 3) (0 0)))
  (non-orig esk aik)
  (uniq-orig v n)
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 83)
  (parent 82)
  (unrealized (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (operation encryption-test (displaced 3 1 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (2 0))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 85)
  (parent 84)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (pcrvals mesg) (v n data) (esk skey) (k aik aik-0 akey)
    (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals pcrvals) (k k) (aik aik-0)
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig esk aik aik-0 (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation nonce-test (added-strand tpm-decrypt 4) v (0 0) (enc v k))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcrvals aik-0)) (recv c pcrvals) (send v)))
  (label 86)
  (parent 85)
  (unrealized (3 1) (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 4 2 tpm-create-key 2)
    (enc "created" k pcrvals aik-0) (3 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v)))
  (label 87)
  (parent 86)
  (unrealized (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (3 2))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 88)
  (parent 87)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))
    ((4 2) (3 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (3 2))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (enc "extend" "obtain" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 89)
  (parent 87)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (v n data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 90)
  (parent 88)
  (unrealized (5 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 6 1 alice 1)
    (enc "extend" n esk-0) (5 0))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 91)
  (parent 90)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (v n data) (esk skey) (k aik akey) (c chan))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig v n k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (5 1))
  (traces ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 92)
  (parent 91)
  (realized)
  (shape)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (origs (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (defrule ordered-extends
    (forall ((y z strd) (c chan))
      (implies
        (and (p "tpm-extend" y (idx 3)) (p "tpm-extend" z (idx 3))
          (p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
        (or
          (= y z)
          (prec y (idx 2) z (idx 3))
          (prec z (idx 2) y (idx 3))))))
  (defrule esk-same-as-chan
    (forall ((y z strd) (esk skey) (c c-0 chan))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "esk" y esk)
          (p "tpm-extend-enc" "esk" z esk) (p "tpm-extend-enc" "c" y c)
          (p "tpm-extend-enc" "c" z c-0))
        (= c c-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 93)
  (unrealized (0 0) (1 2))
  (preskeleton)
  (origs (v (1 3)) (n (1 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((1 3) (0 0)))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 94)
  (parent 93)
  (unrealized (0 0) (1 2))
  (origs (v (1 3)) (n (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk-0) (k k) (aik aik))
  (precedes ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k (hash (hash "0" n) "obtain") aik) (1 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 95)
  (parent 94)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (displaced 3 1 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (2 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 96)
  (parent 95)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik) (0 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))))
  (label 97)
  (parent 96)
  (unrealized (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "refuse")) (3 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse"))))
  (label 98)
  (parent 97)
  (unrealized (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))
    ((4 2) (3 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "refuse")) (3 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (enc "extend" "refuse" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse"))))
  (label 99)
  (parent 97)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (4 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 100)
  (parent 98)
  (unrealized (5 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 6 1 alice 1)
    (enc "extend" n esk-0) (5 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 101)
  (parent 100)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
    ((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (5 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "quote" (enc v k)))
      (recv c (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 102)
  (parent 101)
  (realized)
  (shape)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (origs (n (1 0)) (k (2 1)) (v (1 3))))

(comment "Nothing left to do")

(defprotocol envelope basic
  (defrole tpm-power-on
    (vars (c chan))
    (trace (recv "power on") (send c "0"))
    (conf c)
    (auth c))
  (defrole tpm-extend
    (vars (value current-value mesg) (c chan))
    (trace (recv (cat "extend" value)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (conf c)
    (auth c))
  (defrole tpm-extend-enc
    (vars (value current-value mesg) (esk skey) (c chan))
    (trace (recv (enc "extend" value esk)) (recv c current-value)
      (send c (hash current-value value)) (send "ext ok"))
    (non-orig esk)
    (conf c)
    (auth c))
  (defrole tpm-quote
    (vars (nonce current-value mesg) (c chan) (aik akey))
    (trace (recv (cat "quote" nonce)) (recv c current-value)
      (send (enc "quote" current-value nonce aik)))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole tpm-create-key
    (vars (k aik akey) (pcrval mesg) (esk skey))
    (trace (recv (enc "create key" pcrval esk))
      (send (enc "created" k pcrval aik)))
    (non-orig esk aik (invk k))
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcrvals mesg) (k aik akey) (c chan))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
    (non-orig aik)
    (conf c)
    (auth c))
  (defrole alice
    (vars (n v data) (esk skey) (k aik akey))
    (trace (send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    (non-orig esk aik)
    (uniq-orig n v))
  (defrule ordered-extends
    (forall ((y z strd) (c chan))
      (implies
        (and (p "tpm-extend" y (idx 3)) (p "tpm-extend" z (idx 3))
          (p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
        (or
          (= y z)
          (prec y (idx 2) z (idx 3))
          (prec z (idx 2) y (idx 3))))))
  (defrule esk-same-as-chan
    (forall ((y z strd) (esk skey) (c c-0 chan))
      (implies
        (and (p "tpm-extend-enc" y (idx 3))
          (p "tpm-extend-enc" z (idx 3))
          (p "tpm-extend-enc" "esk" y esk)
          (p "tpm-extend-enc" "esk" z esk) (p "tpm-extend-enc" "c" y c)
          (p "tpm-extend-enc" "c" z c-0))
        (= c c-0))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 103)
  (unrealized (0 0) (1 0) (2 2))
  (preskeleton)
  (origs (v (2 3)) (n (2 0)))
  (comment "Not a skeleton"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)))
  (non-orig esk aik)
  (uniq-orig n v)
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k))))
  (label 104)
  (parent 103)
  (unrealized (0 0) (2 2))
  (origs (v (2 3)) (n (2 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk-0) (k k) (aik aik))
  (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k (hash (hash "0" n) "obtain") aik) (2 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 105)
  (parent 104)
  (unrealized (0 0) (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (operation encryption-test (displaced 4 2 alice 2)
    (enc "create key" (hash (hash "0" n) "obtain") esk-0) (3 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 106)
  (parent 105)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (pcrvals mesg) (n v data) (esk skey) (k aik aik-0 akey)
    (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals pcrvals) (k k) (aik aik-0)
    (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig esk aik aik-0 (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k pcrvals aik-0)) (recv c pcrvals) (send v)))
  (label 107)
  (parent 106)
  (unrealized (0 0) (4 1) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 5 3 tpm-create-key 2)
    (enc "created" k pcrvals aik-0) (4 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v)))
  (label 108)
  (parent 107)
  (unrealized (0 0) (4 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (4 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 109)
  (parent 108)
  (unrealized (0 0) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend-enc 3 (value "obtain")
    (current-value (hash "0" n)) (esk esk-0) (c c))
  (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2))
    ((4 3) (1 0)) ((5 2) (4 2)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash (hash "0" n) "obtain")) (4 2))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (enc "extend" "obtain" esk-0)) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain"))))
  (label 110)
  (parent 108)
  (unrealized (0 0) (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c (hash "0" n)) (5 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk-0)) (recv c "0") (send c (hash "0" n))))
  (label 111)
  (parent 109)
  (unrealized (0 0) (6 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation encryption-test (displaced 7 2 alice 1)
    (enc "extend" n esk-0) (6 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
  (label 112)
  (parent 111)
  (unrealized (0 0) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c)
  (auth c)
  (operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
    (6 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0")))
  (label 113)
  (parent 112)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik) (0 0))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))))
  (label 114)
  (parent 113)
  (unrealized (8 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
  (non-orig esk aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend 3)
    (ch-msg c-0 (hash (hash "0" n) "refuse")) (8 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse"))))
  (label 115)
  (parent 114)
  (unrealized (9 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend-enc 3 (value "refuse")
    (current-value (hash "0" n)) (esk esk-0) (c c-0))
  (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
    ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
    ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c-0 (hash (hash "0" n) "refuse")) (8 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (enc "extend" "refuse" esk-0)) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse"))))
  (label 116)
  (parent 114)
  (unrealized (9 0) (9 1))
  (dead)
  (comment "empty cohort"))

(defskeleton envelope
  (vars (n v data) (esk esk-0 skey) (k aik akey) (c c-0 chan))
  (deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
  (deflistener v)
  (defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
  (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
    (esk esk) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
    (k k) (aik aik) (c c))
  (defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
    (c c))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
    (c c))
  (defstrand tpm-power-on 2 (c c))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
  (defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
    (c c-0))
  (defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk-0)
    (c c-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
    ((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
    ((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
    ((10 2) (9 1)))
  (non-orig esk esk-0 aik (invk k))
  (uniq-orig n v k)
  (conf c c-0)
  (auth c c-0)
  (operation channel-test (added-strand tpm-extend-enc 3)
    (ch-msg c-0 (hash "0" n)) (9 1))
  (traces
    ((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv v) (send v))
    ((send (enc "extend" n esk))
      (send (enc "create key" (hash (hash "0" n) "obtain") esk))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (send (enc v k)))
    ((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik)))
    ((recv (cat "decrypt" (enc v k)))
      (recv (enc "created" k (hash (hash "0" n) "obtain") aik))
      (recv c (hash (hash "0" n) "obtain")) (send v))
    ((recv (cat "extend" "obtain")) (recv c (hash "0" n))
      (send c (hash (hash "0" n) "obtain")))
    ((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
    ((recv "power on") (send c "0"))
    ((recv (cat "quote" (enc v k)))
      (recv c-0 (hash (hash "0" n) "refuse"))
      (send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
    ((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
      (send c-0 (hash (hash "0" n) "refuse")))
    ((recv (enc "extend" n esk-0)) (recv c-0 "0")
      (send c-0 (hash "0" n))))
  (label 117)
  (parent 115)
  (unrealized (10 0) (10 1))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")