README.md

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.

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.

Execution Instructions

The Tamarin prover is required to verify the model. Our files have been developed and verified with Tamarin version 1.6.0. The README files in the subfolders Security_Properties and 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 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 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). 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) 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 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

Security and Privacy Properties

In the following, we list which property of our extension is addressed by which Tamarin model file.

Security_Properties

Security Property	Tamarin File(s)
SR2 - Secure Credential Installation	daa_pnc_credential_installation.spthy
SR3 - Secure Charge Authorization	daa_pnc_charge_authorisation_online.spthy daa_pnc_charge_authorisation_offline.spthy
SR4 - Charge Data Authenticity	daa_pnc_charge_authorisation_online.spthy daa_pnc_charge_authorisation_offline.spthy

Privacy_Properties The files with the keyword anonymity in their filename contain a model for a weaker version of the properties.