updates implementations

.github/workflows/dh-code.yml

@@ -0,0 +1,36 @@
+name: DH Code Verification
+
+on:
+  push:
+
+jobs:
+  build-verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    container:
+      image: ghcr.io/viperproject/gobra@sha256:1513175b6b66dcdb73042fbcb0bc3fa511c716cbf65ec318e25171283975b955
+    env:
+      VERIFAST_VERSION: 18.02
+    steps:
+      - name: Install prerequisites
+        run: apt-get update && apt-get install -y git curl tar libgomp1
+
+      - name: Checkout repo
+        uses: actions/checkout@v2
+
+      - name: Verify DH initiator in Go using Gobra
+        run: |
+          mkdir -p .gobra
+          java -Xss128m -jar /gobra/gobra.jar \
+            --module "dh-gobra" \
+            --include verification --include . \
+            --directory initiator
+        working-directory: dh/go-implementation
+
+      - name: Verify DH responder in Java using VeriFast
+        run: |
+          curl -q -s -S -L --create-dirs -o VeriFast.zip https://github.com/verifast/verifast/releases/download/${{ env.VERIFAST_VERSION }}/verifast-${{ env.VERIFAST_VERSION }}-linux.tar.gz
+          tar xzf VeriFast.zip
+          # this creates a folder called `verifast-${{ env.VERIFAST_VERSION }}`
+          VERIFAST_PATH="$PWD/verifast-${{ env.VERIFAST_VERSION }}/bin/verifast"
+          $VERIFAST_PATH -allow_assume -c dh/java-implementation/src/main/java/dhgobra/responder/Responder.jarsrc

.github/workflows/model.yml

@@ -1,14 +1,18 @@
-name: Protocol Model Verification
+name: DH & WireGuard Protocol Model Verification
 
 on:
   push:
 
 jobs:
   build-verify:
     runs-on: ubuntu-latest
-    env:
-      IMAGE_ID: ghcr.io/soundverification/wireguard-tamarin
+    timeout-minutes: 20
     steps:
+      - name: Create Image ID
+        run: |
+          REPO_OWNER=$(echo "${{ github.repository_owner }}" | tr '[:upper:]' '[:lower:]')
+          echo "IMAGE_ID=ghcr.io/$REPO_OWNER/tamarin" >> $GITHUB_ENV
+
       - name: Checkout repo
         uses: actions/checkout@v2
 
@@ -24,17 +28,20 @@ jobs:
       - name: Build image
         uses: docker/build-push-action@v2
         with:
-          context: model
+          context: .
           load: true
-          file: model/docker/Dockerfile
+          file: tamarin-docker/Dockerfile
           tags: ${{ env.IMAGE_TAG }}
           labels: "runnumber=${{ github.run_id }}"
           push: false
           cache-from: type=gha, scope=${{ github.workflow }}
           cache-to: type=gha, scope=${{ github.workflow }}
 
-      - name: Verify Tamarin model
-        run: docker run ${{ env.IMAGE_TAG }} ./tamarin-prover --heuristic=O --oraclename="wireguard.oracle" --prove wireguard.spthy
+      - name: Verify DH Tamarin model
+        run: docker run ${{ env.IMAGE_TAG }} ./verify-dh.sh
+
+      - name: Verify WireGuard Tamarin model
+        run: docker run ${{ env.IMAGE_TAG }} ./verify-wireguard.sh
 
       - name: Login to Github Packages
         uses: docker/login-action@v1
@@ -46,8 +53,8 @@ jobs:
       - name: Push image
         uses: docker/build-push-action@v2
         with:
-          context: model
-          file: model/docker/Dockerfile
+          context: .
+          file: tamarin-docker/Dockerfile
           tags: ${{ env.IMAGE_TAG }}
           labels: "runnumber=${{ github.run_id }}"
           push: true

.github/workflows/code.yml → .github/workflows/wireguard-code.yml

@@ -1,14 +1,18 @@
-name: Code Verification
+name: WireGuard Code Verification
 
 on:
   push:
 
 jobs:
   build-verify:
     runs-on: ubuntu-latest
-    env:
-      IMAGE_ID: ghcr.io/soundverification/wireguard-gobra
+    timeout-minutes: 15
     steps:
+      - name: Create Image ID
+        run: |
+          REPO_OWNER=$(echo "${{ github.repository_owner }}" | tr '[:upper:]' '[:lower:]')
+          echo "IMAGE_ID=ghcr.io/$REPO_OWNER/wireguard-gobra" >> $GITHUB_ENV
+
       - name: Checkout repo
         uses: actions/checkout@v2
 
@@ -24,9 +28,9 @@ jobs:
       - name: Build image
         uses: docker/build-push-action@v2
         with:
