Merge branch 'develop' into fix-accountability-examples

tamarin-prover · Dec 5, 2023 · 26c779f · 26c779f
2 parents 68a125a + 1a7df25
commit 26c779f
Show file tree

Hide file tree

Showing 15 changed files with 311 additions and 238 deletions.
diff --git a/case-studies-regression/fast-tests/ccs15/DDH_analyzed-diff.spthy b/case-studies-regression/fast-tests/ccs15/DDH_analyzed-diff.spthy
@@ -17,8 +17,6 @@ rule (modulo E) DDH:
   -->
    [ Out( <g^~x, g^~y, diff(g^~z, g^~x^~y)> ) ]
 
-/* All wellformedness checks were successful. */
-
 diffLemma Observational_equivalence:
 rule-equivalence
   case Rule_DDH
@@ -7557,27 +7555,26 @@ next
   qed
 qed
 
+/* All wellformedness checks were successful. */
+
 /*
 Generated from:
-Tamarin version 1.8.0
-Maude version 3.2.1
-Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
-Compiled at: 2023-08-29 12:56:59.317473841 UTC
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 0194f3b61d6d8b8c1d70bbad8fe0a7143cac0fb3, branch: feature/export-wellformedness
+Compiled at: 2023-10-25 08:40:09.47146758 UTC
 */
 
 end
 /* Output
-maude tool: 'maude'
- checking version: 3.2.1. OK.
- checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/ccs15/DDH.spthy
 
   output:          examples/ccs15/DDH.spthy.tmp
-  processing time: 4.08s
+  processing time: 6.43s
 
   DiffLemma:  Observational_equivalence : verified (2522 steps)
 

diff --git a/case-studies-regression/fast-tests/ccs15/probEnc_analyzed-diff.spthy b/case-studies-regression/fast-tests/ccs15/probEnc_analyzed-diff.spthy
@@ -22,8 +22,6 @@ rule (modulo E) enc:
   -->
    [ Out( diff(~r1, penc(x, pk(k), ~r2)) ) ]
 
-/* All wellformedness checks were successful. */
-
 diffLemma Observational_equivalence:
 rule-equivalence
   case Rule_Destrd_0_fst
@@ -221,27 +219,26 @@ next
   qed
 qed
 
+/* All wellformedness checks were successful. */
+
 /*
 Generated from:
-Tamarin version 1.8.0
-Maude version 3.2.1
-Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
-Compiled at: 2023-08-29 12:56:59.317473841 UTC
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 0194f3b61d6d8b8c1d70bbad8fe0a7143cac0fb3, branch: feature/export-wellformedness
+Compiled at: 2023-10-25 08:40:09.47146758 UTC
 */
 
 end
 /* Output
-maude tool: 'maude'
- checking version: 3.2.1. OK.
- checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/ccs15/probEnc.spthy
 
   output:          examples/ccs15/probEnc.spthy.tmp
-  processing time: 0.16s
+  processing time: 0.32s
 
   DiffLemma:  Observational_equivalence : verified (75 steps)
 

diff --git a/...tudies-regression/fast-tests/csf18-xor/diff-models/CH07-UK3_analyzed-diff-obseqonly.spthy b/...tudies-regression/fast-tests/csf18-xor/diff-models/CH07-UK3_analyzed-diff-obseqonly.spthy
@@ -191,23 +191,6 @@ guarded formula characterizing all satisfying traces:
 */
 by sorry
 
-/*
-WARNING: the following wellformedness checks failed!
-
-Check presence of the --prove/--lemma arguments in theory
-=========================================================
-
-  --> 'Observational_equivalence' from arguments do(es) not correspond to a specified lemma in the theory 
-
-Message Derivation Checks
-=========================
-
-  The variables of the follwing rule(s) are not derivable from their premises, you may be performing unintended pattern matching.
-
-Rule reader2: 
-Failed to derive Variable(s): hash
-*/
-
 diffLemma Observational_equivalence:
 rule-equivalence
   case Rule_Equality
@@ -272,27 +255,41 @@ rule-equivalence
   qed
 qed
 
+/*
+WARNING: the following wellformedness checks failed!
+
+Check presence of the --prove/--lemma arguments in theory
+=========================================================
+
+  --> 'Observational_equivalence' from arguments do(es) not correspond to a specified lemma in the theory 
+
+Message Derivation Checks
+=========================
+
+  The variables of the follwing rule(s) are not derivable from their premises, you may be performing unintended pattern matching.
+
+Rule reader2: 
+Failed to derive Variable(s): hash
+*/
+
 /*
 Generated from:
-Tamarin version 1.8.0
-Maude version 3.2.1
-Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
-Compiled at: 2023-08-29 12:56:59.317473841 UTC
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 0194f3b61d6d8b8c1d70bbad8fe0a7143cac0fb3, branch: feature/export-wellformedness
+Compiled at: 2023-10-25 08:40:09.47146758 UTC
 */
 
 end
 /* Output
-maude tool: 'maude'
- checking version: 3.2.1. OK.
- checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/csf18-xor/diff-models/CH07-UK3.spthy
 
   output:          examples/csf18-xor/diff-models/CH07-UK3.spthy.tmp
-  processing time: 118.44s
+  processing time: 248.08s
 
   WARNING: 2 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/fast-tests/features/equivalence/MacroDiffprobEnc_analyzed-diff.spthy b/case-studies-regression/fast-tests/features/equivalence/MacroDiffprobEnc_analyzed-diff.spthy
@@ -37,8 +37,6 @@ rule (modulo E) gen:
   rule (modulo E) gen:
      [ Fr( ~k ) ] --> [ !Key( ~k ), Out( pk(~k) ) ]
 
-/* All wellformedness checks were successful. */
-
 diffLemma Observational_equivalence:
 rule-equivalence
   case Rule_Destrd_0_fst
