From c435f35d7e7e6ce912a77c5661e6152c910877ac Mon Sep 17 00:00:00 2001 From: Timm Lauser <timm.lauser@h-da.de> Date: Fri, 18 Feb 2022 10:50:03 +0100 Subject: [PATCH] Specified used Tamarin version in README --- README.md | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index 077e458..d4c0ae2 100644 --- a/README.md +++ b/README.md @@ -8,25 +8,27 @@ Our models are based on the models from the following paper: Stephan Wesemeyer, Christopher J.P. Newton, Helen Treharne, Liqun Chen, Ralf Sasse, and Jorden Whitefield. 2020. Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme. In Proceedings of the 15th ACM Asia Conference on Computer and Communications Security (ASIA CCS '20). Association for Computing Machinery, New York, NY, USA, 784–798. DOI:https://doi.org/10.1145/3320269.3372197 -(cf. https://github.com/tamarin-prover/tamarin-prover/tree/dddaccbe981343dde1a321ce0c908585d4525918/examples/asiaccs20-eccDAA) +Their Tamarin models can be found at https://github.com/tamarin-prover/tamarin-prover/tree/dddaccbe981343dde1a321ce0c908585d4525918/examples/asiaccs20-eccDAA. -The Tamarin prover (https://tamarin-prover.github.io/) is required to verify the model. 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. +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. +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. -In the following, we list which property of our extension is addressed by which Tamarin model. + +In the following, we list which property of our extension is addressed by which Tamarin model file. **Security_Properties** -| Security Property | Tamarin File(s) | -|:----------------------------------------|:-----------------------------------| +| Security Property | Tamarin File(s) | +|:--------------------------------------------------|:-------------------------| | _SR<sub>2</sub>_ - Secure Credential Installation | daa_pnc_credential_installation.spthy | | _SR<sub>3</sub>_ - Secure Charge Autorization | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | | _SR<sub>4</sub>_ - Charge Data Authenticity | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy | **Privacy_Properties** -The files with the keyword *anonymity* in their file name contain a model for a weaker version of the properties. -| Privacy Property | Tamarin File(s) | Oracle | -|:-------------------------------------------------|:---------------------------------------------------------------------------------------------------------|:-| +The files with the keyword *anonymity* in their filename contain a model for a weaker version of the properties. +| Privacy Property | Tamarin File(s) | Oracle | +|:-----------------------------------------------------------|:---------------------------------------------------------------------------------------------------------|:-| | _PR<sub>2</sub>_ - Unlinkable Credential Installation | daa_pnc_anonymity_credential_installation.spthy <br> daa_pnc_unlinkability_credential_installation.spthy | oracle_credential_installation.py | | _PR<sub>3</sub>_ - Unlinkable Charge Autorization | daa_pnc_anonymity_charge_authorisation.spthy <br> daa_pnc_unlinkability_charge_authorisation.spthy | oracle_charge_authorisation.py | | _PR<sub>4</sub>_ - Unlinkable CDRs | daa_pnc_anonymity_cdrs.spthy <br> daa_pnc_unlinkability_cdrs.spthy | oracle_cdrs.py | -- GitLab