Add checks for potential modelling errors in rules (tamarin-prover#541)

* Message Derivation Checks (Squashed) * Update all regression case studies to version with ** new warnings (from Message Derivation Checks, this commit) ** tactics included --------- Message Derivation Checks authored-by: Jérôme Schneider <jerome.schneider@inf.ethz.ch> Regression update by: Ralf Sasse <ralf.sasse@gmail.com>
yavivanov · Jun 27, 2023 · b62bb18 · b62bb18
1 parent 8861567
commit b62bb18
Show file tree

Hide file tree

Showing 325 changed files with 7,651 additions and 2,102 deletions.
diff --git a/case-studies-regression/Tutorial_analyzed.spthy b/case-studies-regression/Tutorial_analyzed.spthy
@@ -10,6 +10,8 @@ equations:
 
 
 
+
+
 rule (modulo E) Register_pk:
    [ Fr( ~ltk ) ] --> [ !Ltk( $A, ~ltk ), !Pk( $A, pk(~ltk) ) ]
 
@@ -230,14 +232,20 @@ qed
 
 
 
+
+
+
+
+
+
 /* All wellformedness checks were successful. */
 
 /*
 Generated from:
 Tamarin version 1.7.1
 Maude version 3.2.1
-Git revision: 334a0df7d8ae5ec03764051e4e8eef985c6a4080, branch: develop
-Compiled at: 2023-01-27 13:01:52.341920052 UTC
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
 */
 
 end
@@ -252,7 +260,7 @@ summary of summaries:
 analyzed: examples/Tutorial.spthy
 
   output:          examples/Tutorial.spthy.tmp
-  processing time: 0.14s
+  processing time: 0.17s
 
   Client_session_key_secrecy (all-traces): verified (5 steps)
   Client_auth (all-traces): verified (11 steps)

diff --git a/case-studies-regression/ake/bilinear/Chen_Kudla_analyzed.spthy b/case-studies-regression/ake/bilinear/Chen_Kudla_analyzed.spthy
@@ -10,6 +10,8 @@ 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,14 +2584,32 @@ qed
 
 
 
-/* All wellformedness checks were successful. */
+
+
+
+
+
+
+/*
+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: 334a0df7d8ae5ec03764051e4e8eef985c6a4080, branch: develop
-Compiled at: 2023-01-27 13:01:52.341920052 UTC
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
 */
 
 end
@@ -2604,7 +2624,10 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Chen_Kudla.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla.spthy.tmp
-  processing time: 41.37s
+  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)

diff --git a/case-studies-regression/ake/bilinear/Chen_Kudla_eCK_analyzed.spthy b/case-studies-regression/ake/bilinear/Chen_Kudla_eCK_analyzed.spthy
@@ -10,6 +10,8 @@ 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,14 +513,32 @@ qed
 
 
 
-/* All wellformedness checks were successful. */
+
+
+
+
+
+
+/*
+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: 334a0df7d8ae5ec03764051e4e8eef985c6a4080, branch: develop
-Compiled at: 2023-01-27 13:01:52.341920052 UTC
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
 */
 
 end
@@ -533,7 +553,10 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Chen_Kudla_eCK.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla_eCK.spthy.tmp
-  processing time: 31.05s
+  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)
 

diff --git a/case-studies-regression/ake/bilinear/Joux_EphkRev_analyzed.spthy b/case-studies-regression/ake/bilinear/Joux_EphkRev_analyzed.spthy
@@ -11,6 +11,8 @@ equations:
 
 
 
+
+
 section{* The Joux Protocol using Signatures*}
 
 
