Changelog of @hackage/cpsa 3.6.8

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

* cpsa.cabal (Version): Tagged as 3.6.8

2021-11-05 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Lib/Strand.hs (addBaseListener): Added a stronger
method for solving some Diffie-Hellman authentication tests.  The
method handles the special case in which the critical term has the
form (exp (gen) (mul ...)) and all of variables in the exponent
are random exponents (rndx).  It uses baseRndx to add listeners.

* src/CPSA/DiffieHellman/Algebra.hs (baseRndx): When all of the
factors in a group use rndx variables, baseRndx returns a list of
concatenations of each variable with the base term exponentiated
with the group without the variable.

2021-11-02 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/Graph/ExpandedView.hs (tdrawer): Added POV link in
tree.

2021-09-10 John D. Ramsdell ramsdell@mitre.org

* src/CPSA/lib/Expand.hs (macroExpand): Made it an error to apply
a macro to the wrong number of arguments.

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

* cpsa.cabal (Version): Tagged as 3.6.7

2021-04-27 Joshua D. Guttman guttman@mitre.org

* cpsa.cabal:  Clarified package description (deorigination)

2021-04-14 John D. Ramsdell ramsdell@mitre.org

* Makefile: Vastly simplified.

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

* cpsa.cabal (Data-Files): Added missing examples to Data-files.

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.