proofs: support for Tamarin 1.8.0

.github/workflows/proofs.yml

@@ -0,0 +1,35 @@
+name: proofs
+on:
+  workflow_dispatch:
+
+jobs:
+  proofs:
+    runs-on: ubuntu-22.04
+    steps:
+    -
+      uses: actions/checkout@master
+    -
+      name: Run main design (centralized-time)
+      run: |
+        cd proofs
+        make prove MODEL=centralized-time THREADS=4 OUT_FILE=output_centralized.spthy
+        docker logs -n 200 tamarin > out/log_centralized.txt
+      timeout-minutes: 10
+    -
+      name: Run alternative design (distributed-time)
+      run: |
+        cd proofs
+        make prove MODEL=distributed-time THREADS=4 OUT_FILE=output_distributed.spthy
+        docker logs -n 200 tamarin > out/log_distributed.txt
+      timeout-minutes: 10
+    -
+      name: Remove temp files
+      run: |
+        cd proofs
+        rm -rf out/theory.spthy out/oracle.py
+    - 
+      name: Upload results
+      uses: actions/upload-artifact@v3
+      with:
+        name: proofs
+        path: proofs/out

proofs/Makefile

@@ -1,9 +1,10 @@
 IMAGE           ?= selfrevocation/tamarin
-VERSION         ?= v1.6.1
+VERSION         ?= v1.8.0
 NAME            ?= tamarin
 MODEL           ?= centralized-time
 THREADS         ?= 4
-OUT_FILE        ?= output.spthy   
+OUT_FILE        ?= output.spthy
+LEMMA           ?=
 
 ENV              = -e LC_ALL=C.UTF-8
 VOLUME           = $(shell cd $(MODEL); pwd)
@@ -15,10 +16,15 @@ ifdef BACKGROUND
 DOCKER_DETACHED  = -d
 endif
 
+LEMMAS		  ?= $(shell echo $(LEMMA) | sed s/,/" --prove="/g)
+
 MKDIR           ?= mkdir -m 777 -p
 
+check: clean_docker __create_out
+	docker run --name $(NAME) $(DOCKER_DETACHED) --entrypoint tamarin-prover $(ENV) -v $(OUT_FOLDER):/home/tamarin $(IMAGE):$(VERSION) -v theory.spthy
+
 prove: clean_docker __create_out
-	docker run --name $(NAME) $(DOCKER_DETACHED) --entrypoint tamarin-prover $(ENV) -v $(OUT_FOLDER):/home/tamarin $(IMAGE):$(VERSION) --prove --output=$(OUT_FILE) theory.spthy +RTS -N$(THREADS) -RTS
+	docker run --name $(NAME) $(DOCKER_DETACHED) --entrypoint tamarin-prover $(ENV) -v $(OUT_FOLDER):/home/tamarin $(IMAGE):$(VERSION) --prove=$(LEMMAS) --output=$(OUT_FILE) theory.spthy +RTS -N$(THREADS) -RTS
 
 interactive: clean_docker __create_out
 	docker run --name $(NAME) --entrypoint tamarin-prover $(ENV) --network host -d -v $(OUT_FOLDER):/home/tamarin $(IMAGE):$(VERSION) interactive theory.spthy +RTS -N$(THREADS) -RTS

proofs/README.md

@@ -17,10 +17,8 @@ V-B). These models are divided in two sub-folders:
 Both models are defined in the files called `theory.spthy`. 
 
 We successfully verified all the lemmas in the models using Tamarin version
-`1.6.1`. Outputs from previous executions are found in `output.txt` and
-`output.spthy`. Very recently, Tamarin released version `1.8.0`: We failed to
-verify our models with this version as we experienced a much higher memory and
-CPU utilization. We will investigate this issue in the future.
+`1.6.1` and `1.8.0`. Outputs from previous executions are found in `output.txt`
+and `output.spthy`.
 
 The oracles `oracle.py` help Tamarin to create efficient proofs and allow it to
 terminate. Without it, Tamarin would either use too much memory or get stuck in
