From 116baa7b1c5f419d090b181f92257a184d95ba35 Mon Sep 17 00:00:00 2001
From: Dustin Kern <dustin.kern@h-da.de>
Date: Sat, 19 Feb 2022 15:48:14 +0100
Subject: [PATCH] details for test machine
---
README.md | 2 +-
Security_Properties/README.md | 6 +-
.../daa_pnc_credential_installation.spthy | 2 +-
...daa_pnc_charge_authorisation_offline.spthy | 349 +-----------------
.../daa_pnc_credential_installation.spthy | 2 +-
5 files changed, 11 insertions(+), 350 deletions(-)
diff --git a/README.md b/README.md
index 89cfbb0..cfdef8b 100644
--- a/README.md
+++ b/README.md
@@ -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.
diff --git a/Security_Properties/README.md b/Security_Properties/README.md
index 58a5d43..7083d47 100644
--- a/Security_Properties/README.md
+++ b/Security_Properties/README.md
@@ -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
diff --git a/Security_Properties/Tamarin_1_6_1/daa_pnc_credential_installation.spthy b/Security_Properties/Tamarin_1_6_1/daa_pnc_credential_installation.spthy
index cbd3793..538a24b 100644
--- a/Security_Properties/Tamarin_1_6_1/daa_pnc_credential_installation.spthy
+++ b/Security_Properties/Tamarin_1_6_1/daa_pnc_credential_installation.spthy
@@ -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)
diff --git a/Security_Properties/daa_pnc_charge_authorisation_offline.spthy b/Security_Properties/daa_pnc_charge_authorisation_offline.spthy
index 55b2048..3a12b8e 100644
--- a/Security_Properties/daa_pnc_charge_authorisation_offline.spthy
+++ b/Security_Properties/daa_pnc_charge_authorisation_offline.spthy
@@ -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
diff --git a/Security_Properties/daa_pnc_credential_installation.spthy b/Security_Properties/daa_pnc_credential_installation.spthy
index 592245c..a1bcb14 100644
--- a/Security_Properties/daa_pnc_credential_installation.spthy
+++ b/Security_Properties/daa_pnc_credential_installation.spthy
@@ -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)
--
GitLab