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

(comment "CPSA 4.4.7")
(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)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 2)
  (parent 1)
  (unrealized (0 0) (2 0))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 3)
  (parent 2)
  (unrealized (0 0))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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))
      (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4)
  (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)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 14)
  (parent 13)
  (unrealized (0 0) (2 0))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 15)
  (parent 14)
  (unrealized (0 0))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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))
      (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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)))
    ((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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9 10)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9 10)
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9 10)
  (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" z (idx 3)) (p "tpm-extend" y (idx 3))
          (p "tpm-extend" "c" z c) (p "tpm-extend" "c" y 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)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 46)
  (parent 45)
  (unrealized (0 0) (2 0))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 47)
  (parent 46)
  (unrealized (0 0))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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))
      (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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" z (idx 3)) (p "tpm-extend" y (idx 3))
          (p "tpm-extend" "c" z c) (p "tpm-extend" "c" y 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)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 57)
  (parent 56)
  (unrealized (0 0) (2 0))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 58)
  (parent 57)
  (unrealized (0 0))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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))
      (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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" z (idx 3)) (p "tpm-extend" y (idx 3))
          (p "tpm-extend" "c" z c) (p "tpm-extend" "c" y 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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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)))
    ((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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9 10)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9 10)
  (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" z (idx 3)) (p "tpm-extend" y (idx 3))
          (p "tpm-extend" "c" z c) (p "tpm-extend" "c" y 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" z (idx 3))
          (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "c" z c-0)
          (p "tpm-extend-enc" "c" y c) (p "tpm-extend-enc" "esk" z esk)
          (p "tpm-extend-enc" "esk" y esk))
        (= 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)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 84)
  (parent 83)
  (unrealized (0 0) (2 0))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 85)
  (parent 84)
  (unrealized (0 0))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 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))
      (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3)
  (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)
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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" z (idx 3)) (p "tpm-extend" y (idx 3))
          (p "tpm-extend" "c" z c) (p "tpm-extend" "c" y 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" z (idx 3))
          (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "c" z c-0)
          (p "tpm-extend-enc" "c" y c) (p "tpm-extend-enc" "esk" z esk)
          (p "tpm-extend-enc" "esk" y esk))
        (= 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)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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-0))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 95)
  (parent 94)
  (unrealized (0 0) (2 0))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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))
      (send (enc "created" k (hash (hash "0" n) "obtain") aik))))
  (label 96)
  (parent 95)
  (unrealized (0 0))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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))
      (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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)
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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" z (idx 3)) (p "tpm-extend" y (idx 3))
          (p "tpm-extend" "c" z c) (p "tpm-extend" "c" y 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" z (idx 3))
          (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "c" z c-0)
          (p "tpm-extend-enc" "c" y c) (p "tpm-extend-enc" "esk" z esk)
          (p "tpm-extend-enc" "esk" y esk))
        (= 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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 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)))
    ((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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (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))
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (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))
  (strand-map 0 1 2 3 4 5 6 7 8 9)
  (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)
  (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
  (comment "empty cohort"))

(comment "Nothing left to do")