Changelog of @hackage/cpsa 3.6.6

2020-05-21 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Tagged as 3.6.6

2020-05-15 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (rlugen): Replaced an incorrect call to
originationNodes to be a call to generationNodes.  This fixes a
bug when using the ugen predicate in the conclusion of a rule.

2020-05-15 Moses D. Liskov mliskov@mitre.org

* src/CPSA/Lib/Strand.hs (preskelWellFormed): Added a check that
all variables used in any terms in any declarations are used in
the terms of the traces.
* src/CPSA/Lib/Strand.hs (verbosePreskelWellFormed): Made a similar
change, but without removing existing more specific messages that
may be informative for users.

2020-04-15 Joshua D. Guttman guttman@mitre.org

* src/CPSA/Lib/Strand.hs (graphCloseAll):  Added a procedure to
generate a transitive closure that includes pairs on the same
strand.  Adapted gprec to use it.

2020-04-02 Ian D. Kretz ikretz@mitre.org

* src/CPSA/Latex/Main.hs (main): Remove number from pubk, privk
newcommand

2020-03-31 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs (Preskel): Added support for unique
generation assertions.

2020-03-20 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Update version number as 3.6.6

2020-03-04 Moses D. Liskov mliskov@mitre.org

* src/CPSA/Prot/Main.hs (main): Added support for state to
cpsaprot.

2020-02-27 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (probIsomorphic): Added quick checks for
thinning isomorphism check.

2020-02-20 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Prot/Main.hs (main):  Improved error messages and added
(chmsg TERM) form for channel messages and clone for roles.

2020-02-13 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Prot/Main.hs (main):  Added cpsaprot program.

2020-02-11 Kretz, Ian D ikretz@mitre.org

* src/CPSA/LaTeX/Main.hs (main):  Added cpsa2latex program.

2019-11-26 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/GoalSat/Main.hs: Added cpsagoalsat program.

2019-11-12 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Tagged as 3.6.5

* src/CPSA/Lib/Strand.hs (tryPermProb): Rewrote tryPermProb so
that it uses tryPerm.

2019-11-08 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (tryPermProb):  Added missing invperm to
the third line of tryPermProb, and reenabled multistrand thinning.

2019-10-21 John D. Ramsdell ramsdell@gootoo.mitre.org

* cpsa.cabal (Version): Tagged as 3.6.4

2019-10-21 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Utilities.hs: Used the C preprocessor to allow
compilation using older versions of GHC.

2019-10-15 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Utilities.hs: Updated code to support the removal
of fail from Monad as implemented in base-4.13.0.0.

2019-09-16 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (thinManyStrands):  Replaced isomorphic
check with probIsomorphic check so that strands in the
point-of-view remain unmodified.

2019-08-26 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Tagged as 3.6.3

2019-08-22 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (doRewritesLoop): Fixed the code that
counts rewrite rules applied so it is accurate.  This allows the
rewrite rule limit to be correctly enforced.

2019-08-21 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (runiqAt): Ensured that rewriting with
uniq-at fails when the index is greater than the strand length.

2019-08-19 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Init/Main.hs (main): Added program cpsainit.  The
programs copies the files Makefile, cpsa4.mk, Make4.hs, and
template.lisp from the CPSA data directory to the current
directory, thereby easing the task of starting a CPSA project.

2019-07-15 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/State.hs: Removed the label field in a transition.
The field was always ignored, and it causes confusion on input.

2019-06-26 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (multiset): Used multisets of trace
briefs to reduce the number of full permutation isomorphism
checks.

2019-06-21 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (brief): Added a summary of trace that
reduces the need for matching during isomorphism checking.

2019-06-04 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Reduction.hs (begin): Reversed todo list after
running rules so as to get the output order correct.

2019-05-20 Joshua D. Guttman guttman@mitre.org

* src/CPSA/Lib/Strand.hs (tryPerm): Fixed bug in isomorphism
checking.  Checking of facts used wrong environment.

2019-05-17 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs (leadstoKey):  Added support for leadsto in
shape analysis sentences.

* src/CPSA/Lib/Strand.hs (kfactVars):  Allow message variables in
facts that occur nowhere else.
(useFactVars):  Add flag that disables message variable in facts
that occur nowhere else and disable it, because isomorphism
checking is broken.

