CPSA NEWS -- history of user-visible changes.

* Changes in version 2.1.0

** Initial comments displayed
The graph program displays the initial comments in an input file.

** New command line options
Four new command line options have been added:

   -d         --displacement     enable displacement
   -c         --check-nonces     check nonces first
   -t         --try-old-strands  try old strands first
   -r         --reverse-nodes    try old nodes first

In rare cases, the use of one of these options may allow normal
termination in a case in which CPSA aborts otherwise.

** GHC 6.8 no longer supported
Use GHC 6.10 or greater.

** Bugs fixes
Some minor bugs were fixed that mostly effect artificially generated
protocols.

* Changes in version 2.0.5

** Performance enhanced
A source of duplicated effort was removed that reduces the run time
for analyzing the NSL5 protocol from about a day to about a minute!
The enhancement doesn't seem to effect the run times of many other
protocols.

** Bugs fixes
Some minor bugs were fixed, and there are now no tests in the test
suite that shows that CPSA fails to find a shape in should.

** CPSA theory document added
A document on authentication tests has been added.  The document is
not installed are the CPSA Specification and the CPSA Design documents.
The sources for the document are provided, and must be built by typing
make in the doc directory.

* Changes in version 2.0.4

** Input skeletons are no longer pruned

** Bug in the acyclic graph checker fixed
In rare cases, the buggy checker allowed skeletons with circular
node orderings.

* Changes in version 2.0.3

** Generalization bug fixed
A bug associated with origination assumption forgetting has been
fixed.

** SWI Prolog tools added
Tools that allows CPSA to be manipulated in Prolog are in the src
directory.  The tools include a pretty printer that uses the same
algorithm as is used in the Haskell pretty printer.

** Cabal description improved
An expanded description of CPSA has been added to its cabal file.

* Changes in version 2.0.2

** Better message terms in graphs
CPSA graph now uses the information in the traces comment when it's
available when printing message terms.

* Changes in version 2.0.1

** Inherited unique origination bug fixed
Added check that unique origination position is preserved by
inheritance.

** Variable printing improved
Improved renaming algorithm used to avoid collisions while printing
variables.

* Changes in version 2.0.0

** CPSA is an open source package

** Better support for Diffie-Hellman
Makefiles use the *.sch the extension for problems that use
Diffie-Hellman.


* Changes in version 1.5.5

** Encryption tests solved before nonce tests
CPSA now solves encryption tests before it tries nonce tests.
Experiments have show this heuristic can lead to substantially smaller
derivation trees in some cases, but in a few cases, derivation trees
are slightly larger.

** Better error messages for ill-formed roles and preskeletons
CPSA generates a more informative message when a role or a preskeleton
is not well-formed.

* Changes in version 1.5.4

** Pruning bug fixed
A check that origination assumptions are honored by the homomorphisms
associated with pruning was added.  As a result, cases in which
erroneous pruning was performed have been eliminated.

** Comments in skeletons are preserved
The comment field in a skeleton given as input is included when it is
printed.

* Changes in version 1.5.3

** Skeleton diagrams improved
In a skeleton diagram, an edge between nodes that do not agree on
their message is displayed with a dashed line.

** Less general skeletons removed from cohort
During contraction and regular augmentation, some skeletons that are
less general than others are removed from consideration.  These
skeletons contribute nothing new.

* Changes in version 1.5.2

** Pruning bug fixed
Added the requirement to pruning that ordering relations associated
with the more general (pruned) strand are implied by the less general
strand.

** Role non-orig length specification added
Added support for delaying the inheritance of a role non-origination
assumption by adding a length specification to role non-origination
declarations.  The non-orig assumption is inherited when the strand
meets the length requirement.

* Changes in version 1.5.1

** Generalization bug fixed
CPSA no longer prunes while generalizing.

** Change license to BSD

* Changes in version 1.5.0

** Diffie-Hellman algebra added
This is an early access release of the Diffie-Hellman algebra.  Its
signature is described in the CPSA User Guide.  It has only been
tested on the example in tst/dh.lisp, and the output seems reasonable.

** Keyword defpreskeleton changed to defskeleton
Most often, the defpreskeleton form described a skeleton.  To reduce
confusion, form has been renamed.  The CPSA program still accepts the
old keyword.  A script that updates the keyword is in src/preskel.sh.

* Changes in version 1.4.9
This version is a bug fix and speed enhancement fix only.

** Obscure display bug fixed