-          context: implementation
+          context: wireguard/implementation
           load: true
-          file: implementation/docker/Dockerfile
+          file: wireguard/implementation/docker/Dockerfile
           tags: ${{ env.IMAGE_TAG }}
           labels: "runnumber=${{ github.run_id }}"
           push: false
@@ -49,8 +53,8 @@ jobs:
       - name: Push image
         uses: docker/build-push-action@v2
         with:
-          context: implementation
-          file: implementation/docker/Dockerfile
+          context: wireguard/implementation
+          file: wireguard/implementation/docker/Dockerfile
           tags: ${{ env.IMAGE_TAG }}
           labels: "runnumber=${{ github.run_id }}"
           push: true

README.md

@@ -1,9 +1,11 @@
 # Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol
-[![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)
-[![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)
+[![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)
 [![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](./LICENSE)
 
 This repository provides the following content:
 - [Full paper](./full_paper.pdf) containing the proofs
-- Subdirectory `model` contains the Tamarin model together with instructions how to verify it
-- Subdirectory `implementation` contains the verified Go implementation together with instructions how to verify and execute it.
+- 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.

dh/faulty-go-implementation/.vscode/settings.json

@@ -0,0 +1,9 @@
+{
+    "gobraSettings.moduleName": "dh-gobra",
+    "gobraSettings.includeDirs": [
+        "verification",
+        "."
+    ],
+    "gobraSettings.autoVerify": false,
+    "gobraSettings.buildVersion": "Stable"
+}

dh/faulty-go-implementation/README.md

@@ -0,0 +1,22 @@
+Build:
+```
+go build
+```
+
+Run:
+```
+./dh-gobra --isInitiator --endpoint localhost:12345 --privateKey "ACvCw0fb1mqTQikmXOas+YEbJnC9O/N4H12k4w/ADVRVg6YAptHsQO57FNzeeS2BtGwHas51wRruj62+y4WpjQ==" --peerPublicKey "H4omvaajENeqxbRiOVCLZoGUrEWIVrVAtJPk5JgoEV8="
+```
+
+The command above configures the Initiator to use Keypair 1 for its own secret key and tries to communicate with the Responder by using Keypair 2's public key.
+
+Note that the Responder has to be started first.
+
+
+Keypair 1:
+    - sk: "ACvCw0fb1mqTQikmXOas+YEbJnC9O/N4H12k4w/ADVRVg6YAptHsQO57FNzeeS2BtGwHas51wRruj62+y4WpjQ=="
+    - pk: "VYOmAKbR7EDuexTc3nktgbRsB2rOdcEa7o+tvsuFqY0="
+
+Keypair 2:
+    - sk: "k2gUarJExuxjji+KlwD8NfclZ+ZCZ8xZk3NGzN3ypwgfiia9pqMQ16rFtGI5UItmgZSsRYhWtUC0k+TkmCgRXw=="
+    - pk: "H4omvaajENeqxbRiOVCLZoGUrEWIVrVAtJPk5JgoEV8="

dh/faulty-go-implementation/go.mod

@@ -0,0 +1,5 @@
+module dh-gobra
+
+go 1.16
+
+require golang.org/x/crypto v0.0.0-20220722155217-630584e8d5aa // indirect

dh/faulty-go-implementation/go.sum

@@ -0,0 +1,9 @@
+golang.org/x/crypto v0.0.0-20220722155217-630584e8d5aa h1:zuSxTR4o9y82ebqCUJYNGJbGPo6sKVl54f/TVDObg1c=
+golang.org/x/crypto v0.0.0-20220722155217-630584e8d5aa/go.mod h1:IxCIyHEi3zRg3s0A5j5BB6A9Jmi73HwBIUl50j+osU4=
+golang.org/x/net v0.0.0-20211112202133-69e39bad7dc2/go.mod h1:9nx3DQGgdP8bBQD5qxJ1jj9UTztislL4KSBs9R2vV5Y=
+golang.org/x/sys v0.0.0-20201119102817-f84b799fce68/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
+golang.org/x/sys v0.0.0-20210423082822-04245dca01da/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
+golang.org/x/sys v0.0.0-20210615035016-665e8c7367d1/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
+golang.org/x/term v0.0.0-20201126162022-7de9c90e9dd1/go.mod h1:bj7SfCRtBDWHUb9snDiAeCFNEtKQo2Wmx5Cou7ajbmo=
+golang.org/x/text v0.3.6/go.mod h1:5Zoc/QRtKVWzQhOtBMvqHzDpF6irO9z98xDceosuGiQ=
+golang.org/x/tools v0.0.0-20180917221912-90fa682c2a6e/go.mod h1:n7NCudcB/nEzxVGmLbDWY5pfWTLqBcC2KZ6jyYvM4mQ=