improves READMEs

viperproject · Aug 18, 2022 · d278754 · d278754
1 parent dd4e546
commit d278754
Show file tree

Hide file tree

Showing 10 changed files with 85 additions and 10 deletions.
diff --git a/README.md b/README.md
@@ -1,4 +1,4 @@
-# Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol
+# Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol and Diffie-Hellman
 [![DH & WireGuard Protocol Model Verification](https://github.com/soundverification/wireguard/actions/workflows/model.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/model.yml?query=branch%3Amain)
 [![DH Code Verification](https://github.com/soundverification/wireguard/actions/workflows/dh-code.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/dh-code.yml?query=branch%3Amain)
 [![WireGuard Code Verification](https://github.com/soundverification/wireguard/actions/workflows/wireguard-code.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/wireguard-code.yml?query=branch%3Amain)

diff --git a/dh/faulty-go-implementation/.gobra/.gitkeep b/dh/faulty-go-implementation/.gobra/.gitkeep
diff --git a/dh/faulty-go-implementation/README.md b/dh/faulty-go-implementation/README.md
@@ -1,3 +1,10 @@
+# Faulty Go Diffie-Hellman Implementation
+[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../../LICENSE)
+
+Verification of this implementation fails as expected because the implementation
+tries to send the DH private key `x` instead of `g^x` in the first message.
+
+## Building & Running the Initiator Role
 Build:
 ```
 go build
@@ -20,3 +27,15 @@ Keypair 1:
 Keypair 2:
     - sk: "k2gUarJExuxjji+KlwD8NfclZ+ZCZ8xZk3NGzN3ypwgfiia9pqMQ16rFtGI5UItmgZSsRYhWtUC0k+TkmCgRXw=="
     - pk: "H4omvaajENeqxbRiOVCLZoGUrEWIVrVAtJPk5JgoEV8="
+
+## Verifying the Initiator Role
+Detailed explanations and Gobra's JAR file are given in WireGuard's implementation folder.
+```
+java -Xss128m -jar ../../wireguard/implementation/gobra.jar -I verification -I ./ --module dh-gobra --directory initiator
+```
+Note that verification of this implementation is expected to fail with the following error message:
+```
+ERROR viper.gobra.Gobra - Gobra has found 1 error(s) in package initiator - initiator
+ERROR viper.gobra.Gobra -       <initiator/initiator.go:201:14> Precondition of call i.l.Send(msg1Data , t1, ridT, xT ) might not hold. 
+Permission to e_OutFact(t, rid, m) might not suffice.
+```
diff --git a/dh/go-implementation/.gobra/.gitkeep b/dh/go-implementation/.gobra/.gitkeep
diff --git a/dh/go-implementation/README.md b/dh/go-implementation/README.md
@@ -1,3 +1,8 @@
+# Go Diffie-Hellman Implementation
+[![DH Code Verification](https://github.com/soundverification/wireguard/actions/workflows/dh-code.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/dh-code.yml?query=branch%3Amain)
+[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../../LICENSE)
+
+## Building & Running the Initiator Role
 Build:
 ```
 go build
@@ -20,3 +25,10 @@ Keypair 1:
 Keypair 2:
     - sk: "k2gUarJExuxjji+KlwD8NfclZ+ZCZ8xZk3NGzN3ypwgfiia9pqMQ16rFtGI5UItmgZSsRYhWtUC0k+TkmCgRXw=="
     - pk: "H4omvaajENeqxbRiOVCLZoGUrEWIVrVAtJPk5JgoEV8="
+
+## Verifying the Initiator Role
+Gobra can be used as follows to successfully verify this implementation.
+Detailed explanations and Gobra's JAR file are given in WireGuard's implementation folder.
+```
+java -Xss128m -jar ../../wireguard/implementation/gobra.jar -I verification -I ./ --module dh-gobra --directory initiator
+```
diff --git a/dh/java-implementation/README.md b/dh/java-implementation/README.md
@@ -1,3 +1,8 @@
+# Java Diffie-Hellman Implementation
+[![DH Code Verification](https://github.com/soundverification/wireguard/actions/workflows/dh-code.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/dh-code.yml?query=branch%3Amain)
+[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../../LICENSE)
+
+## Building & Running the Responder Role
 Build:
 ```
 gradle build
@@ -20,3 +25,9 @@ Keypair 1:
 Keypair 2:
     - sk: "k2gUarJExuxjji+KlwD8NfclZ+ZCZ8xZk3NGzN3ypwgfiia9pqMQ16rFtGI5UItmgZSsRYhWtUC0k+TkmCgRXw=="
     - pk: "H4omvaajENeqxbRiOVCLZoGUrEWIVrVAtJPk5JgoEV8="
+
+## Verifying the Responder Role
+The responder role can successfully be verified using VeriFast release 18.02 using the following command:
+```
+verifast -allow_assume -c src/main/java/dhgobra/responder/Responder.jarsrc
+```
diff --git a/dh/model/README.md b/dh/model/README.md
@@ -0,0 +1,33 @@
+# Tamarin model for Diffie-Hellman
+[![DH & WireGuard Protocol Model Verification](https://github.com/soundverification/wireguard/actions/workflows/model.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/model.yml?query=branch%3Amain)
+[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../../LICENSE)
+
+
+## Files
+
+- The `dh.spthy` file contains the Tamarin model, including the security properties and the auxiliary lemmas.
+
+
+## Prerequisite
+
+To verify our model of DH, you need **Tamarin**
+which can be obtained from [its website](https://tamarin-prover.github.io).
+Version 1.6.0 is known to work.
+
+**Python2** is also required to run the oracle.
+
+
+
+## Instructions
+
+To verify the model with Tamarin, use the following command:
+
+`tamarin-prover --prove dh.spthy`
+
+
+## Verification with Docker
+The model together with Tamarin and its dependencies are provided as a Docker image.
+The image can be pulled and the Tamarin model can be verified as follows (assuming that Docker has been installed):
+```
+docker run -it ghcr.io/soundverification/tamarin:latest tamarin-prover --prove dh.spthy
+```
diff --git a/wireguard/implementation/.gobra/.gitkeep b/wireguard/implementation/.gobra/.gitkeep
diff --git a/wireguard/implementation/README.md b/wireguard/implementation/README.md
@@ -1,6 +1,6 @@
 # Verified Wireguard Implementation
-[![Code Verification](https://github.com/soundverification/wireguard/actions/workflows/code.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/code.yml?query=branch%3Amain)
-[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../LICENSE)
+[![WireGuard Code Verification](https://github.com/soundverification/wireguard/actions/workflows/wireguard-code.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/wireguard-code.yml?query=branch%3Amain)
+[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../../LICENSE)
 
 ## Verifying & Running Initiator & Responder in Docker
 The sources of this verified implementation together with the code verifier Gobra and its dependencies are provided as a Docker image.
@@ -31,19 +31,19 @@ The version of Z3 can be checked by running `z3 -version`.
 Change into the directory `case_studies/wireguard/src`. All subsequent commands are assumed to be executed in this directory.
 To verify the initiator's implementation, run:
 ```
-java -Xss128m -jar <PATH TO GOBRA JAR> -I initiator -I verification -I ./ --module wireguard-gobra/wireguard -i initiator
+java -Xss128m -jar <PATH TO GOBRA JAR> -I verification -I ./ --module wireguard-gobra/wireguard --directory initiator
 ```
 
 Similarly, to verify the responder's implementation, run:
 ```
-java -Xss128m -jar <PATH TO GOBRA JAR> -I responder -I verification -I ./ --module wireguard-gobra/wireguard -i responder
+java -Xss128m -jar <PATH TO GOBRA JAR> -I verification -I ./ --module wireguard-gobra/wireguard --directory responder
 ```
 
 Description of the flags:
 - `-Xss128m` increases the stack size used to run the verifier. The default argument does not suffice and will cause a runtime exception.
-- `-I initiator -I verification -I ./` instructs Gobra to consider the current directory and the `initiator` and `verification` subfolders when performing lookups of imported packages. Note that `initiator` takes precende over `verification` and `verification over the current directory meaning that packages found in these subfolders will be selected over those found in the current directory.
+- `-I verification -I ./` instructs Gobra to consider the current directory and the `verification` subfolders when performing lookups of imported packages. Note that `verification` takes precende over the current directory meaning that packages found in these subfolders will be selected over those found in the current directory.
 - `--module wireguard-gobra/wireguard` informs Gobra that we are currently in this module. This impacts the package resolution as it basically means that Gobra will ignore this prefix. For example, the import statement `import lib "wireguard-gobra/wireguard/library"` results in Gobra looking for the folder `library` in the specified include directories (`-I` option).
-- `-i initiator` specifies the package that is verified
+- `--directory initiator` specifies the package that is verified
 
 
 ## Building & Running this WireGuard Implementation Non-Virtualized

diff --git a/wireguard/model/README.md b/wireguard/model/README.md
@@ -1,6 +1,6 @@
 # Tamarin model for WireGuard key exchange
-[![Protocol Model Verification](https://github.com/soundverification/wireguard/actions/workflows/model.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/model.yml?query=branch%3Amain)
-[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../LICENSE)
+[![DH & WireGuard Protocol Model Verification](https://github.com/soundverification/wireguard/actions/workflows/model.yml/badge.svg?branch=main)](https://github.com/soundverification/wireguard/actions/workflows/model.yml?query=branch%3Amain)
+[![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](../../LICENSE)
 
 
 ## Files
@@ -31,5 +31,5 @@ To verify the model with Tamarin, use the following command:
 The model together with Tamarin and its dependencies are provided as a Docker image.
 The image can be pulled and the Tamarin model can be verified as follows (assuming that Docker has been installed):
 ```
-docker run -it ghcr.io/soundverification/tamarin:latest ./tamarin-prover --heuristic=O --oraclename="wireguard.oracle" --prove wireguard.spthy
+docker run -it ghcr.io/soundverification/tamarin:latest tamarin-prover --heuristic=O --oraclename="wireguard.oracle" --prove wireguard.spthy
 ```