@@ -1031,14 +1033,34 @@ solve( SessionKey( A, (B+C), sessKey ) @ #i )
   qed
 qed
 
-/* All wellformedness checks were successful. */
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+/*
+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:
+  Proto2
+Failed to derive Variable(s): ltkB, ltkC
+*/
 
 /*
 Generated from:
 Tamarin version 1.7.1
 Maude version 3.2.1
-Git revision: 334a0df7d8ae5ec03764051e4e8eef985c6a4080, branch: develop
-Compiled at: 2023-01-27 13:01:52.341920052 UTC
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
 */
 
 end
@@ -1053,7 +1075,10 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Joux_EphkRev.spthy
 
   output:          examples/ake/bilinear/Joux_EphkRev.spthy.tmp
-  processing time: 15.66s
+  processing time: 9.35s
+
+  WARNING: 1 wellformedness check failed!
+           The analysis results might be wrong!
 
   session_key_establish (exists-trace): verified (28 steps)
   Session_Key_Secrecy_PFS (all-traces): falsified - found trace (14 steps)

diff --git a/case-studies-regression/ake/bilinear/Joux_analyzed.spthy b/case-studies-regression/ake/bilinear/Joux_analyzed.spthy
@@ -11,6 +11,8 @@ equations:
 
 
 
+
+
 section{* The Joux Protocol using Signatures*}
 
 
@@ -1047,14 +1049,34 @@ solve( SessionKey( A, (B+C), sessKey ) @ #i )
   qed
 qed
 
-/* All wellformedness checks were successful. */
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+/*
+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:
+  Proto2
+Failed to derive Variable(s): ltkB, ltkC
+*/
 
 /*
 Generated from:
 Tamarin version 1.7.1
 Maude version 3.2.1
-Git revision: 334a0df7d8ae5ec03764051e4e8eef985c6a4080, branch: develop
-Compiled at: 2023-01-27 13:01:52.341920052 UTC
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
 */
 
 end
@@ -1069,7 +1091,10 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Joux.spthy
 
   output:          examples/ake/bilinear/Joux.spthy.tmp
-  processing time: 13.61s
+  processing time: 8.30s
+
+  WARNING: 1 wellformedness check failed!
+           The analysis results might be wrong!
 
   session_key_establish (exists-trace): verified (28 steps)
   Session_Key_Secrecy_PFS (all-traces): verified (22 steps)

diff --git a/case-studies-regression/ake/bilinear/RYY_PFS_analyzed.spthy b/case-studies-regression/ake/bilinear/RYY_PFS_analyzed.spthy
@@ -10,6 +10,8 @@ equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
 
 
+
+
 section{* RYY : UM-like identity based key exchange protocol *}
 
 rule (modulo E) KGC_Setup:
@@ -412,14 +414,20 @@ qed
 
 
 
+
+
+
+
+
+
 /* All wellformedness checks were successful. */
 
 /*
 Generated from:
 Tamarin version 1.7.1
 Maude version 3.2.1
-Git revision: 334a0df7d8ae5ec03764051e4e8eef985c6a4080, branch: develop
-Compiled at: 2023-01-27 13:01:52.341920052 UTC
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
 */
 
 end
@@ -434,7 +442,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/RYY_PFS.spthy
 
   output:          examples/ake/bilinear/RYY_PFS.spthy.tmp
-  processing time: 5.50s
+  processing time: 3.12s
 
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_PFS (all-traces): falsified - found trace (12 steps)

diff --git a/case-studies-regression/ake/bilinear/RYY_analyzed.spthy b/case-studies-regression/ake/bilinear/RYY_analyzed.spthy
@@ -10,6 +10,8 @@ equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
 
 
+
+
 section{* RYY : UM-like identity based key exchange protocol *}
 
 rule (modulo E) KGC_Setup:
@@ -542,14 +544,20 @@ qed
 
 
 
+
+
+
+
+
+
 /* All wellformedness checks were successful. */
 
 /*
 Generated from:
 Tamarin version 1.7.1
 Maude version 3.2.1
-Git revision: 334a0df7d8ae5ec03764051e4e8eef985c6a4080, branch: develop
-Compiled at: 2023-01-27 13:01:52.341920052 UTC
+Git revision: 4b299c253445d7bbc7fce41abf0b0d5659bb1d58, branch: develop
+Compiled at: 2023-06-26 11:54:20.223793825 UTC
 */
 
 end
@@ -564,7 +572,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/RYY.spthy
 
   output:          examples/ake/bilinear/RYY.spthy.tmp
-  processing time: 5.89s
+  processing time: 3.01s
 
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_WPFS (all-traces): verified (53 steps)