ChangeLog

2026-05-24 Paul D. Rowe <prowe@mitre.org>
	* doc/cpsa4manual.pdf: Document new features in manual

	* cpsa.cabal (Version): Tagged as version 4.4.9

2026-05-23 Paul D. Rowe <prowe@mitre.org>
	* src/CPSA/Signature.hs (defaultSig): Added dev as a default
	atomic sort. Also added locn and chan to be valid sorts in the
	message algebra that can appear in messages.

	* src/CPSA/Channel.hs (ChMsg, ChType, ...): Changed the structure
	of ChMsg to include an argument indicating if it is a channel or
	location.

	* src/CPSA/Algebra.hs (isChan, isLocn, ...): Allowed the channel
	and location positions of events to be any message term.

	* src/CPSA/{Algebra.hs,Channel.hs,Cohort.hs,Db/Loader.hs,
	Displayer.hs,GenRules.hs,LoadFormulas.hs,Loader.hs,Protocol.hs,
	Strand.hs}: Threaded necessary changes to ChMsg data type through
	all functions and fixed resulting incompatibilities.

2026-03-16 Paul D. Rowe <prowe@mitre.org>

	* src/CPSA/Loader.hs (loadSExpr): Added a deflemma as a new
	top-level form. A deflemma is marked as no-check (import as a rule
	into the protocol of the same name for subsequent queries) or as
	check (first add the lemma as a query, then add as a rule for
	subsequent queries regardless of whether or not the lemma is
	satisfied).

2026-02-27 Paul D. Rowe <prowe@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.4.8

2026-02-27 Paul D. Rowe <prowe@mitre.org>

	* src/CPSA/Strand.hs (rewrite): Fixed a bug that failed to check
	nullary rules after the success of a unary rule.

2025-12-01 Paul D. Rowe <prowe@mitre.org>

	* src/CPSA/{Strand.hs,Reduction.hs} (unSatReport): Modified how
    to report unsatisfiability of goals to list all predicates that are
	not satisfiable.

2025-05-05  Joshua D. Guttman  <guttman@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.4.6. Removed an
	obscure bug in which the generators were used wrong, causing a
	unification failure.  We improved the generalization code to avoid
	redundancies.  We improved the overall functionality by allowing
	state operations in which stores are not preceded by a load on
	that location.

2025-05-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/cpsa/RoleCoq/Main.hs (emit): Updated Roletran to use rocq
	9.0.0.

2024-07-17  Joshua D. Guttman  <guttman@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.4.5.  Adds cpsa4db and
	cpsa4dbprolog to enable prolog access to the goal language and
	other properties of CPSA output.  Fixes supplementary bugs and
	eliminates redundant occurrences of seen children.

2024-06-21  Joshua D. Guttman  <guttman@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.4.4.  This version has
	important bug fixes especially for the Diffie-Hellman "absence"
	computation.

2023-10-23  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.3.3

2022-04-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Signature.hs (loadSig): Improved language field loading
	error messages.

2022-04-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Loader.hs (findPreskel, findGoal): Updated to use
	protocol's signature.

2022-04-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/{Graph,SAS,Shapes}/Main.hs: Removed extra quotes in
	error messages.

2022-03-25  Joshua D. Guttman  <guttman@mitre.org>

	* src/CPSA/Loader.hs (loadRole etc):  Distinguish state-specific
	generated rules from other generated rules so that only the state
	rules will be omitted if state is not in use.

2022-03-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Loader.hs (hasLocn): Omit adding state rules in a
	protocol that makes no use of state.

2022-03-17  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/SExpr.hs: Allow double quote and backslash in
	strings so that S-expressions can contain Windows file names.

	* src/CPSA/Loader.hs (loadLang): Optionally load a lang field in a
	protocol.

2022-02-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/SVG.hs (kbutton): Made realized skeletions print
	in blue and shapes are now bold.

2021-12-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (origUgenDiffStrand): Flush skeletons that
	have a value that is both uniq orig and uniq gen, and start on
	different strands.

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

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

2021-10-27  Joshua D. Guttman  <guttman@mitre.org>

	* src/CPSA/Strand.hs:  Fixed subtle bug causing generalization to
	fail when uniqs, nons, and pnons can be omitted.  Problem was that
	the code for these operations modifies the preskeleton data
	structure directly, just deleting the basic value.  But the
	preskeleton datastructure as computed fields, especially the gist,
	that need to be recomputed.  RenewPreskel calls newPreskel to
	recompute these fields correctly.

2021-09-14  Joshua D. Guttman  <guttman@mitre.org>

	* src/CPSA/Loader.hs:  Modified the transition rules.  A load
	event will now be asserted to be a transition event in a strand
	only if that strand is long enough to contain a matching stor.
	Previously it counted as a transition as long as the role
	contained a matching stor.  This should avoid unwanted
	consequences when roles may match up to a height that contains the
	load but not the subsequent store.

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-06-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Roletran/Emitter.hs (displayKind): Reverted to coarse
	program variable types for procedures.

2021-06-16  Joshua D. Guttman  <guttman@mitre.org>

	* src/CPSA/Roletran/Protocol.hs:  Distinguished generated rules
	and user-written rules in the protocol datatype.  Caused Loader to
	separate the two kinds of rules, and Displayer to display the
	generated rules as defgenrule.

2021-05-07  John D. Ramsdell  <ramsdell@mitre.org>

	* Roletran correctly handles long term keys, key inverses, and
	named asymmetric keys.

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

	* clarified package description (deorigination)

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

	* Makefile: Vastly simplified.

	* CPSA/Roletran/Derivation.hs (deriveEvent): Added missing checks
	that determine if sent messages and returned messages are
	receivable.

2021-03-10  John D. Ramsdell  <ramsdell@mitre.org>

	* CPSA/Roletran/Emitter.hs (Kind):  Added refined program
	variable types for procedures.

2021-01-12  John D. Ramsdell  <ramsdell@mitre.org>

	* CPSA/Roletran/Derivation.hs (deriveInputs): Allowed inputs to
	contain any term as long as they can be reduced using previous
	inputs.

2020-11-10  John D. Ramsdell  <ramsdell@mitre.org>

	* coq: Changed the representation of procedures to use statement
	lists.

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

	* src/CPSA/RoleCoq/Main.hs: Added program cpsa4rolecoq that
	translates the roles in the first protocol of CPSA input into Coq.

	* src/CPSA/Coq/Main.hs: Added program cpsa4coq that translates the
	output of cpsa4roletran into Coq.

	* coq: Added Coq libraries that can be used to verify that an
	output of cpsa4roletran is valid.

2020-09-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Roletran/Main.hs: Added cpsa4roletran

2020-08-28  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/Preskeleton.hs (nodeColor):  Added colors for
	load and stor.

2020-08-10  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.3.0

2020-04-20  Joshua D. Guttman  <guttman@mitre.org>

	* src/CPSA/Strand.hs (isAuth):  Added locations with point
	structure and uniqueness assumptions.

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

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

2020-03-05  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Extra-Source-Files): Remove defunct CGI scripts.

2020-03-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Prot/Main.hs (maybeExpand): Added -e option that causes
	cpsa4prot to expand macros before it generates protocols.

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

	* src/CPSA/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.

2020-02-18  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Prot/Main.hs (msg): Added role cloning in cpsa4prot.

	* doc/cpsa4.mk: Added preprocessing rule for *.prot files that
	invoke cpsa4prot.

	* src/CPSA/Prot/Main.hs (main): Added cpsa4prot program that
	translates protocols in Alice and Bob notation into defprotocol
	syntax.

2020-02-15  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.2.3

2020-02-14  John D. Ramsdell  <ramsdell@mitre.org>

	* Makefile: Updated for Cabal 3.0.0.0

	* cpsatst: Updated for Cabal 3.0.0.0

2020-02-14  Ian D. Kretz  <ikretz@mitre.org>

	* src/CPSA/Latex/Main.hs: Added the cpsa2latex program.

2019-12-19  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/src/cpsafoundation.tex: Added document titled "Strand Spaces
	with Channels and Rules".

2019-12-06  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 4.2.2

2019-11-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/GoalSat/Main.hs (main):  Added the cpsa4goalsat program.

2019-11-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (soothePreskel):  Fixed the filters for
	channels by testing with all channel variables rather than all
	message variables.

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

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

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

	* cpsa.cabal (Version): Tagged as version 4.2.1

	* src/CPSA/Lib/ReturnFail.hs: Used the C preprocessor to allow
	compilation using older versions of GHC.  In particular, defined
	MonadFail to be Monad when the base library is less than 4.13.

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

	* src/CPSA/Lib/ReturnFail.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/Strand.hs (probIsomorphic): In thinning, replaced
	isomorphic check with probIsomorphic check so that strands in the
	point-of-view remain unmodified.

