Skip to content
Snippets Groups Projects
Commit 116baa7b authored by Dustin Kern's avatar Dustin Kern
Browse files

details for test machine

parent d9fdfd17
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
README.md
+ 1
− 1
View file @ 116baa7b
......@@ -8,7 +8,7 @@ In the following, we first provide usage instructions for our model, then we lis
## Execution Instructions
The [Tamarin prover](https://tamarin-prover.github.io/) is required to verify the model. Our files have been developed and verified with [Tamarin version 1.6.0](https://github.com/tamarin-prover/tamarin-prover/releases/tag/1.6.0). At the beginning of each model file, the command to generate the corresponding Tamarin proof(s) is given, together with its expected output and the verification times on our test machine, which can be used as an orientation. Please note that these instructions are for Tamarin 1.6.0, later versions of Tamarin might require minor modifications. For example, in Tamarin 1.6.1, the precedence of specified heuristics has been changed, affecting proof generation for the [Security_Properties](Security_Properties/) model files.
The [Tamarin prover](https://tamarin-prover.github.io/) is required to verify the model. Our files have been developed and verified with [Tamarin version 1.6.0](https://github.com/tamarin-prover/tamarin-prover/releases/tag/1.6.0). At the beginning of each model file, the command to generate the corresponding Tamarin proof(s) is given, together with its expected output and the verification times on our test machine (a Lenovo ThinkPad T14 Gen 1 with an AMD® Ryzen 7 pro 4750u CPU and 16GB RAM), which can be used as an orientation. Please note that these instructions are for Tamarin 1.6.0, later versions of Tamarin might require minor modifications. For example, in Tamarin 1.6.1, the precedence of specified heuristics has been changed, affecting proof generation for the [Security_Properties](Security_Properties/) model files.
Please consult the [Tamarin-Prover Manual](https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf) for installation and usage instructions. In addition, Python is required for the oracles.
......
Security_Properties/README.md
+ 5
− 1
View file @ 116baa7b
......@@ -4,8 +4,12 @@ These files have been developed and verified with Tamarin version 1.6.0.
They can be verified with the following Tamarin command:
`tamarin-prover <filename> --heuristic=I --prove --quit-on-warning`
`tamarin-prover <filename> --heuristic=<I|S> --prove --quit-on-warning`
Hereby, `<filename>` has to be replaced with the name of the file that shall be verified (see the comment at the beginning of the files). Optionally, the number of Thread used by Tamarin can be specified by appending ` +RTS -N<number of threads> -RTS`, which can improve verification times.
Depending on `<filename>`, the heuristic should be set to `I` or `S` to optimize verification times. For `daa_pnc_credential_installation.spthy` use `--heuristic=S`.
For both `daa_pnc_charge_authorisation_*.spthy` models use `--heuristic=I`.
Some lemmas use an oracle heuristic (via `[heuristic=o]` at the lemma definition), which overwrites the commandline `--heuristic=<I|S>` argument in Tamarin version 1.6.0.
As the python oracle is used during verification, it is important that it is located in the same folder as the command is run (and that the oracle file is executable).
\ No newline at end of file
Security_Properties/Tamarin_1_6_1/daa_pnc_credential_installation.spthy
+ 1
− 1
View file @ 116baa7b
......@@ -37,7 +37,7 @@ time tamarin-prover daa_pnc_credential_installation.spthy\
==============================================================================
summary of summaries:
analyzed: join2_wCP2test3.spthy
analyzed: daa_pnc_credential_installation.spthy
forwarded_credential_res_source (all-traces): verified (265 steps)
secrecy_of_cps_private_key (all-traces): verified (3 steps)
......
Security_Properties/daa_pnc_charge_authorisation_offline.spthy
+ 3
− 346
View file @ 116baa7b
......@@ -75,23 +75,12 @@ analyzed: daa_pnc_charge_authorisation_offline.spthy
auth_non_injective_agreement_charge_data (all-traces): verified (146 steps)
auth_injective_agreement_charge_data (all-traces): verified (154 steps)
SP3_Unforgeability_Off (all-traces): verified (100 steps)
test_auth_non_injective_agreement_CP_sessKey (all-traces): verified (46 steps)
test_auth_non_injective_agreement_CP (all-traces): verified (47 steps)
test_auth_injective_agreement_CP (all-traces): verified (133 steps)
test_new_test_CP_sessKey (all-traces): verified (88 steps)
test_key_tpm_binding_test2 (all-traces): verified (87 steps)
test_new_auth_non_injective_agreement_CP_data (all-traces): verified (105 steps)
test_new_auth_injective_agreement_CP_data (all-traces): verified (111 steps)
test_auth_injective_agreement_CP_test2 (all-traces): verified (9 steps)
test_test1 (all-traces): verified (45 steps)
test_test2 (all-traces): verified (100 steps)
test_test (all-traces): verified (84 steps)
==============================================================================
real 25m16,817s
user 131m36,396s
sys 38m37,382s
real 21m16,613s
user 107m28,518s
sys 30m39,522s
*/
......@@ -2932,336 +2921,4 @@ lemma SP3_Unforgeability_Off [heuristic=o]:
"
//------------------
/*
test_auth_non_injective_agreement_CP_sessKey (all-traces): verified (39 steps)
test_auth_non_injective_agreement_CP (all-traces): verified (34 steps)
test_auth_injective_agreement_CP (all-traces): verified (90 steps)
test_test1 (all-traces): verified (38 steps)
test_test2 (all-traces): verified (74 steps)
test_test (all-traces): verified (82 steps)
test_new_test_CP_sessKey (all-traces): verified (42 steps)
test_new_test2 (all-traces): verified (35 steps)
test_new_auth_non_injective_agreement_CP_data (all-traces): verified (41 steps)
test_new_auth_injective_agreement_CP_data (all-traces): verified (43 steps)
==============================================================================
real 4m3,337s
user 21m27,048s
sys 5m8,335s
*/
lemma test_auth_non_injective_agreement_CP_sessKey [heuristic=o]:
"
All CP g n #i .
(
(
CommitCP( CP, pk(g), n ) @ i
)
==>
(
// Implies there exists a running issuer on the same term
(Ex TPM Host #j . DeriveSessionKey( TPM, Host, g ) @ j)
|
(Ex sigma f #j #kr .
VerifiedCertificate2( CP, sigma, pk(g), f ) @ j
& KeyReveal('TPM_DAAReveal_f', f) @ kr)
|
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
)
)
"
lemma test_auth_non_injective_agreement_CP:
"
All CP g n TPM Host #i #i2 .
(
(
CommitCP( CP, pk(g), n ) @ i
&
DeriveSessionKey(TPM, Host, g) @ i2
)
==>
(
// Implies there exists a running issuer on the same term
(Ex #j . RunningEV_Sign2( TPM, Host, CP, n ) @ j)
|
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
|
(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
)
)
"
lemma test_auth_injective_agreement_CP:
"
All CP g n TPM Host #i #i2 .
(
(
CommitCP( CP, pk(g), n ) @ i
&
DeriveSessionKey(TPM, Host, g) @ i2
)
==>
(
// Implies there exists a running issuer on the same term
(
Ex #j . RunningEV_Sign2( TPM, Host, CP, n ) @ j
&
(#j<#i)
&
// And each commited JOIN session corresponds to a unique issuer run
( not(
Ex CP2 g2 #i3 . ( CommitCP( CP2, pk(g2), n) @ i3 & not(#i3=#i) )
)
)
)
|
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
|
(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
)
)
"
//New:
/*
test_new_test_CP_sessKey (all-traces): verified (42 steps)
test_new_test2 (all-traces): verified (35 steps)
test_new_auth_non_injective_agreement_CP_data (all-traces): verified (41 steps)
test_new_auth_injective_agreement_CP_data (all-traces): verified (43 steps)
*/
lemma test_new_test_CP_sessKey [heuristic=o]:
"
All CP g sk_emaid #i .
(
(
CP_DataRec2( CP, pk(g), sk_emaid ) @ i
)
==>
(
// Implies there exists a running issuer on the same term
(Ex TPM Host #j . DeriveSessionKey( TPM, Host, g ) @ j)
|
(Ex sigma f #j #kr .
VerifiedCertificate2( CP, sigma, pk(g), f ) @ j
& KeyReveal('TPM_DAAReveal_f', f) @ kr)
|
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
)
)
"
lemma test_key_tpm_binding_test2 [heuristic=o]:
"
All CP g sk_emaid TPM Host #i #i2 .
// For all commited JOIN sessions running between a platform and issuer on the term(s) n
(
CP_DataRec2( CP, pk(g), sk_emaid ) @ i
&
DeriveSessionKey(TPM, Host, g) @ i2
==> // Implies that an issuer has previously been involved in a protocol run
( (Ex TPM Host #k2 .
EMAIDkey_Imported2(TPM, Host, sk_emaid) @k2)
|
// or there has been a key reveal of the entities involved in the Commit
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
|
(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
)
)
"
lemma test_new_auth_non_injective_agreement_CP_data [heuristic=o]:
"
All CP g dataTBS TPM Host #i #i2 .
(
(
CP_DataRec3(CP, pk(g), dataTBS) @ i
&
DeriveSessionKey(TPM, Host, g) @ i2
)
==>
(
// Implies there exists a running issuer on the same term
(
Ex #j . RunningEV_Data3( TPM, Host, CP, dataTBS ) @ j
&
(#j<#i)
)
|
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
|
(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
)
)
"
lemma test_new_auth_injective_agreement_CP_data [heuristic=o]:
"
All CP g dataTBS TPM Host #i #i2 .
(
(
CP_DataRec3(CP, pk(g), dataTBS) @ i
&
DeriveSessionKey(TPM, Host, g) @ i2
)
==>
(
// Implies there exists a running issuer on the same term
(
Ex #j . RunningEV_Data3( TPM, Host, CP, dataTBS ) @ j
&
(#j<#i)
&
// And each commited JOIN session corresponds to a unique issuer run
( not(
Ex CP2 g2 #i3 . ( CP_DataRec3( CP2, pk(g2), dataTBS) @ i3 & not(#i3=#i) )
)
)
)
|
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
|
(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
)
)
"
lemma test_auth_injective_agreement_CP_test2 [heuristic=o]:
"
All CP Iss tM_auth g TPM Host #i #i2 .
(
(
CommitCP3( CP, Iss, tM_auth, pk(g)) @ i
&
DeriveSessionKey(TPM, Host, g) @ i2
)
==>
(
// Implies there exists a running issuer on the same term
(
Ex pke #j . EMSP_Offline_Calc2(Iss, CP, pke, tM_auth) @ j
&
(#j<#i)
&
// And each commited JOIN session corresponds to a unique issuer run
( not(
Ex CP2 Iss2 g2 #i3 . ( CommitCP3( CP2, Iss2, tM_auth, pk(g2)) @ i3 & not(#i3=#i)
&
not(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i3))
)
)
)
|
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
|
(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
)
)
"
//--------------------
/*
test1 (all-traces): verified (2560 steps)
==============================================================================
real 68m15,750s
user 164m30,666s
sys 114m23,677s
test2 (all-traces): verified (1285 steps)
==============================================================================
real 25m38,519s
user 67m8,266s
sys 42m21,408s
test (all-traces): verified (115 steps)
==============================================================================
real 3m18,929s
user 14m9,277s
sys 3m55,545s
*/
lemma test_test1[reuse, heuristic=o]:
"
All CP g sk_emaid #i .
// For all commited JOIN sessions running between a platform and issuer on the term(s) n
(
CP_DataRec2(CP, pk(g), sk_emaid) @ i
==> // Implies that an issuer has previously been involved in a protocol run
( (Ex TPM Host #k .
DeriveSessionKey(TPM, Host, g) @ k)
|
// or there has been a key reveal of the entities involved in the Commit
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr)
)
)
"
lemma test_test2[reuse, hide_lemma=test1, heuristic=o]:
"
All CP g sk_emaid #i .
// For all commited JOIN sessions running between a platform and issuer on the term(s) n
(
CP_DataRec2(CP, pk(g), sk_emaid) @ i
==> // Implies that an issuer has previously been involved in a protocol run
( (Ex TPM Host #k2 .
EMAIDkey_Imported2(TPM, Host, sk_emaid) @k2)
|
// or there has been a key reveal of the entities involved in the Commit
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr)
)
)
"
lemma test_test:
"
All CP g sk_emaid #i .
// For all commited JOIN sessions running between a platform and issuer on the term(s) n
(
CP_DataRec2(CP, pk(g), sk_emaid) @ i
==> // Implies that an issuer has previously been involved in a protocol run
( (Ex TPM Host #k #k2 .
DeriveSessionKey(TPM, Host, g) @ k
&
EMAIDkey_Imported2(TPM, Host, sk_emaid) @k2)
|
// or there has been a key reveal of the entities involved in the Commit
(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr)
)
)
"
end
Security_Properties/daa_pnc_credential_installation.spthy
+ 1
− 1
View file @ 116baa7b
......@@ -37,7 +37,7 @@ time tamarin-prover daa_pnc_credential_installation.spthy\
==============================================================================
summary of summaries:
analyzed: join2_wCP2test3.spthy
analyzed: daa_pnc_credential_installation.spthy
forwarded_credential_res_source (all-traces): verified (265 steps)
secrecy_of_cps_private_key (all-traces): verified (3 steps)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment