regenerates I/O spec for DH

Author: ArquintL

dh/implementation/verification/fact/fact.gobra

@@ -147,20 +147,20 @@ ghost type Fact domain {
 
 }
 ghost
-decreases
 // returns a multiset containing just the persistent facts of l all with multiplicity 1
 ensures forall f Fact :: { f # result } (f # result) == (persistent(f) && (f # l) > 0 ? 1 : 0)
+decreases
 pure func persistentFacts(l mset[Fact]) (result mset[Fact])
 
 ghost
-decreases
 // returns a multiset containing just the non-persistent facts of l while retaining their multiplicity
 ensures forall f Fact :: { f # result } (f # result) == (persistent(f) ? 0 : (f # l))
+decreases
 pure func linearFacts(l mset[Fact]) (result mset[Fact])
 
 ghost
-decreases
 ensures res == (linearFacts(l) subset s && persistentFacts(l) subset s)
+decreases
 pure func M(l mset[Fact], s mset[Fact]) (res bool) {
     // non-persistent facts
     return linearFacts(l) subset s &&
@@ -169,6 +169,6 @@ pure func M(l mset[Fact], s mset[Fact]) (res bool) {
 }
 
 ghost
-decreases
 ensures result == s setminus linearFacts(l) union r
+decreases
 pure func U(l mset[Fact], r mset[Fact], s mset[Fact]) (result mset[Fact])

dh/implementation/verification/iospec/permissions_Alice_internal.gobra

@@ -14,58 +14,58 @@ import . "dh-gobra/verification/fresh"
 pred e_Alice_send(ghost tami_p Place, ghost ridA Term, ghost A Term, ghost B Term, ghost skA Term, ghost skB Term, ghost x Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Alice_send(tami_p, ridA, A, B, skA, skB, x, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Alice_send_placeDst(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Alice_send(tami_p, ridA, A, B, skA, skB, x, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Alice_send_placeDst(tami_p, ridA, A, B, skA, skB, x, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Alice_send(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 
 
 // permission e_Alice_recvAndSend
 pred e_Alice_recvAndSend(ghost tami_p Place, ghost ridA Term, ghost A Term, ghost B Term, ghost skA Term, ghost skB Term, ghost x Term, ghost Y Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Alice_recvAndSend(tami_p, ridA, A, B, skA, skB, x, Y, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Alice_recvAndSend_placeDst(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, Y Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Alice_recvAndSend(tami_p, ridA, A, B, skA, skB, x, Y, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Alice_recvAndSend_placeDst(tami_p, ridA, A, B, skA, skB, x, Y, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Alice_recvAndSend(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, Y Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 
 
 // permission e_Alice_sendMsg
 pred e_Alice_sendMsg(ghost tami_p Place, ghost ridA Term, ghost A Term, ghost B Term, ghost skA Term, ghost skB Term, ghost x Term, ghost Y Term, ghost msgIn Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Alice_sendMsg(tami_p, ridA, A, B, skA, skB, x, Y, msgIn, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Alice_sendMsg_placeDst(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, Y Term, msgIn Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Alice_sendMsg(tami_p, ridA, A, B, skA, skB, x, Y, msgIn, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Alice_sendMsg_placeDst(tami_p, ridA, A, B, skA, skB, x, Y, msgIn, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Alice_sendMsg(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, Y Term, msgIn Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 
 
 // permission e_Alice_recvMsg
 pred e_Alice_recvMsg(ghost tami_p Place, ghost ridA Term, ghost A Term, ghost B Term, ghost skA Term, ghost skB Term, ghost x Term, ghost Y Term, ghost msgOut Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Alice_recvMsg(tami_p, ridA, A, B, skA, skB, x, Y, msgOut, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Alice_recvMsg_placeDst(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, Y Term, msgOut Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Alice_recvMsg(tami_p, ridA, A, B, skA, skB, x, Y, msgOut, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Alice_recvMsg_placeDst(tami_p, ridA, A, B, skA, skB, x, Y, msgOut, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Alice_recvMsg(tami_p Place, ridA Term, A Term, B Term, skA Term, skB Term, x Term, Y Term, msgOut Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 

dh/implementation/verification/iospec/permissions_Bob_internal.gobra

@@ -14,58 +14,58 @@ import . "dh-gobra/verification/fresh"
 pred e_Bob_recvAndSend(ghost tami_p Place, ghost ridB Term, ghost B Term, ghost A Term, ghost skB Term, ghost skA Term, ghost y Term, ghost X Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Bob_recvAndSend(tami_p, ridB, B, A, skB, skA, y, X, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Bob_recvAndSend_placeDst(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Bob_recvAndSend(tami_p, ridB, B, A, skB, skA, y, X, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Bob_recvAndSend_placeDst(tami_p, ridB, B, A, skB, skA, y, X, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Bob_recvAndSend(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 
 
 // permission e_Bob_recv
 pred e_Bob_recv(ghost tami_p Place, ghost ridB Term, ghost B Term, ghost A Term, ghost skB Term, ghost skA Term, ghost y Term, ghost X Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Bob_recv(tami_p, ridB, B, A, skB, skA, y, X, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Bob_recv_placeDst(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Bob_recv(tami_p, ridB, B, A, skB, skA, y, X, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Bob_recv_placeDst(tami_p, ridB, B, A, skB, skA, y, X, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Bob_recv(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 
 
 // permission e_Bob_recvMsg
 pred e_Bob_recvMsg(ghost tami_p Place, ghost ridB Term, ghost B Term, ghost A Term, ghost skB Term, ghost skA Term, ghost y Term, ghost X Term, ghost msgOut Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Bob_recvMsg(tami_p, ridB, B, A, skB, skA, y, X, msgOut, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Bob_recvMsg_placeDst(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, msgOut Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Bob_recvMsg(tami_p, ridB, B, A, skB, skA, y, X, msgOut, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Bob_recvMsg_placeDst(tami_p, ridB, B, A, skB, skA, y, X, msgOut, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Bob_recvMsg(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, msgOut Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 
 
 // permission e_Bob_sendMsg
 pred e_Bob_sendMsg(ghost tami_p Place, ghost ridB Term, ghost B Term, ghost A Term, ghost skB Term, ghost skA Term, ghost y Term, ghost X Term, ghost msgIn Term, ghost tami_lp mset[Fact], ghost tami_ap mset[Claim], ghost tami_rp mset[Fact])
 
 ghost
-decreases
 requires e_Bob_sendMsg(tami_p, ridB, B, A, skB, skA, y, X, msgIn, tami_lp, tami_ap, tami_rp)
+decreases
 pure func get_e_Bob_sendMsg_placeDst(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, msgIn Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (placeDst Place)
 
 ghost
-decreases
 requires token(tami_p) && e_Bob_sendMsg(tami_p, ridB, B, A, skB, skA, y, X, msgIn, tami_lp, tami_ap, tami_rp)
 ensures token(tami_pp) && tami_pp == old(get_e_Bob_sendMsg_placeDst(tami_p, ridB, B, A, skB, skA, y, X, msgIn, tami_lp, tami_ap, tami_rp))
+decreases
 func internBIO_e_Bob_sendMsg(tami_p Place, ridB Term, B Term, A Term, skB Term, skA Term, y Term, X Term, msgIn Term, tami_lp mset[Fact], tami_ap mset[Claim], tami_rp mset[Fact]) (tami_pp Place)
 

dh/implementation/verification/iospec/permissions_in.gobra

@@ -14,84 +14,84 @@ import . "dh-gobra/verification/fresh"
 pred e_FrFact(ghost tami_p Place, ghost tami_rid Term)
 
 ghost
-decreases
 requires e_FrFact(tami_p, tami_rid)
+decreases
 pure func get_e_FrFact_r1(tami_p Place, tami_rid Term) (r1 Term)
 
 ghost
-decreases
 requires e_FrFact(tami_p, tami_rid)
+decreases
 pure func get_e_FrFact_placeDst(tami_p Place, tami_rid Term) (placeDst Place)
 
 
 // permission e_InFact
 pred e_InFact(ghost tami_p Place, ghost tami_rid Term)
 
 ghost
-decreases
 requires e_InFact(tami_p, tami_rid)
+decreases
 pure func get_e_InFact_r1(tami_p Place, tami_rid Term) (r1 Term)
 
 ghost
-decreases
 requires e_InFact(tami_p, tami_rid)
+decreases
 pure func get_e_InFact_placeDst(tami_p Place, tami_rid Term) (placeDst Place)
 
 
 // permission e_Setup_Alice
 pred e_Setup_Alice(ghost tami_p Place, ghost tami_rid Term)
 
 ghost
-decreases
 requires e_Setup_Alice(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Alice_r1(tami_p Place, tami_rid Term) (r1 Term)
 
 ghost
-decreases
 requires e_Setup_Alice(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Alice_r2(tami_p Place, tami_rid Term) (r2 Term)
 
 ghost
-decreases
 requires e_Setup_Alice(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Alice_r3(tami_p Place, tami_rid Term) (r3 Term)
 
 ghost
-decreases
 requires e_Setup_Alice(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Alice_r4(tami_p Place, tami_rid Term) (r4 Term)
 
 ghost
-decreases
 requires e_Setup_Alice(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Alice_placeDst(tami_p Place, tami_rid Term) (placeDst Place)
 
 
 // permission e_Setup_Bob
 pred e_Setup_Bob(ghost tami_p Place, ghost tami_rid Term)
 
 ghost
-decreases
 requires e_Setup_Bob(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Bob_r1(tami_p Place, tami_rid Term) (r1 Term)
 
 ghost
-decreases
 requires e_Setup_Bob(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Bob_r2(tami_p Place, tami_rid Term) (r2 Term)
 
 ghost
-decreases
 requires e_Setup_Bob(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Bob_r3(tami_p Place, tami_rid Term) (r3 Term)
 
 ghost
-decreases
 requires e_Setup_Bob(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Bob_r4(tami_p Place, tami_rid Term) (r4 Term)
 
 ghost
-decreases
 requires e_Setup_Bob(tami_p, tami_rid)
+decreases
 pure func get_e_Setup_Bob_placeDst(tami_p Place, tami_rid Term) (placeDst Place)
 

dh/implementation/verification/iospec/permissions_out.gobra

@@ -14,7 +14,7 @@ import . "dh-gobra/verification/fresh"
 pred e_OutFact(ghost tami_p Place, ghost tami_rid Term, ghost new_x Term)
 
 ghost
-decreases
 requires e_OutFact(tami_p, tami_rid, new_x)
+decreases
 pure func get_e_OutFact_placeDst(tami_p Place, tami_rid Term, new_x Term) (placeDst Place)
 

dh/model/README.md

@@ -14,3 +14,8 @@ Version 1.10.0 is known to work.
 To verify the model with Tamarin, use the following command:
 
 `tamarin-prover --prove dh.spthy --derivcheck-timeout=0`
+
+
+## Generate I/O specification
+Adapt the absolute paths in `generate-spec.sh` and `generate-spec-config.txt` to point to the files in this repository and the specification generator from the [`viperproject/protocol-verification-refinement` repository](https://github.com/viperproject/protocol-verification-refinement) before running `generate-spec.sh`.
+The resulting files will be stored in the `generated_iospecs` directory.

dh/model/generate-spec.sh

@@ -1,7 +1,7 @@
 #!/bin/bash
 
 cwd=$(pwd)
-cd /Users/arquintlinard/ETH/PhD/tamigloo-compiler/tamarin-prover || exit
+cd /Users/arquintlinard/ETH/PhD/protocol-verification-refinement/specification-generator/src || exit
 echo $PWD
 stack build
 stack exec -- tamarin-prover --tamigloo-compiler "$cwd"/generate-spec-config.txt

docker/Dockerfile

@@ -47,7 +47,7 @@ RUN curl -q -s -S -L --create-dirs -o maude.zip $MAUDE_URL && \
     chmod a+x /.local/bin/maude
 
 # install tamarin-prover
-ENV TAMARIN_VERSION="1.8.0"
+ENV TAMARIN_VERSION="1.10.0"
 RUN curl -q -s -S -L --create-dirs -o tamarin.tar.gz https://github.com/tamarin-prover/tamarin-prover/releases/download/$TAMARIN_VERSION/tamarin-prover-$TAMARIN_VERSION-linux64-ubuntu.tar.gz && \
     tar -x -C /.local/bin/ -f tamarin.tar.gz && \
     rm tamarin.tar.gz && \