2019-09-11  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (dropInbnd):  Enabled strong pruning as a
	compile time switch.  Also, when using either form of pruning,
	thinning is disabled.

2019-09-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (prune):  Added pruning as a compile time
	option controlled by Strand.usePruning.  When True, CPSA prunes
	before it attempts to thin.

2019-09-05  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (fperms):  Added support for variables that
	occur in facts but do not occur in strands.  The tricky part was
	making isomorphism checking work, and fperms is the key function.

2019-09-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Reduction.hs (step): Added goals-sat option (-g) so
	that CPSA4 stops pursuing a branch when a set of goals are
	satisfied.

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

	* cpsa.cabal (Version): Tagged as version 4.2.0

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

	* src/CPSA/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/Strand.hs (runiqAt): Ensured that rewriting with
	uniq-at fails when the index is greater than the strand length.
	(rluniq): Fixed existing check to using kunique instead of knon.

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, and Make4.hs from
	the CPSA data directory to the current directory, thereby easing
	the task of starting a CPSA project.

2019-08-12  John D. Ramsdell  <ramsdell@mitre.org>

	* Added support for channels.

2019-08-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (krules): Added a field in Preskel that
	tracks the names of applied rules.

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/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/Reduction.hs (begin): Reversed todo list after running
	rules so as to get the output order correct.

2019-05-20  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (tryPerm):  Fixed bug in isomorphism
	checking.  Second check of facts used wrong permutation.

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

	* 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/Strand.hs (verbosePreskelWellFormed):  Added a check
	that ensures the every variable that occurs in a fact also occurs
	in some strand.

2019-03-13  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/src/cpsaspec.tex (Critical Position Solved): Corrected item
	3 in the definition and improved its presentation.

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

	* src/CPSA/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/Reduction.hs (step): Changed default depth bound to
	zero representing no bound and ignored the check when the bound is
	not positive.

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

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

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-13  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (firstSkeleton): Added a field pprob to
	Preskel and use it record the strand map from a preskeleton to the
	first skeleton.  This is used when printing the strand map of a
	skeleton on the fringe.

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-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/Strand.hs (soothePreskel): Made soothe cleans facts.

	* src/CPSA/Strand.hs (tryPerm): Added case for reverse match of
	facts.

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.

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

	* src/CPSA/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>

	* cpsa.cabal (Version):  Tagged as version 4.1.1

2018-05-31  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/src/cpsagoals.tex: Added DoorSEP explanation as Section 6.2.

2018-05-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Reduction.hs (begin): Change "Not in theory" message to
	"Not closed under rules".

2018-05-29  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Cohort.hs (maximize): Eliminated generalizations that
	fail to satisfy the rules of the skeleton's protocol.  Otherwise,
	generalizations can undo the effects of applying rules.

2018-05-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (changeLocations,deleteNodeRest): Flushed
	facts that referred to variables that no long exists a skeleton's
	instances.

2018-05-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (doRewriteOne):  Ensured that the skeletons
	produced by rule application are well-formed.  When rules produce
	non well-formed skeletons, havoc ensues.

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

	* tst/fluffy_draft03_gske.scm (fluffy-rule): Added fluffy example
	with some rules.

2018-02-14  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 4.1.0

2018-02-13  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Data-Files): Removed the overview document.

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

	* Many files:  Removed support for nodes in facts.

2018-02-09  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Cohort.hs (filterSame):  Added a filter that removes
	skeletons in the cohort that are isomorphic to the parent.  Rule
	application produced the skeletons filtered out.

2018-02-07  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/src/cpsagoals.tex (section{Rules}):  Added a description of
	rules and the DoorSEP example.

	* src/CPSA/{Strand.hs,...}: Replaced unsorted rule language with
	one that uses the security goal language.  This means a rule can
	refer to all of the function symbols provided by the message
	algebra.

2018-01-26  John D. Ramsdell  <ramsdell@mitre.org>

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

2018-01-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (doForm, uMatchForm): Use transitive closure
	of prec relation instead of just the contents of the ordering
	field.  Otherwise, rules can loop.

	* src/CPSA/Strand.hs (doForm): In case of UPrec, fail when strand
	index is too large, instead of raising an error.

2018-01-17  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (deleteNode): Update facts correctly when
	deleting a node.

	* src/CPSA/Reduction.hs (begin): Start up an analysis by applying
	as many rules as possible.  Also, added protocol transformations
	test case.

2018-01-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Loader.hs (loadUForm,loadUTerm): Improved loader error
	messages for rules.

2018-01-14  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/{*.tex,*.mp,Makefile}: Moved LaTeX sources to doc/src.

2018-01-13  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/*.hs: Added rules to protocols enabling rewriting based
	on geometric formulas.

	* doc/cpsauser.html: Added a description of rules and facts.

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

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

2018-01-10  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/{cpsauser.html,cpsaprimer.tex}: Added a description of the
	displaced test kind in the operation field.

2018-01-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Loader.hs (loadConclusion): Added false as an alias for
	(or) in the goal language.

2017-12-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (Fact): Added facts to skeletons and the goal
	language.

2017-08-18  John D. Ramsdell  <ramsdell@mitre.org>

	* Updated README and doc/cpsauser.html.

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

	* src/CPSA/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-05-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Strand.hs (soothPreskel): Modified isomorphism check
	and thinning so that it no longer uses matchRenaming and
	identityEnvFor, which have been removed from the algebra module.
	The new version of thinning follows the definition of thinning
	more closely, and the spec has been updated to reflect the change.

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

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

2017-01-27  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsagoals.tex: Updated document for the strand-oriented
	logic language.

	* cpsa.cabal (Version): Tagged as version 4.0.0

2017-01-22  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaspec.tex (chapter{Shape Analysis Sentence}): Update
	chapter for the strand-oriented logic language.

2017-01-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Characteristic.hs (strdRoleLength): Allowed two role
	length atoms with the same strand as long as they agree on the
	role.

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

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

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

	* Changed the goal language to one that is strand-oriented.

2016-12-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/*.hs: Added Haddock comments.

	* cpsa4.cabal: Reorganized source directory structure.  CPSA
	specific modules are now in src/CPSA.

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

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

	* src/CPSA/Lib/Algebra.hs (loadInvk): Enabled reading of invk
	(pubk ...).

	* tst/reflect.scm: Added reflect protocol example.

	* src/CPSA/Lib/Algebra.hs (mkVar): code cleanup: better version of
	mkVar for loadVar

	* Enabled compilation using GHC 8.01 by removing the Algebra
	class.

	* Purged programs cpsaannotations and cpsaparameters.

2016-04-13  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa4.cabal (Version): Updated version number to 4.0.0.

	* Made it so that cpsa4diff, cpsa4shapes, cpsa4graph, cpsa4pp, and
	cpsa4json do not rely on CPSA.Lib.Algebra.

	* src/CPSA/Graph/Main.hs: Purged support for infix notation.

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 with 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: Add escapeSet to Term class and remove
	protectors, thus computing the escape set in a more
	straightforward way.

2016-01-12  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Description): Added sentence saying CPSA was
	designed and implemented at The MITRE Corporation.

	* cpsa.cabal (Version): Tagged as version 2.5.4

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

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

2015-08-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/*/*.h:  Removed leading tabs.

	* src/CPSA/Annotations/Formulas.hs (EitherS): Made EitherS an
	instance of Applicative.

	* cpsa.cabal (Version): Tagged as version 2.5.3

2015-08-07  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsagoals.tex: Corrected the definition of satisfaction.

2015-08-06  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsagoals.tex: Made minor fixes due to another review.  Also
	fixed the definition of a characteristic skeleton.

2015-08-04  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaprimer.tex (section{Macros}\label{sec:macros}):  Added
	text describing splicing.

2015-07-27  John D. Ramsdell  <ramsdell@mitre.org>

	* README: Updated to reflect that Haskell Platform should always
	be used.

	* cpsa.cabal (Version): Tagged as version 2.5.2

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

	* src/CPSA/Graph/ExpandedView.hs (purgeTraces): Added -p flag to
	the graph program.  When present, the graph program purges traces
	in skeletons it prints.

2015-07-08  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.5.1

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

	* src/CPSA/Basic/Algebra.hs (occursIn): Restricted first argument
	of occursIn to variables as the implementation returns incorrect
	answers for other cases.  The code was called with a variable in
	its first argument, so this correction does not change any
	results.

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-06-18  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/{cpsaprimer,cpsagoals}.tex: Repaired errors and made
	improvements in response to a review of this document.

