Merge remote-tracking branch 'origin' into pr-spthy-config-mirror

.github/workflows/tamarin-integration-test.yaml

@@ -15,7 +15,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install graphviz
-          
+
       - name: Caching
         uses: actions/cache@v2
         with:
@@ -37,8 +37,8 @@ jobs:
           curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
           chmod a+x ~/.local/bin/stack
           stack --no-terminal setup
-          curl -L https://github.com/tamarin-prover/tamarin-prover/releases/download/1.6.0/Maude-2.7.1-linux.zip > maude.zip
-          unzip -o maude.zip -d ~/.local/bin/
+          curl -L https://github.com/SRI-CSL/Maude/releases/download/3.2.1/Maude-3.2.1-linux.zip > maude.zip
+          unzip -oj maude.zip -d ~/.local/bin/
           mv -f ~/.local/bin/maude.linux64 ~/.local/bin/maude
           chmod a+x ~/.local/bin/maude
           mkdir -p case-studies case-studies/ake case-studies/ake/bilinear case-studies/ake/dh case-studies/related_work

.gitignore

@@ -42,8 +42,14 @@ stack.yaml.lock
 
 *.iml
 .idea/
+.vscode/
 out/
 
 *.pv
 
 .worktree
+
+
+**/benchmark
+**/input
+**/diff

Makefile

@@ -36,9 +36,9 @@ profiling:
 tamarin-clean:
 	stack clean
 
-# Clean Tamarin and SAPIC
+# Clean Tamarin
 .PHONY: clean
-clean:	tamarin-clean sapic-clean
+clean:	tamarin-clean
 
 # ###########################################################################
 # NOTE the remainder makefile is FOR DEVELOPERS ONLY.
@@ -411,7 +411,7 @@ auto-sources-case-studies:	$(AUTO_SOURCES_CS_TARGETS)
 ## Regression (old issues)
 ##########################
 
-REGRESSION_CASE_STUDIES=issue216.spthy issue193.spthy issue310.spthy
+REGRESSION_CASE_STUDIES=issue216.spthy issue193.spthy issue310.spthy issue519.spthy
 
 REGRESSION_TARGETS=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies$(SUBDIR)regression/trace/,$(REGRESSION_CASE_STUDIES)))
 

case-studies-regression/Tutorial_analyzed.spthy

@@ -2,15 +2,16 @@ theory Tutorial begin
 
 // Function signature and definition of the equational theory E
 
-functions: adec/2, aenc/2, fst/1[destructor], h/1, pair/2, pk/1,
-           snd/1[destructor]
+functions: adec/2, aenc/2, fst/1, h/1, pair/2, pk/1, snd/1
 equations:
     adec(aenc(m, pk(k)), k) = m,
     fst(<x.1, x.2>) = x.1,
     snd(<x.1, x.2>) = x.2
 
 
 
+
+
 rule (modulo E) Register_pk:
    [ Fr( ~ltk ) ] --> [ !Ltk( $A, ~ltk ), !Pk( $A, pk(~ltk) ) ]
 
@@ -231,36 +232,36 @@ qed
 
 
 
-/* All well-formedness checks were successful. */
 
-end
-/* Output
-maude tool: 'maude'
- checking version: 3.0. OK.
- checking installation: OK.
 
 
-analyzing: examples/Tutorial.spthy
 
-------------------------------------------------------------------------------
-analyzed: examples/Tutorial.spthy
 
-  output:          examples/Tutorial.spthy.tmp
-  processing time: 0.148807957s
-  Client_session_key_secrecy (all-traces): verified (5 steps)
-  Client_auth (all-traces): verified (11 steps)
-  Client_auth_injective (all-traces): verified (15 steps)
-  Client_session_key_honest_setup (exists-trace): verified (5 steps)
 
-------------------------------------------------------------------------------
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.1
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.1. OK.
+ checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/Tutorial.spthy
 
   output:          examples/Tutorial.spthy.tmp
-  processing time: 0.148807957s
+  processing time: 0.17s
+
   Client_session_key_secrecy (all-traces): verified (5 steps)
   Client_auth (all-traces): verified (11 steps)
   Client_auth_injective (all-traces): verified (15 steps)

case-studies-regression/ake/bilinear/Chen_Kudla_analyzed.spthy

@@ -3,13 +3,15 @@ theory Chen_Kudla begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing
-functions: fst/1[destructor], h/1, hp/1, kdf/1, pair/2, snd/1[destructor]
+functions: fst/1, h/1, hp/1, kdf/1, pair/2, snd/1
 equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
 
 
 
 
+
+
 section{* A variant of the Chen-Kudla protocol that uses ordered concatenation instead 
           addition of points *}
 
@@ -2582,34 +2584,51 @@ qed
 
 
 
-/* All well-formedness checks were successful. */
 
