(herald "Envelope Protocol" (bound 20))
(comment "CPSA 3.4.0")
(comment "All input read from envelope.scm")
(comment "Strand count bounded at 20")

Trees: 0 59.

Tree 0.

(defprotocol envelope basic
  (defrole tpm-power-on (vars) (trace (init "0")))
  (defrole tpm-quote
    (vars (nonce pcr mesg) (aik akey))
    (trace (recv (cat "quote" nonce)) (obsv pcr)
      (send (enc "quote" pcr nonce aik)))
    (non-orig aik))
  (defrole tpm-extend-enc
    (vars (value state mesg) (esk skey) (tne tno data) (tpmkey akey))
    (trace (recv (cat "establish transport" tpmkey (enc esk tpmkey)))
      (send (cat "establish transport" tne))
      (recv
        (cat "execute transport" (cat "extend" (enc value esk)) tno
          "false"
          (hash esk
            (hash "execute transport" (hash "extend" (enc value esk)))
            tne tno "false"))) (tran state (hash value state)))
    (non-orig (invk tpmkey))
    (uniq-orig tne))
  (defrole tpm-create-key
    (vars (k aik akey) (pcr mesg) (esk skey))
    (trace (recv (enc "create key" pcr esk))
      (send (enc "created" k pcr aik)))
    (non-orig (invk k) aik esk)
    (uniq-orig k))
  (defrole tpm-decrypt
    (vars (m pcr mesg) (k aik akey))
    (trace (recv (cat "decrypt" (enc m k)))
      (recv (enc "created" k pcr aik)) (obsv pcr) (send m))
    (non-orig aik))
  (defrole alice
    (vars (v n tne tno data) (esk1 esk skey) (k aik tpmkey akey)
      (pcr mesg))
    (trace (send (cat "establish transport" tpmkey (enc esk tpmkey)))
      (recv (cat "establish transport" tne))
      (send
        (cat "execute transport" (cat "extend" (enc n esk)) tno "false"
          (hash esk
            (hash "execute transport" (hash "extend" (enc n esk))) tne
            tno "false"))) (recv pcr)
      (send (enc "create key" (hash "obtain" (hash n pcr)) esk1))
      (recv (enc "created" k (hash "obtain" (hash n pcr)) aik))
      (send (enc v k)))
    (non-orig aik esk1 (invk tpmkey))
    (uniq-orig v n tno esk)
    (neq (tno n))))

Item 0, Child: 1.