2015-05-21  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.5.0

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>

	* cpsa.cabal (Source-Repository): Added github source repository.

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-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (hull): Removed the hulling by
	deorigination mode and returned to the hulling by compression
	algorithm.  Hulling is only used on the initial preskeleton.

	* src/CPSA/SAS/SAS.hs (form): Changed the output form from defsas
	to defgoal.

2015-03-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Loader.hs (loadPrimary): Improved the error
	messages for ill-formed atomic formulas.

	* src/CPSA/SAS/SAS.hs (loadPOV, loadOtherPreskel): Flushed the
	check that an atom assumed to uniquely originate must originate in
	a skeleton.  In this case, cpsasas generates a uniq assertion
	rather than a uniq-at assertion.

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

	* src/CPSA/Lib/Loader.hs (findGoal): Allow more than one sentence
	in a defgoal.

	* src/CPSA/SAS/SAS.hs (Preskel): Added pnon predicate symbol.

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

2015-03-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/{Characteristic,Strand,Loader}.hs: Added new
	toplevel form: defgoal.  The characteristic skeleton of the
	antecedent in the goal is extracted and used as the initial
	skeleton.

2015-03-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/{Reduction,Strand,Loader}.hs: Made it so that when
	a shape does not satisfy a goal, an environment showing why is
	printed.  For each goal, the output is yes when the goal is
	satisfied or (no (VAR VAL)...).

2015-03-20  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/{Goal,Strand,Loader}.hs: Added goal loading and
	satisfaction checking.  When a shape satisfies all goals in a
	point-of-view skeleton, the shape is annotated with
	(satifies-all-goals).

2015-03-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (Term): Added node variables and
	constants for security goals.

	* src/CPSA/SAS/SAS.hs (form): Changed the format of a shape
	analysis sentences.  Instead of a bare formula, the formula is
	wrapped in a defsas form, as in (defsas PROT SAS).  Removed the
	protocol from role position predicates and parameter predicates.
	Replaced function symbols uniq and sprec with uniq-at and str-prec
	respectively.

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

	* src/CPSA/SAS/SAS.hs (displayEq): Use = for function symbol
	instead of equal.

2014-11-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/prover9.pl: Added missing mesg predicates in output.

2014-11-17  John D.  Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.4.0

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

	* src/CPSA/SAS/SAS.hs (nodeForm): Fixed bug where some role
	predicates were mistakenly omitted.

2014-11-13  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaspec.tex: Updated the appendix of shape analysis
	sentences to agree with what is produced by cpsasas.

2014-11-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/SAS/SAS.hs (reduce): Added a function that eliminates
	trivial homomorphism equations by substituting equivalent
	variables and simplifying.

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

	* cpsasas: Added a program that produces shape analysis sentences
	using the goal language used with protocol transformations.  This
	language is superior to the one used by the cpsalogic program.

	* cpsalogic: Removed this program as it has been replaced with
	cpsasas.

2014-09-05  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.3.5

2014-09-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/unsorted.pl (decl_as_pairs):  Fixed bug in the case of
	variables of sort mesg.

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-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/JSON/Main.hs: Added the program cpsajson 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-06  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.3.4

	* doc/cpsauser.html:  Commented out Diffie-Hellman algebra
	description.

	* src/CPSA/Lib/Main.hs (useDiffieHellman): Added a compile time
	switch that is used to disable the Diffie-Hellman algebra in a
	release.

2014-04-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Expand.hs:  Added splicing to the macro expander.
	The splice symbol is ^.

2014-04-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs (agSolve): Added missing omit
	when generating new equation.

	* src/CPSA/DiffieHellman/Algebra.hs (genVars): Removed code that
	conditionally generates new variables because the condition was
	not reliable.

2014-03-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs: Changed the sort structure
	of exponents.  The sort of exponents is now expr, and there is as
	subsort for basis elements called expn.  Unification and matching
	have been change so as to respect this sort structure.  This
	change allows CPSA to solve Diffie-Hellman key exchange.

2014-02-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs (specialize): Expunged specialize from
	the interface and the algebras.

2014-02-25  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs (isAcquiredVar): Changed the
	definition so that both variables of sort base and sort mesg are
	acquired.

	* src/CPSA/Lib/Algebra.hs (Term): Renamed isMesgVar to
	isAcquiredVar.

2014-02-24  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal:  Expunged Simple Diffie-Hellman and
	Diffie-Hellman No Reciprocal algebras.

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

	* cpsa.cabal (Version): Tagged as version 2.3.3

2014-02-05  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs: Purged code for pruning.

	* doc/cpsaspec.tex: Documented thinning and removed material on
	pruning.

2014-02-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (useThinning): Set flag to True so as use
	thinning by default.

2014-01-07  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.3.2

2013-12-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/prover9.pl: Reverted to work with strings as tags fixing a
	bug introduced in version 2.3.1.

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

	* cpsa.cabal (Extra-Source-Files):  Sorted the files.

2013-10-15  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.3.1

	* src/unsorted.pl: Added a missing occurs check and substitution.

2013-10-11  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (prioritizeVertices): Reversed the sort
	predicate so that high numbered priorities are considered first.

2013-10-09  John D. Ramsdell  <ramsdell@mitre.org>

	* tst/epmo_acctnum.lisp: Stopped running this example as part of
	the standard test suite because it now takes nearly 5000 steps.

	* src/CPSA/Lib/Algebra.hs: Removed moreGeneral because the mgs
	filter alleviates the need for this function.

2013-10-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/{Strand.hs,Cohort.hs} (mgs): Replaced filters with
	a most general homomorphism filter.

2013-10-05  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (mga): Added a most general augmentation
	filter as the MGU filter added to transformingNode did not remove
	enough.

2013-10-01  Moses D. Liskov  <mliskov@mitre.org>

	* src/CPSA/Lib/Cohort.hs (transformingNode): Applied the MGU
	filter to the result of just one carried binding, not all of them.

2013-10-01  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Extra-Source-Files): Deleted Diffie-Hellman tests as
	support for DH never worked.

2013-09-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/sexpr.pl: Reverted back to the case in which tags are
	encoded as SWI-Prolog strings.

