Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol and Diffie-Hellman

⚠️ This repository has permanently moved to `viperproject/protocol-verification-refinement`

This repository provides the following content:

Subdirectory wireguard/model contains the Tamarin model together with instructions how to verify it
Subdirectory wireguard/implementation contains the verified Go implementation together with instructions how to verify and execute it.
The subdirectory dh contains the verified DH protocol model together with a verified Go and Java implementations. Additionally, dh/faulty-go-implementation contains a Go implementation that tries to send the DH private key in plaintext for which verification fails because the IO specification does not permit such a send operation.
The subdirectory specification-generator contains the sources of our tool to generate I/O specifications for Gobra & VeriFast from a Tamarin model.

Name		Name	Last commit message	Last commit date
Latest commit History 9 Commits
.github/workflows		.github/workflows
dh		dh
specification-generator		specification-generator
tamarin-docker		tamarin-docker
wireguard		wireguard
LICENSE		LICENSE
README.md		README.md