(defskeleton envelope
  (vars (pcr mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (neq (tno n))
  (non-orig esk1 aik (invk tpmkey))
  (uniq-orig v n tno esk)
  (label 0)
  (unrealized (0 0) (1 0) (2 5))
  (preskeleton)
  (comment "Not a skeleton"))

Item 1, Parent: 0, Children: 2 3.

(defskeleton envelope
  (vars (pcr mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (precedes ((2 6) (0 0)) ((2 6) (1 0)))
  (neq (tno n))
  (non-orig esk1 aik (invk tpmkey))
  (uniq-orig v n tno esk)
  (label 1)
  (parent 0)
  (unrealized (0 0) (2 5))
  (origs (esk (2 0)) (n (2 2)) (tno (2 2)) (v (2 6)))
  (comment "2 in cohort - 2 not yet seen"))

Item 2, Parent: 1.

(defskeleton envelope
  (vars (pcr nonce mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey aik-0 akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (enc "created" k (hash "obtain" (hash n pcr)) aik))
    (aik aik-0))
  (precedes ((2 6) (0 0)) ((2 6) (1 0)) ((3 2) (2 5)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk tpmkey))
  (uniq-orig v n tno esk)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "created" k (hash "obtain" (hash n pcr)) aik) (2 5))
  (label 2)
  (parent 1)
  (unrealized (0 0) (3 1))
  (comment "empty cohort"))

Item 3, Parent: 1, Children: 4 5.

(defskeleton envelope
  (vars (pcr mesg) (v n tne tno data) (esk1 esk esk-0 skey)
    (k aik tpmkey akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk-0) (k k) (aik aik))
  (precedes ((2 6) (0 0)) ((2 6) (1 0)) ((3 1) (2 5)))
  (neq (tno n))
  (non-orig esk1 esk-0 aik (invk k) (invk tpmkey))
  (uniq-orig v n tno esk k)
  (operation encryption-test (added-strand tpm-create-key 2)
    (enc "created" k (hash "obtain" (hash n pcr)) aik) (2 5))
  (label 3)
  (parent 1)
  (unrealized (0 0) (1 0) (3 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 4, Parent: 3.

(defskeleton envelope
  (vars (pcr nonce mesg) (v n tne tno data) (esk1 esk esk-0 skey)
    (k aik tpmkey aik-0 akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk-0) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (enc "create key" (hash "obtain" (hash n pcr)) esk-0))
    (aik aik-0))
  (precedes ((2 6) (0 0)) ((2 6) (1 0)) ((3 1) (2 5)) ((4 2) (3 0)))
  (neq (tno n))
  (non-orig esk1 esk-0 aik aik-0 (invk k) (invk tpmkey))
  (uniq-orig v n tno esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "create key" (hash "obtain" (hash n pcr)) esk-0) (3 0))
  (label 4)
  (parent 3)
  (unrealized (0 0) (1 0) (4 1))
  (comment "empty cohort"))

Item 5, Parent: 3, Children: 6 7.

(defskeleton envelope
  (vars (pcr mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk1) (k k) (aik aik))
  (precedes ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (1 0)) ((3 1) (2 5)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey))
  (uniq-orig v n tno esk k)
  (operation encryption-test (displaced 4 2 alice 5)
    (enc "create key" (hash "obtain" (hash n pcr)) esk-0) (3 0))
  (label 5)
  (parent 3)
  (unrealized (0 0) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 6, Parent: 5.

(defskeleton envelope
  (vars (pcr nonce mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey aik-0 akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-quote 3 (nonce nonce) (pcr v) (aik aik-0))
  (precedes ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 1)) ((3 1) (2 5))
    ((4 2) (1 0)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey))
  (uniq-orig v n tno esk k)
  (operation nonce-test (added-strand tpm-quote 3) v (1 0) (enc v k))
  (label 6)
  (parent 5)
  (unrealized (0 0) (4 1))
  (comment "empty cohort"))

Item 7, Parent: 5, Children: 8 9.

(defskeleton envelope
  (vars (pcr pcr-0 mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey aik-0 akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr pcr-0) (k k) (aik aik-0))
  (precedes ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0)) ((3 1) (2 5))
    ((4 3) (1 0)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey))
  (uniq-orig v n tno esk k)
  (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k))
  (label 7)
  (parent 5)
  (unrealized (0 0) (4 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 8, Parent: 7.

(defskeleton envelope
  (vars (pcr pcr-0 nonce mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey aik-0 aik-1 akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr pcr-0) (k k) (aik aik-0))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (enc "created" k pcr-0 aik-0)) (aik aik-1))
  (precedes ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0)) ((3 1) (2 5))
    ((3 1) (5 1)) ((4 3) (1 0)) ((5 2) (4 1)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 aik-1 (invk k) (invk tpmkey))
  (uniq-orig v n tno esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "created" k pcr-0 aik-0) (4 1))
  (label 8)
  (parent 7)
  (unrealized (0 0) (5 1))
  (comment "empty cohort"))

Item 9, Parent: 7, Child: 10.

(defskeleton envelope
  (vars (pcr mesg) (v n tne tno data) (esk1 esk skey)
    (k aik tpmkey akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n pcr)))
    (k k) (aik aik))
  (precedes ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0)) ((3 1) (2 5))
    ((4 3) (1 0)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey))
  (uniq-orig v n tno esk k)
  (operation encryption-test (displaced 5 3 tpm-create-key 2)
    (enc "created" k pcr-0 aik-0) (4 1))
  (label 9)
  (parent 7)
  (unrealized (0 0) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

Item 10, Parent: 9, Child: 11.

(defskeleton envelope
  (vars (pcr mesg) (v n tne tno tne-0 tno-0 data) (esk1 esk esk-0 skey)
    (k aik tpmkey tpmkey-0 akey))
  (deflistener (enc "quote" (hash "refuse" (hash n pcr)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr pcr) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n pcr)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n pcr)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n pcr))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (precedes ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0)) ((3 1) (2 5))
    ((4 3) (1 0)) ((5 3) (4 2)))
  (leadsto ((5 3) (4 2)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0))
  (uniq-orig v n tno tne-0 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "obtain" (hash n pcr)) (4 2))
  (label 10)
  (parent 9)
  (unrealized (0 0) (5 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 11, Parent: 10, Children: 12 13 14.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 3) (5 3)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash n state) (5 3))
  (label 11)
  (parent 10)
  (unrealized (0 0) (6 2))
  (comment "3 in cohort - 3 not yet seen"))

