diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,72 @@
+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
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,12 @@
 CPSA NEWS
 
+  August 2019:
+
+* Release 3.6.3 adds the cpsainit program and fixes bugs.  The
+  cpsainit program copies files from the CPSA data directory into a
+  fresh CPSA project directory.  The files ease the task of automating
+  the use of the various CPSA tools.
+
   March, 2019:
 
 * Release 3.6.2 adds the leads-to predicate to the rule language, adds
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,5 +1,5 @@
 Name:			cpsa
-Version:		3.6.2
+Version:		3.6.3
 Maintainer:		mliskov@mitre.org
 Cabal-Version:		>= 1.6
 License:		BSD3
@@ -71,6 +71,7 @@
   examples/fluffy_draft03_gske.scm
   examples/fluffy_draft03_improving_pske.scm
   examples/fluffy_draft03_pske.scm examples/eq_test.scm
+  init/Makefile init/template.lisp
   examples/eq_test.xhtml
 Data-Dir:	    	doc
 Extra-Source-Files:
@@ -233,3 +234,12 @@
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Match.Match
     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra
+
+Executable cpsainit
+  Main-Is:		CPSA/Init/Main.hs
+  Build-Depends:	base, directory
+  GHC-Options:
+    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
+  Hs-Source-Dirs:	src
+  Other-Modules:
+    Paths_cpsa
diff --git a/doc/cpsamanual.pdf b/doc/cpsamanual.pdf
Binary files a/doc/cpsamanual.pdf and b/doc/cpsamanual.pdf differ
diff --git a/doc/init/Makefile b/doc/init/Makefile
new file mode 100644
--- /dev/null
+++ b/doc/init/Makefile
@@ -0,0 +1,12 @@
+CPSAFLAGS = +RTS -M512m -N1 -RTS
+CPSATIME = time
+
+SRCS := $(wildcard *.scm) $(wildcard *.lsp)
+
+include cpsa.mk
+
+all:    $(SRCS:%.scm=%_shapes.xhtml) $(SRCS:%.scm=%.xhtml) \
+        $(SRCS:%.lsp=%_shapes.xhtml) $(SRCS:%.lsp=%.xhtml)
+
+clean:
+	-rm *.txt *.xhtml
diff --git a/doc/init/template.lisp b/doc/init/template.lisp
new file mode 100644
--- /dev/null
+++ b/doc/init/template.lisp
@@ -0,0 +1,39 @@
+;; This is a minimal template for a CPSA input file.
+
+;; Replace <TITLE> with the desired title and <PROTONAME>
+;; with the desired name of your project.
+
+;; The defrole template below may be copied and used as
+;; a starting point for the roles of your protocol.
+;; Change the <ROLENAME> field in each copy as desired.
+;; Roles must have distinct names.
+
+;; The basic cryptoalgebra is selected by default. If
+;; your project requires the diffie-hellman algebra,
+;; delete "basic" on the defprotocol line, uncomment
+;; "diffie-hellman" on this same line and uncomment
+;; the "(algebra diffie-hellman)" statement in the
+;; herald.
+
+;; Refer to the CPSA manual for more information
+;; about syntax and additional features.
+
+(herald "<TITLE>"
+	;; (algebra diffie-hellman)
+	)
+
+(defprotocol <PROTONAME> basic ;; diffie-hellman
+
+  (defrole <ROLENAME>
+    (vars )
+    (trace
+
+     )
+    )
+
+  )
+
+(defskeleton <PROTONAME>
+  (vars )
+  (defstrand )
+  )
diff --git a/src/CPSA/Init/Main.hs b/src/CPSA/Init/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/CPSA/Init/Main.hs
@@ -0,0 +1,112 @@
+--  Copies important files from the CPSA data directory to the current
+--  directory.
+
+-- Copyright (c) 2019 The MITRE Corporation
+--
+-- This program is free software: you can redistribute it and/or
+-- modify it under the terms of the BSD License as published by the
+-- University of California.
+
+module Main (main) where
+
+import System.IO
+import System.Environment
+import System.Console.GetOpt
+import System.Exit
+import System.Directory (copyFile, doesFileExist)
+import Data.List (elemIndex)
+import Data.Version
+import Paths_cpsa
+
+main :: IO ()
+main =
+  do
+    argv <- getArgs
+    (flags, _) <- opts options argv
+    interp flags
+    copy ["init/Makefile", "cpsa.mk", "Make.hs", "init/template.lisp"]
+
+-- Copy the file only if it does not already exist
+
+copy :: [String] -> IO ()
+copy [] = return ()
+copy (f : fs) =
+  do
+    let b = basename f
+    exist <- doesFileExist b
+    case exist of
+      True ->
+        hPutStrLn stderr ("File " ++ b ++ " exists, not overwriting")
+      False ->
+        do
+          fp <- getDataFileName f
+          copyFile fp b
+          hPutStrLn stderr ("Created " ++ b)
+    copy fs
+
+basename :: String -> String
+basename f =
+  case elemIndex '/' f of
+    Nothing -> f
+    Just i -> basename (drop (i + 1) f)
+
+-- Command-line options
+
+data Flag
+    = Help                      -- Help
+    | Info                      -- Version information
+      deriving Show
+
+options :: [OptDescr Flag]
+options =
+    [ Option ['h'] ["help"]     (NoArg Help)           "show help message",
+      Option ['v'] ["version"]  (NoArg Info)           "show version number" ]
+
+opts :: [OptDescr a] -> [String] -> IO ([a], [String])
+opts options argv =
+    case getOpt RequireOrder options argv of
+      (o, n, []) -> return (o, n)
+      (_, _, errs) ->
+          do
+            msg <- use options errs
+            abort msg
+
+use :: [OptDescr a] -> [String] -> IO String  -- Return usage string
+use options errs =
+    do
+      name <- getProgName
+      datadir <- getDataDir
+      let header = "Usage: " ++ name ++ " [OPTIONS]"
+      let footer = "\nDocumentation directory: " ++ datadir
+      return (concat errs ++ usageInfo header options ++ footer)
+
+-- Interpret option flags
+
+interp :: [Flag] -> IO ()
+interp flags =
+    loop flags
+    where
+      loop [] = return ()
+      loop (Info : _) =
+          success cpsaVersion
+      loop (Help : _) =
+          do                    -- Show help then exit with success
+            msg <- use options []
+            success msg
+
+-- From CPSA.Lib.Entry
+
+cpsaVersion :: String
+cpsaVersion = showString "CPSA " (showVersion version)
+
+abort :: String -> IO a         -- Print message then exit with failure
+abort msg =
+    do
+      hPutStrLn stderr msg
+      exitFailure
+
+success :: String -> IO a       -- Print message then exit with success
+success msg =
+    do
+      hPutStrLn stderr msg
+      exitWith ExitSuccess
diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs
--- a/src/CPSA/Lib/Cohort.hs
+++ b/src/CPSA/Lib/Cohort.hs
@@ -63,7 +63,7 @@
         case derivable (avoid k) ts t of
           True -> (acc, ns')
           False -> (graphNode n : acc, ns')
-    Sync (Tran (Just _, _, _))
+    Sync (Tran (Just _, _))
       | not (explainable k n (leadsto k)) ->
           (graphNode n : acc, ns)
     _ -> (acc, ns)
@@ -688,9 +688,9 @@
       loop (ht + 1) acc c
     loop ht acc (Out _ : c) =
       loop (ht + 1) acc c
-    loop ht acc (Sync (Tran (_, Nothing, _)) : c) =
+    loop ht acc (Sync (Tran (_, Nothing)) : c) =
       loop (ht + 1) acc c
-    loop ht acc (Sync (Tran (_, Just next, _)) : c) =
+    loop ht acc (Sync (Tran (_, Just next)) : c) =
       loop (ht + 1) acc' c
       where
         acc' = nextNodeA now g role ht next acc
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
@@ -52,7 +52,7 @@
 displayImpl ctx g =
   L () [S () "implies",
         displayConj ctx (antec g),
-        displayDisj ctx (zip (evars g) (concl g)) ]
+        displayDisj ctx (consq g) ]
 
 displayDisj :: Algebra t p g s e c => c -> [([t], [AForm t])] -> SExpr ()
 displayDisj _ [] = L () [S () "false"]
@@ -180,20 +180,13 @@
       displayDt (Sync t) = L () (displayTran ctx t)
 
 displayTran :: Algebra t p g s e c => c -> Tran t -> [SExpr ()]
-displayTran ctx (Tran(Just now, Just next, Nothing)) =
+displayTran ctx (Tran(Just now, Just next)) =
   [S () "tran", displayTerm ctx now,  displayTerm ctx next]
-displayTran ctx (Tran(Just now, Just next, Just label)) =
-  [S () "tran", displayTerm ctx now,  displayTerm ctx next,
-                displayTerm ctx label]
-displayTran ctx (Tran(Just now, Nothing, Nothing)) =
+displayTran ctx (Tran(Just now, Nothing)) =
   [S () "obsv", displayTerm ctx now]
-displayTran ctx (Tran(Just now, Nothing, Just label)) =
-  [S () "obsv", displayTerm ctx now, displayTerm ctx label]
-displayTran ctx (Tran(Nothing, Just next, Nothing)) =
+displayTran ctx (Tran(Nothing, Just next)) =
   [S () "init", displayTerm ctx next]
-displayTran ctx (Tran(Nothing, Just next, Just label)) =
-  [S () "init", displayTerm ctx next, displayTerm ctx label]
-displayTran _ (Tran(Nothing, Nothing, _)) =
+displayTran _ (Tran(Nothing, Nothing)) =
   assertError("Displayer.displayTran: encountered sync node with current or next state")
 
 -- Display of preskeletons
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
@@ -424,7 +424,7 @@
       fail (shows pos (key ++ " declaration too late in enclosing form"))
     | otherwise = badKey keys xs
 badKey _ _ = return ()
- 
+
 loadTrace :: (Algebra t p g s e c, Monad m) => [t] ->
              [SExpr Pos] -> m [Event t]
 loadTrace vars xs = mapM (loadEvt vars) xs
@@ -443,31 +443,15 @@
     do
       t0 <- loadTerm vars True t0
       t1 <- loadTerm vars True t1
-      return $ Sync $ Tran (Just t0, Just t1, Nothing)
-loadEvt vars (L _ [S _ "tran", t0, t1, t2]) =
-    do
-      t0 <- loadTerm vars True t0
-      t1 <- loadTerm vars True t1
-      t2 <- loadTerm vars True t2
-      return $ Sync $ Tran (Just t0, Just t1, Just t2)
+      return $ Sync $ Tran (Just t0, Just t1)
 loadEvt vars (L _ [S _ "obsv", t0]) =
     do
       t0 <- loadTerm vars True t0
-      return $ Sync $ Tran (Just t0, Nothing, Nothing)
-loadEvt vars (L _ [S _ "obsv", t0, t1]) =
-    do
-      t0 <- loadTerm vars True t0
-      t1 <- loadTerm vars True t1
-      return $ Sync $ Tran (Just t0, Nothing, Just t1)
+      return $ Sync $ Tran (Just t0, Nothing)
 loadEvt vars (L _ [S _ "init", t0]) =
     do
       t0 <- loadTerm vars True t0
-      return $ Sync $ Tran (Nothing, Just t0, Nothing)
-loadEvt vars (L _ [S _ "init", t0, t1]) =
-    do
-      t0 <- loadTerm vars True t0
-      t1 <- loadTerm vars True t1
-      return $ Sync $ Tran (Nothing, Just t0, Just t1)
+      return $ Sync $ Tran (Nothing, Just t0)
 loadEvt _ (L pos [S _ dir, _]) =
     fail (shows pos $ "Malformed direction: " ++ dir)
 loadEvt _ x = fail (shows (annotation x) "Malformed event")
@@ -612,7 +596,7 @@
     | otherwise =
         case trace (insts !! s) !! i of
           Out _ -> fail (shows pos "Priority declaration disallowed on sending")
-          Sync (Tran (Nothing, _, _))
+          Sync (Tran (Nothing, _))
             -> fail (shows pos
                      "Priority declaration disallowed on initializers")
           _ -> do
@@ -937,12 +921,13 @@
   do
     antec <- loadCheckedConj md pos prot vars vars a
     (g, vc) <- loadConclusion pos prot g vars c
-    let (evars, concl) = unzip vc
+    let f (evars, form) = (evars, map snd form)
+    let consq = map f vc        -- Expunge position info
     let goal =
           Goal { uvars = vars,
                  antec = map snd antec,
-                 evars = evars,
-                 concl = map (map snd) concl }
+                 consq = consq,
+                 concl = map snd consq }
     return (g, goal, antec)
 loadImplication _ pos _ _ _ _ = fail (shows pos "Malformed goal implication")
 
