This repository provides the following content:
wireguard/model contains the Tamarin model together with instructions how to verify itwireguard/implementation contains the verified Go implementation together with instructions how to verify and execute it.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.specification-generator contains the sources of our tool to generate I/O specifications for Gobra & VeriFast from a Tamarin model.