Item 12, Parent: 11, Child: 15.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr
      (hash esk-1
        (hash "execute transport" (hash "extend" (enc n esk-1))) tne-1
        tno-1 "false")) (aik aik-0))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 3) (5 3))
    ((7 2) (6 2)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (hash esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false") (6 2))
  (label 12)
  (parent 11)
  (unrealized (0 0) (6 2) (7 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 13, Parent: 11, Children: 16 17 18.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey-1))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tne tno tne-0 esk k)
  (operation encryption-test (displaced 7 2 alice 3)
    (hash esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false") (6 2))
  (label 13)
  (parent 11)
  (unrealized (0 0) (6 0))
  (comment "3 in cohort - 3 not yet seen"))

Item 14, Parent: 11, Children: 19 20.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test
    (added-listener
      (cat esk-1
        (hash "execute transport" (hash "extend" (enc n esk-1))) tne-1
        tno-1 "false"))
    (hash esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false") (6 2))
  (label 14)
  (parent 11)
  (unrealized (0 0) (6 2) (7 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 15, Parent: 12.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr
      (hash esk-1
        (hash "execute transport" (hash "extend" (enc n esk-1))) tne-1
        tno-1 "false")) (aik aik-0))
  (defstrand tpm-extend-enc 4 (value esk-1)
    (state
      (cat (hash "execute transport" (hash "extend" (enc n esk-1)))
        tne-1 tno-1 "false")) (tne tne-2) (tno tno-2) (esk esk-2)
    (tpmkey tpmkey-2))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (8 3))
    ((6 3) (5 3)) ((7 2) (6 2)) ((8 3) (7 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tno tne-0 tne-1 tne-2 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false") (7 1))
  (label 15)
  (parent 12)
  (unrealized (0 0) (6 2) (8 3))
  (comment "empty cohort"))

Item 16, Parent: 13, Children: 21 22.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0))
  (uniq-orig v n tne tno tne-0 esk k)
  (operation nonce-test (contracted (tpmkey-1 tpmkey)) esk (6 0)
    (enc esk tpmkey))
  (label 16)
  (parent 13)
  (unrealized (0 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 17, Parent: 13.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey-1))
  (defstrand tpm-quote 3 (nonce nonce) (pcr esk) (aik aik-0))
  (precedes ((2 0) (7 1)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (6 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tne tno tne-0 esk k)
  (operation nonce-test (added-strand tpm-quote 3) esk (6 0)
    (enc esk tpmkey))
  (label 17)
  (parent 13)
  (unrealized (0 0) (7 1))
  (comment "empty cohort"))

Item 18, Parent: 13, Child: 23.

(defskeleton envelope
  (vars (state pcr mesg) (v n tne tno tne-0 tno-0 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey-1))
  (defstrand tpm-decrypt 4 (m esk) (pcr pcr) (k tpmkey) (aik aik-0))
  (precedes ((2 0) (7 0)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)) ((7 3) (6 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tne tno tne-0 esk k)
  (operation nonce-test (added-strand tpm-decrypt 4) esk (6 0)
    (enc esk tpmkey))
  (label 18)
  (parent 13)
  (unrealized (0 0) (7 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 19, Parent: 14, Child: 24.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "execute transport" (hash "extend" (enc n esk-1))))
    (aik aik-0))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 2) (7 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (hash "execute transport" (hash "extend" (enc n esk-1))) (7 0))
  (label 19)
  (parent 14)
  (unrealized (0 0) (6 2) (8 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 20, Parent: 14, Children: 25 26.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test
    (added-listener
      (cat "execute transport" (hash "extend" (enc n esk-1))))
    (hash "execute transport" (hash "extend" (enc n esk-1))) (7 0))
  (label 20)
  (parent 14)
  (unrealized (0 0) (6 2) (8 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 21, Parent: 16, Child: 27.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (4 0))
    ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0))
  (uniq-orig v n tne tno tne-0 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik) (0 0))
  (label 21)
  (parent 16)
  (unrealized (7 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 22, Parent: 16.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
    (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (4 0))
    ((2 6) (7 1)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0))
  (uniq-orig v n tne tno tne-0 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik) (0 0))
  (label 22)
  (parent 16)
  (unrealized (7 1))
  (comment "empty cohort"))

Item 23, Parent: 18.