2013-09-11  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs: Removed heldBy from the interface.

	* src/CPSA/*/*.hs: Removed contexts from all datatypes.  This
	language extension is deprecated and will soon be removed.

2013-09-09  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs (groupChase):  Add missing
	case of chasing though group variables.

2013-07-23  John D. Ramsdell  <ramsdell@mitre.org>

        * cpsa.cabal (Version):  Tagged as version 2.3.0

	* src/CPSA/Lib/*.hs:  Added priorities to help guide the search.

	* src/CPSA/Lib/Protocol.hs (mkRole): Positions are now used to
	specify non-origination introductions rather than heights.

	* doc/cpsaspec.tex: Reverted back to zero-based indexing.

	* doc/cpsauser.tex: Removed Diffie-Hellman documentation as the
	implementation of the algebra continues to have serious issues.

2013-07-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/Tree.hs (makeTree): Skeletons without children
	that are not marked "empty cohort" are now counted as live.

2013-06-13  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs: Added isMesgVar for acquires check.

	* src/CPSA/Lib/Strand.hs (thinStrand, thinManyStrands):  Added
	transitive reduction before thinning.

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

2013-04-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/prover9.pl: Removed erroneous quotes that were added to the
	translation of constants.

2013-04-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/prover9.pl: Changed the formula translation algorithm so
	that predicates for the sort declarations of variables are added
	to generated formulas.  Previously, the sort information was
	ignored.

2013-03-29  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs (mgu): Changed so function
	performs substitutions on all vars on LHS, not just the ones not
	that were originally on the LHS.

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

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

2013-03-06  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs (sLoad):  Added code that
	allows testing of unification and matching in GHCi.

2013-02-28  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/*.html:  Convert to HTML 5 mainly by eliminating the DOCTYPE
	element.

	* cpsa.cabal (Version):  Tagged as version 2.2.13

2013-02-12  Paul D. Rowe  <prowe@mitre.org>

	* src/perm.pl:  Fix permutation bug.

2013-01-22  John D. Ramsdell  <ramsdell@mitre.org>

	* tst/Makefile ($EXE): Added optional extension for Cygwin users.
	On Cygwin, put "export EXE=.exe" in a startup file.

2012-11-13  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaspec.tex (chapter{Generalization}): Corrected the
	definition of a location in the text describing variable
	separation.

2012-11-09  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.12.

2012-11-06  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/index.tex:  Added a section on useful tips.

	* doc/cpsauser.tex:  Added description of Emacs Compilation Mode
	support.

2012-10-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/cpsaperm.scm: Added a Scheme program that renumbers the
	strands in a skeleton while preserving all information in the
	skeleton.

2012-10-29  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaintroslides.tex:  Added introductory slides for new
	users.

2012-10-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/cpsa.pl: Added support for penetrator non-origination
	assumptions.

2012-10-25  John D. Ramsdell  <ramsdell@mitre.org>

	* src/perm.pl: Added a program that renumbers the strands within a
	skeleton.  This program also strips the skeleton of non-essential
	information.

2012-10-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Pretty/Main.hs (pjson):  Added JSON output option.

2012-08-24  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.11.

	* doc/cpsaprimer.tex (Appendix B): Added a discussion on shapes
	that CPSA fails to find.  It explains that the missing shapes only
	occur when interpreting roles unnaturally.

	* tst/incompleteness_example.scm: Added the example used in the
	primer that shows a shape CPSA fails to find.

2012-08-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Expand.hs (include): Added a top-level form that
	includes source file while performing macro expansion.

2012-08-06  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Reduction.hs (breadth): Added comments describing
	loop variables.

	* src/CPSA/Lib/Strand.hs (skeletonize): Expunged hulling by
	compression code.

2012-08-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Reduction.hs (breadth,step): Added the tobig
	variable so that all skeletons are produced that are below the
	strand bound.

	* src/CPSA/Lib/Main.hs (main,select,go): Added source file name to
	"All input read" comment.

2012-06-28  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.10.

	* src/CPSA/Lib/Entry.hs (tryIO): Made error option in return value
	a string so that error messages are correctly parsed by Emacs.

2012-06-06  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Entry.hs (tryIO): The use of System.IO.Error.try
	has been deprecated, so CPSA.LIB.Entry now exports a replacement.

2012-06-06  John D. Ramsdell  <ramsdell@mitre.org>

	* {doc,tst}/Make.hs: Changed imports so that ExitCode and system
	come from System.Exit and System.process, not System, which is
	part of the haskell98 package that is now hidden by default.

2012-05-25  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.9.

	* src/CPSA/Lib/Reduction.hs (begin, search): Collapsing is
	performed as a pre-processing stage before any tests are solved.
	As a result, there is no need for hulling, and it has been
	disabled.

2012-05-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (augment): Removed the ability to turn
	off displacement.

	* src/CPSA/Lib/Strand.hs (augmentAndDisplace): Put skeletons
	produced by displacement before the ones created by augmentation.

2012-05-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/*.hs:  Added penetrator non-origination
	assumptions (pen-non-orig).

2012-05-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/SimpleDiffieHellman/Algebra.hs (normalize): Equality,
	comparison, and substitution normalize exponentiated values.

2012-05-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/SimpleDiffieHellman/Algebra.hs (idSubst, substChase):
	Produce canonical form for double exponents.

	* src/CPSA/SimpleDiffieHellman/Algebra.hs (equalTerm)
	(compareTerm): Compare double exponents using lists for efficiency
	and readability.

2012-05-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellmanNoReciprocal/LinDiophEq.hs: Used the
	method in the paper by Contejean and Devie for solving an
	inhomogeneous equation using the algorithm for the homogeneous
	equation solver.  The previous version buggy.

2012-05-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/SVG.hs (kbutton): In a tree drawing, the label of
	a shape is now blue.

2012-02-27  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.8.

2012-02-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (separateVariablesLimit): Added a hard
	coded limit to the number of attempts to perform variable
	separation during generalization.

2012-02-22  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsa.mk,doc/Make.hs: Removed rules for *.sch files.

2012-02-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (usePrunedStrandNotInPOV): Turned this
	flag on.  It never was supposed to be off except for when
	experimenting.

2012-02-01  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.7.

	* doc/cpsasdha.tex: Added a document describing the current
	implementation of a Diffie-Hellman algebra.

2012-01-25  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/*/Algebra.hs (encryptions): Used the C preprocessor to
	all support for GHC 6.x while eliminating the annoying warnings
	because Data.Map.foldWithKey has been deprecated in newer versions
	of GHC.

	* src/CPSA/Lib/Algebra.hs (encryptions): Changed the signature so
	that an encryption returned by this function may have more than
	one key used to prepare it as in the case of Diffie-Hellman
	algebras.

2011-12-20  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (match): Handle algebra equation with
	the rule match(invk(t), t', env) -> match(t, invk(t'), env) when
	t' is not of the form invk(t").  Corrects a missing case in
	previous algorithm.

	* src/CPSA/Lib/Notation.hs (mesg): Print (hash a b ... z)
	as #(a, b, ..., z).

2011-12-09  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/SVG.hs (tooltip): Display tool tips with
	<g><title>TOOLTIP</title>...</g> instead of <a
	xlink:title='MESSAGE'>...</a> so that tool tips work in Firefox
	and Chrome again.

	* cpsa.cabal (Version):  Tagged as version 2.2.6.

2011-11-18  John D. Ramsdell  <ramsdell@mitre.org>

	* tst/deorig_mesg.scm (deorig-mesg):  Added an example showing
	that variables of sort mesg make deorigination very hard.