** Role origination check bug fixed
The origination check is now omitted when the inheriting strand is too
short to inherit a unique origination assumption.

** Role origination check bug fixed

** Outer most encryptions preferred for encryption tests
When choosing among encryptions for critical messages, CPSA prefers
outer most encryptions over ones within another encryption. 

* Changes in version 1.4.8

** Support for key usage added
A name may be associated with more than one asymmetric key using the
binary form of pubk, where the first argument is a quoted constant.
For example, (pubk "sig" a) and (pubk "enc" a) can be used to describe
name a's public signature and encryption key.

** Progressive refinement technique described
The advice section of the CPSA Primer describes the progressive
refinement technique.

* Changes in version 1.4.7

** Unused role variables are silently ignored
Unused role variables used to cause an error.  This behavior
interfered with the practice of submitting output as input with small
modifications.

** Isomorphism check performance improved

** Added an overview section to the CPSA Specification

* Changes in version 1.4.6

** Added no isomorphism checking mode (--noisochk)
In noisochk mode, isomorphism checks are avoided by not identifying
duplicate skeletons and by not generalizing realized skeletons.
Isomorphism checks between two skeletons with a large number of
strands can take a long time, so for some problems, CPSA runs faster
in this mode.  Warning, in this mode, CPSA reports that each realized
skeleton is a shape even when it is not one.  In this way, the
cpsashapes program can be used to extract the realized skeletons from
the run.

** Added LaTeX output mode to cpsagraph
The cpsagraph program generates LaTeX source that places S-expressions
in verbatim environments and generates XY-pic diagrams of skeletons.
The XHTML output should always be preferred, however, LaTeX output is
useful when generating a report or a briefing on the results of using
CPSA.

** CPSA Primer updated
The example output has been updated to reflect recent changes,
numerous editorial improvements were made, and the advice section
has been augmented with some recently learned tricks.

** CPSA algorithm specified
At last.  The CPSA Specification contains a specification of all of
the parts of the CPSA algorithm.  In particular, a description of
the augmentation algorithm is in writing.

** CPSA Design rewritten
Most of the material that was once duplicated in both The CPSA
Specification and The CPSA Design has been purged from the design
document.  The document now assumes its reader have already read The
CPSA Specification.  As a result, it focuses solely on implementation
issues, and leaves correctness issues to the specification.

** Aborted output is no longer generalized
CPSA will abort when a strand bound or a step count is exceeded.
Since generalization involves isomorphism checks, the old abort
implementation could take a very long time to finish.

* Changes in version 1.4.5

** CPSA macros expanded by cpsa program
CPSA now expands macros rather than using a preprocessor for the task.
The cpsapp program now just pretty prints its input.

** Memory leak fixed
Permutations no longer memoized--can cause excessive use of memory.

** In rely/guarantee formulas, "t" and "f" are no longer keywords
Use (and) for truth and (or) for falsehood.

* Changes in version 1.4.4
This is a correctness critical update to CPSA.

** Shape search design error fixed.
The shape search algorithm includes a new shape collapsing operation
that allows CPSA to find shapes it used to miss.  The operation
includes the symbol "collapsed" followed by the two strands that were
merged.  The Otway-Rees example in tst/or.scm makes use of the new
operation.

** Pruning bug fixed.
The pruning operation now uses a substitution that is idempotent for
strands other than the pruned strand.

** Specification document added.
The sources to the CPSA document that specifies CPSA as a reduction
system are now included and can be used to build doc/cpsaspec.pdf.

** S-expression reader bug fixed.
The S-expression reader now reads much larger input files.  This means
cpsashapes can be used on larger files.

** Multiprocessor enabled CPSA built by default.
See the README for instructions on how to build CPSA when the parallel
libraries are missing.

* Changes in version 1.4.3

** Improved performance due to better substitution data structure.

** Corrected a bug in substitution associated with variables of sort mesg.
The fix changes the output for tst/dy.scm.

** Corrected a bug in substitution composition
The fix changes the output for tst/dy.scm.

** Corrected a bug that caused some valid generalizations to be rejected.

** Sort "term" is no longer a synonym for "mesg".

* Changes in version 1.4.2

** Fixed a contraction and an augmentation bug.

** The protocol specification checker cpsaparameters added.
The cpsaparameters program detects some specification errors by
performing a base term usage analysis.

** Parallel search available on SMPs.
Semi-explicit parallelism annotations were added to the CPSA search
routine.  Enable with -fpar during configuration.

