diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,24 @@
+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.
+
+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
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,12 @@
 CPSA NEWS -- history of user-visible changes.
 
+* Changes in version 2.5.3
+
+** Corrected errors in the documentation on security goals.
+
+** Enabled compilation using GHC 7.10 by making some monads
+   applicative.
+
 * Changes in version 2.5.2
 
 ** Added an option to purge traces in skeletons while graphing
diff --git a/README b/README
--- a/README
+++ b/README
@@ -1,8 +1,9 @@
 CPSA: A Crptographic Protocol Shapes Analyzer
 
 This program has been built and tested using Haskell Platform.
-It is available from <http://haskell.org> or from
-an operating system specific source.
+It is available from <http://haskell.org> or from an operating
+system specific source.  The name of the Linux package is usually
+haskell-platform.
 
 $ cabal update
 $ cabal install cpsa
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,5 +1,5 @@
 Name:			cpsa
-Version:		2.5.2
+Version:		2.5.3
 Maintainer:		ramsdell@mitre.org
 Cabal-Version:		>= 1.6
 License:		BSD3
@@ -92,7 +92,7 @@
   tst/neuman-stubblebine.tst tst/no_contraction.scm
   tst/no_contraction.tst tst/nonaug-prune.scm tst/nonaug-prune.tst
   tst/non_transforming.scm tst/non_transforming.tst tst/nsl3.scm
-  tst/nsl3.tst tst/nsl4cm1.lsp tst/nsl4cm1.tst tst/nsl4.lisp
+  tst/nsl3.tst tst/nsl4cm1.lisp tst/nsl4.lisp
   tst/nsl4resp2.lisp tst/nsl5i.lisp tst/nsl5.lisp tst/ns-l.scm
   tst/nslsk.scm tst/nslsk.tst tst/ns-l.tst tst/ns.scm tst/ns.tst
   tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst
diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf
Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ
diff --git a/doc/cpsagoals.pdf b/doc/cpsagoals.pdf
Binary files a/doc/cpsagoals.pdf and b/doc/cpsagoals.pdf differ
diff --git a/doc/cpsagoals.tex b/doc/cpsagoals.tex
--- a/doc/cpsagoals.tex
+++ b/doc/cpsagoals.tex
@@ -174,7 +174,7 @@
 existentially quantified conjunction of atomic formulas, but in
 general, the conclusion is a disjunction of existentially quantified
 conjunctions of atomic formulas.  In what follows, \sym{(false)} is a
-synonym for \sym{(or)}.
+synonym for the empty disjunction, \sym{(or)}.
 
 \begin{center}\scshape
   \begin{tabular}{rcl}
@@ -215,18 +215,19 @@
 contains three tokens, \texttt{p}, a string that names a role, and a
 string that names a role variable.  For role~$r$, there is role
 parameter predicate for each variable declared by~$r$.  Thus
-\verb|(p "init" 2 "n1" z0 n1)| is an atomic formula using the role
+\verb|(p "init" "n1" z0 n1)| is an atomic formula using the role
 parameter predicate for parameter \text{n1} in the \texttt{init} role
 of the protocol.
 
 The empty string names the listener role of a protocol.  The role
 has the variable \texttt{x} of sort \texttt{mesg} as its only role
-variable.  There are two positions in the listener role.
+variable.  There are two positions in the listener role.  Its trace is
+\texttt{(trace (recv x) (send x))}.
 
 When a variable of sort \sym{node} occurs in a formula, its position
 must be specified using a role position formula.  When an algebra
-variable occurs in formula, its association with the parameter of some
-role must be specified using a role parameter formula.
+variable occurs in a formula, its association with the parameter of
+some role must be specified using a role parameter formula.
 
 \begin{table}
 \begin{center}
@@ -283,8 +284,8 @@
 Our aim now is to specify how to decide if a security goal is true in
 all possible executions of a protocol.  A skeleton defines a set of
 executions that contain the skeleton's structure.  We say a skeleton
-\emph{satisfies} a formula if the formula is true in all executions
-that contain the skeleton's structure.  To decide if a skeleton
+\emph{satisfies} a formula if the skeleton contains all of the
+structure specified by the formula.  To decide if a skeleton
 satisfies a formula, we decide if it satisfies each of its atomic
 formulas, and combine the results using the rules of first-order
 logic.
@@ -373,12 +374,13 @@
 
 When {\cpsa} performs a shape analysis, every shape it generates
 refines the input skeleton.  Skeleton refinement is defined
