Skip to content
Snippets Groups Projects
README.md 3.86 KiB
Newer Older
  • Learn to ignore specific revisions
  • Timm Lauser's avatar
    Timm Lauser committed
    # DAA-PnC-Tamarin
    
    Tamarin models for the paper "Integrating Privacy into the Electric Vehicle Charging Architecture" which is currently under review.
    
    In the paper, we propose a privacy-preserving extension to the existing Plug and Charge (PnC) architecture. Here, we provide the Tamarin models we use for formal verification of the security and privacy properties of our proposed extension.
    
    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
    
    
    Their Tamarin models can be found at https://github.com/tamarin-prover/tamarin-prover/tree/dddaccbe981343dde1a321ce0c908585d4525918/examples/asiaccs20-eccDAA.
    
    Timm Lauser's avatar
    Timm Lauser committed
    
    
    
    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.
    
    Timm Lauser's avatar
    Timm Lauser committed
    
    
    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.
    
    Timm Lauser's avatar
    Timm Lauser committed
    
    
    
    In the following, we list which property of our extension is addressed by which Tamarin model file.
    
    Timm Lauser's avatar
    Timm Lauser committed
    
    **Security_Properties**
    
    | 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 |
    
    Timm Lauser's avatar
    Timm Lauser committed
    
    **Privacy_Properties**
    
    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 |
    | _PR<sub>5</sub>_ - Unlinkability of EV Users and Locations | daa_pnc_anonymity_ev_users_locations.spthy <br> daa_pnc_unlinkability_ev_users_locations.spthy           | oracle_ev_users_locations.py |