Release commit:

* version number to 1.6.0 * updated CHANGE log Note that some csf18-xor case studies take significantly longer due to a bugfix; this is known and acceptable. One example in csf12 already did not run in 1.4.1 and is renamed so it does not get run again when producing releases.
tamarin-prover · Sep 9, 2020 · a631d75 · a631d75
1 parent 1056393
commit a631d75
Show file tree

Hide file tree

Showing 10 changed files with 30 additions and 15 deletions.
diff --git a/CHANGES b/CHANGES
@@ -1,12 +1,26 @@
-* current develop
+* 1.6.0
+  - SAPIC integration
+
+  - New feature: auto sources - compute sources lemmas automatically
+
+  - New feature: predicate support
+
   - Observational equivalence concludes with attack more quickly, without requiring instantiation to public values for free variables.
 
   - Add a true (sequential) depth-first search (DFS) option: --stop-on-trace=seqdfs
 
-  - SAPIC bug fix
-
   - nixOS development simplification
 
+  - Allow Maude 3.0.0 (in addition to 2.7.1)
+
+  - Change: --prove=name only verifies lemma named 'name', to prove all lemmas with the prefix 'name' use --prove=name* instead; adjusted existing examples
+
+  - Numerous bug fixes
+
+  - Multiple new case studies
+
+  - Using stack LTS resolver 16.12 and GHC 8.8.4 now [stack update, stack upgrade needed]
+
 * 1.4.1
   - Variants are now computed in Maude, for a pre-computation speedup for theories with many variants. Old internal variant computation still accessible by setting the environment variable "TAMARIN_NO_MAUDE_VARIANTS".
 

diff --git a/Makefile b/Makefile
@@ -50,7 +50,7 @@ clean:	tamarin-clean sapic-clean
 # It is by no means official in any form and should be IGNORED :-)
 # ###########################################################################
 
-VERSION=1.5.1
+VERSION=1.6.0
 
 ###############################################################################
 ## Case Studies

diff --git a/examples/csf12/SignedDH_eCK.spthy → examples/csf12/SignedDH_eCK.spthy_nontermOOM b/examples/csf12/SignedDH_eCK.spthy → examples/csf12/SignedDH_eCK.spthy_nontermOOM
diff --git a/lib/sapic/tamarin-prover-sapic.cabal b/lib/sapic/tamarin-prover-sapic.cabal
@@ -2,7 +2,7 @@ name:               tamarin-prover-sapic
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            1.5.1
+version:            1.6.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers

diff --git a/lib/term/tamarin-prover-term.cabal b/lib/term/tamarin-prover-term.cabal
@@ -2,7 +2,7 @@ name:               tamarin-prover-term
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            1.5.1
+version:            1.6.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers

diff --git a/lib/theory/tamarin-prover-theory.cabal b/lib/theory/tamarin-prover-theory.cabal
@@ -2,7 +2,7 @@ name:               tamarin-prover-theory
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            1.5.1
+version:            1.6.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers

diff --git a/lib/utils/tamarin-prover-utils.cabal b/lib/utils/tamarin-prover-utils.cabal
@@ -2,7 +2,7 @@ name:               tamarin-prover-utils
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            1.5.1
+version:            1.6.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers

diff --git a/src/Main/Console.hs b/src/Main/Console.hs
@@ -78,7 +78,7 @@ versionStr = unlines
     [ programName
     , " "
     , showVersion version
-    , ", (C) David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt, ETH Zurich 2010-2019"
+    , ", (C) David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt, ETH Zurich 2010-2020"
     ]
   , concat
     [ "Git revision: "

diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal
@@ -1,7 +1,7 @@
 cabal-version:      >= 1.10
 build-type:         Simple
 name:               tamarin-prover
-version:            1.5.1
+version:            1.6.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -12,7 +12,7 @@ author:             Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>,
 maintainer:         Simon Meier <simon.meier@inf.ethz.ch>,
                     Jannik Dreier <research@jannikdreier.net>,
                     Ralf Sasse <ralf.sasse@gmail.com>
-copyright:          Benedikt Schmidt, Simon Meier, Jannik Dreier, Ralf Sasse, ETH Zurich, 2010-2018
+copyright:          Benedikt Schmidt, Simon Meier, Jannik Dreier, Ralf Sasse, ETH Zurich, 2010-2020
 synopsis:           The Tamarin prover for security protocol analysis.
 description:
 
@@ -158,10 +158,10 @@ executable tamarin-prover
       , yesod-core
       , yesod-static
 
-      , tamarin-prover-utils  == 1.5.1
-      , tamarin-prover-term   == 1.5.1
-      , tamarin-prover-theory == 1.5.1
-      , tamarin-prover-sapic == 1.5.1
+      , tamarin-prover-utils  == 1.6.0
+      , tamarin-prover-term   == 1.6.0
+      , tamarin-prover-theory == 1.6.0
+      , tamarin-prover-sapic == 1.6.0
 
     other-modules:
       Paths_tamarin_prover

diff --git a/version-change.sh b/version-change.sh
@@ -9,3 +9,4 @@ tamarin-prover.cabal \
 lib/term/tamarin-prover-term.cabal \
 lib/theory/tamarin-prover-theory.cabal \
 lib/utils/tamarin-prover-utils.cabal \
+lib/sapic/tamarin-prover-sapic.cabal \