@@ -49,8 +47,8 @@ Dockerfile to install Python 3, in order to run our oracles.
 
 The Docker images are publicly available at `selfrevocation/tamarin`. Different
 tags use different Tamarin versions:
-- `latest` (or `v1.7.1`) was built from commit
-  `ba7f2b8b259c3808441b093b4fff039430753332`.
+- `latest` (or `v1.8.0`) was built from tag `1.8.0`, which corresponds to the
+  official Tamarin release `1.8.0`.
 - `v1.6.1` was built from tag `1.6.1`, which corresponds to the official
   Tamarin release `1.6.1`.
 
@@ -131,21 +129,32 @@ make clean
 
 ## Run locally
 
-Python 3 is required to run the oracles: `sudo apt install python3`
+Python 3 is required to run the oracles: `sudo apt install python3`.
+[Homebrew](https://brew.sh/) is also required to install Tamarin.
 
-**NOTE**: As mentioned above, Tamarin `1.8.0` is currently not able to verify
-our models efficiently. The instructions below will install Tamarin `1.6.1`.
+Below we give instructions to install the latest Tamarin version (currently
+1.8.0), or version 1.6.1. Choose the version you prefer. More installation
+instructions are provided
+[here](https://tamarin-prover.com/manual/master/book/002_installation.html).
 
-### Tamarin installation
+### Tamarin installation (LATEST VERSION)
 
-First of all, install [Homebrew](https://brew.sh/) and make sure that the `brew`
-command works. Then, install Tamarin as shown below:
+```bash
+# Install Tamarin
+brew install tamarin-prover/tap/tamarin-prover
+
+# Check version
+tamarin-prover --version
+```
+
+
+### Tamarin installation (VERSION 1.6.1)
 
 ```bash
 # Get brew formula of Tamarin 1.6.1
 wget https://raw.githubusercontent.com/tamarin-prover/homebrew-tap/e6696f0f3c1f131b633c98aa657c5792c6d07737/Formula/tamarin-prover.rb -O tamarin-prover.rb
 
-# Install tamarin
+# Install Tamarin
 brew install tamarin-prover.rb
 
 # Check that we have indeed installed tamarin 1.6.1

proofs/centralized-time/oracle.py

@@ -77,7 +77,7 @@ def add_goal(ranking, goal):
       add_goal(50, num)
     elif "!KU(" in line and not "sign" in line:
       add_goal(60, num)
-    elif "'1'+'1'" in line:
+    elif "'1'+'1'" in line or "'1'++'1'" in line:
       add_goal(70, num)
 
     # hard goals
@@ -139,11 +139,14 @@ def add_goal(ranking, goal):
       add_goal(3, num)
     elif "!KU( sign(<prl.2, t>, ~ltk)" in line:
       add_goal(4, num)
-    elif "#vr < #k" in line and "cnt+z" in line:
+    elif "#vr < #k" in line and ("cnt+z" in line or "cnt++z" in line):
       add_goal(5, num)
-    elif "#k < #vr.3" in line and "'1'+cnt" in line:
+    elif "#k < #vr.3" in line and ("'1'+cnt" in line or "'1'++cnt" in line):
       add_goal(6, num)
-    elif "t_rev" in line and ("('1'+'1'+t)" in line or "('1'+'1'+t+tv)" in line):
+    elif "t_rev" in line and (
+      "('1'+'1'+t)" in line or "('1'++'1'++t)" in line or
+      "('1'+'1'+t+tv)" in line or "('1'++'1'++t++tv)" in line
+      ):
       add_goal(7, num)
 
   elif lemma in [
@@ -169,11 +172,11 @@ def add_goal(ranking, goal):
     # constraints
     elif "#vr." in line and ("#j" in line or "#k" in line):
       add_goal(40, num)
-    elif "!Time" not in line and "('1'+t+tv)" in line:
+    elif "!Time" not in line and ("('1'+t+tv)" in line or "('1'++t++tv)" in line):
       add_goal(41, num)
-    elif "('1'+t)" in line:
+    elif "('1'+t)" in line or "('1'++t)" in line:
       add_goal(42, num)
-    elif "'1'+" in line:
+    elif "'1'+" in line or "'1'++" in line:
       add_goal(43, num)
     elif "!Time( 'TC'" in line:
       add_goal(100, num)

proofs/centralized-time/theory.spthy

@@ -329,6 +329,7 @@ rule RA_issue_revocation:
         !Time('RA', t)
       , !Pseudonym(ps)
       , !PRL(prl, cnt)
+      , In(prl) // helps with partial deconstructions. PRL is public anyway.
     ]
     --[ 
         /* restrictions */
@@ -349,6 +350,8 @@ rule RA_issue_revocation:
 rule RA_advance_time:
     [
         !Time('RA', t)
+      , In(t) // helps with partial deconstructions. Time is public anyway.
+
     ]
     --[ 
         /* restrictions */

proofs/distributed-time/oracle.py

@@ -25,10 +25,13 @@ def add_goal(ranking, goal):
       add_goal(1, num)
     if "tout" not in line and (
       ("('1'+t_rev+z+z.1)" in line and "('1'+'1'+t.1)" in line) or
-      ("('1'+t_rev+tv+z+z.1)" in line and "('1'+'1'+tv+t.1)" in line)
+      ("('1'++t_rev++z++z.1)" in line and "('1'++'1'++t.1)" in line) or
+      ("('1'+t_rev+tv+z+z.1)" in line and "('1'+'1'+tv+t.1)" in line) or
+      ("('1'++t_rev++tv++z++z.1)" in line and "('1'++'1'++tv++t.1)" in line)
     ):
       add_goal(2, num)
-    elif "!Time( ('1'+t_rev+z)" in line or "!Time( ('1'+t_rev+tv+z)" in line:
+    elif "!Time( ('1'+t_rev+z)" in line or "!Time( ('1'++t_rev++z)" in line or \
+    "!Time( ('1'+t_rev+tv+z)" in line or "!Time( ('1'++t_rev++tv++z)" in line:
       add_goal(3, num)
     elif "!KU( sign(<prl.1, t_hb>, ~ltk)" in line:
       add_goal(4, num)    
@@ -50,9 +53,11 @@ def add_goal(ranking, goal):
       add_goal(2, num)
     elif "!KU( sign(<prl, t_hb>, ~ltk)" in line:
       add_goal(3, num)
-    elif "!Time( ('1'+t_rev+z)" in line or "!Time( ('1'+t_rev+tv+z)" in line:
+    elif "!Time( ('1'+t_rev+z)" in line or "!Time( ('1'++t_rev++z)" in line or \
+        "!Time( ('1'+t_rev+tv+z)" in line or "!Time( ('1'++t_rev++tv++z)" in line:
       add_goal(4, num)
-    if "(('1'+t_rev+z)" in line or "(('1'+t_rev+tv+z)" in line:
+    if "(('1'+t_rev+z)" in line or "(('1'++t_rev++z)" in line or \
+        "(('1'+t_rev+tv+z)" in line or "(('1'++t_rev++tv++z)" in line:
       add_goal(5, num)
     elif "!Timeout" in line:
       add_goal(6, num)
@@ -109,7 +114,8 @@ def add_goal(ranking, goal):
   elif lemma in [
     "effective_revocation"
   ]:
-    if "((t_v2v+tv.1) = (t_rev+z+tv.1+tv.1))" in line:
+    if "((t_v2v+tv.1) = (t_rev+z+tv.1+tv.1))" in line or \
+      "((t_v2v++tv.1) = (t_rev++z++tv.1++tv.1))" in line:
       add_goal(1, num)
     else:
       add_goal(900, num)

proofs/distributed-time/theory.spthy

@@ -382,6 +382,7 @@ rule RA_issue_revocation:
         !Time(t)
       , !Pseudonym(ps)
       , !PRL(prl, cnt)
+      , In(prl) // helps with partial deconstructions. PRL is public anyway.
     ]
     --[ 
         /* restrictions */
@@ -402,6 +403,7 @@ rule RA_issue_revocation:
 rule advance_time:
     [
         !Time(t)
+      , In(t) // helps with partial deconstructions. Time is public anyway.
     ]
     --[ 
         /* restrictions */