2011-11-07  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/*: Delete cpsatheory.tex, and replace references to it with
	ones to the MTR "Completeness of CPSA".

	* src/CPSA/Lib/Loader.hs (notListenerPrefix): Ensure each role
	does not have the pattern <-t, +t, ...> so as to avoid confusion
	with listeners.q

2011-08-16  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.5.

2011-08-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/cpsa.pl: Changed the internal form so that compound terms
	are represented as function symbols applied to terms, not as
	S-expressions.

2011-08-12  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/*: Updated documentation to reflect support for hashing.

2011-08-11  Paul Rowe  <prowe@mitre.org>

	* src/CPSA/Basic/Algebra.hs: Added support for hashing.

2011-07-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (ksubst): Made the flag validate the
	first argument.

	* src/CPSA/Lib/Strand.hs (compress): Added a flag validate.  When
	false, compression does not check for intrastrand orderings that
	create cycles.  Used in thinning.

2011-05-18  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.4.

2011-05-16  John D. Ramsdell  <ramsdell@mitre.org>

	* src/prover9.pl: Added a translator from cpsalogic output to
	prover9 syntax.

2011-05-13  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Reduction.hs (parMap): The option to compile CPSA
	without using the parallel runtime has been removed.  The parallel
	library comes with Haskell Platform, so it is always available
	these days.

	* cpsa.cabal (Executable cpsa): Added the GHC option -rtsopts when
	the compiler is version 7.0.0 or greater.  In 7.0.0, needed
	runtime option have been disabled for security reasons by default.

2011-05-12  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Logic/Logic.hs (precForm): Shortened the predicate's
	name from precedes to prec.

	* src/CPSA/Logic/Logic.hs (origForm): Added the orig predicate
	which asserts the node of origination for each uniquely originating
	atom.

	* src/CPSA/Lib/Reduction.hs (origs): Added nodes of origination
	of uniquely originating atoms for POV and shapes for cpsalogic.

	* src/CPSA/Lib/Reduction.hs (commentPreskel):  Rewrote this
	function so as to make its much more understandable.

2011-05-09  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaspec.tex: Added the orig predicate to shape analysis
	sentences so that eliminate a counterexample to Conjecture B.1.
	The addition of this predicate in necessary because with out it,
	there is no way to ensure that skeletons that model a description
	of a skeleton preserve nodes of origination of uniquely
	originating atoms.

2011-05-04  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.3.

2011-05-02  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaprimer.tex: Added sections on macros, cpsaparameters,
	and cpsalogic.

	* doc/cpsaspec.tex: Extensively rewritten to improve readability
	and reflect the current code base.  Added Appendix B that
	describes the theory behind shape analysis sentences and
	cpsalogic.

	* src/CPSA/Lib/Strand.hs (pruneStrand): Added check for
	homomorphism.  This fix slightly reduces CPSA's ability to prune.
	This problem was notice while rewriting The CPSA Specification.

2011-04-25  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Reduction.hs (commentPreskel): The format of the
	homomorphism comment in a shape changed to (maps (STRAND-MAP
	SUBST) ...), where there may be more than one homomorphism.

2011-04-18  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Logic/Logic.hs (logic): Added the cpsalogic program.
	It extracts an axiom in the language of first-order logic for each
	problem and its shapes from a CPSA run. The axiom is modeled by
	all realized skeletons.

2011-04-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Reduction.hs (commentPreskel): Added the
	preskeleton symbol to input that is not the point-of-view
	skeleton, but is the one used to generate it.

2011-04-11  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Reduction.hs (commentPreskel): For each shape,
	added the homomorphism from the POV skeleton to it as a comment
	using the key map.  The format is (map STRAND-MAP SUBST...), where
	there may be more than one substitution depending on the algebra.

	* src/CPSA/Lib/Algebra.hs: Added displayEnv to a Context.

2011-04-06  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsadesign.tex: Updated to reflect the current code base.

2011-03-29  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.2.

	* src/CPSA/Lib/Cohort.hs (cowt): Added a duplicate substitution
	removal filter so as to resolve a large memory usage bug when
	analyzing Wang's Fair Exchange Protocol.

	* tst/wang.lisp ("Wang's Fair Exchange Protocol"): Added new
	test.

2011-03-22  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaprimer.tex: Added the hashed value as key idea:
	(defmacro (hash x) (enc "hash" (cat "hash" x)))

	* tst/epmo-key-hash.scm, tst/epmo_acctnum-key-hash.lsp: Variants
	of epmo and empo_acctnum that use the hashed value as the key.

2011-02-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (solved): Disabled condition 2a for
	protocols with role variables that are all atoms.  The use of
	condition 2a is never fruitful in this case.

2011-02-01  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (solved): Added condition 2a to the
	solved predicate so that CPSA now finds the shape in targetterms8.

	* src/CPSA/Lib/Notation.hs (decl): The sort in a declaration is
	now printed after the variables, as in "a, b: name".

2010-12-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/SExpr.hs (abort): Close input handle when reporting
	a failure.

	* src/CPSA/Lib/SExpr.hs (isSym, isStr): Non-ASCII characters are
	accepted as constituents of symbols and strings.

2010-12-20  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.1.

2010-12-16  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Diff/Main.hs (showDiff): Closed output handle when a
	difference is found so as to ensure the output is flushed before
	exiting signaling failure.

2010-12-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/ExpandedView.hs (treelessView): Added
	treelessView, an output format that just prints the skeletons.
	It's meant to be used on cpsagraph input that is too large to
	handle otherwise.

2010-12-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/Loader.hs (loadFirst, loadNext): The loader
	returns one preskeleton per call, rather than returning the list
	of all preskeletons in the input.  This allows modes of operation
	in which only a small portion of the input is in memory at any one
	time.

2010-12-10  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsa.mk, doc/Make.hs: Changed the extension associated with
	cpsagraph output from .xml to .xhtml.

	* doc/cpsa.mk, doc/Make.hs: Changed the extension associated with
	cpsaparameters output from .params to _parameters.txt.

2010-12-09  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/Tree.hs: Dump commented out copy of the old
	algorithm.

	* src/CPSA/Graph/ExpandedView.hs (kdrawer): Replaced tree
	sorting with a queue to produce a breadth first ordering of the
	tree on output.  This change has a big impact on performance on
	large inputs.

2010-12-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/ExpandedView.hs (zoomControl): Omit need to run a
	script at load time by adding the attribute onchange="zoom(event)".

2010-12-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/ExpandedView.hs: Changed the scripting to better
	support very large documents.  Instead of running a script to
	insert the new control, this version builds the controls into the
	document.  The script run a load time just registers event
	handlers.

	* src/CPSA/Graph/Tree.hs (forest): Changed data structures used to
	form the forest so as to replace linear searches on lists with
	binary searches on maps and sets.

2010-12-01  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version):  Tagged as version 2.2.0.

2010-11-29  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/Preskeleton.hs (addNode): Use the color blue to
	distinguish realized reception nodes from transmission nodes.

	* src/CPSA/Lib/Strand.hs (augment): Removed hullForAugmentation.
	Hulling is now always performed after contractions, regular
	augmentations, and listener augmentations.

2010-11-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/*.hs: Added support for the cpsagraph option
	--zoom.  This option adds support for SVG diagram scaling in
	the expanded format, the one that generates an XML compound
	document.  If the browser supports HTML5 sliders, cpsagraph
	generates them, otherwise, it generates old style drop down lists.

2010-11-19  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/*.scm: Updated examples to use herald forms.

	* src/CPSA/Lib/Main.hs (getHerald): Added support for a herald
	form that allows options specified on the command line to be
	specified within an input file.

	* src/CPSA/SimpleDiffieHellman/Algebra.hs (outFlow, inFlow):
	Updated to handle (gen) and (exp h x).

2010-11-16  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (testStrand): Corrected a flaw in which
	this function incorrectly computed the public messages available
	at a node when the node ordering is reversed, such as when using
	the -r option or a reverse-search role hint.

2010-11-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Diff/Main.hs (main): Added cpsadiff, a program that
	compares CPSA output files S-expression by S-expression, and
	prints the first skeleton that differs.

	* src/CPSA/Lib/Protocol.hs (Role):  Added the rsearch boolean that
	is used to determine the order in which a strand is searched for a
	test node.  The search is reversed if the role includes the
	"reverse-search" key as one of its comments.

	* src/CPSA/Lib/Entry.hs (gentlyReadSExpr): Added a version of the
	S-expression reader that gently fails on error by printing the
	error message to standard error and returning EOF.  Changed
	cpsagraph, cpsashapes, and cpsapp to use this reader.  That way,
	an aborted run can be processed by these programs.

2010-11-05  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.1.2.

	* src/CPSA/Lib/Main.hs (interp): Enabled displacement by default,
	and changed the sense of the -d option.

2010-10-25  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/SimpleDiffieHellman/Algebra.hs: Changed algebra
	signature so that gen is a constant.

2010-10-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (homomorphismFilter): Added a filter that
	ensures there is a homomorphism from the parent to each member of
	a cohort.

2010-10-20  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (hullByDeOrigination): Added a mode to
	hulling based on deorigination.

2010-10-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/SimpleDiffieHellman/Algebra.hs (loadVar): For now,
	variables of sort base are forbidden to deal with missing
	contractions in the Diffie-Hellman Man-In-The-Middle example.

2010-10-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/SimpleDiffieHellman/Algebra.hs: Made the Simple
	Diffie-Hellman algebra what one gets where one requests the
	algebra diffie-hellman.

2010-10-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/{Basic,SimpleDiffieHellman}/Algebra.hs (places,
	replace): Corrected these definitions so that they handle
	occurrences of variables without a sort inclusion function.  For
	example, the old version would not find I when in akey(invk(I))
	when looking for the places at which akey(I) occurs.

2010-10-13  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/SimpleDiffieHellman/Algebra.hs: Added an implementation
	of the Simple Diffie-Hellman algebra, one that supports only
	commutativity in exponents.

	* src/CPSA/SimpleDiffieHellman/Algebra.hs (foldCarriedTerms,
	carriedPlaces): Despite there names, these two functions follow
	the definition of heldBy, not carriedBy.

  	* src/CPSA/Lib/Protocol.hs (originates, originationPos): carriedBy
	-> heldBy.

	* src/CPSA/Lib/Cohort.hs (testNode): carriedBy -> heldBy.

	* src/CPSA/Lib/Strand.hs (gainedPos, preskelWellFormed)
	(deleteNodeRest): carriedBy -> heldBy.

2010-10-12  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs: Changed the signature of unify and
	match so they return a list rather than a Maybe.

2010-10-06  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs (specialize): Added code to
	specialize an environment by mapping all generated variables to
	one.  This is used when producing an environment for an instance.

2010-10-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/DiffieHellman/Algebra.hs: Modified algebra so that
	bases are no longer atoms, and implemented a more realistic
	version of derivability.

2010-10-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs: Added heldBy to support
	Diffie-Hellman.

2010-09-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Notation.hs (mesg): Use [x,y,..]k instead of
	E(k;x,y,...).

2010-09-17  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/LaTeXView.hs (writeLnPreskel): Add Tree number
	before printing a protocol.

2010-09-10  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.1.1.

	* src/CPSA/Graph/Tree.hs (assemble): To handle incomplete outputs,
	assemble ignores unavailable seen children instead of signaling an
	error.

2010-08-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (augCollapses): Pruning is now performed
	only after augmentation, and only when the augmented strand is
	involved.

2010-08-12  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/LaTeXView.hs (matrix):  When drawing a skeleton,
	communication edges between nodes with different messages is shown
	with a dotted arrow as is already done for SVG diagrams.

2010-08-09  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Notation.hs: Added an infix notation for XHTML and
	LaTeX output.  Enable by specifying the -i flag when invoking
	cpsagraph or cpsapp.

2010-07-29  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.1.0.

2010-07-23  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Cabal-Version): CPSA now assumes Cabal is version
	1.6 or greater, and support for GHC 6.8 has been withdrawn.

	* src/CPSA/Graph/Loader.hs (loadDefs): The graph program displays
	the initial comments in an input file.

2010-07-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Main.hs (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

2010-07-09  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (contractAndOrder): Support for this
	addition to authentication test solving has been removed.

	* src/CPSA/Lib/Cohort.hs (contractions): Contraction has changed
	so that it only solves the test for one position of the critical
	message in the test node, not every position.  Previously, CPSA
	was missing most general solutions due to contracting too many
	positions at the same time.

	* src/CPSA/Lib/Strand.hs (pruneStrands): The pruning condition now
	checks to see that there is a variable renaming between the
	preskeletons involved.  Previously, the only check ensured the map
	was idempotent.

2010-07-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (useEcapeSetInTargetTerms): Added an
	option to include the escape set in the set of target terms.

2010-06-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (gainedPos): In a skeleton, a node with a
	uniquely originating atom that is gained must be after the node of
	origination.  It used to be that only nodes in which the atom is
	acquired must have the ordering.

2010-06-18  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.0.5.

	* doc/cpsatheory.tex: Added theory document on authentication
	tests.

2010-06-11  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (augCollapses): Added a collapsing phase
	after adding a strand so that hulling succeeds without when
	origination points on augmented strands move.

	* src/CPSA/Lib/Strand.hs (hull): Added a better algorithm for
	finding pairs of strands to hull.

2010-06-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (cowt): As does cows, the cowt has to
	iterate to ensure all places are considered.  This change fixes
	the bug exposed by the tst/non_transforming.scm text case.

2010-06-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (transformingNode): Removed junk in
	output by applying the mgu filter to more substitutions used to
	construct augmentations.  This fix has a dramatic effect on
	performance for the NSL4 and NSL5 test cases.

2010-05-06  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (cows): Update function to better match
	correctness result in the upcoming algebra paper.

2010-04-28  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.0.4.

	* cpsa.cabal: Base versions are now base >= 3 &&< 5.

2010-04-20  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (acyclicOrder): Fix acyclic check by
	analyzing all edges in graph, not just communication edges.

2010-04-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (firstSkeleton): Input skeletons are no
	longer pruned.

2010-03-30  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.0.3.

	* src/CPSA/Lib/Cohort.hs (useEncryptionFirstOrder): Added switch
	to determine critical message search order.

	* src/CPSA/Lib/Strand.hs (skelNons, skelUniques): Use inheritRnon,
	and inheritRunique for inherited origination assumptions.

2010-03-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/pp.pl: Added an SWI-Prolog version of the pretty printer in
	CPSA.Lib.Pretty.

	* src/cpsa.pl: Added an SWI-Prolog version of the CPSA specific
	pretty printer in CPSA.Lib.Printer and support for skeleton
	transformations.

2010-03-11  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.0.2.

	* src/CPSA/Graph/Loader.hs (itrace): When computing the trace of
	an instance, use the traces comment if it is available.

2010-03-11  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.0.1.

2010-03-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/cpsa.el: Added Emacs support for skeleton transformations.

2010-03-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (rootName):  Improved renaming
	algorithm used to avoid collisions while printing variables.

2010-03-05  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (roleOrigCheck): Added check that
	unique origination position is preserved by inheritance.

2010-03-04  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 2.0.0, the first release
	for the public.

2010-03-01  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/SExpr.hs (load): Load now returns one S-expression
	per call.

2010-02-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Loader.hs (loadPosBaseTerm): Added a missing check
	that ensures a non-originating term at given length is an atom.

	* doc/Make.hs (cpsa): Made *.sch the extension for problems
	that use Diffie-Hellman.

2010-02-15  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.5.5.

	* src/CPSA/Lib/Loader.hs:  Added better error messages for roles
	and preskeletons that are not well formed.

2010-02-13  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs:  Enforce a canonical form for terms
	so that term equality is just structural equality.

2010-02-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (testNode): Changed order in which
	critical message are picked to look at encryption tests before
	nonce tests.

2010-02-05  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.5.4.

2010-02-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (origCheck): For pruning, added a check
	that insures that origination assumptions are honored by the
	homomorphisms associated with pruning.

2010-01-29  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsauser.html (Visualization): Added a comment that notes
	that cpsagraph draws dashed lines between nodes with terms that
	are equivalent, but not syntactically identical.

	* src/CPSA/Lib/Strand.hs (Preskel): Preskeletons retain a comment
	that is given in the input.

2010-01-21  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsa.mk (%.sch): Added a rule that runs CPSA with the
	Diffie-Hellman algebra for *.sch files.

	* tst/completeness-test.scm: Added new example

2010-01-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (copresentVertices): Fixed a bug, and now
	contractions with ordering codes works, when
	Cohort.useContractionsWithOrdering is True.

2010-01-06  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.5.3.

2009-12-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (mgus): Enabled mgu filtering on
	contractions and regular augmentation.

2009-12-20  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (moreGeneral): Original implementation
	failed to consider variables in the range of the more general
	substitution.

2009-12-17  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/Preskeleton.hs (addEdge): In a skeleton diagram,
	an edge between nodes that do not agree on their message is
	displayed with a dashed line.

2009-11-16  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.5.2.

2009-11-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (precedesCheck): Added the requirement to
	pruning that ordering relations associated with the more
	general (pruned) strand are implied by the less general strand.

2009-10-31  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Protocol.hs (Role): Added support for delaying the
	inheritance of a role non-origination assumption by adding a
	length specification to role non-origination declarations.

2009-10-26  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.5.1.

2009-10-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (specialization): Generalization no
	longer uses pruning.

2009-10-24  John D. Ramsdell  <ramsdell@mitre.org>

	* license.txt: Changed license to BSD.

2009-10-15  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.5.0.

2009-10-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/preskel.sh: Added a script to change defpreskeleton to
	defskeleton.

	* src/CPSA/Lib/Loader.hs (loadSExpr): Changed defpreskeleton
	keyword to defskeleton.

2009-10-10  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Extra-Source-Files): Added files left out of a
	distribution so that the documentation compiles.

	* {doc,tst}/README: Added a doc and tst read me

2009-10-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (checkOrigs): Isomorphism orig check now
	uses matching.  Isomorphism checking now works in diffie-hellman.

2009-10-01  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs (encryptions): Encryptions that occur in
	other encryption are now required to be later in the list.

	* cpsa.cabal (Version): Tagged as version 1.4.9.

2009-09-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (roleOrigCheck): Role origination check
	is now omitted when the inheriting strand is too short to inherit
	a unique origination assumption.

2009-09-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (useMguFilter): Turned off all mgu
	filtering for contractions and augmentations.

	* src/CPSA/Lib/Algebra.hs: Changed signature for unification and
	matching so as to pass through a variable generator for
	Diffie-Hellman.  Threaded the variable generator throughout the
	library as needed.

	* src/CPSA/Diffie-Hellman/Algebra.hs:  Added a module for
	analyzing protocols that use Diffie-Hellman.  Its unifier and
	matcher make use of fresh variable generation.

2009-09-16  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (mgus): Added a filter that removes
	non-most general unifiers from a list of contractions after the
	list has been filtered to ensure each member solves the test.  For
	each role considered during augmentation, added a filter that
	removes non-most general unifiers from the list of augmentations
	after the list has been filtered to ensure each member solves the
	test.

2009-08-28  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (testDestroyingContractions): Added a
	filter that removes non-most general unifiers from the generated
	list of potential contractions.

2009-08-18  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Displayer.hs (displayOpTerm, displayOpTerms): Terms
	in the operation field may contain variables not in the skeleton.
	Two functions were added for printing terms is the operation
	field.  These functions extend the display context as needed.

2009-08-05  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.8.

	* tst/{encsig.scm,sigenc.scm}: Added tests for labeled named akey
	operations.

2009-08-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs:  Added labeled named akey operations
	(pubk STRING ID) and (privk STRING ID).

2009-08-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs (lte):  Added more general substitution
	predicate to the algebra interface.

2009-07-24  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.7.

	* src/CPSA/Lib/Strand.hs (permutations): Reversed the order in
	which strands are matched, and found a big performance
	improvement.

	* src/CPSA/Lib/Loader.hs (loadRole): Unused variables in a role
	are now silently dropped instead of causing an error message.

2009-07-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (permutations): Intertwined the
	computation of permutations with the substitutions that match
	traces.

2009-07-11  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.6.

2009-07-08  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaprimer.tex (Section Advice): Added a description of how
	to use CPSA for protocol design and made other improvements.

2009-07-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (maybeAug): Use a role's trace as a
	template instead of generating a fresh instance for that purpose.

2009-07-01  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/LaTeXView.hs (latexView):

2009-06-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (solve): The top-level search loop is now
	implemented in the IO monad using tail recursive functions so as to
	ensure data is released when it should.

2009-06-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (solve): Added no isomorphism checking
	mode (--noisochk).  In noisochk mode, isomorphism checks are
	avoided by not identifying duplicate skeletons and by not
	generalizing realized skeletons.

	* src/CPSA/Lib/Search.hs (Params): Collected runtime parameters
	into a record.

	* src/CPSA/Lib/Search.hs (dump): Dump no longer generalizes
	realized skeletons.  It just dumps them quickly.

2009-06-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (generalize): Perform variable separation
	last as it could take a long time.

2009-06-17  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaprimer.tex: Updated the Needham-Schroeder example, added
	the collapsing operation, and fix other minor problems.

2009-06-14  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsadesign.tex: This document was rewritten.  It now assumes
	its reader have already read the CPSA specification
	(doc/cpsaspec.tex).  As a result, it focuses on implementation
	issues, and leaves correctness issues to the specification.

2009-06-11  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (instRnon,instRunique): Filter
	origination assumptions using the terms in the instance's trace.

	* src/CPSA/Lib/Strand.hs (separateVariable): Don't memoize subsets
	computation.  It causes memory problems when a large permutation
	is used infrequently.

2009-06-10  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.5.

2009-05-29  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (isomorphic): Don't memoize
	permutations--can cause excessive use of memory.

2009-05-28  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Entry.hs: Code common to several programs has been
	moved into the Entry module and shared.

2009-05-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/{Search.hs,Expand.hs}: CPSA now expands macros
	rather than using a preprocessor for the task.  The cpsapp program
	now just pretty prints its input.

	* src/CPSA/Pretty/Main.hs: The source for the cpsapp program has
	moved into another directory as it no longer macro expands its
	input.

	* doc/cpsa.mk: Makefile no longer has preprocessor support.

	* doc/cpsaoverview.tex: Add a short overview of CPSA.

	* src/CPSA/Annotations/Formulas.hs (keywords): "t" and "f" are no
	longer keywords in formulas.  Use (and) for truth and (or) for
	falsehood.

2009-05-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Macros/Main.hs (prettyPrint): Add -p option so that
	cpsapp pretty prints without macro expansion.

	* doc/cpsa.mk: Makefile now save preprocessor output.

2009-05-12  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.4.

	* cpsa.cabal (Flag par): Changed the default for the par flag to
	true so that CPSA is compiled with multiprocessor support by
	default.

2009-05-11  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/SExpr.hs (Tokens): Added strictness annotations
	that allows the reading of much larger input files and improves
	performance.

2009-05-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (collapse): Added the collapse operation
	which applies to a shape.  It attempts to unify pairs of strands
	and searches for shapes starting from the results.

	* src/CPSA/Shapes/Shapes.hs (shapes): Reduced memory requirements
	by use of shape notes and added support for output in which a
	shape is a descendent of a shape.

2009-05-09  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (commentPreskel): Added a shape note to
	be used by the cpsashapes program.

2009-05-07  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (hull, enrich, prune): With the
	correction of the pruning algorithm, the preskeleton reduction
	rules are now applied in the order of hull, enrich, and then
	prune.

2009-05-05  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaspec.tex: Added the sources to the CPSA document that
	specifies CPSA as a reduction system.

2009-05-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (pruneStrands): The pruning operation
	now uses a substitution that is idempotent for strands other than
	the pruned strand.

2009-04-29  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.3.

	* src/CPSA/Lib/Cohort.hs (specialization): The homomorphism check
	is applied to the preskeleton because it matches the strand
	mapping.  This fixes a bug that reject some valid generalizations.

2009-04-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs (Subst): A substitution is now required
	to be ordered.

	* src/CPSA/Basic/Algebra.hs (unifyChase): The exported version of
	a substitution no longer requires chasing to find the canonical
	representative of the equivalence class of variables determined to
	be equal.  This means there is a canonical representation of an
	external version of a substitution that is ordered.

	* src/CPSA/Basic/Algebra.hs (substitute): Corrected a bug in
	substitution associated with variables of sort mesg.  The
	correction effects tst/dy.scm only.

2009-04-18  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (IdMap): Use Data.Map Id Term for
	substitutions instead of association lists.

	* src/CPSA/Basic/Algebra.hs (loadVar): Removed sort "term" as a
	synonym for "mesg".

2009-04-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (compose):  Corrected a bug in the
	code that removes the trivial bindings from s2 to form s4.  The
	fix changes the output for tst/dy.scm.

2009-03-30  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.2.

2009-03-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (parMap): Added support for SMP
	parallelism.  To enable, configure with -fpar.

2009-03-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Printer.hs: Added a CPSA specific pretty printer
	and made it so that the roles in protocols are laid out using the
	group layout.

2009-03-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Pretty.hs (grp): Added support for the group layout
	and used it for the top-level lists.

2009-03-01  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (unifyTerm): For contraction, the
	unifyOnPaths function does not check to see if its result has the
	desired properties and it turns out that sometimes it doesn't.
	Now unifyTerm repeats its operations until the desired properties
	hold.

	* src/CPSA/Lib/Cohort.hs (unifyPast): For augmentation, the
	original unifyPast failed to each to see if the final result has
	the desired properties, and it turns out that sometimes it
	doesn't.  Now unifyPast repeats its operations until the desired
	properties hold.

2009-02-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Loader.hs (loadInsts): Check for preskeletons
	with no strands.

2009-02-21  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Parameters/Main.hs,Flow.hs: Added a data flow analysis
	of roles.

2009-02-16  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.1.

	* doc/*: Update document to reflect changes.

2009-02-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Macros/*.hs: Added the macro preprocessor cpsapp.

2009-02-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Annotations/Annotations.hs (loadFormulas): Allow base
	terms as principals so as to allow keys as principals.

2009-01-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (changeLocations): Changed variable
	separation so that so that two candidates are generated for a
	location configuration, one that maps the changes to uniques, and
	the other does not.  This fixes a generalization bug.

2009-01-31  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (solved): The cohort is now filtered so
	that every member is solved.

2009-01-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (changeLocations): When separating a
	uniquely originating base term, either the term or its clone is
	uniquely originating.

2008-12-28  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (Symbol): Removed tag as a sort, and
	made tags constants of sort mesg.

2008-12-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (matchVarRenaming): Use sets to
	improve injective test.

2008-12-09  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.4.0.

2008-12-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (nextState): Added the --dfs command line
	option to allow the selection of depth first search.

	* src/CPSA/Graph/SVG.hs (kbutton): Duplicate nodes are now
	rendered in italic so as to make it easier to distinguish them
	from tree nodes.

	* src/CPSA/*/{Main.hs,Search.hs}: Added default option values to
	command line help message.

