Newer
Older
# 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.
Timm Lauser
committed
In the following, we first provide usage instructions for our model, then we list which model files are relevant for which property specified in our paper. Finally, we reference the original Tamarin models for DAA, which have been developed as part of another research, and describe the necessary changes for our models.
Timm Lauser
committed
## 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).
The README files in the subfolders [Security_Properties](Security_Properties/) and [Privacy_Properties](Privacy_Properties/) provide a general explanation of how to run the Tamarin proof(s).
Additionally, at the beginning of each model file, the specific 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.
In short, the verification times for security-related models range from 14 to 20 minutes and for privacy-related models from 9 to 333 minutes.
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 following subsections provide examples on how to setup Tamarin 1.6.0 using either Homebrew or Docker.
Please consult the [Tamarin-Prover Manual](https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf) for more details on installation and usage instructions.
### Tamarin Setup using Homebrew
The Tamarin documentation recommends to use Homebrew for the installation (cf. [Tamarin Installation](https://tamarin-prover.github.io/manual/book/002_installation.html)).
Homebrew can, for example, be used to install Tamarin 1.6.0 as follows (tested on Ubuntu 20.04.1 LTS):
```
# Install Homebrew:
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
# Add Homebrew to your PATH:
echo 'eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"' >> $HOME/.profile
eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"
# Install Tamarin:
wget https://github.com/tamarin-prover/tamarin-prover/releases/download/1.6.0/tamarin-prover-1.6.0.x86_64_linux.bottle.tar.gz
export HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK=1
brew install tamarin-prover/tap/maude graphviz haskell-stack
brew install tamarin-prover-1.6.0.x86_64_linux.bottle.tar.gz
sudo cp -s /home/linuxbrew/.linuxbrew/bin/maude /usr/bin/maude
sudo cp -s /home/linuxbrew/.linuxbrew/bin/tamarin-prover /usr/bin/tamarin-prover
# Check Version:
tamarin-prover --version
```
If `brew install` exits with the `Error: Too many open files`, simply rerunning the command usually fixes it.
In addition, Python is required for the oracles (installation, e.g., via `apt-get install python3`).
### Tamarin Setup using Docker
Alternatively, the provided Dockerfile (based on the file found [here](https://github.com/rsasse/tamarin-prover-docker/blob/0d1b7fa10943fbae731772ad15f6a919f61a7dcf/Dockerfile)) can be used to setup Tamarin 1.6.0 and run the proofs as follows (tested on Ubuntu 20.04.1 LTS; assumes that [Docker](https://docs.docker.com/) is already installed):
```
# Clone the git and build the docker image
git clone https://code.fbi.h-da.de/seacop/daa-pnc-tamarin.git
cd daa-pnc-tamarin
sudo docker build -t tamarin .
# Afterwards the proofs can be run via the docker image by replacing 'tamarin-prover' with 'docker run --rm -v $PWD:/workspace tamarin'
# in the respective commands that are described in the subfolders Security_Properties and Privacy_Properties, e.g.:
cd Security_Properties
time sudo docker run --rm -v $PWD:/workspace tamarin daa_pnc_credential_installation.spthy \
--heuristic=S --quit-on-warning --prove +RTS -N8 -RTS
```
Timm Lauser
committed
## Security and Privacy Properties
In the following, we list which property of our extension is addressed by which Tamarin model file.
| Security Property | Tamarin File(s) |
|:--------------------------------------------------|:-------------------------|
| _SR<sub>2</sub>_ - Secure Credential Installation | [daa_pnc_credential_installation.spthy](Security_Properties/daa_pnc_credential_installation.spthy) |
| _SR<sub>3</sub>_ - Secure Charge Autorization | [daa_pnc_charge_authorisation_online.spthy](Security_Properties/daa_pnc_charge_authorisation_online.spthy) <br> [daa_pnc_charge_authorisation_offline.spthy](Security_Properties/daa_pnc_charge_authorisation_offline.spthy) |
| _SR<sub>4</sub>_ - Charge Data Authenticity | [daa_pnc_charge_authorisation_online.spthy](Security_Properties/daa_pnc_charge_authorisation_online.spthy) <br> [daa_pnc_charge_authorisation_offline.spthy](Security_Properties/daa_pnc_charge_authorisation_online.spthy) |
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](Privacy_Properties/daa_pnc_anonymity_credential_installation.spthy) <br> [daa_pnc_unlinkability_credential_installation.spthy](Privacy_Properties/daa_pnc_unlinkability_credential_installation.spthy) | [ObsEquOracle_credential_installation.py](Privacy_Properties/ObsEquOracle_credential_installation.py) |
| _PR<sub>3</sub>_ - Unlinkable Charge Autorization | [daa_pnc_anonymity_charge_authorisation.spthy](Privacy_Properties/daa_pnc_anonymity_charge_authorisation.spthy) <br> [daa_pnc_unlinkability_charge_authorisation.spthy](Privacy_Properties/daa_pnc_unlinkability_charge_authorisation.spthy) | [ObsEquOracle_charge_authorisation.py](Privacy_Properties/ObsEquOracle_charge_authorisation.py) |
| _PR<sub>4</sub>_ - Unlinkable CDRs | [daa_pnc_anonymity_cdrs.spthy](Privacy_Properties/daa_pnc_anonymity_cdrs.spthy) <br> [daa_pnc_unlinkability_cdrs.spthy](Privacy_Properties/daa_pnc_unlinkability_cdrs.spthy) | [ObsEquOracle_cdrs.py](Privacy_Properties/ObsEquOracle_cdrs.py) |
| _PR<sub>5</sub>_ - Unlinkability of EV Users and Locations | [daa_pnc_anonymity_ev_users_locations.spthy](Privacy_Properties/daa_pnc_anonymity_ev_users_locations.spthy) <br> [daa_pnc_unlinkability_ev_users_locations.spthy](Privacy_Properties/daa_pnc_unlinkability_ev_users_locations.spthy) | [ObsEquOracle_ev_users_locations.py](Privacy_Properties/ObsEquOracle_ev_users_locations.py) |
Timm Lauser
committed
## Original Tamarin DAA model
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
committed
The changes/extension to their model can be summarized as follows: (i) Adaptions/additions to the model rules in order to represent the e-mobility-specific roles/processes within the context (e.g., the introduction of the CPS role between the host and issuer in the credential provisioning process or the validation of charge authorization via the EMSP in addition to the DAA-Signature verification by the CP/Verifier), (ii) changes to model rules in order to represent the changes to the base DAA Join and Certify processes; e.g., the possibility of no live interaction with the credential issuer during installation due to the use of credential pools or the binding of session keys to the ISO 15118 session), (iii) definition of new lemmas in order to verify correctness as well as the identified security/privacy requirements, and (iv) performance optimizations such that the new models terminate within a reasonable time frame via the adaption of oracles (to work with the new/changed rules) and the addition of source/reuse lemmas.
Our changes roughly amount to 54 new rules, 16 changed rules, 32 new lemmas, 18 changed lemmas, and 5 adapted oracles.