* src/CPSA/Strand.hs (doRewriteOne):  Values associated with
existential variables in rules are freshly generated so that
parameter terms can be compound.

2019-04-03 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (verbosePreskelWellFormed): Added a check
that ensures the every variable that occurs in a fact also occurs
in some strand.

2019-03-18 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Tagged as 3.6.2

2019-02-22 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Reduction.hs (addAnnoKey):  Added structured
annotations to skeleton output to facilitate post processing
programs besides cpsagraph.  The new keys are (aborted),
(satisfied-all), and (dead).

2019-02-04 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Reduction.hs (step):  Changed default depth bound
to zero representing no bound and ignored the check when the bound
is not positive.  This matches what is documented in the manual.

2019-01-31 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Loader.hs (badKey): Added checks for bad keys in
alists for skeletons ("defstrand" and "deflistener") and protocols
("defrole" and "defrule").

2018-11-28 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Protocol.hs (AForm):  Added the leads-to predicate
to the goal language.

2018-11-19 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Printer.hs (formula):  Added special pretty
printing rules for formulas in defgoal and defrule.

2018-11-09 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs (loadPOV): Use a preskeleton as a POV
instead of insisting on using a skeleton.

2018-08-29 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Tagged as 3.6.1

2018-08-22 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Strand.hs (doRewrites): Added a limit on the number of
rules that can be applied after solving an authentication test.

2018-08-20 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (cleansPreskel): Cleansed facts from a
skeleton purged of a strand.  This changes fixes a nasty display
bug that occurred when a variable in a fact did not occur in any
strand.

2018-08-06 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Loader.hs (loadConclusion):  Removed mode flag as
this routine should always be using mode RoleSpec.  This resolves
a bug in which CPSA could not load a Shape Analysis Sentence as
rule because equality was before the protocol specific formulas.

* src/CPSA/Lib/Strand.hs (newPreskel):  Changed newPreskel so that
it removed duplicates in the leadsto field when creating a new
preskeleton.  This resolved a bug in which CPSA produced to shapes
that appeared to be isomorphic, but instead, one shape had
duplicates in its leadsto field.

2018-06-25 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Tagged as 3.6.0

2018-06-18 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (gparam): Added support for binding the
strand variable in gparam as opposed to relying on it being bound
by a role length predicate.

