cpsa-4.4.4: tst/envelope_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald "Envelope Protocol" (bound 15))
(comment "CPSA 4.3.1")
(comment "All input read from tst/envelope.scm")
(comment "Strand count bounded at 15")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig v n)
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 0)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (v n data) (esk pcrkey skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(pcrkey pcrkey) (k k) (aik aik))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig v n k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey)) (5 1))
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv (enc (hash (hash "0" n) "obtain") (hash pcrkey))) (send v))
((recv (cat "extend" "obtain"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "obtain") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey)))))
(label 13)
(parent 0)
(realized)
(shape)
(maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 15)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk pcrkey skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (pcrkey pcrkey)
(aik aik))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig n v k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey)) (5 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "quote" (enc v k)))
(recv (enc (hash (hash "0" n) "refuse") (hash pcrkey)))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "refuse") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey)))))
(label 27)
(parent 15)
(realized)
(shape)
(maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 29)
(unrealized (0 0) (1 0) (2 2))
(preskeleton)
(origs (v (2 3)) (n (2 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk pcrkey skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(pcrkey pcrkey) (k k) (aik aik))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (pcrkey pcrkey)
(aik aik))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(pcrkey pcrkey))
(precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
((6 2) (9 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig n v k)
(operation encryption-test (displaced 10 6 tpm-extend-enc 3)
(enc (hash "0" n) (hash pcrkey-0)) (9 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv (enc (hash (hash "0" n) "obtain") (hash pcrkey))) (send v))
((recv (cat "extend" "obtain"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "obtain") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey))))
((recv (cat "quote" (enc v k)))
(recv (enc (hash (hash "0" n) "refuse") (hash pcrkey)))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "refuse") (hash pcrkey)))))
(label 48)
(parent 29)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(defskeleton envelope
(vars (n v data) (esk pcrkey skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(pcrkey pcrkey) (k k) (aik aik))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (pcrkey pcrkey)
(aik aik))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
((6 2) (5 1)) ((7 1) (6 1)) ((7 1) (10 1)) ((8 2) (0 0))
((9 2) (8 1)) ((10 2) (9 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig n v k)
(operation encryption-test (displaced 11 7 tpm-power-on 2)
(enc "0" (hash pcrkey-0)) (10 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv (enc (hash (hash "0" n) "obtain") (hash pcrkey))) (send v))
((recv (cat "extend" "obtain"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "obtain") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey))))
((recv (cat "quote" (enc v k)))
(recv (enc (hash (hash "0" n) "refuse") (hash pcrkey)))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "refuse") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey)))))
(label 53)
(parent 29)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(defskeleton envelope
(vars (n v data) (esk pcrkey pcrkey-0 skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(pcrkey pcrkey) (k k) (aik aik))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (pcrkey pcrkey-0)
(aik aik))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(pcrkey pcrkey-0))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey-0) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey-0))
(precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
((10 2) (9 1)) ((11 1) (10 1)))
(non-orig esk pcrkey pcrkey-0 aik (invk k))
(uniq-orig n v k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey-0)) (10 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv (enc (hash (hash "0" n) "obtain") (hash pcrkey))) (send v))
((recv (cat "extend" "obtain"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "obtain") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey))))
((recv (cat "quote" (enc v k)))
(recv (enc (hash (hash "0" n) "refuse") (hash pcrkey-0)))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse"))
(recv (enc (hash "0" n) (hash pcrkey-0)))
(send (enc (hash (hash "0" n) "refuse") (hash pcrkey-0))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey-0)))
(send (enc (hash "0" n) (hash pcrkey-0))))
((recv "power on") (send (enc "0" (hash pcrkey-0)))))
(label 54)
(parent 29)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (pcrkey skey))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "pcrkey" y pcrkey)
(p "tpm-extend" "pcrkey" z pcrkey))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig v n)
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 56)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (v n data) (esk pcrkey skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(pcrkey pcrkey) (k k) (aik aik))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig v n k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey)) (5 1))
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv (enc (hash (hash "0" n) "obtain") (hash pcrkey))) (send v))
((recv (cat "extend" "obtain"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "obtain") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey)))))
(label 68)
(parent 56)
(realized)
(shape)
(maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (pcrkey skey))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "pcrkey" y pcrkey)
(p "tpm-extend" "pcrkey" z pcrkey))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 70)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk pcrkey skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (pcrkey pcrkey)
(aik aik))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig n v k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey)) (5 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "quote" (enc v k)))
(recv (enc (hash (hash "0" n) "refuse") (hash pcrkey)))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "refuse") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey)))))
(label 81)
(parent 70)
(realized)
(shape)
(maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (pcrkey skey))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "pcrkey" y pcrkey)
(p "tpm-extend" "pcrkey" z pcrkey))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 83)
(unrealized (0 0) (1 0) (2 2))
(preskeleton)
(origs (v (2 3)) (n (2 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk pcrkey pcrkey-0 skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(pcrkey pcrkey) (k k) (aik aik))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (pcrkey pcrkey-0)
(aik aik))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(pcrkey pcrkey-0))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey-0) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey-0))
(precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
((10 2) (9 1)) ((11 1) (10 1)))
(non-orig esk pcrkey pcrkey-0 aik (invk k))
(uniq-orig n v k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey-0)) (10 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv (enc (hash (hash "0" n) "obtain") (hash pcrkey))) (send v))
((recv (cat "extend" "obtain"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "obtain") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey))))
((recv (cat "quote" (enc v k)))
(recv (enc (hash (hash "0" n) "refuse") (hash pcrkey-0)))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse"))
(recv (enc (hash "0" n) (hash pcrkey-0)))
(send (enc (hash (hash "0" n) "refuse") (hash pcrkey-0))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey-0)))
(send (enc (hash "0" n) (hash pcrkey-0))))
((recv "power on") (send (enc "0" (hash pcrkey-0)))))
(label 104)
(parent 83)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (pcrkey skey))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "pcrkey" y pcrkey)
(p "tpm-extend" "pcrkey" z pcrkey))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defrule esk-same-as-pcrkey
(forall ((y z strd) (esk pcrkey pcrkey-0 skey))
(implies
(and (p "tpm-extend-enc" y 3) (p "tpm-extend-enc" z 3)
(p "tpm-extend-enc" "esk" y esk)
(p "tpm-extend-enc" "esk" z esk)
(p "tpm-extend-enc" "pcrkey" y pcrkey)
(p "tpm-extend-enc" "pcrkey" z pcrkey-0))
(= pcrkey pcrkey-0))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig v n)
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 106)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (v n data) (esk pcrkey skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(pcrkey pcrkey) (k k) (aik aik))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig v n k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey)) (5 1))
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv (enc (hash (hash "0" n) "obtain") (hash pcrkey))) (send v))
((recv (cat "extend" "obtain"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "obtain") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey)))))
(label 118)
(parent 106)
(realized)
(shape)
(maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (pcrkey skey))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "pcrkey" y pcrkey)
(p "tpm-extend" "pcrkey" z pcrkey))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defrule esk-same-as-pcrkey
(forall ((y z strd) (esk pcrkey pcrkey-0 skey))
(implies
(and (p "tpm-extend-enc" y 3) (p "tpm-extend-enc" z 3)
(p "tpm-extend-enc" "esk" y esk)
(p "tpm-extend-enc" "esk" z esk)
(p "tpm-extend-enc" "pcrkey" y pcrkey)
(p "tpm-extend-enc" "pcrkey" z pcrkey-0))
(= pcrkey pcrkey-0))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 120)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk pcrkey skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (pcrkey pcrkey)
(aik aik))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(pcrkey pcrkey))
(defstrand tpm-extend-enc 3 (value n) (current-value "0")
(pcrkey pcrkey) (esk esk))
(defstrand tpm-power-on 2 (pcrkey pcrkey))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk pcrkey aik (invk k))
(uniq-orig n v k)
(operation encryption-test (added-strand tpm-power-on 2)
(enc "0" (hash pcrkey)) (5 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "quote" (enc v k)))
(recv (enc (hash (hash "0" n) "refuse") (hash pcrkey)))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse"))
(recv (enc (hash "0" n) (hash pcrkey)))
(send (enc (hash (hash "0" n) "refuse") (hash pcrkey))))
((recv (enc "extend" n esk)) (recv (enc "0" (hash pcrkey)))
(send (enc (hash "0" n) (hash pcrkey))))
((recv "power on") (send (enc "0" (hash pcrkey)))))
(label 131)
(parent 120)
(realized)
(shape)
(maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (pcrkey skey))
(trace (recv "power on") (send (enc "0" (hash pcrkey))))
(non-orig pcrkey))
(defrole tpm-extend
(vars (value current-value mesg) (pcrkey skey))
(trace (recv (cat "extend" value))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey))
(defrole tpm-extend-enc
(vars (value current-value mesg) (pcrkey esk skey))
(trace (recv (enc "extend" value esk))
(recv (enc current-value (hash pcrkey)))
(send (enc (hash current-value value) (hash pcrkey)))
(send "ext ok"))
(non-orig pcrkey esk))
(defrole tpm-quote
(vars (nonce current-value mesg) (pcrkey skey) (aik akey))
(trace (recv (cat "quote" nonce))
(recv (enc current-value (hash pcrkey)))
(send (enc "quote" current-value nonce aik)))
(non-orig pcrkey aik))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (pcrkey skey))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik))
(recv (enc pcrvals (hash pcrkey))) (send m))
(non-orig pcrkey aik))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (pcrkey skey))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "pcrkey" y pcrkey)
(p "tpm-extend" "pcrkey" z pcrkey))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defrule esk-same-as-pcrkey
(forall ((y z strd) (esk pcrkey pcrkey-0 skey))
(implies
(and (p "tpm-extend-enc" y 3) (p "tpm-extend-enc" z 3)
(p "tpm-extend-enc" "esk" y esk)
(p "tpm-extend-enc" "esk" z esk)
(p "tpm-extend-enc" "pcrkey" y pcrkey)
(p "tpm-extend-enc" "pcrkey" z pcrkey-0))
(= pcrkey pcrkey-0))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 133)
(unrealized (0 0) (1 0) (2 2))
(preskeleton)
(origs (v (2 3)) (n (2 0)))
(comment "Not a skeleton"))
(comment "Nothing left to do")