(defskeleton envelope
  (vars (state pcr nonce mesg) (v n tne tno tne-0 tno-0 data)
    (esk1 esk esk-0 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 aik-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey-1))
  (defstrand tpm-decrypt 4 (m esk) (pcr pcr) (k tpmkey) (aik aik-0))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (enc "created" tpmkey pcr aik-0)) (aik aik-1))
  (precedes ((2 0) (7 0)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)) ((7 3) (6 0)) ((8 2) (7 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 aik-1 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tne tno tne-0 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "created" tpmkey pcr aik-0) (7 1))
  (label 23)
  (parent 18)
  (unrealized (0 0) (8 1))
  (comment "empty cohort"))

Item 24, Parent: 19, Child: 28.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "execute transport" (hash "extend" (enc n esk-1))))
    (aik aik-0))
  (defstrand tpm-extend-enc 4 (value "execute transport")
    (state (hash "extend" (enc n esk-1))) (tne tne-2) (tno tno-2)
    (esk esk-2) (tpmkey tpmkey-2))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 2) (7 0)) ((9 3) (8 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((9 3) (8 1)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tno tne-0 tne-1 tne-2 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "execute transport" (hash "extend" (enc n esk-1))) (8 1))
  (label 24)
  (parent 19)
  (unrealized (0 0) (6 2) (9 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 25, Parent: 20, Child: 29.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "extend" (enc n esk-1))) (aik aik-0))
  (precedes ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0)) ((9 2) (8 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (hash "extend" (enc n esk-1)) (8 0))
  (label 25)
  (parent 20)
  (unrealized (0 0) (6 2) (9 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 26, Parent: 20, Children: 30 31 32.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (deflistener (cat "extend" (enc n esk-1)))
  (precedes ((2 2) (9 0)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0)) ((9 1) (8 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test
    (added-listener (cat "extend" (enc n esk-1)))
    (hash "extend" (enc n esk-1)) (8 0))
  (label 26)
  (parent 20)
  (unrealized (0 0) (9 0))
  (comment "3 in cohort - 3 not yet seen"))

Item 27, Parent: 21, Child: 33.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 4) (3 0)) ((2 6) (4 0))
    ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0)) ((8 3) (7 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tne tno tne-0 tne-1 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "refuse" (hash n state)) (7 1))
  (label 27)
  (parent 21)
  (unrealized (8 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 28, Parent: 24.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 tne-3 tno-3 data)
    (esk1 esk esk-0 esk-1 esk-2 esk-3 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 tpmkey-2 tpmkey-3 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "execute transport" (hash "extend" (enc n esk-1))))
    (aik aik-0))
  (defstrand tpm-extend-enc 4 (value "execute transport")
    (state (hash "extend" (enc n esk-1))) (tne tne-2) (tno tno-2)
    (esk esk-2) (tpmkey tpmkey-2))
  (defstrand tpm-extend-enc 4 (value "extend") (state (enc n esk-1))
    (tne tne-3) (tno tno-3) (esk esk-3) (tpmkey tpmkey-3))
  (precedes ((2 2) (10 3)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 2) (7 0)) ((9 3) (8 1))
    ((10 3) (9 3)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((9 3) (8 1)) ((10 3) (9 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2) (invk tpmkey-3))
  (uniq-orig v n tno tne-0 tne-1 tne-2 tne-3 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "extend" (enc n esk-1)) (9 3))
  (label 28)
  (parent 24)
  (unrealized (0 0) (6 2) (10 3))
  (comment "empty cohort"))

Item 29, Parent: 25.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "extend" (enc n esk-1))) (aik aik-0))
  (defstrand tpm-extend-enc 4 (value "extend") (state (enc n esk-1))
    (tne tne-2) (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (precedes ((2 2) (10 3)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0)) ((9 2) (8 0))
    ((10 3) (9 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((10 3) (9 1)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tno tne-0 tne-1 tne-2 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "extend" (enc n esk-1)) (9 1))
  (label 29)
  (parent 25)
  (unrealized (0 0) (6 2) (10 3))
  (comment "empty cohort"))

Item 30, Parent: 26, Children: 34 35.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk) (tpmkey tpmkey-1))
  (deflistener
    (cat esk (hash "execute transport" (hash "extend" (enc n esk)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk))))
  (deflistener (cat "extend" (enc n esk)))
  (precedes ((2 0) (6 0)) ((2 2) (9 0)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0))
    ((9 1) (8 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation nonce-test (contracted (esk-1 esk)) n (9 0) (enc n esk))
  (label 30)
  (parent 26)
  (unrealized (0 0) (6 0) (7 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 31, Parent: 26.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (deflistener (cat "extend" (enc n esk-1)))
  (defstrand tpm-quote 3 (nonce nonce) (pcr n) (aik aik-0))
  (precedes ((2 2) (10 1)) ((2 4) (3 0)) ((2 6) (0 0)) ((2 6) (4 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (7 0))
    ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0)) ((9 1) (8 0))
    ((10 2) (9 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation nonce-test (added-strand tpm-quote 3) n (9 0) (enc n esk))
  (label 31)
  (parent 26)
  (unrealized (0 0) (10 1))
  (comment "empty cohort"))

Item 32, Parent: 26, Children: 36 37.

(defskeleton envelope
  (vars (state mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey) (k aik tpmkey tpmkey-0 tpmkey-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (deflistener (cat "extend" (enc n esk-1)))
  (deflistener esk)
  (precedes ((2 0) (10 0)) ((2 2) (9 0)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 1) (9 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation nonce-test (added-listener esk) n (9 0) (enc n esk))
  (label 32)
  (parent 26)
  (unrealized (0 0) (10 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 33, Parent: 27, Children: 38 39.

(defskeleton envelope
  (vars (state mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 3) (8 3)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash n state) (8 3))
  (label 33)
  (parent 27)
  (unrealized (9 2))
  (comment "2 in cohort - 2 not yet seen"))

Item 34, Parent: 30.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk) (tpmkey tpmkey-1))
  (deflistener
    (cat esk (hash "execute transport" (hash "extend" (enc n esk)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk))))
  (deflistener (cat "extend" (enc n esk)))
  (defstrand tpm-quote 3 (nonce nonce) (pcr esk) (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 1)) ((2 2) (9 0)) ((2 4) (3 0))
    ((2 6) (0 0)) ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2))
    ((8 1) (7 0)) ((9 1) (8 0)) ((10 2) (7 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation nonce-test (added-strand tpm-quote 3) esk (7 0)
    (enc esk tpmkey))
  (label 34)
  (parent 30)
  (unrealized (0 0) (6 0) (10 1))
  (comment "empty cohort"))

Item 35, Parent: 30, Child: 40.

(defskeleton envelope
  (vars (state pcr mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 skey) (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk) (tpmkey tpmkey-1))
  (deflistener
    (cat esk (hash "execute transport" (hash "extend" (enc n esk)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk))))
  (deflistener (cat "extend" (enc n esk)))
  (defstrand tpm-decrypt 4 (m esk) (pcr pcr) (k tpmkey) (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 2) (9 0)) ((2 4) (3 0))
    ((2 6) (0 0)) ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2))
    ((8 1) (7 0)) ((9 1) (8 0)) ((10 3) (7 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation nonce-test (added-strand tpm-decrypt 4) esk (7 0)
    (enc esk tpmkey))
  (label 35)
  (parent 30)
  (unrealized (0 0) (6 0) (10 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 36, Parent: 32.

(defskeleton envelope
  (vars (state nonce mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (deflistener (cat "extend" (enc n esk-1)))
  (deflistener esk)
  (defstrand tpm-quote 3 (nonce nonce) (pcr esk) (aik aik-0))
  (precedes ((2 0) (11 1)) ((2 2) (9 0)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 1) (9 0)) ((11 2) (10 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation nonce-test (added-strand tpm-quote 3) esk (10 0)
    (enc esk tpmkey))
  (label 36)
  (parent 32)
  (unrealized (0 0) (11 1))
  (comment "empty cohort"))

Item 37, Parent: 32, Child: 41.

(defskeleton envelope
  (vars (state pcr mesg) (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (deflistener (cat "extend" (enc n esk-1)))
  (deflistener esk)
  (defstrand tpm-decrypt 4 (m esk) (pcr pcr) (k tpmkey) (aik aik-0))
  (precedes ((2 0) (11 0)) ((2 2) (9 0)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 1) (9 0)) ((11 3) (10 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation nonce-test (added-strand tpm-decrypt 4) esk (10 0)
    (enc esk tpmkey))
  (label 37)
  (parent 32)
  (unrealized (0 0) (11 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 38, Parent: 33, Child: 42.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr
      (hash esk-2
        (hash "execute transport" (hash "extend" (enc n esk-2))) tne-2
        tno-2 "false")) (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 3) (8 3)) ((10 2) (9 2)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (hash esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false") (9 2))
  (label 38)
  (parent 33)
  (unrealized (9 2) (10 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 39, Parent: 33, Children: 43 44.

(defskeleton envelope
  (vars (state mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation encryption-test
    (added-listener
      (cat esk-2
        (hash "execute transport" (hash "extend" (enc n esk-2))) tne-2
        tno-2 "false"))
    (hash esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false") (9 2))
  (label 39)
  (parent 33)
  (unrealized (9 2) (10 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 40, Parent: 35.

(defskeleton envelope
  (vars (state pcr nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 data) (esk1 esk esk-0 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 aik-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk) (tpmkey tpmkey-1))
  (deflistener
    (cat esk (hash "execute transport" (hash "extend" (enc n esk)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk))))
  (deflistener (cat "extend" (enc n esk)))
  (defstrand tpm-decrypt 4 (m esk) (pcr pcr) (k tpmkey) (aik aik-0))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (enc "created" tpmkey pcr aik-0)) (aik aik-1))
  (precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 2) (9 0)) ((2 4) (3 0))
    ((2 6) (0 0)) ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2))
    ((8 1) (7 0)) ((9 1) (8 0)) ((10 3) (7 0)) ((11 2) (10 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 aik-1 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "created" tpmkey pcr aik-0) (10 1))
  (label 40)
  (parent 35)
  (unrealized (0 0) (6 0) (11 1))
  (comment "empty cohort"))

Item 41, Parent: 37.

(defskeleton envelope
  (vars (state pcr nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 aik-0 aik-1 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-1)
    (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (deflistener
    (cat esk-1 (hash "execute transport" (hash "extend" (enc n esk-1)))
      tne-1 tno-1 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-1))))
  (deflistener (cat "extend" (enc n esk-1)))
  (deflistener esk)
  (defstrand tpm-decrypt 4 (m esk) (pcr pcr) (k tpmkey) (aik aik-0))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (enc "created" tpmkey pcr aik-0)) (aik aik-1))
  (precedes ((2 0) (11 0)) ((2 2) (9 0)) ((2 4) (3 0)) ((2 6) (0 0))
    ((2 6) (4 0)) ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2))
    ((6 1) (7 0)) ((6 3) (5 3)) ((7 1) (6 2)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 1) (9 0)) ((11 3) (10 0)) ((12 2) (11 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 aik-1 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1))
  (uniq-orig v n tno tne-0 tne-1 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (enc "created" tpmkey pcr aik-0) (11 1))
  (label 41)
  (parent 37)
  (unrealized (0 0) (12 1))
  (comment "empty cohort"))

Item 42, Parent: 38.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 tne-3 tno-3 data)
    (esk1 esk esk-0 esk-1 esk-2 esk-3 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 tpmkey-3 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr
      (hash esk-2
        (hash "execute transport" (hash "extend" (enc n esk-2))) tne-2
        tno-2 "false")) (aik aik-0))
  (defstrand tpm-extend-enc 4 (value esk-2)
    (state
      (cat (hash "execute transport" (hash "extend" (enc n esk-2)))
        tne-2 tno-2 "false")) (tne tne-3) (tno tno-3) (esk esk-3)
    (tpmkey tpmkey-3))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (11 3)) ((9 3) (8 3)) ((10 2) (9 2))
    ((11 3) (10 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3))
    ((11 3) (10 1)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2) (invk tpmkey-3))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 tne-3 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false") (10 1))
  (label 42)
  (parent 38)
  (unrealized (9 2) (11 3))
  (comment "empty cohort"))

Item 43, Parent: 39, Child: 45.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "execute transport" (hash "extend" (enc n esk-2))))
    (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 2) (10 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (hash "execute transport" (hash "extend" (enc n esk-2))) (10 0))
  (label 43)
  (parent 39)
  (unrealized (9 2) (11 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 44, Parent: 39, Children: 46 47.

(defskeleton envelope
  (vars (state mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-2))))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 1) (10 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation encryption-test
    (added-listener
      (cat "execute transport" (hash "extend" (enc n esk-2))))
    (hash "execute transport" (hash "extend" (enc n esk-2))) (10 0))
  (label 44)
  (parent 39)
  (unrealized (9 2) (11 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 45, Parent: 43, Child: 48.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 tne-3 tno-3 data)
    (esk1 esk esk-0 esk-1 esk-2 esk-3 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 tpmkey-3 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "execute transport" (hash "extend" (enc n esk-2))))
    (aik aik-0))
  (defstrand tpm-extend-enc 4 (value "execute transport")
    (state (hash "extend" (enc n esk-2))) (tne tne-3) (tno tno-3)
    (esk esk-3) (tpmkey tpmkey-3))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 2) (10 0)) ((12 3) (11 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3))
    ((12 3) (11 1)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2) (invk tpmkey-3))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 tne-3 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "execute transport" (hash "extend" (enc n esk-2))) (11 1))
  (label 45)
  (parent 43)
  (unrealized (9 2) (12 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 46, Parent: 44, Child: 49.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-2))))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "extend" (enc n esk-2))) (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (9 2)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 1) (10 0)) ((12 2) (11 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation encryption-test (added-strand tpm-quote 3)
    (hash "extend" (enc n esk-2)) (11 0))
  (label 46)
  (parent 44)
  (unrealized (9 2) (12 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 47, Parent: 44, Children: 50 51 52.

(defskeleton envelope
  (vars (state mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-2))))
  (deflistener (cat "extend" (enc n esk-2)))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (12 0)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 1) (10 0)) ((12 1) (11 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation encryption-test
    (added-listener (cat "extend" (enc n esk-2)))
    (hash "extend" (enc n esk-2)) (11 0))
  (label 47)
  (parent 44)
  (unrealized (12 0))
  (comment "3 in cohort - 3 not yet seen"))

Item 48, Parent: 45.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 tne-3 tno-3 tne-4
      tno-4 data) (esk1 esk esk-0 esk-1 esk-2 esk-3 esk-4 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 tpmkey-3 tpmkey-4
      akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "execute transport" (hash "extend" (enc n esk-2))))
    (aik aik-0))
  (defstrand tpm-extend-enc 4 (value "execute transport")
    (state (hash "extend" (enc n esk-2))) (tne tne-3) (tno tno-3)
    (esk esk-3) (tpmkey tpmkey-3))
  (defstrand tpm-extend-enc 4 (value "extend") (state (enc n esk-2))
    (tne tne-4) (tno tno-4) (esk esk-4) (tpmkey tpmkey-4))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (13 3)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 2) (10 0)) ((12 3) (11 1)) ((13 3) (12 3)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3))
    ((12 3) (11 1)) ((13 3) (12 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2) (invk tpmkey-3) (invk tpmkey-4))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 tne-3 tne-4 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "extend" (enc n esk-2)) (12 3))
  (label 48)
  (parent 45)
  (unrealized (9 2) (13 3))
  (comment "empty cohort"))

Item 49, Parent: 46.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 tne-3 tno-3 data)
    (esk1 esk esk-0 esk-1 esk-2 esk-3 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 tpmkey-3 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-2))))
  (defstrand tpm-quote 3 (nonce nonce)
    (pcr (hash "extend" (enc n esk-2))) (aik aik-0))
  (defstrand tpm-extend-enc 4 (value "extend") (state (enc n esk-2))
    (tne tne-3) (tno tno-3) (esk esk-3) (tpmkey tpmkey-3))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (13 3)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 1) (10 0)) ((12 2) (11 0)) ((13 3) (12 1)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3))
    ((13 3) (12 1)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2) (invk tpmkey-3))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 tne-3 esk k)
  (operation state-passing-test (added-strand tpm-extend-enc 4)
    (hash "extend" (enc n esk-2)) (12 1))
  (label 49)
  (parent 46)
  (unrealized (9 2) (13 3))
  (comment "empty cohort"))

