Artifacts of research paper "A Unified Symbolic Analysis of WireGuard"¹, co-authored by Pascal Lafourcade, Dhekra Mahmoud and Sylvain Ruhault, for NDSS 2024 Conference

This project gathers symbolic analyses of WireGuard² protocol, with the help of Sapic+, Tamarin and ProVerif proof assistants. The following properties are verified: agreement, secrecy and anonymity.

Agreement and secrecy are modeled as trace properties and are verified with Sapic+ in both ProVerif and Tamarin.

Anonymity is modeled as equivalence property and is not reached for WireGuard. We proposed two fixes that are verified with Sapic+ in ProVerif.

Licence

GNU General Public License v3³.

Prerequisites

As Sapic+⁴ has been integrated in Tamarin release version 1.8.0, we use this version of Tamarin.

This project uses the following:

• Tamarin⁵ release version 1.8.0
• ProVerif version 2.04⁶.
• Python version 3.11.4 ⁷.
• Package sympy⁸.
• GNU parallel⁹.

All our files are publicly available and can be accessed online either through Gitlab repository or Docker image. Docker image contains all softwre pre-installed and requires a running Docker Engine¹⁰. Gitlab repository contains an installation script that has been successfully tested on a fresh Ubuntu Server 22.04.3 LTS, installed from ISO image¹¹.

Access through Gitlab and software installation

git clone https://gitlab.limos.fr/palafour/ndss2024-AE364
cd ndss2024-AE364
sh run_install-dep-tam-pv.sh

Access through Docker (no installation required)

docker pull wganalysis/artifacts
docker run -it wganalysis/artifacts bash

Basic tests

In both cases (installation script or Docker image), perform basic tests with the following commands:

• Test for Tamarin

tamarin-prover test

In the end you should see the following:

