cpsa-4.4.4: tst/chan-envelope_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald "Envelope Protocol With Channels" (bound 15))
(comment "CPSA 4.3.1")
(comment "All input read from tst/chan-envelope.scm")
(comment "Strand count bounded at 15")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig v n)
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 0)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey) (c chan))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(k k) (aik aik) (c c))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk aik (invk k))
(uniq-orig v n k)
(conf c)
(auth c)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
(5 1))
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv c (hash (hash "0" n) "obtain")) (send v))
((recv (cat "extend" "obtain")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "obtain")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0")))
(label 11)
(parent 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 (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 12)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey) (c chan))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk aik (invk k))
(uniq-orig n v k)
(conf c)
(auth c)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
(5 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "quote" (enc v k)))
(recv c (hash (hash "0" n) "refuse"))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "refuse")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0")))
(label 22)
(parent 12)
(realized)
(shape)
(maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 23)
(unrealized (0 0) (1 0) (2 2))
(preskeleton)
(origs (v (2 3)) (n (2 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey) (c chan))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(k k) (aik aik) (c c))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(c c))
(precedes ((2 0) (6 0)) ((2 1) (3 0)) ((2 3) (4 0)) ((2 3) (8 0))
((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2)) ((6 2) (5 1))
((6 2) (9 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1)))
(non-orig esk aik (invk k))
(uniq-orig n v k)
(conf c)
(auth c)
(operation channel-test (displaced 10 6 tpm-extend-enc 3)
(ch-msg c-0 (hash "0" n)) (9 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv c (hash (hash "0" n) "obtain")) (send v))
((recv (cat "extend" "obtain")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "obtain")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0"))
((recv (cat "quote" (enc v k)))
(recv c (hash (hash "0" n) "refuse"))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "refuse"))))
(label 39)
(parent 23)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey) (c chan))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(k k) (aik aik) (c c))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
((6 2) (5 1)) ((7 1) (6 1)) ((7 1) (10 1)) ((8 2) (0 0))
((9 2) (8 1)) ((10 2) (9 1)))
(non-orig esk aik (invk k))
(uniq-orig n v k)
(conf c)
(auth c)
(operation channel-test (displaced 11 7 tpm-power-on 2)
(ch-msg c-0 "0") (10 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv c (hash (hash "0" n) "obtain")) (send v))
((recv (cat "extend" "obtain")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "obtain")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0"))
((recv (cat "quote" (enc v k)))
(recv c (hash (hash "0" n) "refuse"))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "refuse")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n))))
(label 42)
(parent 23)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(k k) (aik aik) (c c))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(c c-0))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c-0))
(defstrand tpm-power-on 2 (c c-0))
(precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
((10 2) (9 1)) ((11 1) (10 1)))
(non-orig esk aik (invk k))
(uniq-orig n v k)
(conf c c-0)
(auth c c-0)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c-0 "0")
(10 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv c (hash (hash "0" n) "obtain")) (send v))
((recv (cat "extend" "obtain")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "obtain")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0"))
((recv (cat "quote" (enc v k)))
(recv c-0 (hash (hash "0" n) "refuse"))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
(send c-0 (hash (hash "0" n) "refuse")))
((recv (enc "extend" n esk)) (recv c-0 "0") (send c-0 (hash "0" n)))
((recv "power on") (send c-0 "0")))
(label 43)
(parent 23)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (c chan))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
(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 44)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey) (c chan))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(k k) (aik aik) (c c))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk aik (invk k))
(uniq-orig v n k)
(conf c)
(auth c)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
(5 1))
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv c (hash (hash "0" n) "obtain")) (send v))
((recv (cat "extend" "obtain")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "obtain")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0")))
(label 54)
(parent 44)
(realized)
(shape)
(maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (c chan))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
(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 55)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey) (c chan))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk aik (invk k))
(uniq-orig n v k)
(conf c)
(auth c)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
(5 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "quote" (enc v k)))
(recv c (hash (hash "0" n) "refuse"))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "refuse")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0")))
(label 64)
(parent 55)
(realized)
(shape)
(maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (c chan))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
(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 65)
(unrealized (0 0) (1 0) (2 2))
(preskeleton)
(origs (v (2 3)) (n (2 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey) (c c-0 chan))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(k k) (aik aik) (c c))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (aik aik) (c c-0))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(c c-0))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c-0))
(defstrand tpm-power-on 2 (c c-0))
(precedes ((2 0) (6 0)) ((2 0) (10 0)) ((2 1) (3 0)) ((2 3) (4 0))
((2 3) (8 0)) ((3 1) (2 2)) ((4 3) (1 0)) ((5 2) (4 2))
((6 2) (5 1)) ((7 1) (6 1)) ((8 2) (0 0)) ((9 2) (8 1))
((10 2) (9 1)) ((11 1) (10 1)))
(non-orig esk aik (invk k))
(uniq-orig n v k)
(conf c c-0)
(auth c c-0)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c-0 "0")
(10 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv c (hash (hash "0" n) "obtain")) (send v))
((recv (cat "extend" "obtain")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "obtain")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0"))
((recv (cat "quote" (enc v k)))
(recv c-0 (hash (hash "0" n) "refuse"))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse")) (recv c-0 (hash "0" n))
(send c-0 (hash (hash "0" n) "refuse")))
((recv (enc "extend" n esk)) (recv c-0 "0") (send c-0 (hash "0" n)))
((recv "power on") (send c-0 "0")))
(label 81)
(parent 65)
(realized)
(shape)
(maps ((0 1 2) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (2 0)) (k (3 1)) (v (2 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (c chan))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defrule esk-same-as-chan
(forall ((y z strd) (esk skey) (c c-0 chan))
(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" "c" y c)
(p "tpm-extend-enc" "c" z c-0))
(= c c-0))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig v n)
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 82)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (v n data) (esk skey) (k aik akey) (c chan))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-decrypt 4 (m v) (pcrvals (hash (hash "0" n) "obtain"))
(k k) (aik aik) (c c))
(defstrand tpm-extend 3 (value "obtain") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 3) (0 0)) ((4 2) (3 2)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk aik (invk k))
(uniq-orig v n k)
(conf c)
(auth c)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
(5 1))
(traces ((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "decrypt" (enc v k)))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(recv c (hash (hash "0" n) "obtain")) (send v))
((recv (cat "extend" "obtain")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "obtain")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0")))
(label 92)
(parent 82)
(realized)
(shape)
(maps ((0 1) ((v v) (n n) (esk esk) (k k) (aik aik))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (c chan))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defrule esk-same-as-chan
(forall ((y z strd) (esk skey) (c c-0 chan))
(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" "c" y c)
(p "tpm-extend-enc" "c" z c-0))
(= c c-0))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 93)
(unrealized (0 0) (1 2))
(preskeleton)
(origs (v (1 3)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey) (c chan))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(defstrand tpm-create-key 2 (pcrval (hash (hash "0" n) "obtain"))
(esk esk) (k k) (aik aik))
(defstrand tpm-quote 3 (nonce (enc v k))
(current-value (hash (hash "0" n) "refuse")) (aik aik) (c c))
(defstrand tpm-extend 3 (value "refuse") (current-value (hash "0" n))
(c c))
(defstrand tpm-extend-enc 3 (value n) (current-value "0") (esk esk)
(c c))
(defstrand tpm-power-on 2 (c c))
(precedes ((1 0) (5 0)) ((1 1) (2 0)) ((1 3) (3 0)) ((2 1) (1 2))
((3 2) (0 0)) ((4 2) (3 1)) ((5 2) (4 1)) ((6 1) (5 1)))
(non-orig esk aik (invk k))
(uniq-orig n v k)
(conf c)
(auth c)
(operation channel-test (added-strand tpm-power-on 2) (ch-msg c "0")
(5 1))
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
((recv (enc "create key" (hash (hash "0" n) "obtain") esk))
(send (enc "created" k (hash (hash "0" n) "obtain") aik)))
((recv (cat "quote" (enc v k)))
(recv c (hash (hash "0" n) "refuse"))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv (cat "extend" "refuse")) (recv c (hash "0" n))
(send c (hash (hash "0" n) "refuse")))
((recv (enc "extend" n esk)) (recv c "0") (send c (hash "0" n)))
((recv "power on") (send c "0")))
(label 102)
(parent 93)
(realized)
(shape)
(maps ((0 1) ((n n) (v v) (k k) (aik aik) (esk esk))))
(origs (n (1 0)) (k (2 1)) (v (1 3))))
(comment "Nothing left to do")
(defprotocol envelope basic
(defrole tpm-power-on
(vars (c chan))
(trace (recv "power on") (send c "0"))
(conf c)
(auth c))
(defrole tpm-extend
(vars (value current-value mesg) (c chan))
(trace (recv (cat "extend" value)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(conf c)
(auth c))
(defrole tpm-extend-enc
(vars (value current-value mesg) (esk skey) (c chan))
(trace (recv (enc "extend" value esk)) (recv c current-value)
(send c (hash current-value value)) (send "ext ok"))
(non-orig esk)
(conf c)
(auth c))
(defrole tpm-quote
(vars (nonce current-value mesg) (c chan) (aik akey))
(trace (recv (cat "quote" nonce)) (recv c current-value)
(send (enc "quote" current-value nonce aik)))
(non-orig aik)
(conf c)
(auth c))
(defrole tpm-create-key
(vars (k aik akey) (pcrval mesg) (esk skey))
(trace (recv (enc "create key" pcrval esk))
(send (enc "created" k pcrval aik)))
(non-orig esk aik (invk k))
(uniq-orig k))
(defrole tpm-decrypt
(vars (m pcrvals mesg) (k aik akey) (c chan))
(trace (recv (cat "decrypt" (enc m k)))
(recv (enc "created" k pcrvals aik)) (recv c pcrvals) (send m))
(non-orig aik)
(conf c)
(auth c))
(defrole alice
(vars (n v data) (esk skey) (k aik akey))
(trace (send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k)))
(non-orig esk aik)
(uniq-orig n v))
(defrule ordered-extends
(forall ((y z strd) (c chan))
(implies
(and (p "tpm-extend" y 3) (p "tpm-extend" z 3)
(p "tpm-extend" "c" y c) (p "tpm-extend" "c" z c))
(or (= y z) (prec y 2 z 3) (prec z 2 y 3)))))
(defrule esk-same-as-chan
(forall ((y z strd) (esk skey) (c c-0 chan))
(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" "c" y c)
(p "tpm-extend-enc" "c" z c-0))
(= c c-0))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton envelope
(vars (n v data) (esk skey) (k aik akey))
(deflistener (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(deflistener v)
(defstrand alice 4 (n n) (v v) (esk esk) (k k) (aik aik))
(non-orig esk aik)
(uniq-orig n v)
(traces
((recv (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik))
(send (enc "quote" (hash (hash "0" n) "refuse") (enc v k) aik)))
((recv v) (send v))
((send (enc "extend" n esk))
(send (enc "create key" (hash (hash "0" n) "obtain") esk))
(recv (enc "created" k (hash (hash "0" n) "obtain") aik))
(send (enc v k))))
(label 103)
(unrealized (0 0) (1 0) (2 2))
(preskeleton)
(origs (v (2 3)) (n (2 0)))
(comment "Not a skeleton"))
(comment "Nothing left to do")