Changelog for cpsa-3.6.10

2022-03-20 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.10 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. 2022-01-04 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.9 2021-12-08 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (origUgenDiffStrand): Expunge skeletons that have a value that is both uniq orig and uniq gen, and start on different strands. 2021-11-12 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.8 2021-11-05 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (addBaseListener): Added a stronger method for solving some Diffie-Hellman authentication tests. The method handles the special case in which the critical term has the form (exp (gen) (mul ...)) and all of variables in the exponent are random exponents (rndx). It uses baseRndx to add listeners. * src/CPSA/DiffieHellman/Algebra.hs (baseRndx): When all of the factors in a group use rndx variables, baseRndx returns a list of concatenations of each variable with the base term exponentiated with the group without the variable. 2021-11-02 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Graph/ExpandedView.hs (tdrawer): Added POV link in tree. 2021-09-10 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/lib/Expand.hs (macroExpand): Made it an error to apply a macro to the wrong number of arguments. 2021-04-27 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.7 2021-04-27 Joshua D. Guttman <guttman@mitre.org> * cpsa.cabal: Clarified package description (deorigination) 2021-04-14 John D. Ramsdell <ramsdell@mitre.org> * Makefile: Vastly simplified. 2020-10-27 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Data-Files): Added missing examples to Data-files. 2020-05-21 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.6 2020-05-15 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (rlugen): Replaced an incorrect call to originationNodes to be a call to generationNodes. This fixes a bug when using the ugen predicate in the conclusion of a rule. 2020-05-15 Moses D. Liskov <mliskov@mitre.org> * src/CPSA/Lib/Strand.hs (preskelWellFormed): Added a check that all variables used in any terms in any declarations are used in the terms of the traces. * src/CPSA/Lib/Strand.hs (verbosePreskelWellFormed): Made a similar change, but without removing existing more specific messages that may be informative for users. 2020-04-15 Joshua D. Guttman <guttman@mitre.org> * src/CPSA/Lib/Strand.hs (graphCloseAll): Added a procedure to generate a transitive closure that includes pairs on the same strand. Adapted gprec to use it. 2020-04-02 Ian D. Kretz <ikretz@mitre.org> * src/CPSA/Latex/Main.hs (main): Remove number from pubk, privk newcommand 2020-03-31 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs (Preskel): Added support for unique generation assertions. 2020-03-20 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Update version number as 3.6.6 2020-03-04 Moses D. Liskov <mliskov@mitre.org> * src/CPSA/Prot/Main.hs (main): Added support for state to cpsaprot. 2020-02-27 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (probIsomorphic): Added quick checks for thinning isomorphism check. 2020-02-20 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Prot/Main.hs (main): Improved error messages and added (chmsg TERM) form for channel messages and clone for roles. 2020-02-13 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Prot/Main.hs (main): Added cpsaprot program. 2020-02-11 Kretz, Ian D <ikretz@mitre.org> * src/CPSA/LaTeX/Main.hs (main): Added cpsa2latex program. 2019-11-26 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/GoalSat/Main.hs: Added cpsagoalsat program. 2019-11-12 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.5 * src/CPSA/Lib/Strand.hs (tryPermProb): Rewrote tryPermProb so that it uses tryPerm. 2019-11-08 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (tryPermProb): Added missing invperm to the third line of tryPermProb, and reenabled multistrand thinning. 2019-10-21 John D. Ramsdell <ramsdell@gootoo.mitre.org> * cpsa.cabal (Version): Tagged as 3.6.4 2019-10-21 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Utilities.hs: Used the C preprocessor to allow compilation using older versions of GHC. 2019-10-15 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Utilities.hs: Updated code to support the removal of fail from Monad as implemented in base-4.13.0.0. 2019-09-16 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (thinManyStrands): Replaced isomorphic check with probIsomorphic check so that strands in the point-of-view remain unmodified. 2019-08-26 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.3 2019-08-22 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (doRewritesLoop): Fixed the code that counts rewrite rules applied so it is accurate. This allows the rewrite rule limit to be correctly enforced. 2019-08-21 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (runiqAt): Ensured that rewriting with uniq-at fails when the index is greater than the strand length. 2019-08-19 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Init/Main.hs (main): Added program cpsainit. The programs copies the files Makefile, cpsa4.mk, Make4.hs, and template.lisp from the CPSA data directory to the current directory, thereby easing the task of starting a CPSA project. 2019-07-15 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/State.hs: Removed the label field in a transition. The field was always ignored, and it causes confusion on input. 2019-06-26 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (multiset): Used multisets of trace briefs to reduce the number of full permutation isomorphism checks. 2019-06-21 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (brief): Added a summary of trace that reduces the need for matching during isomorphism checking. 2019-06-04 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Reduction.hs (begin): Reversed todo list after running rules so as to get the output order correct. 2019-05-20 Joshua D. Guttman <guttman@mitre.org> * src/CPSA/Lib/Strand.hs (tryPerm): Fixed bug in isomorphism checking. Checking of facts used wrong environment. 2019-05-17 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs (leadstoKey): Added support for leadsto in shape analysis sentences. * src/CPSA/Lib/Strand.hs (kfactVars): Allow message variables in facts that occur nowhere else. (useFactVars): Add flag that disables message variable in facts that occur nowhere else and disable it, because isomorphism checking is broken. * src/CPSA/Strand.hs (doRewriteOne): Values associated with existential variables in rules are freshly generated so that parameter terms can be compound. 2019-04-03 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (verbosePreskelWellFormed): Added a check that ensures the every variable that occurs in a fact also occurs in some strand. 2019-03-18 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.2 2019-02-22 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Reduction.hs (addAnnoKey): Added structured annotations to skeleton output to facilitate post processing programs besides cpsagraph. The new keys are (aborted), (satisfied-all), and (dead). 2019-02-04 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Reduction.hs (step): Changed default depth bound to zero representing no bound and ignored the check when the bound is not positive. This matches what is documented in the manual. 2019-01-31 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Loader.hs (badKey): Added checks for bad keys in alists for skeletons ("defstrand" and "deflistener") and protocols ("defrole" and "defrule"). 2018-11-28 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Protocol.hs (AForm): Added the leads-to predicate to the goal language. 2018-11-19 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Printer.hs (formula): Added special pretty printing rules for formulas in defgoal and defrule. 2018-11-09 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs (loadPOV): Use a preskeleton as a POV instead of insisting on using a skeleton. 2018-08-29 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.1 2018-08-22 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Strand.hs (doRewrites): Added a limit on the number of rules that can be applied after solving an authentication test. 2018-08-20 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (cleansPreskel): Cleansed facts from a skeleton purged of a strand. This changes fixes a nasty display bug that occurred when a variable in a fact did not occur in any strand. 2018-08-06 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Loader.hs (loadConclusion): Removed mode flag as this routine should always be using mode RoleSpec. This resolves a bug in which CPSA could not load a Shape Analysis Sentence as rule because equality was before the protocol specific formulas. * src/CPSA/Lib/Strand.hs (newPreskel): Changed newPreskel so that it removed duplicates in the leadsto field when creating a new preskeleton. This resolved a bug in which CPSA produced to shapes that appeared to be isomorphic, but instead, one shape had duplicates in its leadsto field. 2018-06-25 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.0 2018-06-18 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (gparam): Added support for binding the strand variable in gparam as opposed to relying on it being bound by a role length predicate. 2018-06-11 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/*.hs: Implemented geometric formulas as rewrite rules. The rules are applied after each cohort step. 2018-06-05 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/*.hs: Converted the goal language to be strand-oriented. The goal language in incompatible with the previous, node-oriented language. 2018-05-22 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Cohort.hs (unrealizedInNode, nextNodeA): Lifted to top-level to satisfy new ambiguity check in GHC 8.4.2. 2018-04-17 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.5.0. 2018-03-20 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/DiffieHellman/Algebra.hs (displayVar, mkVar): Changed sort names. expn -> rndx and expr -> expt. 2018-02-12 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs (disjoin): Changed output to (false) on an empty disjunction instead of (or). 2018-01-12 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Loader.hs (mkListenerRole): Changed do pattern to be irrefutable. 2017-09-15 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/DiffieHellman/Algebra.hs (unifyTerms): Added calls to chase before calling unifyBase which prevents a failure in the occurs check. 2017-09-14 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (tryPerm): Add missing inverse permutation to second checkOrigs in tryPerm. 2017-09-12 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal: Removed CPSA.Lib.CPSA globally and removed unnecessary dependencies. 2017-08-30 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal: Added missing modules and source repository location. * src/CPSA/Lib/DebugLibrary.hs (zi): Fixed erroneous parameters in Instance. 2017-08-28 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Cohort.hs (solved): Fixed condition 5. It was using ct instead of ct'. 2017-06-30 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Cohort.hs (transformingNode, maybeAug, nextNode): Rewrote code so that it no longer fails the ambiguity check. 2017-05-26 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/DiffieHellman/Algebra.hs (mkInitMatchDecis): Ensure initial distinctions to not include fresh variables. (partition): Do not move variables of sort expn to lhs, even if they are freshly generated. 2017-05-16 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/DiffieHellman/Algebra.hs (displaySubst): Removed erroneous substitution to fix substitution displaying. 2017-05-10 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Strand.hs (findReplacement, permutations): Merge generators so that no variable in a term has an identifier that is greater than or equal to the generator. 2017-02-02 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Basic/Algebra.hs (loadInvk): Added support for reading (invk (privk ...)) and (invk (invk ...)). 2017-01-17 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs (strandForm): Remove conjoin and use concatMap when creating a characteristic skeleton. 2017-01-09 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Loader.hs (loadPrimary): Removed generator parameter that was not used. 2016-12-21 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Cohort.hs (solved): In Condition 4, applied substitutions to the encryption keys before testing for derivability. 2016-10-04 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Basic/Algebra.hs (matchRenaming): Make isomorphism check work in presence of asymmetric keys. 2016-09-30 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Algebra.hs: Added isObtainedVar for variables of sort expr in the Diffie-Hellman algebra. 2016-08-12 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs (form): Changed "defsas" to "defgoal" as the keyword for a generated shape analysis sentence. This makes the program compatible with its documentation. 2016-06-22 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Extension): Add allow ambiguous types when compiling with GHC 8.0.0 or later. 2016-06-21 Moses D. Liskov <mliskov@mitre.org> * src/CPSA/DiffieHellman/Algebra.hs: Added code to implement the "tag" sort, which quoted string tags belong to. 2016-06-03 Moses D. Liskov <mliskov@mitre.org> * doc/examples/IKE_variants.tar.gz: Added this compressed archive of IKEv1 and IKEv2 variant input files. 2016-03-30 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs: Added support for fringe skeletons so that cpassas makes use of depth limited output. When a tree depth limit is exceeded, a fringe labeled skeleton is printed. cpsasas produces a sentence with a right-hand-side that encodes both the shapes and the fringe. Thus, when cpsa is running the a tree depth limit of one, cpsasas computes a cohort analysis sentence. 2016-03-29 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Reduction.hs (LPreskel): Added a depth field, so that CPSA aborts when the depth of one branch exceeds a bound. * src/CPSA/Lib/Algebra.hs: Added escapeSet to Term class and remove protectors, thus computing the escape set in a more straightforward way. 2015-11-23 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/Main.hs (main): Changed start up so that the herald is read and used to find the correct algebra for further processing. 2015-10-02 John D. Ramsdell <ramsdell@mitre.org> * doc/{index,cpsauser}.html: Added width limit of 48em. 2015-07-09 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Graph/ExpandedView.hs (purgeTraces): By default, the graph program now does not show traces in skeletons. Added --show-traces option to the graph program, which restores the previous behavior and traces are displayed in skeletons. 2015-07-02 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Algebra.hs: Added constituent to the algebra interface and the algebras. An atom is a constituent of a term if the atom is among the set of atoms required to construct the term. Changed occursIn so that it just applies to variables. 2015-07-01 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/{Basic,DiffieHellman}/Algebra.hs (occursIn): Restricted first argument of occursIn to variables and atoms and corrected the implementation. 2015-06-30 John D. Ramsdell <ramsdell@mitre.org> * cpsa3.cabal (Version): Tagged as 3.2.2. 2015-06-25 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (geq): Removed dynamic role specific test because it erroneously reports violations. The existing static role specific test correctly does the job. 2015-05-26 John D. Ramsdell <ramsdell@mitre.org> * cpsa3.cabal (Version): Tagged as 3.2.1. * src/CPSA/DiffieHellman/Algebra.hs (displayTerm): Made it so that CPSA prints each bltk atoms in a canonical form so that the graph program draws solid arrows when it should. 2015-04-27 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Loader.hs (ReturnFail): Added ReturnFail Monad so that fail is correctly handled. Added Functor and Applicative instance to support GHC 7.10 base library. 2015-04-20 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Characteristic.hs (mkDcls): Fixed tag for non-orig and pen-non-orig. 2015-04-10 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (mkListener): The role used for listener strands is now the one stored in the protocol. It has a single variable x of sort mesg as its set of variables. This change enables satisfaction checking on skeleton that include listeners. 2015-04-07 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (toSkeleton): Removed hulling to the process of converting an input preskeleton into a skeleton as it causes bugs in printing. * Imported CPSA2's implementation of goals and expunged support for subgoals. 2015-03-27 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (toSkeleton): Added hulling to the process of converting an input preskeleton into a skeleton. 2015-03-25 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Goal.hs: Added uniq to goal language. 2015-03-17 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs (form): Generate a defsas form rather than a naked sentence. * src/CPSA/Lib/Loader.hs (loadPrimary): Renamed equals function symbol to =. 2015-03-05 John D. Ramsdell <ramsdell@mitre.org> * cpsa3.cabal (Version): Tagged as 3.2.0. 2015-02-20 John D. Ramsdell <ramsdell@mitre.org> * Added support for subgoals within point-of-view skeletons. The subgoals are evaluated for each shape, and (satisfies-a-subgoal) is added to a shape when it satisfies one of the subgoals. 2014-12-11 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Entry.hs (defaultOptions): Changed the default strand bound to 12. 2014-11-15 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/SAS.hs: Changed the language used for a shape analysis sentence to be node-oriented. 2014-11-07 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Loader.hs (loadPriorities): Allowed priority declarations on state synchronization nodes other than initiatizers. 2014-11-07 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Cohort.hs (explainable): Added the nodes reachable by strand succession so that a transition can be explained by a previous transition within a strand. 2014-10-31 John D. Ramsdell <ramsdell@mitre.org> * Changed the name of the logic producing program to cpsa3sas. 2014-09-01 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/Strand.hs (noStateSplit): An observer node should have at most one transition node after it too. 2014-08-31 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/State.hs: Made labels optional. Use "tran" for state synchronization events with labels, and "sync" for ones without. 2014-08-29 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/Lib/*.hs: Added support for analyzing protocols with state. A state synchronization event sync was added to the events that can occur in a trace, along with a new method for state-based augmentation. An example using sync events is in tst/envelope.scm. 2014-08-26 John D. Ramsdell <ramsdell@mitre.org> * cpsa3.cabal: Removed cpsaparameters program. 2014-08-25 John D. Ramsdell <ramsdell@mitre.org> * src/split.py: Added the skeleton split program that copies the skeletons in a CPSA source file into separate files. 2014-08-23 John D. Ramsdell <ramsdell@mitre.org> * src/cpsajson.py (load): Added a reader in Python for JSON produced by CPSA's pretty printer program cpsa3pp -j. 2014-08-22 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/JSON/Main.hs: Added the program cpsa3json that translates JSON encoded CPSA into CPSA S-Expressions. It expects the JSON input to follow the conventions of the JSON produced by the cpsapp program when given the -j option. * src/CPSA/Lib/SExpr.hs (numOrSym): Enabled parsing a number with a plus sign by removing the sign before translating the string of digits into a number. 2014-06-12 John D. Ramsdell <ramsdell@mitre.org> * cpsa3.cabal (Version): Tagged as 3.0.3. 2014-02-06 John D. Ramsdell <ramsdell@mitre.org> * cpsa3.cabal (Version): Tagged as 3.0.2. 2013-12-14 John D. Ramsdell <ramsdell@mitre.org> * cpsa3.cabal (Version): Tagged as 3.0.1. * cpsa3.cabal (Extra-Source-Files): Added more DH tests 2013-03-12 John D. Ramsdell <ramsdell@mitre.org> * src/CPET/Annotations/Annotations.hs (obligation): Replaced an irrefutable pattern that raised an exception with a maybeToList. 2013-02-21 John D. Ramsdell <ramsdell@mitre.org> * src/CPET/DiffieHellman/Algebra.hs: Added the Diffie-Hellman algebra based on Abelian groups. * src/CPET/Basic/Algebra.hs: Removed support for GHC 6.x. 2013-02-06 John D. Ramsdell <ramsdell@mitre.org> * cpet.cabal (Version): Tagged as 0.0.0.