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.