2018-06-11 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/*.hs: Implemented geometric formulas as rewrite
rules.  The rules are applied after each cohort step.

2018-06-05 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/*.hs: Converted the goal language to be
strand-oriented.  The goal language in incompatible with the
previous, node-oriented language.

2018-05-22 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Cohort.hs (unrealizedInNode, nextNodeA):  Lifted to
top-level to satisfy new ambiguity check in GHC 8.4.2.

2018-04-17 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Version): Tagged as 3.5.0.

2018-03-20 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/DiffieHellman/Algebra.hs (displayVar, mkVar): Changed
sort names.  expn -> rndx and expr -> expt.

2018-02-12 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs (disjoin): Changed output to (false) on an
empty disjunction instead of (or).

2018-01-12 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Loader.hs (mkListenerRole): Changed do pattern to
be irrefutable.

2017-09-15 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/DiffieHellman/Algebra.hs (unifyTerms):  Added calls to
chase before calling unifyBase which prevents a failure in the
occurs check.

2017-09-14 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (tryPerm): Add missing inverse
permutation to second checkOrigs in tryPerm.

2017-09-12 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal:  Removed CPSA.Lib.CPSA globally and removed
unnecessary dependencies.

2017-08-30 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal: Added missing modules and source repository
location.

* src/CPSA/Lib/DebugLibrary.hs (zi): Fixed erroneous parameters in
Instance.

2017-08-28 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Cohort.hs (solved): Fixed condition 5.  It was
using ct instead of ct'.

2017-06-30 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Cohort.hs (transformingNode, maybeAug, nextNode):
Rewrote code so that it no longer fails the ambiguity check.

2017-05-26 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/DiffieHellman/Algebra.hs (mkInitMatchDecis): Ensure
initial distinctions to not include fresh variables.
(partition): Do not move variables of sort expn to lhs, even if
they are freshly generated.

2017-05-16 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/DiffieHellman/Algebra.hs (displaySubst):  Removed
erroneous substitution to fix substitution displaying.

2017-05-10 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Strand.hs (findReplacement, permutations): Merge
generators so that no variable in a term has an identifier that is
greater than or equal to the generator.

2017-02-02 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Basic/Algebra.hs (loadInvk): Added support for reading
(invk (privk ...)) and (invk (invk ...)).

2017-01-17 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs (strandForm): Remove conjoin and use
concatMap when creating a characteristic skeleton.

2017-01-09 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Loader.hs (loadPrimary): Removed generator
parameter that was not used.

2016-12-21 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Cohort.hs (solved): In Condition 4, applied
substitutions to the encryption keys before testing for
derivability.

2016-10-04 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Basic/Algebra.hs (matchRenaming):  Make isomorphism
check work in presence of asymmetric keys.

2016-09-30 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Algebra.hs: Added isObtainedVar for variables of
sort expr in the Diffie-Hellman algebra.

2016-08-12 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs (form): Changed "defsas" to "defgoal" as the
keyword for a generated shape analysis sentence.  This makes the
program compatible with its documentation.

2016-06-22 John D. Ramsdell ramsdell@mitre.org

* cpsa.cabal (Extension): Add allow ambiguous types when compiling
with GHC 8.0.0 or later.

2016-06-21 Moses D. Liskov mliskov@mitre.org

* src/CPSA/DiffieHellman/Algebra.hs: Added code to implement the
"tag" sort, which quoted string tags belong to.

2016-06-03 Moses D. Liskov mliskov@mitre.org

* doc/examples/IKE_variants.tar.gz: Added this compressed archive
of IKEv1 and IKEv2 variant input files.

2016-03-30 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs: Added support for fringe skeletons so that
cpassas makes use of depth limited output.  When a tree depth
limit is exceeded, a fringe labeled skeleton is printed.  cpsasas
produces a sentence with a right-hand-side that encodes both the
shapes and the fringe.  Thus, when cpsa is running the a tree
depth limit of one, cpsasas computes a cohort analysis sentence.

2016-03-29 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Reduction.hs (LPreskel): Added a depth field, so
that CPSA aborts when the depth of one branch exceeds a bound.

* src/CPSA/Lib/Algebra.hs: Added escapeSet to Term class and remove
protectors, thus computing the escape set in a more
straightforward way.

2015-11-23 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/Main.hs (main): Changed start up so that the herald
is read and used to find the correct algebra for further
processing.

2015-10-02 John D. Ramsdell ramsdell@mitre.org

* doc/{index,cpsauser}.html: Added width limit of 48em.

2015-07-09 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Graph/ExpandedView.hs (purgeTraces): By default, the
graph program now does not show traces in skeletons.  Added
--show-traces option to the graph program, which restores the
previous behavior and traces are displayed in skeletons.

2015-07-02 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Algebra.hs: Added constituent to the algebra
interface and the algebras.  An atom is a constituent of a term if
the atom is among the set of atoms required to construct the term.
Changed occursIn so that it just applies to variables.

2015-07-01 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/{Basic,DiffieHellman}/Algebra.hs (occursIn): Restricted
first argument of occursIn to variables and atoms and corrected
the implementation.

2015-06-30 John D. Ramsdell ramsdell@mitre.org

* cpsa3.cabal (Version): Tagged as 3.2.2.

2015-06-25 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (geq): Removed dynamic role specific test
because it erroneously reports violations.  The existing static
role specific test correctly does the job.

2015-05-26 John D. Ramsdell ramsdell@mitre.org

* cpsa3.cabal (Version): Tagged as 3.2.1.

* src/CPSA/DiffieHellman/Algebra.hs (displayTerm):  Made it so
that CPSA prints each bltk atoms in a canonical form so that the
graph program draws solid arrows when it should.

2015-04-27 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Loader.hs (ReturnFail): Added ReturnFail Monad so
that fail is correctly handled.  Added Functor and Applicative
instance to support GHC 7.10 base library.

2015-04-20 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Characteristic.hs (mkDcls): Fixed tag for non-orig
and pen-non-orig.

2015-04-10 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (mkListener): The role used for listener
strands is now the one stored in the protocol.  It has a single
variable x of sort mesg as its set of variables.  This change
enables satisfaction checking on skeleton that include listeners.

2015-04-07 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (toSkeleton): Removed hulling to the
process of converting an input preskeleton into a skeleton as it
causes bugs in printing.

* Imported CPSA2's implementation of goals and expunged support
for subgoals.

2015-03-27 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (toSkeleton): Added hulling to the
process of converting an input preskeleton into a skeleton.

2015-03-25 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Goal.hs: Added uniq to goal language.

2015-03-17 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs (form): Generate a defsas form rather than a
naked sentence.

* src/CPSA/Lib/Loader.hs (loadPrimary): Renamed equals function
symbol to =.

2015-03-05 John D. Ramsdell ramsdell@mitre.org

* cpsa3.cabal (Version): Tagged as 3.2.0.

2015-02-20 John D. Ramsdell ramsdell@mitre.org

* Added support for subgoals within point-of-view skeletons.  The
subgoals are evaluated for each shape, and (satisfies-a-subgoal)
is added to a shape when it satisfies one of the subgoals.

2014-12-11 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Entry.hs (defaultOptions): Changed the default
strand bound to 12.

2014-11-15 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/SAS/SAS.hs: Changed the language used for a shape
analysis sentence to be node-oriented.

2014-11-07 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Loader.hs (loadPriorities): Allowed priority
declarations on state synchronization nodes other than
initiatizers.

2014-11-07 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Cohort.hs (explainable): Added the nodes reachable
by strand succession so that a transition can be explained by a
previous transition within a strand.

2014-10-31 John D. Ramsdell ramsdell@mitre.org

*  Changed the name of the logic producing program to cpsa3sas.

2014-09-01 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (noStateSplit): An observer node should have
at most one transition node after it too.

2014-08-31 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/State.hs: Made labels optional.  Use "tran" for
state synchronization events with labels, and "sync" for ones
without.

2014-08-29 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/*.hs: Added support for analyzing protocols with
state.  A state synchronization event sync was added to the events
that can occur in a trace, along with a new method for state-based
augmentation.  An example using sync events is in
tst/envelope.scm.

2014-08-26 John D. Ramsdell ramsdell@mitre.org

* cpsa3.cabal:  Removed cpsaparameters program.

2014-08-25 John D. Ramsdell ramsdell@mitre.org

* src/split.py: Added the skeleton split program that copies the
skeletons in a CPSA source file into separate files.

2014-08-23 John D. Ramsdell ramsdell@mitre.org

* src/cpsajson.py (load): Added a reader in Python for JSON
produced by CPSA's pretty printer program cpsa3pp -j.

2014-08-22 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/JSON/Main.hs: Added the program cpsa3json that
translates JSON encoded CPSA into CPSA S-Expressions.  It expects
the JSON input to follow the conventions of the JSON produced by
the cpsapp program when given the -j option.

* src/CPSA/Lib/SExpr.hs (numOrSym): Enabled parsing a number with
a plus sign by removing the sign before translating the string of
digits into a number.

2014-06-12 John D. Ramsdell ramsdell@mitre.org

* cpsa3.cabal (Version): Tagged as 3.0.3.

2014-02-06 John D. Ramsdell ramsdell@mitre.org

* cpsa3.cabal (Version): Tagged as 3.0.2.

2013-12-14 John D. Ramsdell ramsdell@mitre.org

* cpsa3.cabal (Version): Tagged as 3.0.1.

* cpsa3.cabal (Extra-Source-Files): Added more DH tests

2013-03-12 John D. Ramsdell ramsdell@mitre.org

* src/CPET/Annotations/Annotations.hs (obligation): Replaced an
irrefutable pattern that raised an exception with a maybeToList.

2013-02-21 John D. Ramsdell ramsdell@mitre.org

* src/CPET/DiffieHellman/Algebra.hs: Added the Diffie-Hellman
algebra based on Abelian groups.

* src/CPET/Basic/Algebra.hs:  Removed support for GHC 6.x.

2013-02-06 John D. Ramsdell ramsdell@mitre.org

* cpet.cabal (Version): Tagged as 0.0.0.