** Pretty printer changed.
All lists in a defrole and a defpreskeleton are now broken whenever
one of them is.

** Preskeletons	with no strands are detected, and an error is signaled.

* Changes in version 1.4.1

** The macro preprocessor cpsapp added.
The preprocessor was added to ease the task of specifying protocols
with reoccurring message patterns. It can also be used to pretty print
cpsa input.

** Base terms allowed as principals in annotations.
Base terms as principals are now allowed so as to allow keys as
principals.

** Cohort filtering added.
The cohort is now filtered so that every member is solved.  The
filtering removes dead ends earlier in the computation.

** Fixed a minimization bug.
When separating a uniquely originating base term, either the term or
its clone is uniquely originating.

* Changes in version 1.4.0

** Variable declaration syntax changed.
More than one variable can be declared to be of a given sort in a
single declaration form.

** New sort added.
The sort data was added, a sort that is similar to sort text.  The new
sort can be used to partition nonce-like data from ordinary text-like
data.  See tst/epmo.scm for an example of its use.

** Sort symbol changed.
The symbol used for the top sort has been changed from term to mesg.

** Default output format for cpsagraph changed.
The default output format for cpsagraph is now the expanded format.

* Changes in version 1.3.2
This is a bug fix only release.

** Fixed a minimization bug.
Use the transitive closure of the communication ordering before
deleting a node.

** Added new well-formed preskeleton check.
Every uniquely originating role term mapped by in instance must be
mapped to a term that originates on the instance's strand.

* Changes in version 1.3.1
This is a bug fix only release.

** Bad listener augmentation bug fixed.
Listeners are now added only for the decryption keys of the top most
encryptions in the escape set.  This fixes a bug reported by Eric Bush.

* Changes in version 1.3.0
This release changes the external syntax and fixes bugs.

** Encryption syntax simplified.
To reduce clutter, when enc has more that two terms, a concatenation
is added to all but the last term.

** New name for document.
The CPSA Tutorial was renamed to the CPSA Primer.

** The cpsaannotations program has documentation.
Preliminary documentation is in the CPSA User Guide.

** A make system for Windows was added.
The file doc/Make.hs allows the use of Windows without Cygwin or MinGW.

** A strand augmentation bug was fixed.
This change allows CPSA to find the flaw in the Dolev-Yao Example 1.3
test case.

** Assumption forgetting works again.
This is a fix to a bug that was introduced in the previous release.

** Isomorphism bug fixed.
A strand permutation map was applied to the wrong ordering.

* Changes in version 1.2.3
This is a bug fix only release.

** Illegal comments no longer generated.
The comment generated for non-default strand bounded or step count
limited runs contained an illegal character that has been removed.
As a result, the graphing programs work again.

** A substitution printing failure has been fix.

** The augmentation bug fix in 1.2.2 had a problem that is now fixed.

** Role variables in protocols are printing in the order they were read.
In previous version, role variables were printed in reverse order.

** Better title generated for the expanded view.
The name of the first protocol is included in the title of the
generated XML document.

** Testing showed enabling multiprocess support gives no speedup. 

* Changes in version 1.2.2

** This release fixes a bug.
During augmentation, previously, when a role was searched for a
transforming edge, only the shortest instance was returned as a
candidate for augmentation.  Now all instances are returned.

** Multiprocessor support is available.
The README describes how to enable multiprocessor support.  This
feature is untested.

** Partial support for Rely-Guarantee annotations has been added.
The cpsaannotations program annotates shapes when given an annotated
protocol.  The is no documentation yet, but you can test it with:
$ (cd tst; make epmo-accounts-nums_annotations.xml)

* Changes in version 1.2.1

** This is a bug fix release. There are no user-visible changes.

* Changes in version 1.2.0

** Tags are now non-atomic terms in the Basic Crypto Algebra.

** The expanded view (-x) option is available as an output for cpsagraph.

** Support for local installation was added.

** A standard set of GNU Make rules was added.

** Comments as S-expressions may appear at the file level of input.

** The program cpsabasic was renamed to cpsa.

** The --bound option to cpsa limits the number of strands in a skeleton.

** The current shape search is known to be not complete. See tst/dy.scm.

* Changes in version 1.1.0

** Support for indeterminates was added to the Basic Crypto Algebra.
Variables of sort term, also called indeterminates, are now available
in the Basic Crypto Algebra.

** The CPSA Tutorial was added.

* Initial version released as version 1.0.0

Local variables:
mode:outline
End: