(herald "Envelope Protocol, location-based version" (bound 30) (limit 1200)) (comment "CPSA 4.4.7") (comment "All input read from tst/locn_envelope.scm") (comment "Step count limited to 1200") (comment "Strand count bounded at 30") (defprotocol envelope basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defgenrule neqRl_indx (forall ((x indx)) (implies (fact neq x x) (false)))) (defgenrule neqRl_strd (forall ((x strd)) (implies (fact neq x x) (false)))) (defgenrule neqRl_mesg (forall ((x mesg)) (implies (fact neq x x) (false)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig v n) (conf tpm) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 0) (unrealized (0 0) (1 2)) (preskeleton) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "Not a skeleton")) (defskeleton envelope (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (precedes ((1 3) (0 0))) (non-orig aik) (uniq-orig v n) (conf tpm) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 1) (parent 0) (unrealized (1 2)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (v n data) (pcr-id text) (k aik akey) (tpm tpm-0 chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0)) (precedes ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik) (1 2)) (strand-map 0 1) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))) (label 2) (parent 1) (unrealized (0 0) (2 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm) (operation channel-test (displaced 3 1 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (2 0)) (strand-map 0 1 2) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))) (label 3) (parent 2) (unrealized (0 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (current-value mesg) (v n data) (pcr-id pcr-id-0 text) (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value current-value) (pcr-id pcr-id-0) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))) (non-orig aik aik-0 (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm) (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 tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 current-value aik-0)) (load pcr (cat pt current-value)) (send v))) (label 4) (parent 3) (unrealized (3 1)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (v n data) (pcr-id text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))) (non-orig aik (invk k)) (uniq-orig v n k) (gen-st (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-decrypt) (operation encryption-test (displaced 4 2 tpm-create-key 2) (enc "created" k pcr-id-0 current-value aik-0) (3 1)) (strand-map 0 1 2 3) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))) (label 5) (parent 4) (unrealized (3 2)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)) ((4 2) (3 2))) (non-orig aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (3 2)) (strand-map 0 1 2 3) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain"))))) (label 6) (parent 5) (unrealized (4 1)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (v n data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-1) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2)) ((5 2) (4 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm-2 (cat "extend" pcr-id-1 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 7) (parent 6) (unrealized (5 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2)) ((5 2) (4 1))) (operation nonce-test (contracted (pcr-id-1 pcr-id) (tpm-2 tpm)) n (5 0) (ch-msg tpm (cat "extend" pcr-id n))) (strand-map 0 1 2 3 4 5) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 8) (parent 7) (realized) (shape) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (pt-0 (5 2)) (pt (4 2)) (k (2 1)) (n (1 0)) (v (1 3)))) (comment "Nothing left to do") (defprotocol envelope basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defgenrule neqRl_indx (forall ((x indx)) (implies (fact neq x x) (false)))) (defgenrule neqRl_strd (forall ((x strd)) (implies (fact neq x x) (false)))) (defgenrule neqRl_mesg (forall ((x mesg)) (implies (fact neq x x) (false)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 9) (unrealized (0 0) (1 2)) (preskeleton) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "Not a skeleton")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((1 3) (0 0))) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 10) (parent 9) (unrealized (0 0) (1 2)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0)) (precedes ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (1 2)) (strand-map 0 1) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 11) (parent 10) (unrealized (0 0) (2 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation channel-test (displaced 3 1 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (2 0)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 12) (parent 11) (unrealized (0 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-quote) (operation encryption-test (added-strand tpm-quote 3) (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik) (0 0)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)))) (label 13) (parent 12) (unrealized (3 1)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)) ((4 2) (3 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "refuse"))) (3 1)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse"))))) (label 14) (parent 13) (unrealized (4 1)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1)) ((5 2) (4 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse")))) ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 15) (parent 14) (unrealized (5 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1)) ((5 2) (4 1))) (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n (5 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 16) (parent 15) (realized) (shape) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (pt-0 (5 2)) (pt (4 2)) (n (1 0)) (k (2 1)) (v (1 3)))) (comment "Nothing left to do") (defprotocol envelope basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defgenrule neqRl_indx (forall ((x indx)) (implies (fact neq x x) (false)))) (defgenrule neqRl_strd (forall ((x strd)) (implies (fact neq x x) (false)))) (defgenrule neqRl_mesg (forall ((x mesg)) (implies (fact neq x x) (false)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 17) (unrealized (0 0) (1 0) (2 2)) (preskeleton) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (2 3)) (n (2 0))) (comment "Not a skeleton")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((2 3) (0 0)) ((2 3) (1 0))) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 18) (parent 17) (unrealized (0 0) (2 2)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (2 3)) (n (2 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0)) (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (2 2)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 19) (parent 18) (unrealized (0 0) (1 0) (3 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation channel-test (displaced 4 2 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 20) (parent 19) (unrealized (0 0) (1 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (current-value mesg) (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value current-value) (pcr-id pcr-id-1) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2)) ((4 3) (1 0))) (non-orig aik aik-0 (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-1 current-value aik-0)) (load pcr (cat pt current-value)) (send v))) (label 21) (parent 20) (unrealized (0 0) (4 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2)) ((4 3) (1 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-decrypt) (operation encryption-test (displaced 5 3 tpm-create-key 2) (enc "created" k pcr-id-1 current-value aik-0) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))) (label 22) (parent 21) (unrealized (0 0) (4 2)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (4 2)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain"))))) (label 23) (parent 22) (unrealized (0 0) (5 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (5 1)) (strand-map 0 1 2 3 4 5) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 24) (parent 23) (unrealized (0 0) (6 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n (6 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5 6) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 25) (parent 24) (unrealized (0 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pt-2 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (rule genStV-if-hashed-tpm-quote) (operation encryption-test (added-strand tpm-quote 3) (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik) (0 0)) (strand-map 0 1 2 3 4 5 6) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)))) (label 26) (parent 25) (unrealized (7 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 1)) (strand-map 0 1 2 3 4 5 6 7) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))) (label 27) (parent 26) (unrealized (8 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 pcr-id-3 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 tpm-4 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-3) (tpm tpm-4) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 1)) (strand-map 0 1 2 3 4 5 6 7 8) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))) ((recv tpm-4 (cat "extend" pcr-id-3 n)) (load pcr-0 (cat pt-4 "0")) (stor pcr-0 (cat pt-3 (hash "0" n))))) (label 28) (parent 27) (unrealized (9 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1))) (operation nonce-test (contracted (pcr-id-3 pcr-id-0) (tpm-4 tpm)) n (9 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5 6 7 8 9) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr-0 (cat pt-4 "0")) (stor pcr-0 (cat pt-3 (hash "0" n))))) (label 29) (parent 28) (realized) (shape) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (pt-3 (9 2)) (pt-2 (8 2)) (pt-0 (6 2)) (pt (5 2)) (k (3 1)) (n (2 0)) (v (2 3)))) (comment "Nothing left to do") (defprotocol envelope-plus basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule ordered-extends (forall ((y z strd) (pcr locn)) (implies (and (p "tpm-extend-enc" z (idx 3)) (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "pcr" z pcr) (p "tpm-extend-enc" "pcr" y pcr)) (or (= y z) (prec y (idx 2) z (idx 1)) (prec z (idx 2) y (idx 1)))))) (defgenrule neqRl_indx (forall ((x indx)) (implies (fact neq x x) (false)))) (defgenrule neqRl_strd (forall ((x strd)) (implies (fact neq x x) (false)))) (defgenrule neqRl_mesg (forall ((x mesg)) (implies (fact neq x x) (false)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope-plus (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig v n) (conf tpm) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 30) (unrealized (0 0) (1 2)) (preskeleton) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "Not a skeleton")) (defskeleton envelope-plus (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (precedes ((1 3) (0 0))) (non-orig aik) (uniq-orig v n) (conf tpm) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 31) (parent 30) (unrealized (1 2)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (v n data) (pcr-id text) (k aik akey) (tpm tpm-0 chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0)) (precedes ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik) (1 2)) (strand-map 0 1) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))) (label 32) (parent 31) (unrealized (0 0) (2 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm) (operation channel-test (displaced 3 1 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (2 0)) (strand-map 0 1 2) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))) (label 33) (parent 32) (unrealized (0 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (current-value mesg) (v n data) (pcr-id pcr-id-0 text) (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value current-value) (pcr-id pcr-id-0) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))) (non-orig aik aik-0 (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm) (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 tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 current-value aik-0)) (load pcr (cat pt current-value)) (send v))) (label 34) (parent 33) (unrealized (3 1)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (v n data) (pcr-id text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))) (non-orig aik (invk k)) (uniq-orig v n k) (gen-st (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-decrypt) (operation encryption-test (displaced 4 2 tpm-create-key 2) (enc "created" k pcr-id-0 current-value aik-0) (3 1)) (strand-map 0 1 2 3) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))) (label 35) (parent 34) (unrealized (3 2)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)) ((4 2) (3 2))) (non-orig aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (3 2)) (strand-map 0 1 2 3) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain"))))) (label 36) (parent 35) (unrealized (4 1)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (v n data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-1) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2)) ((5 2) (4 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm-2 (cat "extend" pcr-id-1 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 37) (parent 36) (unrealized (5 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2)) ((5 2) (4 1))) (operation nonce-test (contracted (pcr-id-1 pcr-id) (tpm-2 tpm)) n (5 0) (ch-msg tpm (cat "extend" pcr-id n))) (strand-map 0 1 2 3 4 5) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 38) (parent 37) (realized) (shape) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (pt-0 (5 2)) (pt (4 2)) (k (2 1)) (n (1 0)) (v (1 3)))) (comment "Nothing left to do") (defprotocol envelope-plus basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule ordered-extends (forall ((y z strd) (pcr locn)) (implies (and (p "tpm-extend-enc" z (idx 3)) (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "pcr" z pcr) (p "tpm-extend-enc" "pcr" y pcr)) (or (= y z) (prec y (idx 2) z (idx 1)) (prec z (idx 2) y (idx 1)))))) (defgenrule neqRl_indx (forall ((x indx)) (implies (fact neq x x) (false)))) (defgenrule neqRl_strd (forall ((x strd)) (implies (fact neq x x) (false)))) (defgenrule neqRl_mesg (forall ((x mesg)) (implies (fact neq x x) (false)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 39) (unrealized (0 0) (1 2)) (preskeleton) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "Not a skeleton")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((1 3) (0 0))) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 40) (parent 39) (unrealized (0 0) (1 2)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0)) (precedes ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (1 2)) (strand-map 0 1) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 41) (parent 40) (unrealized (0 0) (2 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation channel-test (displaced 3 1 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (2 0)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 42) (parent 41) (unrealized (0 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-quote) (operation encryption-test (added-strand tpm-quote 3) (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik) (0 0)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)))) (label 43) (parent 42) (unrealized (3 1)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)) ((4 2) (3 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "refuse"))) (3 1)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse"))))) (label 44) (parent 43) (unrealized (4 1)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1)) ((5 2) (4 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse")))) ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 45) (parent 44) (unrealized (5 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1)) ((5 2) (4 1))) (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n (5 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 46) (parent 45) (realized) (shape) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (pt-0 (5 2)) (pt (4 2)) (n (1 0)) (k (2 1)) (v (1 3)))) (comment "Nothing left to do") (defprotocol envelope-plus basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule ordered-extends (forall ((y z strd) (pcr locn)) (implies (and (p "tpm-extend-enc" z (idx 3)) (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "pcr" z pcr) (p "tpm-extend-enc" "pcr" y pcr)) (or (= y z) (prec y (idx 2) z (idx 1)) (prec z (idx 2) y (idx 1)))))) (defgenrule neqRl_indx (forall ((x indx)) (implies (fact neq x x) (false)))) (defgenrule neqRl_strd (forall ((x strd)) (implies (fact neq x x) (false)))) (defgenrule neqRl_mesg (forall ((x mesg)) (implies (fact neq x x) (false)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 47) (unrealized (0 0) (1 0) (2 2)) (preskeleton) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (2 3)) (n (2 0))) (comment "Not a skeleton")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((2 3) (0 0)) ((2 3) (1 0))) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 48) (parent 47) (unrealized (0 0) (2 2)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (2 3)) (n (2 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0)) (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (2 2)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 49) (parent 48) (unrealized (0 0) (1 0) (3 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation channel-test (displaced 4 2 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 50) (parent 49) (unrealized (0 0) (1 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (current-value mesg) (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value current-value) (pcr-id pcr-id-1) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2)) ((4 3) (1 0))) (non-orig aik aik-0 (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-1 current-value aik-0)) (load pcr (cat pt current-value)) (send v))) (label 51) (parent 50) (unrealized (0 0) (4 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2)) ((4 3) (1 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-decrypt) (operation encryption-test (displaced 5 3 tpm-create-key 2) (enc "created" k pcr-id-1 current-value aik-0) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))) (label 52) (parent 51) (unrealized (0 0) (4 2)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (4 2)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain"))))) (label 53) (parent 52) (unrealized (0 0) (5 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (5 1)) (strand-map 0 1 2 3 4 5) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 54) (parent 53) (unrealized (0 0) (6 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n (6 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5 6) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 55) (parent 54) (unrealized (0 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pt-2 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (rule genStV-if-hashed-tpm-quote) (operation encryption-test (added-strand tpm-quote 3) (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik) (0 0)) (strand-map 0 1 2 3 4 5 6) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)))) (label 56) (parent 55) (unrealized (7 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 1)) (strand-map 0 1 2 3 4 5 6 7) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))) (label 57) (parent 56) (unrealized (8 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 pcr-id-3 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 tpm-4 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-3) (tpm tpm-4) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 1)) (strand-map 0 1 2 3 4 5 6 7 8) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))) ((recv tpm-4 (cat "extend" pcr-id-3 n)) (load pcr-0 (cat pt-4 "0")) (stor pcr-0 (cat pt-3 (hash "0" n))))) (label 58) (parent 57) (unrealized (9 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1))) (operation nonce-test (contracted (pcr-id-3 pcr-id-0) (tpm-4 tpm)) n (9 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5 6 7 8 9) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr-0 (cat pt-4 "0")) (stor pcr-0 (cat pt-3 (hash "0" n))))) (label 59) (parent 58) (realized) (shape) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (pt-3 (9 2)) (pt-2 (8 2)) (pt-0 (6 2)) (pt (5 2)) (k (3 1)) (n (2 0)) (v (2 3)))) (comment "Nothing left to do") (defprotocol envelope-plus-2 basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule pcr-id-identifies-pcr (forall ((y z strd) (pcr-id text) (pcr pcr-0 locn)) (implies (and (p "tpm-extend-enc" z (idx 3)) (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "pcr" z pcr-0) (p "tpm-extend-enc" "pcr" y pcr) (p "tpm-extend-enc" "pcr-id" z pcr-id) (p "tpm-extend-enc" "pcr-id" y pcr-id)) (= pcr pcr-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)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig v n) (conf tpm) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 60) (unrealized (0 0) (1 2)) (preskeleton) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "Not a skeleton")) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (precedes ((1 3) (0 0))) (non-orig aik) (uniq-orig v n) (conf tpm) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 61) (parent 60) (unrealized (1 2)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id text) (k aik akey) (tpm tpm-0 chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0)) (precedes ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik) (1 2)) (strand-map 0 1) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))) (label 62) (parent 61) (unrealized (0 0) (2 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id text) (k aik akey) (tpm chan)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm) (operation channel-test (displaced 3 1 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (2 0)) (strand-map 0 1 2) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)))) (label 63) (parent 62) (unrealized (0 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (current-value mesg) (v n data) (pcr-id pcr-id-0 text) (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value current-value) (pcr-id pcr-id-0) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))) (non-orig aik aik-0 (invk k)) (uniq-orig v n k) (conf tpm) (auth tpm) (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 tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 current-value aik-0)) (load pcr (cat pt current-value)) (send v))) (label 64) (parent 63) (unrealized (3 1)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0))) (non-orig aik (invk k)) (uniq-orig v n k) (gen-st (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-decrypt) (operation encryption-test (displaced 4 2 tpm-create-key 2) (enc "created" k pcr-id-0 current-value aik-0) (3 1)) (strand-map 0 1 2 3) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))) (label 65) (parent 64) (unrealized (3 2)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 3) (0 0)) ((4 2) (3 2))) (non-orig aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (3 2)) (strand-map 0 1 2 3) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain"))))) (label 66) (parent 65) (unrealized (4 1)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-1) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2)) ((5 2) (4 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm-2 (cat "extend" pcr-id-1 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 67) (parent 66) (unrealized (5 0)) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (v n data) (pcr-id pcr-id-0 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-0) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig v n k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 2)) ((5 2) (4 1))) (operation nonce-test (contracted (pcr-id-1 pcr-id) (tpm-2 tpm)) n (5 0) (ch-msg tpm (cat "extend" pcr-id n))) (strand-map 0 1 2 3 4 5) (traces ((recv v) (send v)) ((send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-0 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 68) (parent 67) (realized) (shape) (maps ((0 1) ((v v) (n n) (pcr-id pcr-id) (k k) (aik aik) (tpm tpm)))) (origs (pt-0 (5 2)) (pt (4 2)) (k (2 1)) (n (1 0)) (v (1 3)))) (comment "Nothing left to do") (defprotocol envelope-plus-2 basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule pcr-id-identifies-pcr (forall ((y z strd) (pcr-id text) (pcr pcr-0 locn)) (implies (and (p "tpm-extend-enc" z (idx 3)) (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "pcr" z pcr-0) (p "tpm-extend-enc" "pcr" y pcr) (p "tpm-extend-enc" "pcr-id" z pcr-id) (p "tpm-extend-enc" "pcr-id" y pcr-id)) (= pcr pcr-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)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 69) (unrealized (0 0) (1 2)) (preskeleton) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "Not a skeleton")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((1 3) (0 0))) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 70) (parent 69) (unrealized (0 0) (1 2)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (1 3)) (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0)) (precedes ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (1 2)) (strand-map 0 1) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 71) (parent 70) (unrealized (0 0) (2 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((1 1) (2 0)) ((1 3) (0 0)) ((2 1) (1 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation channel-test (displaced 3 1 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (2 0)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 72) (parent 71) (unrealized (0 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-quote) (operation encryption-test (added-strand tpm-quote 3) (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik) (0 0)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)))) (label 73) (parent 72) (unrealized (3 1)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (precedes ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2)) ((3 2) (0 0)) ((4 2) (3 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "refuse"))) (3 1)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse"))))) (label 74) (parent 73) (unrealized (4 1)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1)) ((5 2) (4 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse")))) ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 75) (parent 74) (unrealized (5 0)) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((4 2) (3 1)) ((5 2) (4 1))) (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n (5 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-1 (cat "extend" pcr-id-1 "refuse")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "refuse")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 76) (parent 75) (realized) (shape) (maps ((0 1) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (pt-0 (5 2)) (pt (4 2)) (n (1 0)) (k (2 1)) (v (1 3)))) (comment "Nothing left to do") (defprotocol envelope-plus-2 basic (defrole tpm-power-on (vars (current-value mesg) (pcr locn) (tpm chan)) (trace (recv tpm "power on") (load pcr current-value) (stor pcr "0"))) (defrole tpm-extend-enc (vars (value current-value mesg) (pcr-id text) (pcr locn) (tpm chan)) (trace (recv tpm (cat "extend" pcr-id value)) (load pcr current-value) (stor pcr (hash current-value value)) (send "ext ok"))) (defrole tpm-quote (vars (nonce current-value mesg) (pcr-id text) (aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "quote" pcr-id nonce)) (load pcr current-value) (send (enc "quote" pcr-id current-value nonce aik)))) (defrole tpm-create-key (vars (k aik akey) (pcr-id text) (pcrval mesg) (tpm chan)) (trace (recv tpm (cat "create-req" pcr-id pcrval)) (send (enc "created" k pcr-id pcrval aik))) (non-orig (invk k)) (uniq-orig k) (auth tpm)) (defrole tpm-decrypt (vars (m current-value mesg) (pcr-id text) (k aik akey) (pcr locn) (tpm chan)) (trace (recv tpm (cat "decrypt" (enc m k))) (recv (enc "created" k pcr-id current-value aik)) (load pcr current-value) (send m)) (non-orig aik)) (defrole alice (vars (n v data) (pcr-id text) (k aik akey) (tpm chan)) (trace (send tpm (cat "extend" pcr-id n)) (send tpm (cat "create-req" pcr-id (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id (hash (hash "0" n) "obtain") aik)) (send (enc v k))) (non-orig aik) (uniq-orig n v) (conf tpm) (neq (k aik))) (defrule genStV-if-hashed-tpm-power-on (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-power-on" z (idx 2)) (p "tpm-power-on" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-extend-enc (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-extend-enc" z (idx 2)) (p "tpm-extend-enc" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-decrypt (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-decrypt" z (idx 3)) (p "tpm-decrypt" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule genStV-if-hashed-tpm-quote (forall ((z strd) (v1 v2 mesg)) (implies (and (p "tpm-quote" z (idx 2)) (p "tpm-quote" "current-value" z (hash v1 v2))) (gen-st (hash v1 v2))))) (defrule pcr-id-identifies-pcr (forall ((y z strd) (pcr-id text) (pcr pcr-0 locn)) (implies (and (p "tpm-extend-enc" z (idx 3)) (p "tpm-extend-enc" y (idx 3)) (p "tpm-extend-enc" "pcr" z pcr-0) (p "tpm-extend-enc" "pcr" y pcr) (p "tpm-extend-enc" "pcr-id" z pcr-id) (p "tpm-extend-enc" "pcr-id" y pcr-id)) (= pcr pcr-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)))) (defgenrule scissorsRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (trans z2 i2) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2)) (and (= z1 z2) (= i1 i2))))) (defgenrule cakeRule (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2)) (false)))) (defgenrule no-interruption (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (leads-to z0 i0 z2 i2) (trans z1 i1) (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2)) (false)))) (defgenrule discreteAfter (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z2 i2) (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2))))) (defgenrule discreteBefore (forall ((z0 z1 z2 strd) (i0 i1 i2 indx)) (implies (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1) (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2)) (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))) (defgenrule trRl_tpm-power-on-at-2 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-power-on-at-1 (forall ((z strd)) (implies (p "tpm-power-on" z (idx 3)) (trans z (idx 1))))) (defgenrule trRl_tpm-extend-enc-at-2 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 2))))) (defgenrule trRl_tpm-extend-enc-at-1 (forall ((z strd)) (implies (p "tpm-extend-enc" z (idx 3)) (trans z (idx 1))))) (defgenrule eff-tpm-quote-2 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-quote" z (idx 3)) (prec z (idx 2) z1 i)) (or (= z z1) (and (p "tpm-quote" z (idx 2)) (prec z (idx 1) z1 i)))))) (defgenrule eff-tpm-decrypt-3 (forall ((i indx) (z1 z strd)) (implies (and (p "tpm-decrypt" z (idx 4)) (prec z (idx 3) z1 i)) (or (= z z1) (and (p "tpm-decrypt" z (idx 3)) (prec z (idx 2) z1 i))))))) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 77) (unrealized (0 0) (1 0) (2 2)) (preskeleton) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (2 3)) (n (2 0))) (comment "Not a skeleton")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((2 3) (0 0)) ((2 3) (1 0))) (non-orig aik) (uniq-orig n v) (conf tpm) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k)))) (label 78) (parent 77) (unrealized (0 0) (2 2)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (v (2 3)) (n (2 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm tpm-0 chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0)) (precedes ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm-0) (operation encryption-test (added-strand tpm-create-key 2) (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik) (2 2)) (strand-map 0 1 2) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 79) (parent 78) (unrealized (0 0) (1 0) (3 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (tpm chan)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (1 0)) ((3 1) (2 2))) (non-orig aik (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation channel-test (displaced 4 2 alice 2) (ch-msg tpm-0 (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (3 0)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)))) (label 80) (parent 79) (unrealized (0 0) (1 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (current-value mesg) (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik aik-0 akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value current-value) (pcr-id pcr-id-1) (k k) (aik aik-0) (tpm tpm-0) (pcr pcr)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2)) ((4 3) (1 0))) (non-orig aik aik-0 (invk k)) (uniq-orig n v k) (conf tpm) (auth tpm) (operation nonce-test (added-strand tpm-decrypt 4) v (1 0) (enc v k)) (strand-map 0 1 2 3) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-1 current-value aik-0)) (load pcr (cat pt current-value)) (send v))) (label 81) (parent 80) (unrealized (0 0) (4 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 text) (k aik akey) (pt pval) (tpm tpm-0 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (precedes ((2 1) (3 0)) ((2 3) (0 0)) ((2 3) (4 0)) ((3 1) (2 2)) ((4 3) (1 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (rule genStV-if-hashed-tpm-decrypt) (operation encryption-test (displaced 5 3 tpm-create-key 2) (enc "created" k pcr-id-1 current-value aik-0) (4 1)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v))) (label 82) (parent 81) (unrealized (0 0) (4 2)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2))) (rule genStV-if-hashed-tpm-extend-enc trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt (hash (hash "0" n) "obtain"))) (4 2)) (strand-map 0 1 2 3 4) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain"))))) (label 83) (parent 82) (unrealized (0 0) (5 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-2) (tpm tpm-2) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr (cat pt-0 (hash "0" n))) (5 1)) (strand-map 0 1 2 3 4 5) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm-2 (cat "extend" pcr-id-2 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 84) (parent 83) (unrealized (0 0) (6 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pval) (tpm tpm-0 tpm-1 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (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 aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (operation nonce-test (contracted (pcr-id-2 pcr-id-0) (tpm-2 tpm)) n (6 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5 6) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n))))) (label 85) (parent 84) (unrealized (0 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 text) (k aik akey) (pt pt-0 pt-1 pt-2 pval) (tpm tpm-0 tpm-1 tpm-2 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1))) (rule genStV-if-hashed-tpm-quote) (operation encryption-test (added-strand tpm-quote 3) (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik) (0 0)) (strand-map 0 1 2 3 4 5 6) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)))) (label 86) (parent 85) (unrealized (7 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (7 1)) (strand-map 0 1 2 3 4 5 6 7) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))))) (label 87) (parent 86) (unrealized (8 1)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 pcr-id-3 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 tpm-4 chan) (pcr pcr-0 locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr-0)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-3) (tpm tpm-4) (pcr pcr-0)) (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1))) (rule trRl_tpm-extend-enc-at-1 trRl_tpm-extend-enc-at-2) (operation channel-test (added-strand tpm-extend-enc 3) (ch-msg pcr-0 (cat pt-3 (hash "0" n))) (8 1)) (strand-map 0 1 2 3 4 5 6 7 8) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr-0 (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr-0 (cat pt-3 (hash "0" n))) (stor pcr-0 (cat pt-2 (hash (hash "0" n) "refuse")))) ((recv tpm-4 (cat "extend" pcr-id-3 n)) (load pcr-0 (cat pt-4 "0")) (stor pcr-0 (cat pt-3 (hash "0" n))))) (label 88) (parent 87) (unrealized (9 0)) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (comment "1 in cohort - 1 not yet seen")) (defskeleton envelope-plus-2 (vars (n v data) (pcr-id pcr-id-0 pcr-id-1 pcr-id-2 text) (k aik akey) (pt pt-0 pt-1 pt-2 pt-3 pt-4 pval) (tpm tpm-0 tpm-1 tpm-2 tpm-3 chan) (pcr locn)) (deflistener (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (deflistener v) (defstrand alice 4 (n n) (v v) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm)) (defstrand tpm-decrypt 4 (m v) (current-value (hash (hash "0" n) "obtain")) (pcr-id pcr-id-0) (k k) (aik aik) (tpm tpm-0) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "obtain") (current-value (hash "0" n)) (pcr-id pcr-id-1) (tpm tpm-1) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (defstrand tpm-quote 3 (nonce (enc v k)) (current-value (hash (hash "0" n) "refuse")) (pcr-id pcr-id) (aik aik) (tpm tpm-2) (pcr pcr)) (defstrand tpm-extend-enc 3 (value "refuse") (current-value (hash "0" n)) (pcr-id pcr-id-2) (tpm tpm-3) (pcr pcr)) (defstrand tpm-extend-enc 3 (value n) (current-value "0") (pcr-id pcr-id-0) (tpm tpm) (pcr pcr)) (precedes ((2 0) (6 0)) ((2 0) (9 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (7 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1)) ((7 2) (0 0)) ((8 2) (7 1)) ((9 2) (8 1))) (non-orig aik (invk k)) (uniq-orig n v k) (gen-st (hash "0" n) (hash (hash "0" n) "obtain") (hash (hash "0" n) "refuse")) (conf tpm) (auth tpm) (leads-to ((5 2) (4 2)) ((6 2) (5 1)) ((8 2) (7 1)) ((9 2) (8 1))) (rule pcr-id-identifies-pcr) (operation nonce-test (contracted (pcr-0 pcr) (pcr-id-3 pcr-id-0) (tpm-4 tpm)) n (9 0) (ch-msg tpm (cat "extend" pcr-id-0 n))) (strand-map 0 1 2 3 4 5 6 7 8 9) (traces ((recv (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik)) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv v) (send v)) ((send tpm (cat "extend" pcr-id-0 n)) (send tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (send (enc v k))) ((recv tpm (cat "create-req" pcr-id-0 (hash (hash "0" n) "obtain"))) (send (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik))) ((recv tpm-0 (cat "decrypt" (enc v k))) (recv (enc "created" k pcr-id-0 (hash (hash "0" n) "obtain") aik)) (load pcr (cat pt (hash (hash "0" n) "obtain"))) (send v)) ((recv tpm-1 (cat "extend" pcr-id-1 "obtain")) (load pcr (cat pt-0 (hash "0" n))) (stor pcr (cat pt (hash (hash "0" n) "obtain")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-1 "0")) (stor pcr (cat pt-0 (hash "0" n)))) ((recv tpm-2 (cat "quote" pcr-id (enc v k))) (load pcr (cat pt-2 (hash (hash "0" n) "refuse"))) (send (enc "quote" pcr-id (hash (hash "0" n) "refuse") (enc v k) aik))) ((recv tpm-3 (cat "extend" pcr-id-2 "refuse")) (load pcr (cat pt-3 (hash "0" n))) (stor pcr (cat pt-2 (hash (hash "0" n) "refuse")))) ((recv tpm (cat "extend" pcr-id-0 n)) (load pcr (cat pt-4 "0")) (stor pcr (cat pt-3 (hash "0" n))))) (label 89) (parent 88) (realized) (shape) (maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (pcr-id pcr-id) (pcr-id-0 pcr-id-0) (tpm tpm)))) (origs (pt-3 (9 2)) (pt-2 (8 2)) (pt-0 (6 2)) (pt (5 2)) (k (3 1)) (n (2 0)) (v (2 3)))) (comment "Nothing left to do")