-in~\cite[Section~6]{cpsaprimer09}, but roughly speaking, skeleton~$A$
-refines skeleton~$B$ if~$A$ contains the structure of skeleton~$B$.
+in~\cite[Section~6]{cpsaprimer09}.  The definition makes precise the
+notion of structure containment, as skeleton~$A$ refines skeleton~$B$
+if and only if~$A$ contains the structure of skeleton~$B$.
 
 The skeleton~$k_0$ extracted from the antecedent of a security goal
-has the property that every skeleton than refines~$k_0$ satisfies the
-antecedent.  A skeleton with this property is called the
+has the property that a skeleton refines~$k_0$ if and only if it
+satisfies the antecedent.  A skeleton with this property is called the
 \emph{characteristic skeleton} of the antecedent.
 
 Given a goal~\(\Phi\), consider a shape analysis starting from the
@@ -388,8 +390,9 @@
 in~$k_0$.  {\cpsa} tells us that each execution is in the executions
 that contain the structure of some~$k_i$.  Furthermore, because~$k_0$
 is a characteristic skeleton, each~$k_i$ satisfies the antecedent
-of~$\Phi$.  Therefore,~$\Phi$ is true in all executions of the
-protocol and maximally informative.
+of~$\Phi$.  Executions that do not contain the structure in~$k_0$ do
+not satisfy the antecedent.  Therefore,~$\Phi$ is true in all
+executions of the protocol and maximally informative.
 
 \section{Examples}\label{sec:examples}
 
diff --git a/doc/cpsaintroslides.pdf b/doc/cpsaintroslides.pdf
Binary files a/doc/cpsaintroslides.pdf and b/doc/cpsaintroslides.pdf differ
diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf
Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ
diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf
Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ
diff --git a/doc/cpsaprimer.tex b/doc/cpsaprimer.tex
--- a/doc/cpsaprimer.tex
+++ b/doc/cpsaprimer.tex
@@ -1132,6 +1132,10 @@
 takes precedence. The {\cpsa} program omits macro definitions from its
 output.
 
+After expanding a list, elements of the list of the form
+\verb|(^ |$\cdots$\verb| )| are spliced into the output.  Thus
+\verb|(a ^(b c) d)| becomes \verb|(a b c d)| after macro expansion.
+
 \section{Includes}\label{sec:include}
 
 While performing macro expansion, {\cpsa} includes other source files
diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf
Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ
diff --git a/doc/macros.tex b/doc/macros.tex
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -1,5 +1,5 @@
 \newcommand{\cpsa}{\textsc{cpsa}}
-\newcommand{\version}{2.5.2}
+\newcommand{\version}{2.5.3}
 \newcommand{\cpsacopying}{\begingroup
   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The
     MITRE Corporation.  Permission to copy without fee all or part of
diff --git a/src/CPSA/Annotations/Annotations.hs b/src/CPSA/Annotations/Annotations.hs
--- a/src/CPSA/Annotations/Annotations.hs
+++ b/src/CPSA/Annotations/Annotations.hs
@@ -85,7 +85,7 @@
             SExpr Pos -> m (g, Role t)
 loadRole gen (L pos (S _ "defrole" :
                      S _ name :
-	             L _ (S _ "vars" : vars) :
+                     L _ (S _ "vars" : vars) :
                      L _ (S _ "trace" : _ : c) :
                      rest)) =
     do
diff --git a/src/CPSA/Annotations/Formulas.hs b/src/CPSA/Annotations/Formulas.hs
--- a/src/CPSA/Annotations/Formulas.hs
+++ b/src/CPSA/Annotations/Formulas.hs
@@ -11,6 +11,7 @@
     displayFormula) where
 
 import Control.Monad
+import Control.Applicative
 import qualified Data.Set as S
 import CPSA.Lib.CPSA
 
@@ -177,6 +178,15 @@
 data EitherS a
     = RightS a
     | LeftS String
+
+instance Functor (EitherS) where
+    fmap _ (LeftS x) = LeftS x
+    fmap f (RightS y) = RightS (f y)
+
+instance Applicative (EitherS) where
+    pure          = RightS
+    LeftS e <*> _ = LeftS e
+    RightS f <*> r = fmap f r
 
 instance Monad EitherS where
     return = RightS
