Skip to content
This repository has been archived by the owner on Dec 9, 2022. It is now read-only.

Latest commit

 

History

History
15 lines (12 loc) · 1.83 KB

README.md

File metadata and controls

15 lines (12 loc) · 1.83 KB
Raw

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

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

DH & WireGuard Protocol Model Verification DH Code Verification WireGuard Code Verification License: MPL 2.0

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.