2008-12-03  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs: Allowed variable declaration forms to
	declare more than one variable of a given sort.

	* src/CPSA/Basic/Algebra.hs: Added the sort data, a second
	sort similar to sort text.  The second sort can be used to
	partition nonce-like data from ordinary text-like data.

	* src/CPSA/Basic/Algebra.hs: Changed the symbol used for the top
	sort from "term" to "mesg".

	* src/CPSA/Lib/SExpr.hs (isStr): The characters that make up a
	string are the ASCII printing characters omitting double quote and
	backslash.

2008-12-02  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (nextState): Switched back to
	breadth-first-search and removed support for parallelism.
	Breadth-first-search makes it more likely shapes are printed in
	ill-fated runs.

	* src/CPSA/Graph/Main.hs (interp): Changed the default output
	format to expanded format.

2008-12-01  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.3.2.

2008-11-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (roleOrigCheck): Added new well-formed
	preskeleton check.  Every uniquely originating role term mapped by
	an instance must be mapped to a term that originates on the
	instance's strand.

2008-11-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (nextState): Switched to
	depth-first-search by adding freshly generated skeletons to the
	front of the to do list.

	* src/CPSA/Lib/Strand.hs (isomorphic): Added same number of
	variables in isomorphism check to speed it up.

	* src/CPSA/Lib/Algebra.hs: (matchVarRenaming) The special purpose
	renaming detector was eliminated in favor of using matching and
	predicate that decides if a match is one-to-one and
	variable-to-variable.