diff --git a/src/CPSA/Graph/Loader.hs b/src/CPSA/Graph/Loader.hs
--- a/src/CPSA/Graph/Loader.hs
+++ b/src/CPSA/Graph/Loader.hs
@@ -200,7 +200,7 @@
 
 loadRole :: Monad m => Pos -> [SExpr Pos] -> m (String, Trace)
 loadRole _ (S _ name :
-	    L _ (S _ "vars" : _) :
+            L _ (S _ "vars" : _) :
             L _ (S _ "trace" : trace) : _) = return (name, trace)
 loadRole pos _ = fail (shows pos "Malformed role")
 
diff --git a/src/CPSA/Lib/Displayer.hs b/src/CPSA/Lib/Displayer.hs
--- a/src/CPSA/Lib/Displayer.hs
+++ b/src/CPSA/Lib/Displayer.hs
@@ -141,11 +141,11 @@
           displayCause (L () (S () "contracted" : substitution)) cause
       Displaced s s' role height cause ->
           displayCause
-	  (L () [S () "displaced", N () s, N () s', S () role, N () height])
+          (L () [S () "displaced", N () s, N () s', S () role, N () height])
           cause
       AddedStrand role height cause ->
           displayCause
-	  (L () [S () "added-strand", S () role, N () height]) cause
+          (L () [S () "added-strand", S () role, N () height]) cause
       AddedListener t cause ->
           displayCause (L () [S () "added-listener", displayOpTerm ctx t]) cause
       Generalized method ->
diff --git a/src/CPSA/Lib/Loader.hs b/src/CPSA/Lib/Loader.hs
--- a/src/CPSA/Lib/Loader.hs
+++ b/src/CPSA/Lib/Loader.hs
@@ -97,7 +97,7 @@
 loadRole :: (Algebra t p g s e c, Monad m) => g -> Pos ->
             [SExpr Pos] -> m (g, Role t)
 loadRole gen pos (S _ name :
-	          L _ (S _ "vars" : vars) :
+                  L _ (S _ "vars" : vars) :
                   L _ (S _ "trace" : evt : c) :
                   rest) =
     do
diff --git a/src/CPSA/Parameters/Flow.hs b/src/CPSA/Parameters/Flow.hs
--- a/src/CPSA/Parameters/Flow.hs
+++ b/src/CPSA/Parameters/Flow.hs
@@ -38,7 +38,7 @@
            SExpr Pos -> m (SExpr ())
 mapRole gen (L _ (S _ "defrole" :
                   S _ name :
-	          L _ (S _ "vars" : vars) :
+                  L _ (S _ "vars" : vars) :
                   L _ (S _ "trace" : trace) :
                   rest)) =
     do
@@ -48,7 +48,7 @@
       trace <- mapM stripEvt trace
       return (L () (S () "defrole" :
                     S () name :
-	            L () (S () "vars" : map strip vars) :
+                    L () (S () "vars" : map strip vars) :
                     L () (S () "trace" : trace) :
                     rest'))
 mapRole _ x = return (strip x)
diff --git a/src/CPSA/SAS/SAS.hs b/src/CPSA/SAS/SAS.hs
--- a/src/CPSA/SAS/SAS.hs
+++ b/src/CPSA/SAS/SAS.hs
@@ -134,7 +134,7 @@
             SExpr Pos -> m (g, Role t c)
 loadRole gen (L _ (S _ "defrole" :
                      S _ name :
-	             L _ (S _ "vars" : vars) :
+                     L _ (S _ "vars" : vars) :
                      L _ (S _ "trace" : _ : _) :
                      _)) =
     do
diff --git a/tst/DH_hack.tst b/tst/DH_hack.tst
--- a/tst/DH_hack.tst
+++ b/tst/DH_hack.tst
@@ -1,6 +1,6 @@
 (herald "DH Hack" (bound 15))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from DH_hack.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/blanchet.tst b/tst/blanchet.tst
--- a/tst/blanchet.tst
+++ b/tst/blanchet.tst
@@ -1,7 +1,7 @@
 (herald "Blanchet's Simple Example Protocol"
   (comment "There is a flaw in this protocol by design"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from blanchet.scm")
 
 (defprotocol blanchet basic
diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst
--- a/tst/completeness-test.tst
+++ b/tst/completeness-test.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from completeness-test.scm")
 
 (defprotocol completeness-test basic
diff --git a/tst/crushing.tst b/tst/crushing.tst
--- a/tst/crushing.tst
+++ b/tst/crushing.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from crushing.scm")
 
 (defprotocol crushing basic
diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst
--- a/tst/dass_simple.tst
+++ b/tst/dass_simple.tst
@@ -1,6 +1,6 @@
 (herald "Distributed Authentication Security Service Protocol Variants")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from dass_simple.scm")
 
 (defprotocol dass-simple basic
diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst
--- a/tst/denning-sacco.tst
+++ b/tst/denning-sacco.tst
@@ -1,6 +1,6 @@
 (herald "Denning-Sacco Protocol")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from denning-sacco.scm")
 
 (defprotocol denning-sacco basic
diff --git a/tst/deorig_contract.tst b/tst/deorig_contract.tst
--- a/tst/deorig_contract.tst
+++ b/tst/deorig_contract.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from deorig_contract.scm")
 
 (defprotocol deorig-contract basic
diff --git a/tst/deorig_mesg.tst b/tst/deorig_mesg.tst
--- a/tst/deorig_mesg.tst
+++ b/tst/deorig_mesg.tst
@@ -1,6 +1,6 @@
 (herald deorig-mesg)
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from deorig_mesg.scm")
 
 (defprotocol deorig-mesg basic
diff --git a/tst/deorig_simple.tst b/tst/deorig_simple.tst
--- a/tst/deorig_simple.tst
+++ b/tst/deorig_simple.tst
@@ -1,6 +1,6 @@
 (herald deorig-simple)
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from deorig_simple.scm")
 
 (defprotocol deorig-simple basic
diff --git a/tst/dy.tst b/tst/dy.tst
--- a/tst/dy.tst
+++ b/tst/dy.tst
@@ -1,6 +1,6 @@
 (herald "Example 1.3 from 1983 Dolev-Yao Paper")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from dy.lsp")
 
 (defprotocol dy basic
diff --git a/tst/encsig.tst b/tst/encsig.tst
--- a/tst/encsig.tst
+++ b/tst/encsig.tst
@@ -1,7 +1,7 @@
 (herald "Encrypted Signed Message Example"
   (comment "Shows examples of key usage of asymmetric keys"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from encsig.scm")
 
 (defprotocol mult-keys-enc-sig basic
diff --git a/tst/epmo-hash.tst b/tst/epmo-hash.tst
--- a/tst/epmo-hash.tst
+++ b/tst/epmo-hash.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol with Key Hashing"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from epmo-hash.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo-key-hash.tst b/tst/epmo-key-hash.tst
--- a/tst/epmo-key-hash.tst
+++ b/tst/epmo-key-hash.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol with Key Hashing"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from epmo-key-hash.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo.tst b/tst/epmo.tst
--- a/tst/epmo.tst
+++ b/tst/epmo.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from epmo.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo_acctnum-key-hash.tst b/tst/epmo_acctnum-key-hash.tst
--- a/tst/epmo_acctnum-key-hash.tst
+++ b/tst/epmo_acctnum-key-hash.tst
@@ -2,7 +2,7 @@
   "Electronic Purchase with Money Order Protocol Variant with Key Hashing"
   (comment "This version includes account numbers in exchanges"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from epmo_acctnum-key-hash.scm")
 
 (defprotocol epmo_acctnum basic
diff --git a/tst/ffgg.tst b/tst/ffgg.tst
--- a/tst/ffgg.tst
+++ b/tst/ffgg.tst
@@ -1,7 +1,7 @@
 (herald "The ffgg Protocol"
   (comment "From A Necessarily Parallel Attack by Jon K. Millen"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from ffgg.scm")
 
 (defprotocol ffgg basic
diff --git a/tst/fragile_pruning.tst b/tst/fragile_pruning.tst
--- a/tst/fragile_pruning.tst
+++ b/tst/fragile_pruning.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from fragile_pruning.scm")
 
 (defprotocol fragile_pruning basic
diff --git a/tst/goals.tst b/tst/goals.tst
--- a/tst/goals.tst
+++ b/tst/goals.tst
@@ -1,6 +1,6 @@
 (herald goals)
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from goals.scm")
 
 (defprotocol ns basic
diff --git a/tst/hashtest-key-hash.tst b/tst/hashtest-key-hash.tst
--- a/tst/hashtest-key-hash.tst
+++ b/tst/hashtest-key-hash.tst
@@ -1,6 +1,6 @@
 (herald "Hashtest")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from hashtest-key-hash.scm")
 
 (defprotocol hashtest basic
diff --git a/tst/hashtest.tst b/tst/hashtest.tst
--- a/tst/hashtest.tst
+++ b/tst/hashtest.tst
@@ -1,6 +1,6 @@
 (herald "Hashtest")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from hashtest.scm")
 
 (defprotocol hashtest basic
diff --git a/tst/incompleteness_example.tst b/tst/incompleteness_example.tst
--- a/tst/incompleteness_example.tst
+++ b/tst/incompleteness_example.tst
@@ -1,7 +1,7 @@
 (herald incompleteness-example
   (comment "Shows a shape not found by CPSA"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from incompleteness_example.scm")
 
 (defprotocol incompleteness-example basic
diff --git a/tst/isoreject.tst b/tst/isoreject.tst
--- a/tst/isoreject.tst
+++ b/tst/isoreject.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from isoreject.scm")
 
 (defprotocol isoreject basic
diff --git a/tst/kelly1.tst b/tst/kelly1.tst
--- a/tst/kelly1.tst
+++ b/tst/kelly1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from kelly1.scm")
 
 (defprotocol kelly1 basic
diff --git a/tst/kerberos.tst b/tst/kerberos.tst
--- a/tst/kerberos.tst
+++ b/tst/kerberos.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from kerberos.scm")
 
 (defprotocol kerberos basic
diff --git a/tst/mass.tst b/tst/mass.tst
--- a/tst/mass.tst
+++ b/tst/mass.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from mass.lsp")
 
 (defprotocol mass basic
diff --git a/tst/mass2.tst b/tst/mass2.tst
--- a/tst/mass2.tst
+++ b/tst/mass2.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from mass2.lsp")
 
 (defprotocol mass2 basic
diff --git a/tst/missing_contraction.tst b/tst/missing_contraction.tst
--- a/tst/missing_contraction.tst
+++ b/tst/missing_contraction.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from missing_contraction.scm")
 
 (defprotocol missing-contraction basic
diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst
--- a/tst/neuman-stubblebine-reauth.tst
+++ b/tst/neuman-stubblebine-reauth.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from neuman-stubblebine-reauth.lsp")
 
 (defprotocol neuman-stubblebine-reauth basic
diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst
--- a/tst/neuman-stubblebine.tst
+++ b/tst/neuman-stubblebine.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from neuman-stubblebine.scm")
 
 (defprotocol neuman-stubblebine basic
diff --git a/tst/no_contraction.tst b/tst/no_contraction.tst
--- a/tst/no_contraction.tst
+++ b/tst/no_contraction.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from no_contraction.scm")
 
 (defprotocol no-contraction basic
diff --git a/tst/non_transforming.tst b/tst/non_transforming.tst
--- a/tst/non_transforming.tst
+++ b/tst/non_transforming.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from non_transforming.scm")
 
 (defprotocol non_transforming basic
diff --git a/tst/nonaug-prune.tst b/tst/nonaug-prune.tst
--- a/tst/nonaug-prune.tst
+++ b/tst/nonaug-prune.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from nonaug-prune.scm")
 
 (defprotocol nonaug-prune basic
diff --git a/tst/ns-l.tst b/tst/ns-l.tst
--- a/tst/ns-l.tst
+++ b/tst/ns-l.tst
@@ -1,7 +1,7 @@
 (herald "Needham-Schroeder-Low Public-Key Protocol"
   (comment "With deflistener's"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from ns-l.scm")
 
 (defprotocol ns basic
diff --git a/tst/ns.tst b/tst/ns.tst
--- a/tst/ns.tst
+++ b/tst/ns.tst
@@ -1,6 +1,6 @@
 (herald "Needham-Schroeder Public-Key Protocol Variants")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from ns.scm")
 
 (defprotocol ns basic
diff --git a/tst/nsl3.tst b/tst/nsl3.tst
--- a/tst/nsl3.tst
+++ b/tst/nsl3.tst
@@ -1,6 +1,6 @@
 (herald "Three Party Needham-Schroeder-Lowe Protocol")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from nsl3.scm")
 
 (defprotocol nsl3 basic
diff --git a/tst/nsl4cm1.lisp b/tst/nsl4cm1.lisp
new file mode 100644
--- /dev/null
+++ b/tst/nsl4cm1.lisp
@@ -0,0 +1,49 @@
+(herald "Four Party Needham-Schroeder-Lowe Protocol")
+
+(defprotocol nsl4cm basic
+   (defrole init
+      (vars (a b c d name) (na nb nc nd text))
+      (trace
+         (send (enc a c d na (pubk b)))
+	 (recv (enc b c d na nb nc nd (pubk a)))
+	 (send (enc nb nc nd (pubk b)))))
+   (defrole resp1
+      (vars (a b c d name) (na nb nc nd text))
+      (trace
+         (recv (enc a c d na (pubk b)))
+	 (send (enc a b d na nb (pubk c)))
+	 (recv (enc nb nc nd (pubk b)))
+	 (send (enc nc nd (pubk c)))))
+   (defrole resp2
+      (vars (a b c d name) (na nb nc nd text))
+      (trace
+         (recv (enc a b d na nb (pubk c)))
+	 (send (enc a b c na nb nc (pubk d)))
+	 (recv (enc nc nd (pubk c)))
+	 (send (enc nd (pubk d)))))
+   (defrole resp3
+      (vars (a b c d name) (na nb nc nd text))
+      (trace
+         (recv (enc a b c na nb nc (pubk d)))
+	 (send (enc b c d na nb nc nd (pubk a)))
+	 (recv (enc nd (pubk d))))))
+
+(defskeleton nsl4cm (vars (a b c d name) (na text))
+  (defstrand init 3 (a a) (b b) (c c) (d d) (na na))
+   (non-orig (privk a) (privk b) (privk c) (privk d))
+   (uniq-orig na))
+
+(comment (defskeleton nsl4cm (vars (a b c d name) (nb text))
+   (defstrand resp1 4 (a a) (b b) (c c) (d d) (nb nb))
+   (non-orig (privk a) (privk b) (privk c) (privk d))
+   (uniq-orig nb))
+
+(defskeleton nsl4cm (vars (a b c d name) (nc text))
+   (defstrand resp2 4 (a a) (b b) (c c) (d d) (nc nc))
+   (non-orig (privk a) (privk b) (privk c) (privk d))
+   (uniq-orig nc))
+
+(defskeleton nsl4cm (vars (a b c d name) (nd text))
+   (defstrand resp3 3 (a a) (b b) (c c) (d d) (nd nd))
+   (non-orig (privk a) (privk b) (privk c) (privk d))
+   (uniq-orig nd)))
diff --git a/tst/nsl4cm1.lsp b/tst/nsl4cm1.lsp
deleted file mode 100644
--- a/tst/nsl4cm1.lsp
+++ /dev/null
@@ -1,49 +0,0 @@
-(herald "Four Party Needham-Schroeder-Lowe Protocol")
-
-(defprotocol nsl4cm basic
-   (defrole init
-      (vars (a b c d name) (na nb nc nd text))
-      (trace
-         (send (enc a c d na (pubk b)))
-	 (recv (enc b c d na nb nc nd (pubk a)))
-	 (send (enc nb nc nd (pubk b)))))
-   (defrole resp1
-      (vars (a b c d name) (na nb nc nd text))
-      (trace
-         (recv (enc a c d na (pubk b)))
-	 (send (enc a b d na nb (pubk c)))
-	 (recv (enc nb nc nd (pubk b)))
-	 (send (enc nc nd (pubk c)))))
-   (defrole resp2
-      (vars (a b c d name) (na nb nc nd text))
-      (trace
-         (recv (enc a b d na nb (pubk c)))
-	 (send (enc a b c na nb nc (pubk d)))
-	 (recv (enc nc nd (pubk c)))
-	 (send (enc nd (pubk d)))))
-   (defrole resp3
-      (vars (a b c d name) (na nb nc nd text))
-      (trace
-         (recv (enc a b c na nb nc (pubk d)))
-	 (send (enc b c d na nb nc nd (pubk a)))
-	 (recv (enc nd (pubk d))))))
-
-(defskeleton nsl4cm (vars (a b c d name) (na text))
-  (defstrand init 3 (a a) (b b) (c c) (d d) (na na))
-   (non-orig (privk a) (privk b) (privk c) (privk d))
-   (uniq-orig na))
-
-(comment (defskeleton nsl4cm (vars (a b c d name) (nb text))
-   (defstrand resp1 4 (a a) (b b) (c c) (d d) (nb nb))
-   (non-orig (privk a) (privk b) (privk c) (privk d))
-   (uniq-orig nb))
-
-(defskeleton nsl4cm (vars (a b c d name) (nc text))
-   (defstrand resp2 4 (a a) (b b) (c c) (d d) (nc nc))
-   (non-orig (privk a) (privk b) (privk c) (privk d))
-   (uniq-orig nc))
-
-(defskeleton nsl4cm (vars (a b c d name) (nd text))
-   (defstrand resp3 3 (a a) (b b) (c c) (d d) (nd nd))
-   (non-orig (privk a) (privk b) (privk c) (privk d))
-   (uniq-orig nd)))
diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst
deleted file mode 100644
# file too large to diff: tst/nsl4cm1.tst
diff --git a/tst/nslsk.tst b/tst/nslsk.tst
--- a/tst/nslsk.tst
+++ b/tst/nslsk.tst
@@ -1,6 +1,6 @@
 (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from nslsk.scm")
 
 (defprotocol nslsk basic
diff --git a/tst/or.tst b/tst/or.tst
--- a/tst/or.tst
+++ b/tst/or.tst
@@ -1,7 +1,7 @@
 (herald "Otway-Rees Protocol"
   (comment "Standard version using variables of sort mesg"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from or.scm")
 
 (defprotocol or basic
diff --git a/tst/pca.tst b/tst/pca.tst
--- a/tst/pca.tst
+++ b/tst/pca.tst
@@ -1,7 +1,7 @@
 (herald "Privacy Certificate Authority" (bound 15)
   (comment "Generation of an Attestation Identity Certificate"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from pca.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/pen-non-orig-test.tst b/tst/pen-non-orig-test.tst
--- a/tst/pen-non-orig-test.tst
+++ b/tst/pen-non-orig-test.tst
@@ -1,6 +1,6 @@
 (herald "pen-non-orig test")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from pen-non-orig-test.scm")
 
 (defprotocol pennonorigtest basic
diff --git a/tst/pkinit.tst b/tst/pkinit.tst
--- a/tst/pkinit.tst
+++ b/tst/pkinit.tst
@@ -1,6 +1,6 @@
 (herald "Kerberos PK init")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from pkinit.scm")
 
 (defprotocol pkinit basic
diff --git a/tst/preprocess.tst b/tst/preprocess.tst
--- a/tst/preprocess.tst
+++ b/tst/preprocess.tst
@@ -1,6 +1,6 @@
 (herald "Pre-processing test example: modified NS with two responders")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from preprocess.scm")
 
 (defprotocol ns basic
diff --git a/tst/print.tst b/tst/print.tst
--- a/tst/print.tst
+++ b/tst/print.tst
@@ -1,7 +1,7 @@
 (herald "Print Test"
   (comment "See if read forms look like printed ones"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from print.scm")
 
 (defprotocol print-test basic
diff --git a/tst/pruning1.tst b/tst/pruning1.tst
--- a/tst/pruning1.tst
+++ b/tst/pruning1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from pruning1.scm")
 
 (defprotocol prune basic
diff --git a/tst/sigenc.tst b/tst/sigenc.tst
--- a/tst/sigenc.tst
+++ b/tst/sigenc.tst
@@ -1,7 +1,7 @@
 (herald "Signed Encrypted Message Example"
   (comment "Shows examples of key usage of asymmetric keys"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from sigenc.scm")
 
 (defprotocol mult-keys-sig-enc basic
diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst
--- a/tst/sorted_epmo_acctnum.tst
+++ b/tst/sorted_epmo_acctnum.tst
@@ -4,7 +4,7 @@
     "This version uses sorts to avoid confusion"
     "between a nonce and other data"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from sorted_epmo_acctnum.scm")
 (comment "Strand count bounded at 12")
 
diff --git a/tst/targetterms2.tst b/tst/targetterms2.tst
--- a/tst/targetterms2.tst
+++ b/tst/targetterms2.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from targetterms2.scm")
 
 (defprotocol targetterms2 basic
diff --git a/tst/targetterms6.tst b/tst/targetterms6.tst
--- a/tst/targetterms6.tst
+++ b/tst/targetterms6.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from targetterms6.scm")
 
 (defprotocol targetterms6 basic
diff --git a/tst/targetterms8.tst b/tst/targetterms8.tst
--- a/tst/targetterms8.tst
+++ b/tst/targetterms8.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from targetterms8.scm")
 
 (defprotocol targetterms8 basic
diff --git a/tst/timestamping.tst b/tst/timestamping.tst
--- a/tst/timestamping.tst
+++ b/tst/timestamping.tst
@@ -1,6 +1,6 @@
 (herald timestamping-service)
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from timestamping.scm")
 
 (defprotocol timestamping-service basic
diff --git a/tst/uncarried_keys.tst b/tst/uncarried_keys.tst
--- a/tst/uncarried_keys.tst
+++ b/tst/uncarried_keys.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from uncarried_keys.scm")
 
 (defprotocol uncarried-keys basic
diff --git a/tst/unilateral.tst b/tst/unilateral.tst
--- a/tst/unilateral.tst
+++ b/tst/unilateral.tst
@@ -1,6 +1,6 @@
 (herald unilateral)
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from unilateral.scm")
 
 (defprotocol unilateral basic
diff --git a/tst/uo.tst b/tst/uo.tst
--- a/tst/uo.tst
+++ b/tst/uo.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from uo.scm")
 
 (defprotocol uniq-orig basic
diff --git a/tst/wang-hash.tst b/tst/wang-hash.tst
--- a/tst/wang-hash.tst
+++ b/tst/wang-hash.tst
@@ -1,6 +1,6 @@
 (herald "Wang's Fair Exchange Protocol" (bound 10))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from wang-hash.scm")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/wang-key-hash.tst b/tst/wang-key-hash.tst
--- a/tst/wang-key-hash.tst
+++ b/tst/wang-key-hash.tst
@@ -1,6 +1,6 @@
 (herald "Wang's Fair Exchange Protocol" (bound 10))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from wang-key-hash.scm")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/weird.tst b/tst/weird.tst
--- a/tst/weird.tst
+++ b/tst/weird.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from weird.scm")
 
 (defprotocol weird basic
diff --git a/tst/wide-mouth-frog-scyther.tst b/tst/wide-mouth-frog-scyther.tst
--- a/tst/wide-mouth-frog-scyther.tst
+++ b/tst/wide-mouth-frog-scyther.tst
@@ -1,7 +1,7 @@
 (herald "Wide-Mouth Frog Protocol from Scyther"
   (comment "This protocol has an infinite number of shapes"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from wide-mouth-frog-scyther.lsp")
 
 (defprotocol wide-mouth-frog basic
diff --git a/tst/wide-mouth-frog.tst b/tst/wide-mouth-frog.tst
--- a/tst/wide-mouth-frog.tst
+++ b/tst/wide-mouth-frog.tst
@@ -1,7 +1,7 @@
 (herald "Wide-Mouth Frog Protocol"
   (comment "This protocol has an infinite number of shapes"))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from wide-mouth-frog.lsp")
 
 (defprotocol wide-mouth-frog basic
diff --git a/tst/wonthull.tst b/tst/wonthull.tst
--- a/tst/wonthull.tst
+++ b/tst/wonthull.tst
@@ -1,6 +1,6 @@
 (herald wonthull (bound 9))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from wonthull.scm")
 (comment "Strand count bounded at 9")
 
diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst
--- a/tst/wonthull2.tst
+++ b/tst/wonthull2.tst
@@ -1,6 +1,6 @@
 (herald wonthull2 (bound 9))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from wonthull2.scm")
 (comment "Strand count bounded at 9")
 
diff --git a/tst/wonthull3.tst b/tst/wonthull3.tst
--- a/tst/wonthull3.tst
+++ b/tst/wonthull3.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from wonthull3.scm")
 
 (defprotocol wonthull3 basic
diff --git a/tst/woolam.tst b/tst/woolam.tst
--- a/tst/woolam.tst
+++ b/tst/woolam.tst
@@ -1,6 +1,6 @@
 (herald "Woo-Lam Protocol")
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from woolam.scm")
 
 (defprotocol woolam basic
diff --git a/tst/yahalom-6.3.6.tst b/tst/yahalom-6.3.6.tst
--- a/tst/yahalom-6.3.6.tst
+++ b/tst/yahalom-6.3.6.tst
@@ -5,7 +5,7 @@
   (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")
   (bound 15))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from yahalom-6.3.6.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/yahalom.tst b/tst/yahalom.tst
--- a/tst/yahalom.tst
+++ b/tst/yahalom.tst
@@ -1,6 +1,6 @@
 (herald "Yahalom Protocol Without Forwarding" (bound 15))
 
-(comment "CPSA 2.5.2")
+(comment "CPSA 2.5.3")
 (comment "All input read from yahalom.scm")
 (comment "Strand count bounded at 15")