cpsa-3.3.0: NEWS

CPSA NEWS

  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.