@@ -999,7 +984,11 @@
   do
     as <- loadConjunction pos prot vars x
     let as' = L.sortBy (\(_, x) (_, y) -> aFormOrder x y) as
-    unbound <- foldM roleSpecific unbound as'
+    let unbound' =
+          if useFactVars
+          then foldl factSpecific unbound as'
+          else unbound
+    unbound <- foldM roleSpecific unbound' as'
     case unbound of
       [] -> return as'
       (v : _) -> fail (shows (annotation x) ("Malformed defgoal: " ++ showst v " not used"))
@@ -1202,3 +1191,9 @@
   | isStrdVar t' = fail (shows pos "Type mismatch in equals")
   | allBound unbound t && allBound unbound t' = return unbound
   | otherwise = fail (shows pos "Unbound variable in equals")
+
+-- Remove unbound message variables that occur in a fact
+factSpecific :: Algebra t p g s e c => [t] -> (Pos, AForm t) -> [t]
+factSpecific unbound (_, AFact _ fs) =
+  unbound L.\\ foldl addVars [] (L.filter (not . isStrdVar) fs)
+factSpecific unbound _ = unbound
diff --git a/src/CPSA/Lib/Protocol.hs b/src/CPSA/Lib/Protocol.hs
--- a/src/CPSA/Lib/Protocol.hs
+++ b/src/CPSA/Lib/Protocol.hs
@@ -80,13 +80,13 @@
 -- Extract the term in an inbound event.
 inbnd :: Event t -> Maybe t
 inbnd (In t) = Just t
