The Tamarin prover is a verification tool for security protocols. (Please also refer to the Tamarin documentation ).
This project contains a symbolic model of the Minimal IKEv2 protocol which can be used with Tamarin to verify the key exchanges' claimed security properties.
There are two models: IKEv2 in a standard setting and "PQ-IKEv2" in a quantum setting, that means: Minimal IKEv2 with the IKE_INTERMEDIATE-extension and an attacker who can break the Diffie-Hellman keys derived in the standard handshake.
First you need to obtain the tamarin-prover binary from the package manager of your choice:
- Arch Linux:
pacman -S tamarin-prover - Nixpkgs:
nix-env -i tamarin-prover
More infos here
Then run the model via the command line tool:
tamarin-prover interactive ikev2.spthy
or:
tamarin-prover interactive pq-ikev2.spthy
And point your browser to:
http://localhost:3001
We used Ubuntu 20.04, as 18.04 did not support the glibc 2.29, which is required by Tamarin. Tamarin das not provide a package for Ubuntu/Debian by using apt/dpkg, hence we installed tamrin with the homebrew package manager
If the package manager includes homebrew:
sudo apt install linuxbrew-wrapper
Otherwise manual installation is required (as it is currently the case in Ubuntu 20.04 LTS):
sudo apt install build-essential curl file git
sh -c "$(curl -fsSL https://raw.githubusercontent.com/Linuxbrew/install/master/install.sh)"
sudo brew install tamarin-prover/tap/tamarin-prover
test -d ~/.linuxbrew && eval $(~/.linuxbrew/bin/brew shellenv)
test -d /home/linuxbrew/.linuxbrew && eval $(/home/linuxbrew/.linuxbrew/bin/brew shellenv)
test -r ~/.bash_profile && echo eval" ($(brew --prefix)/bin/brew shellenv)" >>~/.bash_profile
echo "eval $($(brew --prefix)/bin/brew shellenv)" >>~/.profile
echo 'eval "$(/home/ubuntu/.linuxbrew/bin/brew shellenv)"' >> /home/ubuntu/.profile
eval "$(/home/ubuntu/.linuxbrew/bin/brew shellenv)"
brew install gcc
brew install font-util
brew install tamarin-prover/tap/tamarin-prover
brew install tamarin-prover/tap/maude graphviz haskell-stack
export PATH=$PATH:$HOME/.linuxbrew/var/homebrew/linked/tamarin-prover/bin
tamarin-prover
The code ran in an virtual environment with 40 vCPU cores, 180 GB RAM and with standard Ubuntu 20.04. It took about 30 mins to complete.
Smaller setups may work; the bottleneck is memory, not CPU power.
We model both standard IKEv2 and "PQ-IKEv2". PQ-IKEv2 here means IKEv2 with IKE-Intermediate in a model where the attacker can break classical DH-keys.
The files that relate to the second kind have the prefix "pq-".
The "full model" versions contain models that consider the aliveness-, weak-agreement- and agreement-property not only from the initiator's point of view (as the models in ikev2.spthy and in pq-ikev2.spthy do) but also from the responder's perspective.
We provide the "running-neq-completed" versions to account for the ambiguity in the definitions of aliveness, weak agreement and agreement, which require one of the parties to have "completed" the protocol and the other to have "run" the protocol. In the other versions, "run" is interpreted as "completed"; in the "running-neq-completed" versions, the properties are defined in such a way that aliveness and weak agreement only require the second party to reach any arbitrary step of the protocol, not to complete it.
To check the model, choose the correct file in the Tamarin GUI. In the tab that opens, the model code is on the left.
Click "sorry" at the foot of whichever lemma you want to prove. This opens the "Visualization display". All lemmas can be checked by clicking "a. autoprove".
Depending on whether a lemma makes an "exists trace"-statement or an "all traces"-statements, different results are considered a success. To prove an "exists trace"-statement, Tamarin will output a trace (as a picture) which shows a fulfilling trace for the lemma. Proving an "all traces"-statement means that Tamarin finds no trace that contradicts the statement.
Lemmas that can be proven yield a green trace on the left and, in the case of "exists-trace"-lemmas, a picture of a fulfilling trace. Lemmas that can be disproven yield a red trace on the left and, in the case of "all-traces"-lemmas, a picture of a contradicting trace.