cpsa-3.6.4: NEWS

CPSA NEWS

  October 2019:

* Release 3.6.4 adds support for the latest version of the GHC
  compiler.  As of version 8.8, the Monad type class no longer
  contains the fail method, and that method is now provided by the
  MonadFail type class.  This version of CPSA makes use of the C
  preprocessor to handle this incompatible change.  The release also
  fixes a bug in thinning.

  August 2019:

* Release 3.6.3 adds the cpsainit program and fixes bugs.  The
  cpsainit program copies files from the CPSA data directory into a
  fresh CPSA project directory.  The files ease the task of automating
  the use of the various CPSA tools.

  March, 2019:

* Release 3.6.2 adds the leads-to predicate to the rule language, adds
  better checks for malformed input, and fixes a bug so that now the
  default depth is infinite as is specified in the manual.  It adds
  structured annotations to skeleton output to facilitate post
  processing programs besides cpsagraph.  The sources for OCaml
  programs for processing CPSA input and output are now included.

  August, 2018:

* Release 3.6.1 is a bug fix release.  It includes updates to the CPSA
  manual.  There are no user visible changes.

  June, 2018:

* Release 3.6.0 adds rules and facts.  Rules are associated with
  protocols, and facts are associated with skeletons.  A rule is a
  geometric formula that is used as a rewrite rule, and a fact is a
  named relation between values.

  April, 2018:

* The release of CPSA version 3.5.0 contains one user visiable change.
  The names of the exponent sorts have been changed.  Sort expn is now
  rndx, and expr is now expt.  The change was made because people
  found the old sort name confusing.  For compatibility, the reader
  accepts the old names and translates them into the new ones.

  December, 2017:

* The release of CPSA version 3.4.1 includes the following changes:
  - Fixed a bug that caused a crash in certain situations involving
    generalization
  - Fixed a bug in the chase algorithm that caused the tool to enter
    an infinite loop
  - Added a new declaration "eq" which declares pairs of values to be
    equal to each other.
  - Added a new command-line flag to skip analysis, "noanalyze" / -z.
    This allows defgoal inputs to be read in and characteristic
    skeletons computed, for model debugging.

  September, 2017:

* In CPSA version 3.4, the algorithm for handling Diffie-Hellman
  components in protocols has been substantially altered.  Instead of
  considering "relevant" version of the critical message when it is a
  Diffie-Hellman value, we focus on the exact critical message, but
  add a cohort member for exploring "precursors" of the critical
  message.  The new algorithm no longer requires that exponents always
  be found within an exponentiation.

* Several examples added to the example distribution, including
  "iadh_um", which makes use of the relaxation of requirements on
  Diffie-Hellman exponents to explore forward secrecy.

* A number of serious bug fixes are included in release version 3.4.
  Bugs fixed include:
  - A bug that caused the tool to discard some skeletons incorrectly
    due to over-agressive thinning
  - A bug in Diffie-Hellman matching that caused an infinite loop in
    certain cases
  - A bug that caused inputs with bltk to refuse to execute
  - Bugs in the solved filter that allowed a skeleton to have itself as a child
  - A bug in isomorphism checking that incorrectly identified certain
    Diffie-Hellman skeletons as non-isomorphic.

* Backward compatibility note: "ind-zero-in", a declaration
  automatically added to Diffie-Hellman protocols in the previous
  version, has been renamed to "absent".

  June, 2016:

* New feature: tag sort.  Introduced a new sort "tag" in both the basic and
  diffie-hellman algebras.  Quoted string constants are now considered to be
  of this sort rather than of least sort mesg.  This allows a user to specify
  a variable that may stand for a string constant, without forcing the user to
  use a variable of the mesg sort for that purpose.

* New feature: depth limit.  When a depth limit is specified, analysis of
  skeletons will proceed as long as the skeleton's depth in the search tree
  is below the limit.  Skeletons not analyzed are marked as "(fringe)" to
  indicate the incomplete nature of those branches of the analysis.  Unlike
  hitting a strand bound, the tool does not exit with an error when the depth
  limit is reached.

* IKE_variants.tar.gz added: This is an archive of over 30 variants of
  IKEv1 and IKEv2 protocols modeled in CPSA.  The archive can be found in the
  doc/examples directory.

  February, 2016: CPSA version 3 released to the public.

Version 3 of CPSA is a major update to the tool including many new features.
The most important new features included are:

* Working support for Diffie-Hellman components in protocols, with two
  main restrictions: first, exponent multiplication is modeled but
  exponent addition is not, and second, that "bare" exponents are not
  allowed.  This means that exponents in a role or skeleton must be
  found within an exponentiation, and not directly (e.g. as in a pair
  or encryption).

* Support for protocols that interact with long-term state

* Bidirectional long-term keys, in which the order of the two names is
  ignored.  This more appropriately models shared symmetric keys in a
  setting where participants are not clearly distinguishable as
  clients or servers.

* Numerous declarable constraints that allow a user to more carefully
  limit the tool's search to executions of interest.  Including:
  - inequality of values
  - functional relationships between values
  - a new type of secrecy assumption for potentially leakable long-term secrets

* New, improved documentation.  Included with the release is the CPSA
  manual which thoroughly documents the new and existing features of
  the tool and is also a good starting place for new users.