2008-11-16  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (deleteNode): Use the transitive closure
	of the communication ordering before deleting a node.  This change
	fixes a minimization bug.

2008-11-14  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.3.1.

	* src/CPSA/Lib/Cohort.hs (addListeners):  Listeners are now added
	only for the decryption keys of the top most encryptions in the
	escape set.  This fixes a bug caused by adding listeners for
	decryption keys of internal encryptions in the escape set.

	* src/CPSA/Lib/Algebra.hs (decryptionKey):  Changed the name from
	keysUsedBy to reflect the fact only the decryption key from the
	top most encryption is returned.

	* src/CPSA/Lib/Algebra.hs (protectors): Changed the name from
	decrypts to better reflect the purpose of the function.

2008-11-10  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Annotations/Annotations.hs (obligations): The alist key
	theorems was replaced with obligations as it lists the formulas
	one is obligated to show are theorems to show the protocol is
	sound.

2008-11-07  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.3.0.

	* doc/cpsauser.html:  Added cpsaannotations documentation.

2008-11-02  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsadesign.tex: Added a complete draft of the algorithm part
	of the design document.

2008-10-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (deleteNode): When deleting a strand,
	this function used to apply the inverse of the correct permutation
	to the prob field, but now applies the correct permutation.

2008-10-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/Main.hs (options): Add --compact option to select
	the use of the compact output format.

