Merge pull request tamarin-prover#461 from charlie-j/feature-proverif…

…-output

SAPIC major update

.dockerignore

@@ -2,4 +2,3 @@
 .stack-work
 .worktree
 lib/*/.stack-work
-examples

.gitignore

@@ -43,3 +43,7 @@ stack.yaml.lock
 *.iml
 .idea/
 out/
+
+*.pv
+
+.worktree

case-studies-regression/Tutorial_analyzed.spthy

@@ -2,7 +2,8 @@ theory Tutorial begin
 
 // Function signature and definition of the equational theory E
 
-functions: adec/2, aenc/2, fst/1, h/1, pair/2, pk/1, snd/1
+functions: adec/2, aenc/2, fst/1[destructor], h/1, pair/2, pk/1,
+           snd/1[destructor]
 equations:
     adec(aenc(m, pk(k)), k) = m,
     fst(<x.1, x.2>) = x.1,
@@ -222,6 +223,14 @@ solve( Client_1( S, k ) ▶₀ #i )
   qed
 qed
 
+
+
+
+
+
+
+
+
 /* All well-formedness checks were successful. */
 
 end
@@ -237,7 +246,7 @@ analyzing: examples/Tutorial.spthy
 analyzed: examples/Tutorial.spthy
 
   output:          examples/Tutorial.spthy.tmp
-  processing time: 0.186242502s
+  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)
@@ -251,7 +260,7 @@ summary of summaries:
 analyzed: examples/Tutorial.spthy
 
   output:          examples/Tutorial.spthy.tmp
-  processing time: 0.186242502s
+  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)

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

@@ -3,11 +3,13 @@ theory Chen_Kudla begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing
-functions: fst/1, h/1, hp/1, kdf/1, pair/2, snd/1
+functions: fst/1[destructor], h/1, hp/1, kdf/1, pair/2, snd/1[destructor]
 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 *}
 
@@ -2574,6 +2576,12 @@ next
   qed
 qed
 
+
+
+
+
+
+
 /* All well-formedness checks were successful. */
 
 end
@@ -2589,7 +2597,7 @@ analyzing: examples/ake/bilinear/Chen_Kudla.spthy
 analyzed: examples/ake/bilinear/Chen_Kudla.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla.spthy.tmp
-  processing time: 57.029003883s
+  processing time: 88.051054428s
   key_agreement_reachable (exists-trace): verified (13 steps)
   key_secrecy_ephemeral_no_WPFS (all-traces): verified (679 steps)
 
@@ -2601,7 +2609,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Chen_Kudla.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla.spthy.tmp
-  processing time: 57.029003883s
+  processing time: 88.051054428s
   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,11 +3,13 @@ theory Chen_Kudla begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing
-functions: fst/1, h/1, hp/1, kdf/1, pair/2, snd/1
+functions: fst/1[destructor], h/1, hp/1, kdf/1, pair/2, snd/1[destructor]
 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 *}
 