-end
-/* Output
-maude tool: 'maude'
- checking version: 3.0. OK.
- checking installation: OK.
 
 
-analyzing: examples/ake/bilinear/Chen_Kudla.spthy
 
-------------------------------------------------------------------------------
-analyzed: examples/ake/bilinear/Chen_Kudla.spthy
 
-  output:          examples/ake/bilinear/Chen_Kudla.spthy.tmp
-  processing time: 88.051054428s
-  key_agreement_reachable (exists-trace): verified (13 steps)
-  key_secrecy_ephemeral_no_WPFS (all-traces): verified (679 steps)
 
-------------------------------------------------------------------------------
+/*
+WARNING: the following wellformedness checks failed!
+
+The variables of the follwing rule(s) are not derivable from their premises, you may be performing unintended pattern matching:
+  Reveal_session_key
+Failed to derive Variable(s): sek
+
+  Init_2
+Failed to derive Variable(s): ~s1, ~s2
+
+  Resp_1
+Failed to derive Variable(s): ~msk
+*/
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.1
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.1. OK.
+ checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/ake/bilinear/Chen_Kudla.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla.spthy.tmp
-  processing time: 88.051054428s
+  processing time: 29.07s
+
+  WARNING: 3 wellformedness check failed!
+           The analysis results might be wrong!
+
   key_agreement_reachable (exists-trace): verified (13 steps)
   key_secrecy_ephemeral_no_WPFS (all-traces): verified (679 steps)
 

case-studies-regression/ake/bilinear/Chen_Kudla_eCK_analyzed.spthy

@@ -3,13 +3,15 @@ theory Chen_Kudla begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing
-functions: fst/1[destructor], h/1, hp/1, kdf/1, pair/2, snd/1[destructor]
+functions: fst/1, h/1, hp/1, kdf/1, pair/2, snd/1
 equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
 
 
 
 
+
+
 section{* A variant of the Chen-Kudla protocol that uses ordered concatenation instead 
           addition of points *}
 
@@ -511,33 +513,51 @@ qed
 
 
 
-/* All well-formedness checks were successful. */
 
-end
-/* Output
-maude tool: 'maude'
- checking version: 3.0. OK.
- checking installation: OK.
 
 
-analyzing: examples/ake/bilinear/Chen_Kudla_eCK.spthy
 
-------------------------------------------------------------------------------
-analyzed: examples/ake/bilinear/Chen_Kudla_eCK.spthy
 
-  output:          examples/ake/bilinear/Chen_Kudla_eCK.spthy.tmp
-  processing time: 55.372479208s
-  key_secrecy_eCK_like (all-traces): falsified - found trace (24 steps)
 
-------------------------------------------------------------------------------
+/*
+WARNING: the following wellformedness checks failed!
+
+The variables of the follwing rule(s) are not derivable from their premises, you may be performing unintended pattern matching:
+  Reveal_session_key
+Failed to derive Variable(s): sek
+
+  Init_2
+Failed to derive Variable(s): ~s1, ~s2
+
+  Resp_1
+Failed to derive Variable(s): ~msk
+*/
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.1
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.1. OK.
+ checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/ake/bilinear/Chen_Kudla_eCK.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla_eCK.spthy.tmp
-  processing time: 55.372479208s
+  processing time: 19.03s
+
+  WARNING: 3 wellformedness check failed!
+           The analysis results might be wrong!
+
   key_secrecy_eCK_like (all-traces): falsified - found trace (24 steps)
 
 ==============================================================================