2008-10-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (targetTerms): Added term extraction from
	the escape set for use as targets for binding with the carried
	terms in an outbound when looking for a transforming node.  This
	change allows CPSA to find the flaw in the Dolev-Yao Example 1.3
	test case.

2008-10-14  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (augmentations): Changed the augmentation
	algorithm to use foldCarriedTerms.

	* src/cpsacgi.py: Added expanded graph output to the CGI script.
	Added support for annotations.

2008-10-13  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/cpsaprimer.tex: The CPSA Tutorial was renamed to the CPSA
	Primer.

2008-10-08  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (forgetAssumption): Fix a bug that allows
	assumption forgetting to work again.

2008-10-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Algebra.hs (loadEnc): When enc has more that two
	terms, a concatenation is added to all but the last term.

	* src/CPSA/Lib/Strand.hs (tryPerm): An isomorphism testing bug was
	fixed.  The permutation map was applied to the wrong ordering.

2008-10-03  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.2.3.

	* src/CPSA/Graph/ExpandedView.hs (header): The title generated for
	the expanded view now includes the name of the first protocol to
	be graphed.

	* src/CPSA/Lib/Search.hs (search): The comment generated for
	non-default strand bounded or step count limited runs contained
	an illegal character that has been removed.

	* src/CPSA/Basic/Algebra.hs (displaySubst): This function displays
	substitutions without requiring that the sort of every variable be
	known.  The function that infers enough sort information to
	perform the display was correct, thus fixing a reported bug.

2008-09-30  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs (Context): Changed the interface to
	contexts to allow them to be extended.  Also, eliminated
	displayEnv from the Context type class.  It can be written using
	other functions in the interface.

2008-09-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Cohort.hs (transformingNode): The fix on the 22th
	wasn't right, it unified on all outgoing terms.  The function now
	unifies an outgoing term only when it is a transforming node.

2008-09-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/*/*.hs:  Loading works with all monads.  With this
	change, there is no longer a need for using the flexible instances
	language extension.

2008-09-23  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.2.2.

2008-09-22  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Cabal-Version): Updated to use Cabal 1.2 section
	syntax.

	* src/CPSA/Lib/Cohort.hs (transformingNode): Changed the
	augmentation algorithm so that it continues looking for more
	transforming nodes farther down a trace after it finds one
	transforming node.

	* src/CPSA/Lib/Search.hs (par): Added HAVE_PAR preprocessor symbol
	which should be defined when Control.Parallel is available.

	* src/CPSA/*/*.hs:  A major code clean up was completed.

2008-09-17  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (Gist): Created a data structure designed
	to support only skeleton isomorphism checks, thus improving the
	performance and memory requirements associated with the check.

2008-09-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Annotations/*.hs: Added the cpsaannotations program
	that propagates annotations on protocols to annotations on
	realized skeletons.

2008-09-06  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Main.hs (main): Algebras export a name and the
	origin used to generate fresh variables.

2008-08-29  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (weakenOrderings): Corrected a bug by
	adding the strand succession edges before taking the transitive
	closure.

2008-08-25  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.2.1.

2008-08-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (weakenOrderings): Changed the weakening
	algorithm so as to use the transitive closure.  The result is all
	possible weakenings are considered, and a reported bug was fixed.

2008-08-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Graph/ExpandedView.hs (kdrawer): Added the definition
	of the marker for arrow heads so that arrow heads now appear in
	preskeleton drawings.

2008-08-18  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.2.0.

	* src/CPSA/Lib/Utilities.hs (permutations): Used permutations from
	Haskell 1.3 as a model, and ensured the identity permutation is
	the first one in the result.

	* doc/cpsatutorial.tex, doc/cpsauser.html: Changed the
	introductions to note that the search for shapes in the current
	implementation is known to be not complete.  See tst/dy.scm.

2008-08-11  John D. Ramsdell  <ramsdell@mitre.org>

	* tst/Makefile: Changed the file extensions to be consistent with
	the ones used in doc/cpsa.mk.

	* src/CPSA/Basic/Loader.hs: Added tags as non-atomic terms, and
	removed tagged concatenation.

	* src/CPSA/Graph/ExpandedView.hs: Added support for the expanded
	view option (-x) in cpsagraph.

2008-08-04  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal: Added support for local installation.

	* doc/cpsa.mk: Added GNU Make rules for inclusion.

	* src/CPSA/Lib/Search.hs: Reorganized search loop so that
	S-expression printing is done outside the search code.

	* src/CPSA/Lib/Search.hs: Modified the abort dump routine so that
	it minimizes when it is asked to print a realized skeleton.

2008-07-31  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/*/Loader.hs: Ignore top-level S-expression of the form
	(comment S-EXP*) rather than signal an error so as to allow file
	level comments as S-expressions.

	* src/CPSA/*/*: Renamed cpsabasic to cpsa, as that program can now
	provide support for more than one algebra.

2008-07-28  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs: Added foldTerms to interface. It folds
	a function through a term applying it to each term that occurs in
	the term.

2008-07-26  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Algebra.hs: Added carriedPlaces and ancestors to
	the interface and moved existsOnAllPathsToTarget and
	foldOnAllPathsToTarget to CPSA.Lib.Cohort as they no longer need
	to be implemented by each algebra.

2008-07-25  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/*/*.hs: Reorganized the algebra interface so that as
	algebra exports an algebra specific protocol loader so as to allow
	CPSA to handle more than one algebra at a time.  Algebras are now
	linked into the program in CPSA.Lib.Main.

2008-07-24  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs: Added the --bound option to limit the
	number of strands in a skeleton.

2008-07-15  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (validateSubst): Changed the result of a
	failure to find a uniquely-originating atom to False rather than
	an signaling an error.  The addition of unique origination
	assumption forgetting makes this case no longer an error.

2008-06-16  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Basic/Main.hs (compose): Use algorithm from Handbook of
	Automated Reasoning, remembering to delete identity bindings.

2008-06-05  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as version 1.1.0.

	* doc/cpsadesign.tex: Added document status and other small
	improvements in preparation for release.

2008-05-27  John D. Ramsdell  <ramsdell@mitre.org>

	* doc/strands.mp: Placed strand macros in a separate file.

2008-05-23  John D. Ramsdell  <ramsdell@mitre.org>

	* src/httpd_allow_execmem.te: Added this SELinux refpolicy module
	so as to allow Haskell to run as a CGI script.

2008-05-22  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Displayer.hs (displayOperation): Changed the
	wording for the operation used to derive a skeleton.

2008-05-19  John D. Ramsdell  <ramsdell@mitre.org>

	* src/cpsa.{sh,py}: CGI scripts modified to work with SELinux.

2008-05-13  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Shapes/Main.hs: Added output margin option.

	* src/CPSA/Lib/Strand.hs (Method): Added a parameter to each
	minimization method.

2008-05-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Strand.hs (forgetAssumption): Added the
	origination assumption forgetting minimization operation.

2008-05-04  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Search.hs (options): Added output margin option.

2008-04-30  Joshua D. Guttman  <guttman@mitre.org>

	* src/CPSA/Basic/Main.hs: Re-enabled indeterminates

2008-02-27  John D. Ramsdell  <ramsdell@mitre.org>

	* src/CPSA/Lib/Protocol.hs: Add a comment field in protocols and
	roles.

2008-02-20  John D. Ramsdell  <ramsdell@mitre.org>

	* cpsa.cabal (Version): Tagged as 1.0.0, the initial release.