cpsa-3.6.11: NEWS

CPSA NEWS

  June 2022:

* Release 3.6.11 removes extra quotes in some error messages.

  March 2022:

* Release 3.6.10 allows double quote and backslash in S-expressions so
  that they can contain Windows file names.

  January 2022:

* Release 3.6.9 expunges skeletons that have a value that is both uniq
  orig and uniq gen, and start on different strands.

  November 2021:

* Release 3.6.8 adds a stronger method for solving Diffie-Hellman
  authentication tests for the case in which the test is a base value
  of a special form.  The form is (exp (gen) (mul ...)), where all of
  the variables in the exponent are random exponents and there is more
  than one variable in the exponent.  In this case, it adds a listener
  for each variable in the exponent.  The messages listened to is the
  concatenation of the variable and the base value after the factor
  that involves the variable has been removed.  Thus for (exp (gen)
  (mul x y y)), a listener is created for (cat (exp (gen) (mul y y) x)
  and (cat (exp (gen) x) y).

  May 2020:

* Release 3.6.6 adds a powerful feature: the cpsaprot preprocessing
  tool.  This allows you to specify protocols in cpsa via a more
  intuitive "Alice and Bob" notation where you specify messages being
  sent from one role to another.  The cpsaprot tool builds the
  standard defprotocol from this specification, which can then be run
  through the main CPSA tool.  This helps to reduce duplications in
  the input files actually created by humans and thus reduces the
  occurrence of accidental errors in input.

  November 2019:

* Release 3.6.5 is a bug fix release.  There are no user visible
  changes.

  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.