cpsa-2.2.0: ChangeLog
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.