Item 50, Parent: 47, Children: 53 54.

(defskeleton envelope
  (vars (state mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk) (tpmkey tpmkey-2))
  (deflistener
    (cat esk (hash "execute transport" (hash "extend" (enc n esk)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk))))
  (deflistener (cat "extend" (enc n esk)))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 2) (6 2)) ((2 2) (12 0))
    ((2 4) (3 0)) ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5))
    ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3))
    ((7 2) (0 0)) ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3))
    ((10 1) (9 2)) ((11 1) (10 0)) ((12 1) (11 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation nonce-test (contracted (esk-2 esk)) n (12 0) (enc n esk))
  (label 50)
  (parent 47)
  (unrealized (9 0) (10 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 51, Parent: 47.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-2))))
  (deflistener (cat "extend" (enc n esk-2)))
  (defstrand tpm-quote 3 (nonce nonce) (pcr n) (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 2) (6 2)) ((2 2) (13 1)) ((2 4) (3 0))
    ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5)) ((4 3) (1 0))
    ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3)) ((7 2) (0 0))
    ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3)) ((10 1) (9 2))
    ((11 1) (10 0)) ((12 1) (11 0)) ((13 2) (12 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation nonce-test (added-strand tpm-quote 3) n (12 0) (enc n esk))
  (label 51)
  (parent 47)
  (unrealized (13 1))
  (comment "empty cohort"))