@@ -503,6 +505,12 @@ solve( (∃ matching #i3 #i4 sid.
   qed
 qed
 
+
+
+
+
+
+
 /* All well-formedness checks were successful. */
 
 end
@@ -518,7 +526,7 @@ 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: 45.789046796s
+  processing time: 55.372479208s
   key_secrecy_eCK_like (all-traces): falsified - found trace (24 steps)
 
 ------------------------------------------------------------------------------
@@ -529,7 +537,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Chen_Kudla_eCK.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla_eCK.spthy.tmp
-  processing time: 45.789046796s
+  processing time: 55.372479208s
   key_secrecy_eCK_like (all-traces): falsified - found trace (24 steps)
 
 ==============================================================================

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

@@ -3,7 +3,8 @@ theory Joux_EphkRev begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing, multiset
-functions: fst/1, pair/2, pk/1, sign/2, snd/1, true/0, verify/3
+functions: fst/1[destructor], pair/2, pk/1, sign/2, snd/1[destructor],
+           true/0, verify/3[destructor]
 equations:
     fst(<x.1, x.2>) = x.1,
     snd(<x.1, x.2>) = x.2,
@@ -13,6 +14,12 @@ equations:
 
 section{* The Joux Protocol using Signatures*}
 
+
+
+
+
+
+
 rule (modulo E) Register_pk:
    [ Fr( ~ltk ) ]
   -->
@@ -1040,7 +1047,7 @@ analyzing: examples/ake/bilinear/Joux_EphkRev.spthy
 analyzed: examples/ake/bilinear/Joux_EphkRev.spthy
 
   output:          examples/ake/bilinear/Joux_EphkRev.spthy.tmp
-  processing time: 24.81967429s
+  processing time: 28.081048642s
   session_key_establish (exists-trace): verified (28 steps)
   Session_Key_Secrecy_PFS (all-traces): falsified - found trace (14 steps)
 
@@ -1052,7 +1059,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Joux_EphkRev.spthy
 
   output:          examples/ake/bilinear/Joux_EphkRev.spthy.tmp
-  processing time: 24.81967429s
+  processing time: 28.081048642s
   session_key_establish (exists-trace): verified (28 steps)
   Session_Key_Secrecy_PFS (all-traces): falsified - found trace (14 steps)
 

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

@@ -3,7 +3,8 @@ theory Joux begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing, multiset
-functions: fst/1, pair/2, pk/1, sign/2, snd/1, true/0, verify/3
+functions: fst/1[destructor], pair/2, pk/1, sign/2, snd/1[destructor],
+           true/0, verify/3[destructor]
 equations:
     fst(<x.1, x.2>) = x.1,
     snd(<x.1, x.2>) = x.2,
@@ -13,6 +14,12 @@ equations:
 
 section{* The Joux Protocol using Signatures*}
 
+
+
+
+
+
+
 rule (modulo E) Register_pk:
    [ Fr( ~ltk ) ]
   -->
@@ -1056,7 +1063,7 @@ analyzing: examples/ake/bilinear/Joux.spthy
 analyzed: examples/ake/bilinear/Joux.spthy
 
   output:          examples/ake/bilinear/Joux.spthy.tmp
-  processing time: 21.737366785s
+  processing time: 23.775688128s
   session_key_establish (exists-trace): verified (28 steps)
   Session_Key_Secrecy_PFS (all-traces): verified (22 steps)
 
@@ -1068,7 +1075,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Joux.spthy
 
   output:          examples/ake/bilinear/Joux.spthy.tmp
-  processing time: 21.737366785s
+  processing time: 23.775688128s
   session_key_establish (exists-trace): verified (28 steps)
   Session_Key_Secrecy_PFS (all-traces): verified (22 steps)
 

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

@@ -3,11 +3,13 @@ theory RYY begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing
-functions: fst/1, hp/1, kdf/1, pair/2, snd/1
+functions: fst/1[destructor], hp/1, kdf/1, pair/2, snd/1[destructor]
 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:
@@ -382,6 +384,10 @@ solve( (∃ matching #i3 role2.
   qed
 qed
 
+
+
+
+
 /* All well-formedness checks were successful. */
 
 end
@@ -397,7 +403,7 @@ analyzing: examples/ake/bilinear/RYY_PFS.spthy
 analyzed: examples/ake/bilinear/RYY_PFS.spthy
 
   output:          examples/ake/bilinear/RYY_PFS.spthy.tmp
-  processing time: 7.876468162s
+  processing time: 8.291041154s
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_PFS (all-traces): falsified - found trace (12 steps)
 
@@ -409,7 +415,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/RYY_PFS.spthy
 
   output:          examples/ake/bilinear/RYY_PFS.spthy.tmp
-  processing time: 7.876468162s
+  processing time: 8.291041154s
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_PFS (all-traces): falsified - found trace (12 steps)
 

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

@@ -3,11 +3,13 @@ theory RYY begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing
-functions: fst/1, hp/1, kdf/1, pair/2, snd/1
+functions: fst/1[destructor], hp/1, kdf/1, pair/2, snd/1[destructor]
 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:
@@ -512,6 +514,10 @@ next
   qed
 qed
 
+
+
+
+
 /* All well-formedness checks were successful. */
 
 end
@@ -527,7 +533,7 @@ analyzing: examples/ake/bilinear/RYY.spthy
 analyzed: examples/ake/bilinear/RYY.spthy
 
   output:          examples/ake/bilinear/RYY.spthy.tmp
-  processing time: 7.735757739s
+  processing time: 7.663440743s
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_WPFS (all-traces): verified (53 steps)
 
@@ -539,7 +545,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/RYY.spthy
 
   output:          examples/ake/bilinear/RYY.spthy.tmp
-  processing time: 7.735757739s
+  processing time: 7.663440743s
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_WPFS (all-traces): verified (53 steps)
 

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

@@ -3,11 +3,13 @@ theory Scott begin
 // Function signature and definition of the equational theory E
 
 builtins: diffie-hellman, bilinear-pairing
-functions: fst/1, hp/1, kdf/1, pair/2, snd/1
+functions: fst/1[destructor], hp/1, kdf/1, pair/2, snd/1[destructor]
 equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
 
 
 
+
+
 section{* Scott: MTI-C0 like identity based key exchange protocol *}
 
 rule (modulo E) KGC_Setup:
@@ -292,6 +294,10 @@ solve( (∃ matching #i3 #i4 sid.
   qed
 qed
 
+
+
+
+
 /* All well-formedness checks were successful. */
 
 end
@@ -307,7 +313,7 @@ analyzing: examples/ake/bilinear/Scott_EphkRev.spthy
 analyzed: examples/ake/bilinear/Scott_EphkRev.spthy
 
   output:          examples/ake/bilinear/Scott_EphkRev.spthy.tmp
-  processing time: 23.640088606s
+  processing time: 26.475782942s
   key_agreement_reachable (exists-trace): verified (12 steps)
   key_secrecy (all-traces): falsified - found trace (15 steps)
 
@@ -319,7 +325,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Scott_EphkRev.spthy
 
   output:          examples/ake/bilinear/Scott_EphkRev.spthy.tmp
-  processing time: 23.640088606s
+  processing time: 26.475782942s
   key_agreement_reachable (exists-trace): verified (12 steps)
   key_secrecy (all-traces): falsified - found trace (15 steps)