@@ -236,27 +234,26 @@ next
   qed
 qed
 
+/* All wellformedness checks were successful. */
+
 /*
 Generated from:
-Tamarin version 1.8.0
-Maude version 3.2.1
-Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
-Compiled at: 2023-08-29 12:56:59.317473841 UTC
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 0194f3b61d6d8b8c1d70bbad8fe0a7143cac0fb3, branch: feature/export-wellformedness
+Compiled at: 2023-10-25 08:40:09.47146758 UTC
 */
 
 end
 /* Output
-maude tool: 'maude'
- checking version: 3.2.1. OK.
- checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/features/equivalence/MacroDiffprobEnc.spthy
 
   output:          examples/features/equivalence/MacroDiffprobEnc.spthy.tmp
-  processing time: 0.15s
+  processing time: 0.23s
 
   DiffLemma:  Observational_equivalence : verified (75 steps)
 

diff --git a/case-studies-regression/fast-tests/features/equivalence/N5N6DiffTest_analyzed-diff.spthy b/case-studies-regression/fast-tests/features/equivalence/N5N6DiffTest_analyzed-diff.spthy
@@ -14,8 +14,6 @@ equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 rule (modulo E) Test:
    [ Fr( ~f ) ] --> [ Out( diff(h($A), ~f) ) ]
 
-/* All wellformedness checks were successful. */
-
 diffLemma Observational_equivalence:
 rule-equivalence
   case Rule_Equality
@@ -38,27 +36,26 @@ rule-equivalence
   qed
 qed
 
+/* All wellformedness checks were successful. */
+
 /*
 Generated from:
-Tamarin version 1.8.0
-Maude version 3.2.1
-Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
-Compiled at: 2023-08-29 12:56:59.317473841 UTC
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 0194f3b61d6d8b8c1d70bbad8fe0a7143cac0fb3, branch: feature/export-wellformedness
+Compiled at: 2023-10-25 08:40:09.47146758 UTC
 */
 
 end
 /* Output
-maude tool: 'maude'
- checking version: 3.2.1. OK.
- checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/features/equivalence/N5N6DiffTest.spthy
 
   output:          examples/features/equivalence/N5N6DiffTest.spthy.tmp
-  processing time: 0.08s
+  processing time: 0.11s
 
   DiffLemma:  Observational_equivalence : falsified - found trace (8 steps)
 

diff --git a/case-studies-regression/fast-tests/regression/diff/issue223_analyzed-diff.spthy b/case-studies-regression/fast-tests/regression/diff/issue223_analyzed-diff.spthy
@@ -25,8 +25,6 @@ rule (modulo E) Attack3:
    Out( fake(~ni1, ~rnd1, ~ltkV1, ~ni1) ), Out( ~ltkV1 )
    ]
 
-/* All wellformedness checks were successful. */
-
 diffLemma Observational_equivalence:
 rule-equivalence
   case Rule_Attack3
@@ -3237,27 +3235,26 @@ next
   qed
 qed
 
+/* All wellformedness checks were successful. */
+
 /*
 Generated from:
-Tamarin version 1.8.0
-Maude version 3.2.1
-Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
-Compiled at: 2023-08-29 12:56:59.317473841 UTC
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 0194f3b61d6d8b8c1d70bbad8fe0a7143cac0fb3, branch: feature/export-wellformedness
+Compiled at: 2023-10-25 08:40:09.47146758 UTC
 */
 
 end
 /* Output
-maude tool: 'maude'
- checking version: 3.2.1. OK.
- checking installation: OK.
 
 ==============================================================================
 summary of summaries:
 
 analyzed: examples/regression/diff/issue223.spthy
 
   output:          examples/regression/diff/issue223.spthy.tmp
-  processing time: 2.39s
+  processing time: 4.42s
 
   DiffLemma:  Observational_equivalence : verified (1082 steps)
 

diff --git a/...n/fast-tests/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM_multiset_analyzed.spthy b/...n/fast-tests/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM_multiset_analyzed.spthy
@@ -1263,9 +1263,10 @@ Derivation Checks
 /*
 Generated from:
 Tamarin version 1.9.0
-Maude version 3.2.2
-Git revision: 0194f3b61d6d8b8c1d70bbad8fe0a7143cac0fb3, branch: feature/export-wellformedness
-Compiled at: 2023-10-25 08:40:09.47146758 UTC
+Maude version 3.2.1
+Git revision: 55828cc94e8fd2506948a8324714350e405b4d92 (with uncommited changes), branch: HEAD
+Compiled at: 2023-11-17 17:48:21.524079663 UTC
+
 */
 
 end
@@ -1277,7 +1278,8 @@ summary of summaries:
 analyzed: examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM_multiset.spthy
 
   output:          examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM_multiset.spthy.tmp
-  processing time: 11.61s
+  processing time: 5.49s
+
 
   WARNING: 2 wellformedness check failed!
            The analysis results might be wrong!