Item 52, Parent: 47, Children: 55 56.

(defskeleton envelope
  (vars (state mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 esk-2 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk-2) (tpmkey tpmkey-2))
  (deflistener
    (cat esk-2 (hash "execute transport" (hash "extend" (enc n esk-2)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk-2))))
  (deflistener (cat "extend" (enc n esk-2)))
  (deflistener esk)
  (precedes ((2 0) (6 0)) ((2 0) (13 0)) ((2 2) (6 2)) ((2 2) (12 0))
    ((2 4) (3 0)) ((2 6) (4 0)) ((2 6) (7 0)) ((3 1) (2 5))
    ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (2 1)) ((6 3) (5 3))
    ((7 2) (0 0)) ((8 3) (7 1)) ((9 1) (10 0)) ((9 3) (8 3))
    ((10 1) (9 2)) ((11 1) (10 0)) ((12 1) (11 0)) ((13 1) (12 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation nonce-test (added-listener esk) n (12 0) (enc n esk))
  (label 52)
  (parent 47)
  (unrealized (13 0))
  (comment "2 in cohort - 2 not yet seen"))

Item 53, Parent: 50.

(defskeleton envelope
  (vars (state nonce mesg)
    (v n tne tno tne-0 tno-0 tne-1 tno-1 tne-2 tno-2 data)
    (esk1 esk esk-0 esk-1 skey)
    (k aik tpmkey tpmkey-0 tpmkey-1 tpmkey-2 aik-0 akey))
  (deflistener
    (enc "quote" (hash "refuse" (hash n state)) (enc v k) aik))
  (deflistener v)
  (defstrand alice 7 (pcr state) (v v) (n n) (tne tne) (tno tno)
    (esk1 esk1) (esk esk) (k k) (aik aik) (tpmkey tpmkey))
  (defstrand tpm-create-key 2 (pcr (hash "obtain" (hash n state)))
    (esk esk1) (k k) (aik aik))
  (defstrand tpm-decrypt 4 (m v) (pcr (hash "obtain" (hash n state)))
    (k k) (aik aik))
  (defstrand tpm-extend-enc 4 (value "obtain") (state (hash n state))
    (tne tne-0) (tno tno-0) (esk esk-0) (tpmkey tpmkey-0))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne)
    (tno tno) (esk esk) (tpmkey tpmkey))
  (defstrand tpm-quote 3 (nonce (enc v k))
    (pcr (hash "refuse" (hash n state))) (aik aik))
  (defstrand tpm-extend-enc 4 (value "refuse") (state (hash n state))
    (tne tne-1) (tno tno-1) (esk esk-1) (tpmkey tpmkey-1))
  (defstrand tpm-extend-enc 4 (value n) (state state) (tne tne-2)
    (tno tno-2) (esk esk) (tpmkey tpmkey-2))
  (deflistener
    (cat esk (hash "execute transport" (hash "extend" (enc n esk)))
      tne-2 tno-2 "false"))
  (deflistener (cat "execute transport" (hash "extend" (enc n esk))))
  (deflistener (cat "extend" (enc n esk)))
  (defstrand tpm-quote 3 (nonce nonce) (pcr esk) (aik aik-0))
  (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 0) (13 1)) ((2 2) (6 2))
    ((2 2) (12 0)) ((2 4) (3 0)) ((2 6) (4 0)) ((2 6) (7 0))
    ((3 1) (2 5)) ((4 3) (1 0)) ((5 3) (4 2)) ((6 1) (2 1))
    ((6 3) (5 3)) ((7 2) (0 0)) ((8 3) (7 1)) ((9 1) (10 0))
    ((9 3) (8 3)) ((10 1) (9 2)) ((11 1) (10 0)) ((12 1) (11 0))
    ((13 2) (10 0)))
  (leadsto ((5 3) (4 2)) ((6 3) (5 3)) ((8 3) (7 1)) ((9 3) (8 3)))
  (neq (tno n))
  (non-orig esk1 aik aik-0 (invk k) (invk tpmkey) (invk tpmkey-0)
    (invk tpmkey-1) (invk tpmkey-2))
  (uniq-orig v n tne tno tne-0 tne-1 tne-2 esk k)
  (operation nonce-test (added-strand tpm-quote 3) esk (10 0)
    (enc esk tpmkey))
  (label 53)
  (parent 50)
  (unrealized (9 0) (13 1))
  (comment "empty cohort"))

Item 54, Parent: 50, Child: 57.