cpsa-3.4.0: NEWS

CPSA NEWS

  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.