*** TEST SUMMARY ***
All tests successful.
The tamarin-prover should work as intended.

           :-) happy proving (-:

• Test for ProVerif

eval $(opam env --safe); proverif -help

In the beginning you should see the following:

Proverif 2.04. Cryptographic protocol verifier, by Bruno Blanchet, Vincent Cheval, and Marc Sylvestre

Functional Environments

All our tests have been performed on Linux Ubuntu Server 22.04.3 LTS, hence all script are adapted to this environment.

We obtained all results on a server equipped with 256 cores of CPU 1,5 Ghz and with 512 Go of RAM.

This induces a specific parameter in our scripts:

JOBS=250

This parameter allows to run computations in parallel with GNU parallel. This number is adapted to our architecture, as we use a server equipped with 256 cores which allows such parallel computation. This number shall be adapted on another server with a different architecture.

Security Properties

We assess the following security properties:

• Agreement properties: agreement of RecHello message (from Responder to Initiator), agreement of first TransData message (from Initiator to Responder), agreement of next TransData messages (from Initiator to Responder and from Responder to Initiator), for WireGuard with or without cookies and for two fixed versions of WireGuard.
• Secrecy properties: secrecy and PFS of session key before derivation (named k_6 in protocol description), from Initiator’s and Responder’s view, secrecy and PFS of derivated keys (named C^i and C^r ), from Initiator’s and Responder’s view, for WireGuard with or without cookies and for two fixed versions of WireGuard.
• Anonymity, for WireGuard with or without cookies and for two fixed versions of WireGuard.

This implies 17x4 = 68 security properties.

Steps

As explained in our research paper, our steps are the following, for each security property:

• We model WireGuard as processes in Sapic+.
• We use Tamarin and GNU parallel to generate a set of ProVerif files where each file contains a unique query, corresponding to a case of key compromise combination in a given model.
• We evaluate all these queries with ProVerif and GNU parallel.
• We keep all queries that are satisfied with ProVerif (where assessment is "true").
• From the results, we compute dedicated formulas for each property with to_cnf and to_dnf from sympy package and GNU parallel.
• We deduce from this dedicated formulas dedicated lemmas that we evaluate with Tamarin and GNU parallel.

Files and directories

We model WireGuard in the following cases, each one corresponding to a dedicated directory:

• WireGuard without cookie in directory process_complete_without_cookie
• WireGuard with cookie in directory process_complete_with_cookie
• WireGuard with our fixes, without cookie in directories process_complete_with_fix_guv and process_complete_with_fix_psk : we assess two possible fixes, one based on ecdh product (guv) and one based on pre-shared key (psk).

We also provide a directory process_complete_minimal_tests. It allows to obtain results for Perfect Forward Secrecy of session key before derivation from Initiator's view for WireGuard without cookie. This works on a A standard laptop with 8 cores of CPU 1.8 GHz and 16 Go of RAM.

Each directory contains the same set of files.

We use a set of reference spthy files, which model WireGuard with processes in Applied Pi Calculus. These are:

• wireguard_peer_initiator_reference.spthy: this models Initiator
• wireguard_peer_responder_reference.spthy: this models Responder
• wireguard_proces_reference.spthy: this models the protocol

We use a set of .sh scripts and associated command files, described below, available at the root of each directory. These are:

• run_clean.sh: this cleans up repository (Warning: this delete all generated files and repositories !)
• run_generate-pv.sh: this generates repositories for all properties and all ProVerif files. This uses GNU parallel and command file named wireguard_command_generate_pv.
• run_evaluate-pv.sh: this launches the evaluation of all ProVerif files, for all properties.
• run_generate-cnf-dnf.sh: this computes CNF and DNF for all properties. This uses GNU parallel and command file named wireguard_command_generate_cnf_dnf.
• run_evaluate-tam.sh: this launches the evaluation of all Tamarin files, for all properties.

Directory process_empty contains a set of 4 files, that model builtins, functions, equations, process declarations and delimiters. Analog directory process_empty_with_cookie contains the same set of files, adapted for model with cookie.

Directory queries contains necessary scripts that generates queries adapted to each model and each case of key compromise combinaison.

Dedicated repositories are created for each security property: agreement_rechello, agreement_confirm, agreement_transport_itor, agreement_transport_rtoi, secrecy_isk6, secrecy_rsk6, secrecy_isk_itor, secrecy_isk_rtoi, secrecy_rsk_itor, secrecy_rsk_rtoi. These creations are described below.

A dedicated results directory is created, that contains compact formulas, based on Disjunctive Normal Forms computations, for each security property. This creation is decribed below.

ProVerif files generation

Each security property, except InitHello Agreement, requires the generation of 4860 ProVerif files that will be assessed in parallel. For InitHello Agreement, 540 files are necessary, are less keys are involved.

To generate all files for all properties, the following command shall be used:

sh run_generate-pv.sh

Using GNU parallel⁷, this script generates all queries in directory queries and for each security property, a dedicated directory which contains a dedicated macro .spthy file, all ProVerif files (540 for InitHello Agreement and 4860 for other properties) and a dedicated command file used to evaluate all queries. This dedicated file will be used as input for GNU parallel. On our server, generation of ProVerif files takes at most 12m.

For generation, the following parameters are used in Tamarin

+RTS -N1 -RTS

These parameters allow to configure the number of threads used by Tamarin. Here this number is equal to 1 as Tamarin is used to translate .spthy files to .pv files.

ProVerif queries evaluation

ProVerif queries are evaluated for each security property. For this the following command shall be used:

sh run_evaluate-pv.sh

Using GNU parallel⁷, this script generates for each security property, 4860 .log files (640 .log files for InitHello Agreement), where each file contains the evaluation of the query contained in each corresponding source .pv file.

Performances for ProVerif files evaluations are detailed below: security properties are evaluated in less than 15m, except for Agreement of RecHello message which requires 35m. Note that parallel computation is done at property level, hence all properties are evaluated sequentially. Additionning all, all properties are evaluated in 2h30m on our server.

CNF and DNF computation

For each security property, compact formulas are computed from all queries that are assessed as true with ProVerif. These formulas are computed with to_cnf and to_dnf imports from sympy package⁶. For this the following commands shall be used:

sh run_generate-cnf-dnf.sh

Using GNU parallel, this script generates, for each property, a dedicated .cnfdnf file which contains the following lines:

CNF for [property] = ...
DNF for [property] = ...
DNF* for [property] = ...

All .cnfdnf files are located in results directory.

Tamarin lemma evaluation

For each security property, a dedicated Tamarin lemma is deduced from each DNF* from previous computation and a dedicated Tamarin .spthy file is created. Note that this deduction is not automated and that spthy file creation is also not automated.

Then all Tamarin files are evaluated with the following command:

run_evaluate-tam.sh

For each property, this generates a dedicated .tamarin file. This file contains the log file of the following command, where [tamarin source file] is the Tamarin file that contains one lemma deduced from each previously generated DNF* and [tamarin log file] is the produced log file.

tamarin-prover  --derivcheck-timeout=0 [tamarin source file] --prove +RTS -N10 -RTS > [tamarin log file]

These scripts contain the following parameters:

+RTS -N10 -RTS

These parameters allow to configure the number of threads used by Tamarin (here 10). These numbers are adapted to our architecture, as we use a server equipped with 256 cores. These numbers shall be adapted on another server with a different architecture.

Evaluation of all Tamarin files for all properties takes at most 4h45m on our server.

Note that some evaluations require the use of an oracle, implemented in file myoracle. All .tamarin files are located in results directory.

Performances

Table below provide performances for agreement and secrecy properties evaluation, on our server.

(p): computed in parallel, hence the total duration is the longest one

References