diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml new file mode 100644 index 0000000..7a373fd --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/proofs/Makefile b/proofs/Makefile index 5630bce..25267a2 100644 --- a/proofs/Makefile +++ b/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 diff --git a/proofs/README.md b/proofs/README.md index 9a52ab1..25fc631 100644 --- a/proofs/README.md +++ b/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 diff --git a/proofs/centralized-time/oracle.py b/proofs/centralized-time/oracle.py index 9d49f9a..1b5328b 100755 --- a/proofs/centralized-time/oracle.py +++ b/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(, ~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) diff --git a/proofs/centralized-time/theory.spthy b/proofs/centralized-time/theory.spthy index 210ffc1..7541806 100644 --- a/proofs/centralized-time/theory.spthy +++ b/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 */ diff --git a/proofs/distributed-time/oracle.py b/proofs/distributed-time/oracle.py index c19aca1..43bbf0a 100755 --- a/proofs/distributed-time/oracle.py +++ b/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(, ~ltk)" in line: add_goal(4, num) @@ -50,9 +53,11 @@ def add_goal(ranking, goal): add_goal(2, num) elif "!KU( sign(, ~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) diff --git a/proofs/distributed-time/theory.spthy b/proofs/distributed-time/theory.spthy index 3e0e49b..23bb6b1 100644 --- a/proofs/distributed-time/theory.spthy +++ b/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 */