-inbnd (Sync (Tran (Just t,_,_))) = Just t
+inbnd (Sync (Tran (Just t, _))) = Just t
 inbnd _ = Nothing
 
 -- Extract the term in an outbound event.
 outbnd :: Event t -> Maybe t
 outbnd (Out t) = Just t
-outbnd (Sync (Tran (_,Just t,_))) = Just t
+outbnd (Sync (Tran (_, Just t))) = Just t
 outbnd _ = Nothing
 
 {-
@@ -411,7 +411,8 @@
 data Goal t
   = Goal { uvars :: [t],          -- Universally quantified variables
            antec :: [AForm t],    -- Antecedent
-           evars :: [[t]],        -- Existentially quantified variables
+           -- Consequent with existentially quantified variables
+           consq :: [([t], [AForm t])],
            concl :: [[AForm t]] } -- Conclusion
   deriving Show
 
diff --git a/src/CPSA/Lib/Reduction.hs b/src/CPSA/Lib/Reduction.hs
--- a/src/CPSA/Lib/Reduction.hs
+++ b/src/CPSA/Lib/Reduction.hs
@@ -150,7 +150,7 @@
                 do
                   let lk = LPreskel k n (-1) Nothing
                   let ks'' = L.nubBy (\k1 k2 -> isomorphic (gist k1) (gist k2)) ks'
-                  wrt p h (commentPreskel lk [] (unrealized k) Ordinary 
+                  wrt p h (commentPreskel lk [] (unrealized k) Ordinary
                             Preskeleton "Not a skeleton")
                   let lk_nums = zip [(n+1) .. (n+length(ks'))] ks''
                   let lks' = map (\(n', k')-> withParent k' n' lk) lk_nums
@@ -176,7 +176,7 @@
                        Nada "Not closed under rules")
               let (n', seen', todo', _) =
                     foldl (next lk) (n, seen, todo, []) kids
-              loop n' seen' todo' lks
+              loop n' seen' (reverse todo') lks
 
 -- Apply collapse until all possibilities are exhausted.
 search :: Algebra t p g s e c => Options -> Handle ->
diff --git a/src/CPSA/Lib/State.hs b/src/CPSA/Lib/State.hs
--- a/src/CPSA/Lib/State.hs
+++ b/src/CPSA/Lib/State.hs
@@ -4,47 +4,41 @@
 import CPSA.Lib.Algebra
 import CPSA.Lib.Utilities
 
--- A transition
-newtype Tran t = Tran (Maybe t, Maybe t, Maybe t) deriving (Show, Eq, Ord)
+-- A transition (pre-state, post-state)
+newtype Tran t = Tran (Maybe t, Maybe t) deriving (Show, Eq, Ord)
 
 now :: Tran t -> Maybe t
-now (Tran (t, _, _)) = t
+now (Tran (t, _)) = t
 
 next :: Tran t -> Maybe t
-next (Tran (_, t, _)) = t
-
--- Labels are ignored
--- label :: Tran t -> Maybe t
--- label (Tran (_, _, t)) = t
+next (Tran (_, t)) = t
 
 observer :: Tran t -> Bool
-observer (Tran (_, Nothing, _)) = True
+observer (Tran (_, Nothing)) = True
 observer _ = False
 
 path :: Tran t -> Bool
 path x = not (observer x)
 
 transition :: Tran t -> Bool
-transition (Tran (Just _, Just _, _)) = True
+transition (Tran (Just _, Just _)) = True
 transition _ = False
 
 tranTerms :: Tran t -> [t]
-tranTerms (Tran (Nothing, Nothing, _)) =
+tranTerms (Tran (Nothing, Nothing)) =
   assertError ("Encountered sync with no pre- or post-state in State.hs:tranTerms")
-tranTerms (Tran (now, next, label)) =
-  catMaybes [now, next, label]
+tranTerms (Tran (now, next)) =
+  catMaybes [now, next]
 
 mapTran :: (t -> t) -> Tran t -> Tran t
-mapTran f (Tran (now, next, label)) =
-  Tran (maybe Nothing (Just . f) now, maybe Nothing (Just . f) next,
-        maybe Nothing (Just . f) label)
+mapTran f (Tran (now, next)) =
+  Tran (maybe Nothing (Just . f) now, maybe Nothing (Just . f) next)
 
 matchTran :: Algebra t p g s e c => Tran t -> Tran t -> (g, e) -> [(g, e)]
-matchTran (Tran (c, n, l)) (Tran (c', n', l')) ge =
+matchTran (Tran (c, n)) (Tran (c', n')) ge =
   do
-    ge0 <- matchNext c c' ge
-    ge1 <- matchNext n n' ge0
-    matchNext l l' ge1
+    ge <- matchNext c c' ge
+    matchNext n n' ge
 
 matchNext :: Algebra t p g s e c => Maybe t -> Maybe t -> (g, e) -> [(g, e)]
 matchNext Nothing Nothing ge = [ge]
@@ -52,11 +46,10 @@
 matchNext _ _ _ = []
 
 unifyTran :: Algebra t p g s e c => Tran t -> Tran t -> (g, s) -> [(g, s)]
-unifyTran (Tran (c, n, l)) (Tran (c', n', l')) gs =
+unifyTran (Tran (c, n)) (Tran (c', n')) gs =
   do
-    gs0 <- unifyNext c c' gs
-    gs1 <- unifyNext n n' gs0
-    unifyNext l l' gs1
+    gs <- unifyNext c c' gs
+    unifyNext n n' gs
 
 unifyNext :: Algebra t p g s e c => Maybe t -> Maybe t -> (g, s) -> [(g, s)]
 unifyNext Nothing Nothing ge = [ge]
diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs
--- a/src/CPSA/Lib/Strand.hs
+++ b/src/CPSA/Lib/Strand.hs
@@ -1,4 +1,4 @@
--- on data structures and support functions.
+-- Instance and preskeleton data structures and support functions.
 
 -- Copyright (c) 2009 The MITRE Corporation
 --
@@ -9,7 +9,7 @@
 module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener,
     role, env, trace, height, listenerTerm, Sid, Node, mkPreskel,
     firstSkeleton, Pair, Preskel, gen, protocol, kgoals, insts,
-    orderings, leadsto, kfacts,
+    orderings, leadsto, kfacts, useFactVars,
     pov, korig, kcomment, nstrands, kvars, kpriority, kpriorities,
     strandids, kterms, avoid, preskelWellFormed, verbosePreskelWellFormed,
     Strand, inst, nodes, Vertex, preds, event, kabsent,
@@ -74,6 +74,10 @@
 useDeOrigination :: Bool
 useDeOrigination = False -- useThinning
 
+-- Enable variables in facts that do not occur elsewhere in skeletons
+useFactVars :: Bool
+useFactVars = False -- True
+
 -- Sanity check: ensure no role variable occurs in a skeleton.
 useCheckVars :: Bool
 useCheckVars = False
@@ -468,8 +472,8 @@
       checkLeadsto [] _ = []
       checkLeadsto (((s1,i1),(s2,i2)) : rest) consumed =
         case ((trace (insts !! s1)) !! i1) of
-          Sync (Tran (_, Just t, _)) -> case ((trace (insts !! s2)) !! i2) of
-            Sync (Tran (Just t', nxt, _)) ->
+          Sync (Tran (_, Just t)) -> case ((trace (insts !! s2)) !! i2) of
+            Sync (Tran (Just t', nxt)) ->
                if (t /= t') then error ("Strand.mkPreskel: invalid state edge at " ++ show (s1,i1))
                else case nxt of
                  Nothing -> (((s1,i1),(s2,i2)) : checkLeadsto rest consumed)
@@ -599,9 +603,9 @@
 reducedPairWellOrdered (n0, n1) =
     case (event n0, event n1) of
       (Out _, In _) -> True
-      (Sync (Tran (_, Just _, _)), Sync (Tran (Just _, _, _))) ->
+      (Sync (Tran (_, Just _)), Sync (Tran (Just _, _))) ->
         True
-      (Sync (Tran (_, Nothing, _)), Sync (Tran (Just _, Just _, _))) ->
+      (Sync (Tran (_, Nothing)), Sync (Tran (Just _, Just _))) ->
         True
       (Sync _, In _) -> True
       (Out _, Sync _) -> True
@@ -646,12 +650,14 @@
       numbering = dfs preds start'
 
 -- Variables in this preskeleton, excluding ones in roles, and ones
--- that only occur in a cause.
+-- that only occur in a cause.  The variables in facts are explicitly
+-- included.
 kvars :: Algebra t p g s e c => Preskel t g s e -> [t]
 kvars k =
     S.elems $ foldl addIvars dvars (insts k)
     where
-      dvars = foldl f S.empty $ declsTerms (decls k)
+      factVars = if useFactVars then kfactVars k else S.empty
+      dvars = foldl f factVars $ declsTerms (decls k)
       f s t = foldVars (flip S.insert) s t
 
 traceBase :: Int
@@ -694,6 +700,7 @@
       gfacts :: [Fact t],
       nvars :: !Int,           -- Number of variables
       ntraces :: !Int,         -- Number of traces
+      briefs :: [(Int, Int)],  -- Multiset of trace briefs
       norderings :: !Int,      -- Number of orderings
       nleadsto :: !Int,        -- Number of leadsto pairs
       nsndecls :: [Int],       -- Counts of decls
@@ -711,12 +718,17 @@
            gpatterns = patterns,
            nvars = length (kvars k),
            ntraces = length gtraces,
+           briefs = multiset (map fst gtraces),
            norderings = length gorderings,
            nleadsto = length gleadsto,
            nsndecls = nsds gdecls,
            nfacts = length gfacts }
     where
-      gtraces = map (\i -> (height i, trace i)) (insts k)
+      gtraces = map f (insts k)
+      -- Old: f i = (height i, trace i)
+      f i =
+        (brief c, c)
+        where c = trace i
       gorderings = orderings k
       gleadsto = leadsto k
       gdecls = decls k
@@ -724,6 +736,28 @@
       patterns = L.sort (map (tracePattern . trace) (insts k))
       nsds decls = [length (dknon decls), length (dkpnon decls), length (dkunique decls)]
 
+-- Summarize a trace so that two traces don't match unless they have
+-- the same number.  The summary used to be the height of the trace.
+brief :: Algebra t p g s e c => Trace t -> Int
+brief [] = 0
+brief (In _ : c) = 1 + 4 * brief c
+brief (Out _ : c) = 2 + 4 * brief c
+brief (Sync _ : c) = 3 + 4 * brief c
+
+-- Convert a list of integers into a sorted multiset representation.
+-- The output is a list of pairs, (i, n). Integer n gives the
+-- multiplity of integer i in the input list.  List is sorted based on
+-- the first element in each pair.
+multiset :: [Int] -> [(Int, Int)]
+multiset brf =
+  L.foldl insert [] brf
+  where
+    insert [] b = [(b, 1)]
+    insert ((k, n) : brf) b
+      | k == b = (k, n + 1) : brf
+      | k > b = (b, 1) : (k, n) : brf
+      | otherwise = (k, n) : insert brf b
+
 -- Test to see if two preskeletons are isomorphic
 
 -- First, ensure the two preskeletons have:
@@ -748,6 +782,7 @@
 isomorphic g g' =
 --    nvars g == nvars g' &&  -- Wrong in DH
     ntraces g == ntraces g' &&
+    briefs g == briefs g' &&
     norderings g == norderings g' &&
     gpatterns g == gpatterns g' &&
     nleadsto g == nleadsto g' &&
@@ -836,7 +871,7 @@
     checkOrigs g g' fenv perm &&
     checkOrigs g' g renv (invperm perm) &&
     checkFacts g g' fenv perm &&
-    checkFacts g' g fenv (invperm perm) &&
+    checkFacts g' g renv (invperm perm) &&
     containsMapped (permutePair perm) (gorderings g') (gorderings g) &&
     containsMapped (permutePair perm) (gleadsto g') (gleadsto g)
 
@@ -846,7 +881,7 @@
     checkOrigs g g' fenv perm &&
     checkOrigs g' g renv perm &&
     checkFacts g g' fenv perm &&
-    checkFacts g' g fenv (invperm perm) &&
+    checkFacts g' g renv (invperm perm) &&
     containsMapped (permutePair perm) (gorderings g') (gorderings g) &&
     containsMapped (permutePair perm) (gleadsto g') (gleadsto g) &&
     all (\n -> perm !! (prob !! n) == prob' !! n) [0..((length prob)-1)]
@@ -2086,6 +2121,7 @@
     varSubset (kpnon k) terms &&
     all nonCheck (knon k) &&
     all uniqueCheck (kunique k) &&
+    all factCheck (kfacts k) &&
     origNonNullCheck k && ugenNonNullCheck k &&
     wellOrdered k && acyclicOrder k &&
     roleOrigCheck k && fst (declCheck (decls k))
@@ -2094,6 +2130,7 @@
       mesgterms = kmesgterms k
       nonCheck t = all (not . carriedBy t) mesgterms
       uniqueCheck t = any (carriedBy t) mesgterms
+      factCheck f = factVarsElem (kvars k) f
       origNonNullCheck k = (all (\(_, ns) -> not (null ns)) (korig k))
       ugenNonNullCheck k = (all (\(_, ns) -> not (null ns))
                             (filter (\(t, _) -> not (isNum t)) (kugen k)))
@@ -2118,6 +2155,7 @@
                    $ varSubset (kpnon k) terms
       mapM_ nonCheck $ knon k
       mapM_ uniqueCheck $ kunique k
+      mapM_ factCheck $ kfacts k
       origNonNullCheck k
       uniqgenNonNullCheck k
       failwith "ordered pairs not well formed" $ wellOrdered k
@@ -2135,6 +2173,9 @@
       uniqueCheck t =
           failwith (showString "uniq-orig " $ showst t " not carried")
                        $ any (carriedBy t) mesgterms
+      factCheck f =
+          failwith ("a fact var in " ++  factPred f ++ " not in some strand")
+                       $ factVarsElem (kvars k) f
       origNonNullCheck k =
           let ts = filter (\(_, ns) -> null ns) (korig k) in
           failwith (showString "uniq-orig " $
@@ -2163,7 +2204,7 @@
     loop [] _ = True
     loop ((n0, (s, i)) : es) ns =
       case (trace (insts k !! s) !! i) of
-        Sync (Tran (Just _, Just _, _)) ->
+        Sync (Tran (Just _, Just _)) ->
           S.notMember n0 ns && loop es (S.insert n0 ns)
         _ -> loop es ns
 
@@ -2451,7 +2492,7 @@
                                                  else acc
     f acc _ = acc
     xform = filter g es         -- Edges that transform
-    g (_, (Sync t@(Tran (_, Just _, _)), Sync t'@(Tran (Just _, Just _, _)))) =
+    g (_, (Sync t@(Tran (_, Just _)), Sync t'@(Tran (Just _, Just _)))) =
       next t == now t'
     g _ = False
     h t0 pes =
@@ -2520,6 +2561,9 @@
   = Fact String [FTerm t]
   deriving (Eq, Show)
 
+factPred :: Fact t -> String
+factPred (Fact pred _) = pred
+
 substFTerm :: Algebra t p g s e c => s -> FTerm t -> FTerm t
 substFTerm s (FTerm t) = FTerm $ substitute s t
 substFTerm _ t = t
@@ -2565,6 +2609,17 @@
 cleansFacts vs facts =
   L.filter (factVarsElem vs) facts
 
+kfactVars :: Algebra t p g s e c => Preskel t g s e -> Set t
+kfactVars k =
+  foldl (foldFactTerms $ foldVars $ flip S.insert) S.empty (kfacts k)
+
+foldFactTerms :: Algebra t p g s e c => (a -> t -> a) -> a -> Fact t -> a
+foldFactTerms f z (Fact _ ts) =
+  foldl g z ts
+  where
+    g a (FSid _) = a
+    g a (FTerm t) = f a t
+
 {-
 instvars :: Algebra t p g s e c => [Instance t e] -> [t]
 instvars insts =
@@ -2895,7 +2950,7 @@
         if null vas then
           loop rs               -- Rule does not apply
         else
-          Just $ doRewrites 0 prules k r vas
+          Just $ doRewrites prules k r vas
 
 -- Returns the environments that show satifaction of the antecedent
 -- but fail to be extendable to show satifaction of one of the
@@ -2912,24 +2967,31 @@
 ruleLimit = 500
 
 -- Repeatedly applies rules until no rule applies.
-doRewrites :: Algebra t p g s e c => Int -> [Rule t] -> Preskel t g s e ->
+doRewrites :: Algebra t p g s e c => [Rule t] -> Preskel t g s e ->
               Rule t -> [(g, e)] -> [Preskel t g s e]
-doRewrites lim _ _ _ _
+doRewrites rules k r vas =
+  doRewritesLoop rules k (length vas) (doRewrite k r vas) []
+
+doRewritesLoop :: Algebra t p g s e c => [Rule t] -> Preskel t g s e ->
+                  Int -> [Preskel t g s e] -> [Preskel t g s e] ->
+                  [Preskel t g s e]
+doRewritesLoop _ _ lim _ _
   | lim >= ruleLimit =
     error ("Aborting after applying " ++ show ruleLimit ++
            " rules and more are applicable")
-doRewrites lim rules k r vas =
-  concatMap f (doRewrite k r vas)
+doRewritesLoop _ _ _ [] ks = reverse ks
+doRewritesLoop rules k lim (k' : todo) ks =
+  loop rules
   where
-    f k = loop rules
-      where
-        loop [] = [k]           -- No rules apply
-        loop (r : rs) =
-          let vas = tryRule k r in
-            if null vas then
-              loop rs           -- Rule does not apply
-            else
-              doRewrites (lim + 1) rules k r vas
+    loop [] =                   -- No rules apply
+      doRewritesLoop rules k lim todo (k' : ks)
+    loop (r : rs) =
+      let vas = tryRule k' r in
+        if null vas then
+          loop rs               -- Rule does not apply
+        else
+          let new = doRewrite k' r vas in
+            doRewritesLoop rules k (lim + length vas) (todo ++ new) ks
 
 -- Apply rewrite rule at all assignments
 doRewrite :: Algebra t p g s e c => Preskel t g s e ->
@@ -2942,8 +3004,9 @@
                 Rule t -> (g, e) -> [Preskel t g s e]
 doRewriteOne k r e =
   do
-    cl <- concl $ rlgoal r
-    (k, _) <- doConj (rlname r) cl k e
+    (evars, cl) <- consq $ rlgoal r
+    let e' = foldl fresh e evars
+    (k, _) <- doConj (rlname r) cl k e'
     k <- wellFormedPreskel k
     k <- toSkeleton True k
     return $ f k                -- Add comment about rule application
@@ -2951,6 +3014,16 @@
                   L () [S () "rule", S () (rlname r)] :
                   kcomment k }
 
+fresh :: Algebra t p g s e c => (g, e) -> t -> (g, e)
+fresh (g, e) t
+  | isStrdVar t = (g, e)
+  | otherwise =
+      case match t t' (g', e) of
+        e' : _ -> e'
+        [] -> error "Strand.fresh: Cannot match logical variable to clone"
+    where
+      (g', t') = clone g t
+
 type Rewrite t g s e =
   Preskel t g s e -> (g, e) -> [(Preskel t g s e, (g, e))]
 
@@ -3060,30 +3133,29 @@
     Just s
       | height inst < h -> []
       | rname (role inst) == rname r ->
-        rParam k (g, e) t t'
+        rParam name k (g, e) t t'
       | otherwise ->
         do
           (k, (g, e)) <- rDisplace e k' ns s
-          rParam k (g, e) t t'
+          rParam name k (g, e) t t'
       where
         inst = strandInst k s
         t' = instantiate (env inst) v
         k' = addStrand g k r h
         ns = nstrands k
     Nothing ->
-      error ("In rule " ++ name ++ ", parameter predicate for " ++
-             rname r ++ " did not get a strand")
+      error ("In rule " ++ name ++
+             ", parameter predicate did not get a strand")
 
-rParam :: Algebra t p g s e c => Preskel t g s e ->
+rParam :: Algebra t p g s e c => String -> Preskel t g s e ->
           (g, e) -> t -> t -> [(Preskel t g s e, (g, e))]
-rParam k (g, e) t t' =
+rParam name k (g, e) t t' =
   case matched e t of
-    False ->
-      do
-        (g, e) <- match t t' (g, e)
-        return (k, (g, e))
     True ->
       rUnify k (g, e) (instantiate e t) t'
+    False ->
+      error ("In rule " ++ name ++
+             ", parameter predicate did not get a value")
 
 rUnify :: Algebra t p g s e c => Preskel t g s e ->
           (g, e) -> t -> t -> [(Preskel t g s e, (g , e))]
@@ -3196,6 +3268,7 @@
     (True, Just s)
       | elem (t', (s, i)) (dkuniqFull $ decls k) -> [(k, (g, e))]
       | not $ isAtom t' -> []
+      | i >= height (strandInst k s) -> []
       | otherwise ->
         [(k', (g, e))]
         where
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
@@ -258,6 +258,7 @@
       insts :: [Instance t c],
       strands :: [t],           -- A variable for each instance
       orderings :: [((t, Int), (t, Int))],
+      leadsto :: [((t, Int), (t, Int))],
       nons :: [t],
       pnons :: [t],
       uniqs :: [t],
@@ -276,6 +277,7 @@
       insts <- loadInsts prot kvars [] xs
       let heights = map height insts
       orderings <- loadOrderings heights (assoc precedesKey xs)
+      leadsto <- loadOrderings heights (assoc leadstoKey xs)
       nons <- loadBaseTerms kvars (assoc nonOrigKey xs)
       pnons <- loadBaseTerms kvars (assoc pnonOrigKey xs)
       uniqs <- loadBaseTerms kvars (assoc uniqOrigKey xs)
@@ -291,6 +293,7 @@
                         insts = insts,
                         strands = M.elems varmap,
                         orderings = map f orderings,
+                        leadsto = map f leadsto,
                         nons = nons,
                         pnons = pnons,
                         uniqs = uniqs,
@@ -523,6 +526,10 @@
 precedesKey :: String
 precedesKey = "precedes"
 
+-- The key used in preskeletons for leadsto orderings
+leadstoKey :: String
+leadstoKey = "leadsto"
+
 -- The key used in preskeletons for non-originating atoms
 nonOrigKey :: String
 nonOrigKey = "non-orig"
@@ -618,6 +625,7 @@
       insts = map (mapInst env) (insts k),
       strands = zs,
       orderings = mapPair (instantiate env) (orderings k),
+      leadsto = mapPair (instantiate env) (leadsto k),
       nons = map (instantiate env) (nons k),
       pnons = map (instantiate env) (pnons k),
       uniqs = map (instantiate env) (uniqs k),
@@ -666,6 +674,7 @@
    map (lengthForm kctx k) (M.assocs (varmap k)) ++
    concatMap (paramForm kctx) (zip (strands k) $ insts k) ++
    map (precForm kctx) (orderings k) ++
+   map (leadsToForm kctx) (leadsto k) ++
    map (unary "non" kctx) (nons k) ++
    map (unary "pnon" kctx) (pnons k) ++
    -- Not possible map (unary "uniq" kctx) (noOrigUniqs k) ++
@@ -714,6 +723,10 @@
 -- Creates the atomic formula used to describe a node ordering relation
 precForm :: Algebra t p g s e c => c -> ((t, Int), (t, Int)) -> SExpr ()
 precForm = quaternary "prec"
+
+-- Creates the atomic formula used to describe a leads to ordering relation
+leadsToForm :: Algebra t p g s e c => c -> ((t, Int), (t, Int)) -> SExpr ()
+leadsToForm = quaternary "leads-to"
 
 uniqAtForm :: Algebra t p g s e c => c -> (t, (t, Int)) -> SExpr ()
 uniqAtForm = ternary "uniq-at"
diff --git a/src/ocaml/expand.ml b/src/ocaml/expand.ml
--- a/src/ocaml/expand.ml
+++ b/src/ocaml/expand.ml
@@ -95,7 +95,7 @@
 
 let expand o macs x =
   if !need_newline
-  then print_newline ();
+  then output_char o '\n';
   print_sexpr o (expand_all macs x);
   need_newline := true
 
diff --git a/src/ocaml/pp.ml b/src/ocaml/pp.ml
--- a/src/ocaml/pp.ml
+++ b/src/ocaml/pp.ml
@@ -5,7 +5,7 @@
 
 let filter o x =
   if !need_newline
-  then print_newline ();
+  then output_char o '\n';
   print_sexpr o x;
   need_newline := true
 
diff --git a/tst/aik.tst b/tst/aik.tst
--- a/tst/aik.tst
+++ b/tst/aik.tst
@@ -1,6 +1,6 @@
 (herald "Anonymous identity protocol from TCG")
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from aik.scm")
 
 (defprotocol aikprot basic
diff --git a/tst/axiom2.tst b/tst/axiom2.tst
--- a/tst/axiom2.tst
+++ b/tst/axiom2.tst
@@ -1,6 +1,6 @@
 (herald "Axiom 2 Protocol" (bound 20))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from axiom2.scm")
 (comment "Strand count bounded at 20")
 
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 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from blanchet.scm")
 
 (defprotocol blanchet basic
diff --git a/tst/bltk_test.tst b/tst/bltk_test.tst
--- a/tst/bltk_test.tst
+++ b/tst/bltk_test.tst
@@ -1,6 +1,6 @@
 (herald "bltk Test File" (algebra diffie-hellman) (bound 12))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from bltk_test.scm")
 
 (defprotocol test diffie-hellman
diff --git a/tst/dh-ca.tst b/tst/dh-ca.tst
--- a/tst/dh-ca.tst
+++ b/tst/dh-ca.tst
@@ -1,6 +1,6 @@
 (herald dhca (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from dh-ca.scm")
 
 (defprotocol dhca diffie-hellman
diff --git a/tst/dh_mim.tst b/tst/dh_mim.tst
--- a/tst/dh_mim.tst
+++ b/tst/dh_mim.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman protocol, man-in-the-middle attack"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from dh_mim.scm")
 
 (defprotocol dh_mim diffie-hellman
diff --git a/tst/dh_mim2.tst b/tst/dh_mim2.tst
--- a/tst/dh_mim2.tst
+++ b/tst/dh_mim2.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman protocol, man-in-the-middle attack"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from dh_mim2.scm")
 
 (defprotocol dh_mim diffie-hellman
diff --git a/tst/dh_sig.tst b/tst/dh_sig.tst
--- a/tst/dh_sig.tst
+++ b/tst/dh_sig.tst
@@ -1,6 +1,6 @@
 (herald "Signed DH exchange" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from dh_sig.scm")
 
 (defprotocol dh_sig diffie-hellman
diff --git a/tst/dh_test.tst b/tst/dh_test.tst
--- a/tst/dh_test.tst
+++ b/tst/dh_test.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman protocol, man-in-the-middle attack"
   (algebra diffie-hellman) (bound 20))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from dh_test.scm")
 (comment "Strand count bounded at 20")
 
diff --git a/tst/dhnsl_basic.tst b/tst/dhnsl_basic.tst
--- a/tst/dhnsl_basic.tst
+++ b/tst/dhnsl_basic.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from dhnsl_basic.scm")
 
 (defprotocol dhnsl diffie-hellman
diff --git a/tst/dhnsl_use.tst b/tst/dhnsl_use.tst
--- a/tst/dhnsl_use.tst
+++ b/tst/dhnsl_use.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from dhnsl_use.scm")
 
 (defprotocol dhnsl diffie-hellman
diff --git a/tst/enrich.tst b/tst/enrich.tst
--- a/tst/enrich.tst
+++ b/tst/enrich.tst
@@ -1,6 +1,6 @@
 (herald enrich)
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from enrich.scm")
 
 (defprotocol enrich basic
diff --git a/tst/envelope.tst b/tst/envelope.tst
--- a/tst/envelope.tst
+++ b/tst/envelope.tst
@@ -1,6 +1,6 @@
 (herald "Envelope Protocol" (bound 20))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from envelope.scm")
 (comment "Strand count bounded at 20")
 
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 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from ffgg.scm")
 
 (defprotocol ffgg basic
diff --git a/tst/fnof_or.tst b/tst/fnof_or.tst
--- a/tst/fnof_or.tst
+++ b/tst/fnof_or.tst
@@ -2,7 +2,7 @@
   (comment
     "Version using variables of sort mesg, with ltk function emulated."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from fnof_or.scm")
 
 (defprotocol or basic
diff --git a/tst/fnof_test.tst b/tst/fnof_test.tst
--- a/tst/fnof_test.tst
+++ b/tst/fnof_test.tst
@@ -1,7 +1,7 @@
 (herald "Function constraint test protocol"
   (comment "Skeletons 2, 4, and 7 should have no shapes."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from fnof_test.scm")
 
 (defprotocol fnoftest basic
diff --git a/tst/fnof_woolam.tst b/tst/fnof_woolam.tst
--- a/tst/fnof_woolam.tst
+++ b/tst/fnof_woolam.tst
@@ -1,6 +1,6 @@
 (herald "Woo-Lam Protocol, using fnof to emulate ltk function")
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from fnof_woolam.scm")
 
 (defprotocol woolam basic
diff --git a/tst/fnof_yahalom.tst b/tst/fnof_yahalom.tst
--- a/tst/fnof_yahalom.tst
+++ b/tst/fnof_yahalom.tst
@@ -2,7 +2,7 @@
   "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function"
   (bound 12))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from fnof_yahalom.scm")
 
 (defprotocol yahalom 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 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from goals.scm")
 
 (defprotocol ns basic
diff --git a/tst/iadh_um.tst b/tst/iadh_um.tst
# file too large to diff: tst/iadh_um.tst
diff --git a/tst/injection.tst b/tst/injection.tst
--- a/tst/injection.tst
+++ b/tst/injection.tst
@@ -2,7 +2,7 @@
   (comment "This protocol contains a man-in-the-middle"
     "attack discovered by Galvin Lowe."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from injection.scm")
 
 (defprotocol ns diffie-hellman
diff --git a/tst/kerb.tst b/tst/kerb.tst
--- a/tst/kerb.tst
+++ b/tst/kerb.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from kerb.scm")
 
 (defprotocol kerb-flawed 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 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from kerberos++.scm")
 
 (defprotocol kerberos basic
diff --git a/tst/lt_test.tst b/tst/lt_test.tst
--- a/tst/lt_test.tst
+++ b/tst/lt_test.tst
@@ -2,7 +2,7 @@
   (comment "First and third skeletons should have a shape,"
     "second and fourth should be dead."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from lt_test.scm")
 
 (defprotocol lttest basic
diff --git a/tst/neq_test.tst b/tst/neq_test.tst
--- a/tst/neq_test.tst
+++ b/tst/neq_test.tst
@@ -2,7 +2,7 @@
   (comment "First skeleton should have a shape,"
     "second, and hird should be dead."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from neq_test.scm")
 
 (defprotocol neqtest basic
diff --git a/tst/ns.tst b/tst/ns.tst
--- a/tst/ns.tst
+++ b/tst/ns.tst
@@ -2,7 +2,7 @@
   (comment "This protocol contains a man-in-the-middle"
     "attack discovered by Galvin Lowe."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from ns.scm")
 
 (defprotocol ns 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 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from or.scm")
 
 (defprotocol or basic
diff --git a/tst/owang.tst b/tst/owang.tst
--- a/tst/owang.tst
+++ b/tst/owang.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from owang.scm")
 
 (defprotocol wang basic
diff --git a/tst/owat.tst b/tst/owat.tst
--- a/tst/owat.tst
+++ b/tst/owat.tst
@@ -1,7 +1,7 @@
 (herald "One-way Authentication Test with bltk keys"
   (algebra diffie-hellman) (bound 12))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from owat.scm")
 
 (defprotocol owa diffie-hellman
diff --git a/tst/pkinit.tst b/tst/pkinit.tst
--- a/tst/pkinit.tst
+++ b/tst/pkinit.tst
@@ -1,6 +1,6 @@
 (herald "Kerberos PKINIT")
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from pkinit.scm")
 
 (defprotocol pkinit-flawed basic
diff --git a/tst/plaindh.tst b/tst/plaindh.tst
--- a/tst/plaindh.tst
+++ b/tst/plaindh.tst
@@ -1,7 +1,7 @@
 (herald "Plain diffie-hellman protocol with challenge-response"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from plaindh.scm")
 
 (defprotocol plaindh diffie-hellman
diff --git a/tst/priority_test.tst b/tst/priority_test.tst
--- a/tst/priority_test.tst
+++ b/tst/priority_test.tst
@@ -1,6 +1,6 @@
 (herald "Receive priority test protocol")
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from priority_test.scm")
 
 (defprotocol priority_test basic
diff --git a/tst/reflect.tst b/tst/reflect.tst
--- a/tst/reflect.tst
+++ b/tst/reflect.tst
@@ -1,6 +1,6 @@
 (herald reflect)
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from reflect.scm")
 
 (defprotocol reflect basic
diff --git a/tst/staticdh.tst b/tst/staticdh.tst
--- a/tst/staticdh.tst
+++ b/tst/staticdh.tst
@@ -1,6 +1,6 @@
 (herald "Static DH key exchange" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from staticdh.scm")
 
 (defprotocol staticdh1 diffie-hellman
diff --git a/tst/station.tst b/tst/station.tst
--- a/tst/station.tst
+++ b/tst/station.tst
@@ -1,6 +1,6 @@
 (herald "Station-to-station protocol" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from station.scm")
 
 (defprotocol station-to-station diffie-hellman
diff --git a/tst/station2.tst b/tst/station2.tst
--- a/tst/station2.tst
+++ b/tst/station2.tst
@@ -1,6 +1,6 @@
 (herald "Station-to-station protocol" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from station2.scm")
 
 (defprotocol station-to-station diffie-hellman
diff --git a/tst/subsort_test.tst b/tst/subsort_test.tst
--- a/tst/subsort_test.tst
+++ b/tst/subsort_test.tst
@@ -2,7 +2,7 @@
   (comment "First, third, and fourth skeletons should have a shape,"
     "second should be dead."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from subsort_test.scm")
 
 (defprotocol subsorttest basic
diff --git a/tst/test_small.tst b/tst/test_small.tst
--- a/tst/test_small.tst
+++ b/tst/test_small.tst
@@ -1,6 +1,6 @@
 (herald "small test" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from test_small.scm")
 
 (defprotocol test diffie-hellman
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 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from unilateral.scm")
 
 (defprotocol unilateral basic
diff --git a/tst/uniq-gen-test.tst b/tst/uniq-gen-test.tst
--- a/tst/uniq-gen-test.tst
+++ b/tst/uniq-gen-test.tst
@@ -1,7 +1,7 @@
 (herald "Unique generation test protocols."
   (comment "Skeletons 2, 4, and 7 should have no shapes."))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from uniq-gen-test.scm")
 
 (defprotocol uniqgentest 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 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from woolam.scm")
 
 (defprotocol woolam basic
diff --git a/tst/wrap_decrypt.tst b/tst/wrap_decrypt.tst
--- a/tst/wrap_decrypt.tst
+++ b/tst/wrap_decrypt.tst
@@ -1,6 +1,6 @@
 (herald wrap-decrypt (bound 10))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from wrap_decrypt.lsp")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/yahalom.tst b/tst/yahalom.tst
--- a/tst/yahalom.tst
+++ b/tst/yahalom.tst
@@ -1,7 +1,7 @@
 (herald "Yahalom Protocol with Forwarding Removed"
   (algebra diffie-hellman) (bound 12))
 
-(comment "CPSA 3.6.2")
+(comment "CPSA 3.6.3")
 (comment "All input read from yahalom.scm")
 
 (defprotocol yahalom diffie-hellman