diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,23 @@
+2019-10-21  John D. Ramsdell  <ramsdell@gootoo.mitre.org>
+
+	* cpsa.cabal (Version): Tagged as 3.6.4
+
+2019-10-21  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Utilities.hs: Used the C preprocessor to allow
+	compilation using older versions of GHC.
+
+2019-10-15  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Utilities.hs: Updated code to support the removal
+	of fail from Monad as implemented in base-4.13.0.0.
+
+2019-09-16  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Strand.hs (thinManyStrands):  Replaced isomorphic
+	check with probIsomorphic check so that strands in the
+	point-of-view remain unmodified.
+
 2019-08-26  John D. Ramsdell  <ramsdell@mitre.org>
 
 	* cpsa.cabal (Version): Tagged as 3.6.3
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,14 @@
 CPSA NEWS
 
+  October 2019:
+
+* Release 3.6.4 adds support for the latest version of the GHC
+  compiler.  As of version 8.8, the Monad type class no longer
+  contains the fail method, and that method is now provided by the
+  MonadFail type class.  This version of CPSA makes use of the C
+  preprocessor to handle this incompatible change.  The release also
+  fixes a bug in thinning.
+
   August 2019:
 
 * Release 3.6.3 adds the cpsainit program and fixes bugs.  The
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,10 +1,10 @@
-Name:			cpsa
-Version:		3.6.3
-Maintainer:		mliskov@mitre.org
-Cabal-Version:		>= 1.6
-License:		BSD3
-License-File:		license.txt
-Synopsis:		Symbolic cryptographic protocol analyzer
+Name:                   cpsa
+Version:                3.6.4
+Maintainer:             mliskov@mitre.org
+Cabal-Version:          >= 1.6
+License:                BSD3
+License-File:           license.txt
+Synopsis:               Symbolic cryptographic protocol analyzer
 Description:
   The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to
   enumerate all essentially different executions possibe for a
@@ -46,8 +46,8 @@
   F. Doghmi, F. Javier Thayer, Paul D. Rowe, and Moses D. Liskov.
   John D. Ramsdell and Moses D. Liskov implemented the algorithm in
   Haskell.  CPSA was designed and implemented at The MITRE Corporation.
-Category:		Cryptography
-Build-Type:		Simple
+Category:               Cryptography
+Build-Type:             Simple
 Data-Files:
   Make.hs cpsa.mk cpsamanual.pdf examples/blanchet.scm
   examples/blanchet.xhtml examples/bltk_or.scm examples/bltk_or.xhtml
@@ -73,7 +73,7 @@
   examples/fluffy_draft03_pske.scm examples/eq_test.scm
   init/Makefile init/template.lisp
   examples/eq_test.xhtml
-Data-Dir:	    	doc
+Data-Dir:               doc
 Extra-Source-Files:
   Makefile ChangeLog README.txt NEWS ghci cpsatst setup.bat
   src/cpsa.el src/cpsaops.scm src/cpsa.pl src/pp.pl
@@ -112,17 +112,22 @@
   tst/wrap_decrypt.tst tst/yahalom.scm tst/yahalom.tst
   tst/aik.scm tst/aik.tst tst/reflect.scm tst/reflect.tst
   tst/station.scm tst/station.tst tst/kerb.scm tst/kerb.tst
+  tst/attest.scm tst/attest.tst tst/comp_test.scm tst/comp_test.tst
+  tst/fluffy_draft03_gske.scm tst/fluffy_draft03_gske.tst
+  tst/ordered.scm tst/ordered.tst tst/prottrans.scm tst/prottrans.tst
+  tst/role_uniq.scm tst/role_uniq.tst tst/rule-order.scm
+  tst/rule-order.tst tst/trust-anchor.scm tst/trust-anchor.tst
   
 Source-Repository head
   Type:     git
   Location: git://github.com/mitre/cpsa.git
 
 Executable cpsa
-  Main-Is:		CPSA/Lib/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers, parallel
+  Main-Is:              CPSA/Lib/Main.hs
+  Build-Depends:        base >= 4 && < 5, containers, parallel
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded -rtsopts
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities
     CPSA.Lib.Pretty CPSA.Lib.SExpr CPSA.Lib.Printer CPSA.Lib.Entry
@@ -133,11 +138,11 @@
     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra CPSA.Lib.Declaration
 
 Executable cpsagraph
-  Main-Is:		CPSA/Graph/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/Graph/Main.hs
+  Build-Depends:        base >= 4 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Notation CPSA.Lib.Entry CPSA.Lib.Algebra
@@ -147,22 +152,22 @@
     CPSA.Graph.ExpandedView CPSA.Graph.LaTeXView CPSA.Basic.Algebra
 
 Executable cpsashapes
-  Main-Is:		CPSA/Shapes/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/Shapes/Main.hs
+  Build-Depends:        base >= 4 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
     CPSA.Shapes.Shapes CPSA.Basic.Algebra
 
 Executable cpsaannotations
-  Main-Is:		CPSA/Annotations/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/Annotations/Main.hs
+  Build-Depends:        base >= 4 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
@@ -170,76 +175,76 @@
     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra
     
 Executable cpsadiff
-  Main-Is:		CPSA/Diff/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/Diff/Main.hs
+  Build-Depends:        base >= 3 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
     CPSA.Basic.Algebra
 
 Executable cpsasas
-  Main-Is:		CPSA/SAS/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/SAS/Main.hs
+  Build-Depends:        base >= 4 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.SAS.SAS
     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra
 
 Executable cpsapp
-  Main-Is:		CPSA/Pretty/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/Pretty/Main.hs
+  Build-Depends:        base >= 3 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
     CPSA.Basic.Algebra
 
 Executable cpsajson
-  Main-Is:		CPSA/JSON/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/JSON/Main.hs
+  Build-Depends:        base >= 3 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
     CPSA.Basic.Algebra
 
 Executable cpsadebase
-  Main-Is:		CPSA/Debase/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/Debase/Main.hs
+  Build-Depends:        base >= 3 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
     CPSA.Basic.Algebra
 
 Executable cpsamatch
-  Main-Is:		CPSA/Match/Main.hs
-  Build-Depends:	base >= 3 && < 5, containers
+  Main-Is:              CPSA/Match/Main.hs
+  Build-Depends:        base >= 4 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     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
+  Main-Is:              CPSA/Init/Main.hs
+  Build-Depends:        base, directory
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
-  Hs-Source-Dirs:	src
+  Hs-Source-Dirs:       src
   Other-Modules:
     Paths_cpsa
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
@@ -6,6 +6,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Annotations.Annotations (Prot, annotations) where
 
 import Control.Monad
@@ -28,7 +34,7 @@
 -- generator.  The third argument is the protocol information required
 -- for processing preskeletons.
 
-annotations :: (Algebra t p g s e c, Monad m) => String -> g ->
+annotations :: (Algebra t p g s e c, MonadFail m) => String -> g ->
          [Prot t g] -> SExpr Pos -> m ([Prot t g], SExpr Pos)
 annotations name origin ps x@(L pos (S _ "defprotocol" : xs)) =
     do
@@ -61,7 +67,7 @@
 
 -- Load a protocol.  On success, returns a Prot record.
 
-loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->
+loadProt :: (Algebra t p g s e c, MonadFail m) => String -> g ->
             Pos -> [SExpr Pos] -> m (Prot t g)
 loadProt nom origin pos (S _ name : S _ alg : x : xs)
     | alg /= nom =
@@ -78,12 +84,12 @@
 -- every variable that occurs in a preskeleton never occurs in one of
 -- its roles.
 
-loadRoles :: (Algebra t p g s e c, Monad m) => g ->
+loadRoles :: (Algebra t p g s e c, MonadFail m) => g ->
              [SExpr Pos] -> m (g, [Role t])
 loadRoles origin xs =
     mapAccumLM loadRole origin xs
 
-loadRole :: (Algebra t p g s e c, Monad m) => g ->
+loadRole :: (Algebra t p g s e c, MonadFail m) => g ->
             SExpr Pos -> m (g, Role t)
 loadRole gen (L pos (S _ "defrole" :
                      S _ name :
@@ -100,7 +106,7 @@
 loadRole _ x =
     fail (shows (annotation x) "Malformed role")
 
-loadFormulas :: (Algebra t p g s e c, Monad m) => Pos -> [t] -> Int ->
+loadFormulas :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] -> Int ->
                 g -> [SExpr Pos] -> m (g, t, [Formula t])
 loadFormulas pos vars len gen (x : xs) =
     do
@@ -116,7 +122,7 @@
 loadFormulas pos _ _ _ [] =
     fail (shows pos "Role missing annotations")
 
-loadIndexedFormula :: (Algebra t p g s e c, Monad m) => [t] -> Int ->
+loadIndexedFormula :: (Algebra t p g s e c, MonadFail m) => [t] -> Int ->
                       g -> SExpr Pos -> m (g, (Int, Formula t))
 loadIndexedFormula _ len _ (L _ [N pos i, _])
     | i < 0 || i >= len = fail (shows pos "Bad index for formula")
@@ -128,7 +134,7 @@
     fail (shows (annotation x) "Malformed indexed formula")
 
 -- Ensure there are no formulas with the same index
-checkIndices :: (Algebra t p g s e c, Monad m) => Pos ->
+checkIndices :: (Algebra t p g s e c, MonadFail m) => Pos ->
                 [(Int, Formula t)] -> m ()
 checkIndices _ [] = return ()
 checkIndices pos ((i, _) : alist)
@@ -167,7 +173,7 @@
 
 -- Find protocol and then load preskeleton.
 -- Remove any old annotations, and add new ones.
-findPreskel :: (Algebra t p g s e c, Monad m) => Pos ->
+findPreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->
                [Prot t g] -> [SExpr Pos] -> m (SExpr Pos)
 findPreskel pos ps (S _ name : xs) =
     case L.find (\p -> name == pname p) ps of
@@ -178,7 +184,7 @@
             return (L pos (S pos "defskeleton" : S pos name : xs))
 findPreskel pos _ _ = fail (shows pos "Malformed skeleton")
 
-updatePreskel :: (Algebra t p g s e c, Monad m) => Pos ->
+updatePreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->
                  Prot t g -> [SExpr Pos] -> m [SExpr Pos]
 updatePreskel pos prot (vs@(L _ (S _ "vars" : vars)) : xs)
     | not (realized xs) || not (hasKey tracesKey xs) =
@@ -199,7 +205,7 @@
 realized xs =
     null (assoc "unrealized" xs) && hasKey "unrealized" xs
 
-loadPreskel :: (Algebra t p g s e c, Monad m) => Prot t g ->
+loadPreskel :: (Algebra t p g s e c, MonadFail m) => Prot t g ->
                g -> [t] -> [SExpr Pos] -> m (Preskel t g e)
 loadPreskel prot gen kvars xs =
     do
@@ -212,7 +218,7 @@
                         traces = traces,
                         orderings = orderings })
 
-loadInsts :: (Algebra t p g s e c, Monad m) => Prot t g ->
+loadInsts :: (Algebra t p g s e c, MonadFail m) => Prot t g ->
              g -> [t] -> [Instance t e] -> [SExpr Pos] ->
              m [Instance t e]
 loadInsts prot gen kvars insts (L pos (S _ "defstrand" : x) : xs) =
@@ -235,7 +241,7 @@
 loadInsts _ _ _ insts _ =
     return (reverse insts)
 
-loadInst :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadInst :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
             g -> [t] -> String -> Int -> [SExpr Pos] ->
             m (g, Instance t e)
 loadInst pos prot gen kvars role height env =
@@ -248,14 +254,14 @@
       return (gen', Instance { pos = pos, role = Just r,
                                env = env, height = height })
 
-lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t)
+lookupRole :: MonadFail m => Pos -> Prot t g -> String -> m (Role t)
 lookupRole pos prot role =
     case L.find (\r -> role == rname r) (roles prot) of
       Nothing ->
           fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname prot)
       Just r -> return r
 
-loadMaplet :: (Algebra t p g s e c, Monad m) =>
+loadMaplet :: (Algebra t p g s e c, MonadFail m) =>
               [t] -> [t] -> (g, e) -> SExpr Pos -> m (g, e)
 loadMaplet kvars vars env (L pos [domain, range]) =
     do
@@ -268,11 +274,11 @@
 
 -- Load a trace
 
-loadTrace :: Monad m => SExpr Pos -> m Trace
+loadTrace :: MonadFail m => SExpr Pos -> m Trace
 loadTrace (L _ xs) = mapM loadDt xs
 loadTrace x = fail (shows (annotation x) "Malformed trace")
 
-loadDt :: Monad m => SExpr Pos -> m Dir
+loadDt :: MonadFail m => SExpr Pos -> m Dir
 loadDt (L _ [S _ "recv", _]) = return InDir
 loadDt (L _ [S _ "send", _]) = return OutDir
 loadDt (L _ [S _ "sync", _]) = return SyncDir
@@ -282,7 +288,7 @@
 
 -- Load the node orderings
 
-loadOrderings :: Monad m => Strands -> [SExpr Pos] -> m [Pair]
+loadOrderings :: MonadFail m => Strands -> [SExpr Pos] -> m [Pair]
 loadOrderings _ [] = return []
 loadOrderings strands (x : xs) =
     do
@@ -290,7 +296,7 @@
       nps <- loadOrderings strands xs
       return (adjoin np nps)
 
-loadPair :: Monad m => [Int] -> SExpr Pos -> m Pair
+loadPair :: MonadFail m => [Int] -> SExpr Pos -> m Pair
 loadPair heights (L pos [x0, x1]) =
     do
       n0 <- loadNode heights x0
@@ -302,7 +308,7 @@
       sameStrands (s0, _) (s1, _) = s0 == s1
 loadPair _ x = fail (shows (annotation x) "Malformed pair")
 
-loadNode :: Monad m => [Int] -> SExpr Pos -> m Node
+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node
 loadNode heights (L pos [N _ s, N _ p])
     | s < 0 = fail (shows pos "Negative strand in node")
     | p < 0 = fail (shows pos "Negative position in node")
@@ -323,7 +329,7 @@
 type Annotations t = Maybe (t, [Formula t])
 
 -- Construct the annotations for an instance
-instAnnos :: (Algebra t p g s e c, Monad m) =>
+instAnnos :: (Algebra t p g s e c, MonadFail m) =>
              Instance t e -> m (Annotations t)
 -- A listener has no annotations
 instAnnos (Instance { role = Nothing }) = return Nothing
@@ -344,7 +350,7 @@
     addToContext emptyContext vars
 
 -- Instantiate term and ensure all the free variables have been mapped.
-transTerm :: (Algebra t p g s e c, Monad m) => Pos -> [t] -> e -> t -> m t
+transTerm :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] -> e -> t -> m t
 transTerm pos vars env t =
     let t' = instantiate env t in
     case L.find (flip S.member (fv t')) vars of
@@ -356,7 +362,7 @@
       fv t = foldVars (flip S.insert) S.empty t
 
 -- Instantiate formula and ensure all the free variables have been mapped.
-transForm :: (Algebra t p g s e c, Monad m) => Pos -> [t] -> e ->
+transForm :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] -> e ->
              Formula t -> m (Formula t)
 transForm pos vars env f =
     let f' = finstantiate env f in
@@ -427,7 +433,7 @@
 successors strands =
     [((s, p), (s, p + 1)) | (s, n) <- zip [0..] strands, p <- nats (n - 1)]
 
-before :: Monad m => Pos -> Preskel t g e -> m [(Node, [Node])]
+before :: MonadFail m => Pos -> Preskel t g e -> m [(Node, [Node])]
 before pos k =
     case isAcyclic graph nodes of
       False -> fail (shows pos "Cycle found")
@@ -450,7 +456,7 @@
 
 type Obligation t = (Node, t, Formula t)
 
-obligations :: (Algebra t p g s e c, Monad m) => Pos ->
+obligations :: (Algebra t p g s e c, MonadFail m) => Pos ->
                Preskel t g e -> [Annotations t] -> m [Obligation t]
 obligations pos k annos =
     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
@@ -6,12 +6,19 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Annotations.Formulas (Formula, truth, true, says, implies,
     freeVars, finstantiate, mapAccumLM, loadDecls, loadFormula,
     displayFormula) where
 
 import Control.Monad
 import qualified Data.Set as S
+import CPSA.Lib.Utilities
 import CPSA.Lib.SExpr
 import CPSA.Lib.Algebra
 
@@ -136,7 +143,7 @@
 -- the loading process so that every bound variable is quantified
 -- once, and no free variable is bound within a formula.  Use
 -- loadDecls to ensure vars are not keywords.
-loadFormula :: (Algebra t p g s e c, Monad m) => [t] -> g ->
+loadFormula :: (Algebra t p g s e c, MonadFail m) => [t] -> g ->
                SExpr Pos -> m (g, Formula t)
 loadFormula vars gen (L _ (S _ pred : xs)) -- Atomic formula
     | notElem pred keywords =
@@ -175,77 +182,33 @@
 loadFormula _ _ x =
     fail (shows (annotation x) "Malformed formula")
 
-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
-    LeftS l >>= _ = LeftS l
-    RightS r >>= k = k r
-    fail s = LeftS s
-
-{- Monad laws
-
-1. return a >>= k          <==> k a
-
-RightS r >>= k ==> k r
-
-2. m >>= return            <==> m
-
-  Cases on m
-  a. m is RightS r
-     RightS r >>= RightS ==> RightS r ==> m
-  b. m is LeftS l
-     LeftS l >>= RightS ==> LeftS l ==> m
-
-3. m >>= (\x -> k x >>= h) <===> (m >>= k) >>= h
-
-  Cases on m
-  a. m is RightS r
-     1. RightS r >>= (\x -> k x >>= h) ==> k r >>= h
-     2. (RightS r >> k) >>= h ==> k r >>= h
-  b. m is LeftS l ==>
-     1. LeftS l >>= (\x -> k x >>= h) ==> LeftS l
-     2. (LeftS l >>= k) >>= h ==> LeftS l >>= h ==> LeftS l
--}
-
-loadFTerms :: (Algebra t p g s e c, Monad m) => [t] ->
+loadFTerms :: (Algebra t p g s e c, MonadFail m) => [t] ->
               [SExpr Pos] -> m [FTerm t]
 loadFTerms vars xs =
     foldM f [] (reverse xs)
     where
       f acc x =
           case loadFTerm vars x of
-            RightS t -> return (t : acc)
-            LeftS msg -> fail msg
+            Return t -> return (t : acc)
+            Fail msg -> fail msg
 
 -- Load a formula term
 loadFTerm :: Algebra t p g s e c => [t] -> SExpr Pos ->
-             EitherS (FTerm t)
+             ReturnFail (FTerm t)
 loadFTerm vars x =
     case loadTerm vars False x of
-      RightS t -> return (AlgTerm t)
-      LeftS msg ->              -- If x is not an algebra term
+      Return t -> return (AlgTerm t)
+      Fail msg ->               -- If x is not an algebra term
           case x of             -- see if it's an application
             L _ (S pos fun : xs)
                 | elem fun keywords ->
-                    LeftS (shows pos $
+                    Fail (shows pos $
                            "Keyword " ++ fun ++ " used as a function")
                 | otherwise ->
                  case mapM (loadFTerm vars) xs of
-                   RightS ts -> RightS (Application fun ts)
-                   LeftS _ -> LeftS msg
-            _ -> LeftS msg
+                   Return ts -> Return (Application fun ts)
+                   Fail _ -> Fail msg
+            _ -> Fail msg
 
 -- A monad version of map accumulation from the left
 mapAccumLM :: Monad m => (a -> b -> m (a, c)) -> a -> [b] -> m (a, [c])
@@ -260,7 +223,7 @@
 -- Load a quantified formula.  Note that loadVars returns variables in
 -- reverse order, so list append is the correct way to extend the list
 -- of variables that are in scope.
-loadQuantified :: (Algebra t p g s e c, Monad m) =>
+loadQuantified :: (Algebra t p g s e c, MonadFail m) =>
                   ([t] -> Formula t -> Formula t) ->
                   [t] -> g -> [SExpr Pos] -> SExpr Pos ->
                   m (g, Formula t)
@@ -270,7 +233,7 @@
       (gen'', f) <- loadFormula (vars' ++ vars) gen' body
       return (gen'', build (reverse vars') f)
 
-loadDecls :: (Algebra t p g s e c, Monad m) => g ->
+loadDecls :: (Algebra t p g s e c, MonadFail m) => g ->
              [SExpr Pos] -> m (g, [t])
 loadDecls gen decls =
     do
@@ -278,7 +241,7 @@
       loadVars gen decls
 
 -- Fail if a variable is used as a keyword
-checkDecl :: Monad m => SExpr Pos -> m ()
+checkDecl :: MonadFail m => SExpr Pos -> m ()
 checkDecl (L _ (S pos sym : _))
     | elem sym keywords =
         fail (shows pos "Keyword " ++ sym ++ " used as a variable")
diff --git a/src/CPSA/Basic/Algebra.hs b/src/CPSA/Basic/Algebra.hs
--- a/src/CPSA/Basic/Algebra.hs
+++ b/src/CPSA/Basic/Algebra.hs
@@ -14,8 +14,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
-{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiParamTypeClasses, CPP #-}
 
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Basic.Algebra (name, origin) where
 
 import Control.Monad (foldM)
@@ -937,20 +941,20 @@
 
 -- Term specific loading functions
 
-loadVars :: Monad m => Gen -> [SExpr Pos] -> m (Gen, [Term])
+loadVars :: MonadFail m => Gen -> [SExpr Pos] -> m (Gen, [Term])
 loadVars gen sexprs =
     do
       pairs <- mapM loadVarPair sexprs
       (g, vars) <- foldM loadVar (gen, []) (concat pairs)
       return (g, reverse vars)
 
-loadVarPair :: Monad m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)]
+loadVarPair :: MonadFail m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)]
 loadVarPair (L _ (x:y:xs)) =
     let (t:vs) = reverse (x:y:xs) in
     return [(v,t) | v <- reverse vs]
 loadVarPair x = fail (shows (annotation x) "Bad variable declaration")
 
-loadVar :: Monad m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->
+loadVar :: MonadFail m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->
            m (Gen, [Term])
 loadVar (gen, vars) (S pos name, S pos' sort) =
     case loadLookup pos vars name of
@@ -981,25 +985,25 @@
     let name' = idName (varId t) in
     if name' == name then Right t else loadLookup pos u name
 
-loadLookupName :: Monad m => Pos -> [Term] -> String -> m Term
+loadLookupName :: MonadFail m => Pos -> [Term] -> String -> m Term
 loadLookupName pos vars name =
     either fail f (loadLookup pos vars name)
     where
       f t@(F Name [I _]) = return t
       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be a name")
 
-loadLookupAkey :: Monad m => Pos -> [Term] -> String -> m Term
+loadLookupAkey :: MonadFail m => Pos -> [Term] -> String -> m Term
 loadLookupAkey pos vars name =
     either fail f (loadLookup pos vars name)
     where
       f t@(F Akey [I _]) = return t
       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be an akey")
 
-loadTerm2 :: Monad m => [Term] -> Bool -> SExpr Pos -> m Term
+loadTerm2 :: MonadFail m => [Term] -> Bool -> SExpr Pos -> m Term
 loadTerm2 vars _ pos = loadTerm vars pos
 
 -- Load term and check that it is well-formed.
-loadTerm :: Monad m => [Term] -> SExpr Pos -> m Term
+loadTerm :: MonadFail m => [Term] -> SExpr Pos -> m Term
 loadTerm vars (S pos s) =
     either fail return (loadLookup pos vars s)
 loadTerm _ (Q _ t) =
@@ -1012,7 +1016,7 @@
 
 type LoadFunction m = Pos -> [Term] -> [SExpr Pos] -> m Term
 
-loadDispatch :: Monad m => [(String, LoadFunction m)]
+loadDispatch :: MonadFail m => [(String, LoadFunction m)]
 loadDispatch =
     [("pubk", loadPubk)
     ,("privk", loadPrivk)
@@ -1025,7 +1029,7 @@
 
 -- Atom constructors: pubk privk invk ltk
 
-loadPubk :: Monad m => LoadFunction m
+loadPubk :: MonadFail m => LoadFunction m
 loadPubk _ vars [S pos s] =
     do
       t <- loadLookupName pos vars s
@@ -1036,7 +1040,7 @@
       return $ F Akey [F Pubk [C c, I $ varId t]]
 loadPubk pos _ _ = fail (shows pos "Malformed pubk")
 
-loadPrivk :: Monad m => LoadFunction m
+loadPrivk :: MonadFail m => LoadFunction m
 loadPrivk _ vars [S pos s] =
     do
       t <- loadLookupName pos vars s
@@ -1047,7 +1051,7 @@
       return $ F Akey [F Invk [F Pubk [C c, I $ varId t]]]
 loadPrivk pos _ _ = fail (shows pos "Malformed privk")
 
-loadInvk :: Monad m => LoadFunction m
+loadInvk :: MonadFail m => LoadFunction m
 loadInvk _ vars [S pos s] =
     do
       t <- loadLookupAkey pos vars s
@@ -1081,7 +1085,7 @@
         _ -> fail (shows (annotation t) "Expecting an akey")
 loadInvk pos _ _ = fail (shows pos "Malformed invk")
 
-loadLtk :: Monad m => LoadFunction m
+loadLtk :: MonadFail m => LoadFunction m
 loadLtk _ vars [S pos s, S pos' s'] =
     do
       t <- loadLookupName pos vars s
@@ -1091,14 +1095,14 @@
 
 -- Term constructors: cat enc
 
-loadCat :: Monad m => LoadFunction m
+loadCat :: MonadFail m => LoadFunction m
 loadCat _ vars (l : ls) =
     do
       ts <- mapM (loadTerm vars) (l : ls)
       return $ foldr1 (\a b -> F Cat [a, b]) ts
 loadCat pos _ _ = fail (shows pos "Malformed cat")
 
-loadEnc :: Monad m => LoadFunction m
+loadEnc :: MonadFail m => LoadFunction m
 loadEnc pos vars (l : l' : ls) =
     do
       let (butLast, last) = splitLast l (l' : ls)
@@ -1114,7 +1118,7 @@
       loop z x [] = (reverse z, x)
       loop z x (y : ys) = loop (x : z) y ys
 
-loadHash :: Monad m => LoadFunction m
+loadHash :: MonadFail m => LoadFunction m
 loadHash _ vars (l : ls) =
    do
      ts <- mapM (loadTerm vars) (l : ls)
diff --git a/src/CPSA/DiffieHellman/Algebra.hs b/src/CPSA/DiffieHellman/Algebra.hs
--- a/src/CPSA/DiffieHellman/Algebra.hs
+++ b/src/CPSA/DiffieHellman/Algebra.hs
@@ -98,6 +98,10 @@
 
 {-# LANGUAGE MultiParamTypeClasses, CPP #-}
 
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 -- Fail on non-canonical terms with this is defined
 -- #define CANONICAL
 
@@ -2416,20 +2420,20 @@
 
 -- Term specific loading functions
 
-loadVars :: Monad m => Gen -> [SExpr Pos] -> m (Gen, [Term])
+loadVars :: MonadFail m => Gen -> [SExpr Pos] -> m (Gen, [Term])
 loadVars gen sexprs =
     do
       pairs <- mapM loadVarPair sexprs
       (g, vars) <- foldM loadVar (gen, []) (concat pairs)
       return (g, reverse vars)
 
-loadVarPair :: Monad m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)]
+loadVarPair :: MonadFail m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)]
 loadVarPair (L _ (x:y:xs)) =
     let (t:vs) = reverse (x:y:xs) in
     return [(v,t) | v <- reverse vs]
 loadVarPair x = fail (shows (annotation x) "Malformed vars declaration")
 
-loadVar :: Monad m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->
+loadVar :: MonadFail m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->
            m (Gen, [Term])
 loadVar (gen, vars) (S pos name, S pos' sort) =
     case loadLookup pos vars name of
@@ -2442,7 +2446,7 @@
             return (gen', p : vars)
 loadVar _ (x,_) = fail (shows (annotation x) "Bad variable syntax")
 
-mkVar :: Monad m => Pos -> String -> Id -> m Term
+mkVar :: MonadFail m => Pos -> String -> Id -> m Term
 mkVar pos sort x
   | sort == "mesg" = return $ I x
   | sort == "text" = return $ F Text [I x]
@@ -2467,14 +2471,14 @@
     let name' = idName (varId t) in
     if name' == name then Right t else loadLookup pos u name
 
-loadLookupName :: Monad m => Pos -> [Term] -> String -> m Term
+loadLookupName :: MonadFail m => Pos -> [Term] -> String -> m Term
 loadLookupName pos vars name =
     either fail f (loadLookup pos vars name)
     where
       f t@(F Name [I _]) = return t
       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be a name")
 
-loadLookupAkey :: Monad m => Pos -> [Term] -> String -> m Term
+loadLookupAkey :: MonadFail m => Pos -> [Term] -> String -> m Term
 loadLookupAkey pos vars name =
     either fail f (loadLookup pos vars name)
     where
@@ -2482,7 +2486,7 @@
       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be an akey")
 
 -- Load term and check that it is well-formed.
-loadTerm :: Monad m => [Term] -> Bool -> SExpr Pos -> m Term
+loadTerm :: MonadFail m => [Term] -> Bool -> SExpr Pos -> m Term
 loadTerm vars _ (S pos s) =
     either fail return (loadLookup pos vars s)
 loadTerm _ _ (Q _ t) =
@@ -2495,7 +2499,7 @@
 
 type LoadFunction m = Pos -> Bool -> [Term] -> [SExpr Pos] -> m Term
 
-loadDispatch :: Monad m => [(String, LoadFunction m)]
+loadDispatch :: MonadFail m => [(String, LoadFunction m)]
 loadDispatch =
     [("pubk", loadPubk)
     ,("privk", loadPrivk)
@@ -2514,7 +2518,7 @@
 
 -- Atom constructors: pubk privk invk ltk
 
-loadPubk :: Monad m => LoadFunction m
+loadPubk :: MonadFail m => LoadFunction m
 loadPubk _ _ vars [S pos s] =
     do
       t <- loadLookupName pos vars s
@@ -2525,7 +2529,7 @@
       return $ F Akey [F Pubk [C c, I $ varId t]]
 loadPubk pos _ _ _ = fail (shows pos "Malformed pubk")
 
-loadPrivk :: Monad m => LoadFunction m
+loadPrivk :: MonadFail m => LoadFunction m
 loadPrivk _ _ vars [S pos s] =
     do
       t <- loadLookupName pos vars s
@@ -2536,7 +2540,7 @@
       return $ F Akey [F Invk [F Pubk [C c, I $ varId t]]]
 loadPrivk pos _ _ _ = fail (shows pos "Malformed privk")
 
-loadInvk :: Monad m => LoadFunction m
+loadInvk :: MonadFail m => LoadFunction m
 loadInvk _ _ vars [S pos s] =
     do
       t <- loadLookupAkey pos vars s
@@ -2553,7 +2557,7 @@
       return $ F Akey [F Invk [F Pubk [C c, I $ varId t]]]
 loadInvk pos _ _ _ = fail (shows pos "Malformed invk")
 
-loadLtk :: Monad m => LoadFunction m
+loadLtk :: MonadFail m => LoadFunction m
 loadLtk _ _ vars [S pos s, S pos' s'] =
     do
       t <- loadLookupName pos vars s
@@ -2561,7 +2565,7 @@
       return $ F Skey [F Ltk [I $ varId t, I $ varId t']]
 loadLtk pos _ _ _ = fail (shows pos "Malformed ltk")
 
-loadBltk :: Monad m => LoadFunction m
+loadBltk :: MonadFail m => LoadFunction m
 loadBltk _ _ vars [S pos s, S pos' s'] =
     do
       t <- loadLookupName pos vars s
@@ -2571,12 +2575,12 @@
 
 -- Base and exponents
 
-loadGen :: Monad m => LoadFunction m
+loadGen :: MonadFail m => LoadFunction m
 loadGen _ _ _ [] =
     return $ F Base [F Genr []]
 loadGen pos _ _ _ = fail (shows pos "Malformed gen")
 
-loadExp :: Monad m => LoadFunction m
+loadExp :: MonadFail m => LoadFunction m
 loadExp _ _ vars [x, x'] =
     do
       t <- loadBase vars x
@@ -2584,7 +2588,7 @@
       return $ F Base [idSubst emptyIdMap $ F Exp [t, G t']]
 loadExp pos _ _ _ = fail (shows pos "Malformed exp")
 
-loadBase :: Monad m => [Term] -> SExpr Pos -> m Term
+loadBase :: MonadFail m => [Term] -> SExpr Pos -> m Term
 loadBase vars x =
     do
       t <- loadTerm vars False x
@@ -2592,7 +2596,7 @@
         F Base [t] -> return t
         _ -> fail (shows (annotation x) "Malformed base")
 
-loadExpr :: Monad m => [Term] -> Bool -> SExpr Pos -> m Group
+loadExpr :: MonadFail m => [Term] -> Bool -> SExpr Pos -> m Group
 loadExpr vars False x =
     do
       t <- loadTerm vars False x
@@ -2604,13 +2608,13 @@
 --    do
 --      fail (shows (annotation x) "Disallowed bare exponent")
 
-loadOne :: Monad m => LoadFunction m
+loadOne :: MonadFail m => LoadFunction m
 loadOne _ False _ [] =
     return $ G M.empty
 loadOne pos True _ _ = fail (shows pos "Disallowed bare exponent")
 loadOne pos _ _ _ = fail (shows pos "Malformed one")
 
-loadRec :: Monad m => LoadFunction m
+loadRec :: MonadFail m => LoadFunction m
 loadRec _ False vars [x] =
     do
       t <- loadExpr vars False x
@@ -2618,7 +2622,7 @@
 loadRec pos True _ _ = fail (shows pos "Disallowed bare exponent")
 loadRec pos _ _ _ = fail (shows pos "Malformed rec")
 
-loadMul :: Monad m => LoadFunction m
+loadMul :: MonadFail m => LoadFunction m
 loadMul _ False vars xs =
     do
       t <- foldM f M.empty xs
@@ -2632,14 +2636,14 @@
 
 -- Term constructors: cat enc
 
-loadCat :: Monad m => LoadFunction m
+loadCat :: MonadFail m => LoadFunction m
 loadCat _ strict vars (l : ls) =
     do
       ts <- mapM (loadTerm vars strict) (l : ls)
       return $ foldr1 (\a b -> F Cat [a, b]) ts
 loadCat pos _ _ _ = fail (shows pos "Malformed cat")
 
-loadEnc :: Monad m => LoadFunction m
+loadEnc :: MonadFail m => LoadFunction m
 loadEnc pos strict vars (l : l' : ls) =
     do
       let (butLast, last) = splitLast l (l' : ls)
@@ -2655,7 +2659,7 @@
       loop z x [] = (reverse z, x)
       loop z x (y : ys) = loop (x : z) y ys
 
-loadHash :: Monad m => LoadFunction m
+loadHash :: MonadFail m => LoadFunction m
 loadHash _ strict vars (l : ls) =
    do
      ts <- mapM (loadTerm vars strict) (l : ls)
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
@@ -11,6 +11,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Graph.Loader (Preskel, Dir (..), Vertex, protocol, role, env, inst,
                           part, lastVertex, vertices, Node, vnode, aborted,
                           strands, label, parent, seen, unrealized, shape,
@@ -185,7 +191,7 @@
 
 -- Protocols
 
-loadProt :: Monad m => SExpr Pos -> Pos -> [SExpr Pos] ->
+loadProt :: MonadFail m => SExpr Pos -> Pos -> [SExpr Pos] ->
             m (String, Protocol)
 loadProt x _ (S _ name : S _ _ : xs) =
     do
@@ -193,7 +199,7 @@
       return (name, Protocol { name = name, roles = roles, src = x })
 loadProt _ pos _ = fail (shows pos "Malformed protocol")
 
-loadRoles :: Monad m => [SExpr Pos] -> m [(String, Trace)]
+loadRoles :: MonadFail m => [SExpr Pos] -> m [(String, Trace)]
 loadRoles (L pos (S _ "defrole" : x) : xs) =
     do
       r <- loadRole pos x
@@ -201,7 +207,7 @@
       return (r : rs)
 loadRoles _ = return []
 
-loadRole :: Monad m => Pos -> [SExpr Pos] -> m (String, Trace)
+loadRole :: MonadFail m => Pos -> [SExpr Pos] -> m (String, Trace)
 loadRole _ (S _ name :
             L _ (S _ "vars" : _) :
             L _ (S _ "trace" : trace) : _) = return (name, trace)
@@ -209,7 +215,7 @@
 
 -- Preskeletons
 
-loadPreskel :: Monad m => SExpr Pos -> Pos -> [(String, Protocol)] ->
+loadPreskel :: MonadFail m => SExpr Pos -> Pos -> [(String, Protocol)] ->
                Int -> [SExpr Pos] -> m Preskel
 loadPreskel s pos ps tag (S _ name : (L _ (S _ "vars" : _)) : xs) =
     case lookup name ps of
@@ -223,7 +229,7 @@
             loadInsts s pos p tag [] cs xs
 loadPreskel _ pos _ _ _ = fail (shows pos "Malformed skeleton")
 
-loadInsts :: Monad m => SExpr Pos -> Pos -> Protocol -> Int ->
+loadInsts :: MonadFail m => SExpr Pos -> Pos -> Protocol -> Int ->
              [Inst] -> [SExpr Pos] -> [SExpr Pos] -> m Preskel
 loadInsts s top p tag insts cs (L pos (S _ "defstrand" : x) : xs) =
     case x of
@@ -358,7 +364,7 @@
 
 -- Instances
 
-loadInst :: Monad m => Pos -> Protocol -> [SExpr Pos] -> String ->
+loadInst :: MonadFail m => Pos -> Protocol -> [SExpr Pos] -> String ->
             Int -> [SExpr Pos] -> m Inst
 loadInst pos p c role ht env =
     case lookup role (roles p) of
@@ -384,7 +390,7 @@
 itrace env [] (r : rs) =
     subst env r : itrace env [] rs
 
-loadMaplet :: Monad m => [SExpr Pos] -> m [(String, SExpr Pos)]
+loadMaplet :: MonadFail m => [SExpr Pos] -> m [(String, SExpr Pos)]
 loadMaplet (L _ [S _ name, x] : xs) =
     do
       env <- loadMaplet xs
@@ -401,7 +407,7 @@
 subst _ x = x
 
 -- Ensure alist has the proper form
-alist :: Monad m => [SExpr Pos] -> m ()
+alist :: MonadFail m => [SExpr Pos] -> m ()
 alist [] = return ()
 alist ((L _ (S _ _ : _)) : xs) = alist xs
 alist xs = fail (shows (annotation $ head xs) "Malformed association list")
@@ -432,7 +438,7 @@
 -- assoc key alist =
 --    concat [ rest | L _ (S _ head : rest) <- alist, key == head ]
 
-nassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe Int)
+nassoc :: MonadFail m => String -> [SExpr Pos] -> m (Maybe Int)
 nassoc key xs =
     case assoc key xs of
       Nothing -> return Nothing
@@ -443,11 +449,11 @@
       Just (x:_) -> fail (shows (annotation x) "Expecting one number")
       Just [] -> fail (shows (annotation (head xs)) "Expecting one number")
 
-num :: Monad m => SExpr Pos -> m Int
+num :: MonadFail m => SExpr Pos -> m Int
 num (N _ n) = return n
 num x = fail (shows (annotation x) "Expecting a number")
 
-nsassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe [Int])
+nsassoc :: MonadFail m => String -> [SExpr Pos] -> m (Maybe [Int])
 nsassoc key xs =
     case assoc key xs of
       Nothing -> return Nothing
@@ -456,7 +462,7 @@
             ns <- mapM num val
             return (Just ns)
 
-loadOrderings :: Monad m => [Int] -> [SExpr Pos] -> Bool -> m [Pair]
+loadOrderings :: MonadFail m => [Int] -> [SExpr Pos] -> Bool -> m [Pair]
 loadOrderings heights x strict =
     foldM f [] x
     where
@@ -465,7 +471,7 @@
             np <- loadPair heights x strict
             return (adjoin np ns)
 
-loadPair :: Monad m => [Int] -> SExpr Pos -> Bool -> m Pair
+loadPair :: MonadFail m => [Int] -> SExpr Pos -> Bool -> m Pair
 loadPair heights (L pos [x0, x1]) strict =
     do
       n0 <- loadNode heights x0
@@ -477,7 +483,7 @@
       sameStrands (s0, _) (s1, _) = s0 == s1
 loadPair _ x _ = fail (shows (annotation x) "Malformed pair")
 
-loadNode :: Monad m => [Int] -> SExpr Pos -> m Node
+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node
 loadNode heights (L pos [N _ s, N _ p])
     | s < 0 = fail (shows pos "Negative strand in node")
     | p < 0 = fail (shows pos "Negative position in node")
@@ -493,7 +499,7 @@
           | otherwise = height xs (s - 1)
 loadNode _ x = fail (shows (annotation x) "Malformed node")
 
-loadNodes :: Monad m => [Int] -> Maybe [SExpr Pos] -> m (Maybe [Node])
+loadNodes :: MonadFail m => [Int] -> Maybe [SExpr Pos] -> m (Maybe [Node])
 loadNodes _ Nothing = return Nothing
 loadNodes heights (Just xs) =
     do
diff --git a/src/CPSA/Lib/Algebra.hs b/src/CPSA/Lib/Algebra.hs
--- a/src/CPSA/Lib/Algebra.hs
+++ b/src/CPSA/Lib/Algebra.hs
@@ -8,6 +8,12 @@
 
 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Lib.Algebra where
 
 import Data.Set (Set)
@@ -90,7 +96,7 @@
     escapeSet :: Set t -> Set t -> t -> Maybe (Set t)
 
     -- Given a list of variables, load a term from an S-expression.
-    loadTerm :: Monad m => [t] -> Bool -> SExpr Pos -> m t
+    loadTerm :: MonadFail m => [t] -> Bool -> SExpr Pos -> m t
 
     -- Determines if an element is "numeric", meaning that it is
     -- part of a numeric sort.
@@ -162,7 +168,7 @@
     -- Given a generator, load a list of variables or return an error
     -- message.  Each element of the list is an identifier and a sort.
     -- The varibles are returned in the reverse order.
-    loadVars :: Monad m => g -> [SExpr Pos] -> m (g, [t])
+    loadVars :: MonadFail m => g -> [SExpr Pos] -> m (g, [t])
 
     -- For DH
 
diff --git a/src/CPSA/Lib/Characteristic.hs b/src/CPSA/Lib/Characteristic.hs
--- a/src/CPSA/Lib/Characteristic.hs
+++ b/src/CPSA/Lib/Characteristic.hs
@@ -6,10 +6,17 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Lib.Characteristic (Conj, characteristic) where
 
 import Control.Monad
 import qualified Data.List as L
+import CPSA.Lib.Utilities
 import CPSA.Lib.SExpr
 import CPSA.Lib.Algebra
 import CPSA.Lib.Declaration
@@ -27,7 +34,7 @@
 -- Entry point.  Takes a position, a protocol, a variable generator, a
 -- goal, and a skeleton comment and makes a skeleton or fails.  This
 -- function extracts the anecedent and univesally quantified variable.
-characteristic :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+characteristic :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                   [Goal t] -> g -> Conj t -> [SExpr ()] -> m (Preskel t g s e)
 characteristic pos prot goals g antec comment =
   equalsForm pos prot goals g antec comment
@@ -35,7 +42,7 @@
 -- Checks for equals in an antecedent and fails if it finds one.  One
 -- could use unification to solve the equality, and then apply the
 -- result to the remaining parts of the formula.
-equalsForm :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+equalsForm :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
               [Goal t] -> g -> Conj t -> [SExpr ()] -> m (Preskel t g s e)
 equalsForm pos _ _ _ as _ | any isEquals as =
   fail (shows pos "Equals not allowed in antecedent")
@@ -50,7 +57,7 @@
 -- The instance formulas are used to generate the skeleton's
 -- instances, and the skeleton formulas generate the rest.  Make the
 -- instances, and then make the rest.
-splitForm :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+splitForm :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
              [Goal t] -> g -> Conj t -> [SExpr ()] -> m (Preskel t g s e)
 splitForm pos prot goals g as comment =
   do
@@ -67,7 +74,7 @@
 
 -- Make the instances from the instance predicates
 
-mkInsts :: (Algebra t p g s e c, Monad m) => g -> Conj t ->
+mkInsts :: (Algebra t p g s e c, MonadFail m) => g -> Conj t ->
            m ([(t, Sid)], g, [Instance t e])
 mkInsts g as =
   do
@@ -77,7 +84,7 @@
     return (strdMap, g, insts) -- Construct node map for later use
 
 -- Computes a map from strands to roles and lengths
-strdRoleLength :: (Algebra t p g s e c, Monad m) =>
+strdRoleLength :: (Algebra t p g s e c, MonadFail m) =>
                   Conj t -> m [(t, (Role t, Int))]
 strdRoleLength as =
   foldM f [] as
@@ -94,7 +101,7 @@
     f srl _ = return srl
 
 -- Construct instances
-foldInsts :: (Algebra t p g s e c, Monad m) =>
+foldInsts :: (Algebra t p g s e c, MonadFail m) =>
              g -> Conj t -> [(t, (Role t, Int))] ->
              m (g, [Instance t e])
 foldInsts g _ [] = return (g, [])
@@ -106,7 +113,7 @@
 
 -- Construct an instance by extracting maplets from the parameter
 -- predicates associated with the strand.
-mkInst :: (Algebra t p g s e c, Monad m) =>
+mkInst :: (Algebra t p g s e c, MonadFail m) =>
           g -> Conj t -> t -> Role t -> Int -> m (g, Instance t e)
 mkInst g as z r h =
   do
@@ -114,7 +121,7 @@
     return (mkInstance g r env h)
 
 -- Add match from a maplet
-mkMaplet :: (Algebra t p g s e c, Monad m) =>
+mkMaplet :: (Algebra t p g s e c, MonadFail m) =>
             Role t -> t -> (g, e) ->
             (Pos, AForm t) -> m (g, e)
 mkMaplet role z env (pos, Param r v _ z' t)
@@ -138,7 +145,7 @@
 
 -- Create a skeleton given a list of instances
 
-mkSkel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+mkSkel :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
           [Goal t] -> [(t, Sid)] -> g -> [Instance t e] ->
           Conj t -> [SExpr ()] -> m (Preskel t g s e)
 mkSkel pos p goals nmap g insts as comment =
@@ -158,8 +165,8 @@
       False -> fail (shows pos "Terms in skeleton not well formed")
       True -> return ()
     case verbosePreskelWellFormed k of
-      Right () -> return k
-      Left msg -> fail $ shows pos
+      Return () -> return k
+      Fail msg -> fail $ shows pos
                   $ showString "Skeleton not well formed: " msg
   where
     termsInDlist olist = concat $ map dterms (concatMap snd olist)
@@ -211,7 +218,7 @@
         Nothing -> FTerm t
 mkFact _ _ ts = ts
 
-checkUniqAt :: (Algebra t p g s e c, Monad m) => [(t, Sid)] ->
+checkUniqAt :: (Algebra t p g s e c, MonadFail m) => [(t, Sid)] ->
                Preskel t g s e -> (Pos, AForm t) -> m ()
 checkUniqAt nmap k (pos, UniqAt t n) =
   case lookup t $ korig k of
diff --git a/src/CPSA/Lib/Expand.hs b/src/CPSA/Lib/Expand.hs
--- a/src/CPSA/Lib/Expand.hs
+++ b/src/CPSA/Lib/Expand.hs
@@ -6,6 +6,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Lib.Expand (expand, readSExprs) where
 
 import Control.Monad
@@ -82,7 +88,7 @@
       args :: [String],
       body :: SExpr Pos }
 
-defmacro :: Monad m => Pos -> [SExpr Pos] -> m Macro
+defmacro :: MonadFail m => Pos -> [SExpr Pos] -> m Macro
 defmacro _ [L _ (name : args), body] =
     do
       name <- symbol name
@@ -92,13 +98,13 @@
                        body = body}
 defmacro pos _ = fail (shows pos "Malformed macro")
 
-symbol :: Monad m => SExpr Pos -> m String
+symbol :: MonadFail m => SExpr Pos -> m String
 symbol (S _ string) = return string
 symbol x = fail (shows (annotation x) "Malformed macro: Expecting a symbol")
 
 -- Expand an S-expression using a given set of macros
 
-expandAll :: Monad m => [Macro] -> SExpr Pos -> m (SExpr Pos)
+expandAll :: MonadFail m => [Macro] -> SExpr Pos -> m (SExpr Pos)
 expandAll macs sexpr =
     do
       sexpr <- macroExpand macs (annotation sexpr) limit sexpr
@@ -111,7 +117,7 @@
 
 -- Expand one S-expression limiting the number of expansions.
 
-macroExpand :: Monad m => [Macro] -> Pos ->  Int ->
+macroExpand :: MonadFail m => [Macro] -> Pos ->  Int ->
                SExpr Pos -> m (SExpr Pos)
 macroExpand _ pos limit _
     | limit <= 0 = fail (shows pos "Expansion limit exceeded")
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
@@ -6,6 +6,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Lib.Loader (loadSExprs) where
 
 import Control.Monad
@@ -28,14 +34,14 @@
 -- then return a list of preskeletons.  The name of the algebra is
 -- nom, and its variable generator is provided.
 
-loadSExprs :: (Algebra t p g s e c, Monad m) => String -> g ->
+loadSExprs :: (Algebra t p g s e c, MonadFail m) => String -> g ->
               [SExpr Pos] -> m [Preskel t g s e]
 loadSExprs nom origin xs =
     do
       (_, ks) <- foldM (loadSExpr nom origin) ([], []) xs
       return (reverse ks)
 
-loadSExpr :: (Algebra t p g s e c, Monad m) => String -> g ->
+loadSExpr :: (Algebra t p g s e c, MonadFail m) => String -> g ->
              ([Prot t g], [Preskel t g s e]) -> SExpr Pos ->
              m ([Prot t g], [Preskel t g s e])
 loadSExpr nom origin (ps, ks) (L pos (S _ "defprotocol" : xs)) =
@@ -58,7 +64,7 @@
 
 -- load a protocol
 
-loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->
+loadProt :: (Algebra t p g s e c, MonadFail m) => String -> g ->
             Pos -> [SExpr Pos] -> m (Prot t g)
 loadProt nom origin pos (S _ name : S _ alg : x : xs)
     | alg /= nom =
@@ -83,7 +89,7 @@
                 fail (shows pos msg)
 loadProt _ _ pos _ = fail (shows pos "Malformed protocol")
 
-loadRoles :: (Algebra t p g s e c, Monad m) => g -> [SExpr Pos] ->
+loadRoles :: (Algebra t p g s e c, MonadFail m) => g -> [SExpr Pos] ->
              m (g, [Role t], [SExpr Pos])
 loadRoles gen (L pos (S _ "defrole" : x) : xs) =
     do
@@ -93,7 +99,7 @@
 loadRoles gen xs =
   return (gen, [], xs)
 
-loadRole :: (Algebra t p g s e c, Monad m) => g -> Pos ->
+loadRole :: (Algebra t p g s e c, MonadFail m) => g -> Pos ->
             [SExpr Pos] -> m (g, Role t)
 loadRole gen pos (S _ name :
                   L _ (S _ "vars" : vars) :
@@ -129,7 +135,7 @@
 
 loadRole _ pos _ = fail (shows pos "Malformed role")
 
-loadAllPredefRoleDecls :: (Algebra t p g s e c, Monad m) => Int -> [t] ->
+loadAllPredefRoleDecls :: (Algebra t p g s e c, MonadFail m) => Int -> [t] ->
                           [SExpr Pos] -> m [RoleDeclaration t]
 loadAllPredefRoleDecls height vars exprs =
     do
@@ -140,7 +146,7 @@
                 (nats (length formats))
       return result
 
-loadAllPredefSkelDecls :: (Algebra t p g s e c, Monad m) => [Int] -> [t] ->
+loadAllPredefSkelDecls :: (Algebra t p g s e c, MonadFail m) => [Int] -> [t] ->
                           [SExpr Pos] -> m ([SkelDeclaration t])
 loadAllPredefSkelDecls heights vars exprs =
     do
@@ -152,9 +158,10 @@
                 (nats (length formats))
       return result
 
-loadPredefRoleDeclsAux :: (Algebra t p g s e c, Monad m) => Int -> [t] -> String ->
-                       (DeclInFormat, Bool, Bool) ->
-                       [SExpr Pos] -> m [(RoleDeclaration t)]
+loadPredefRoleDeclsAux :: (Algebra t p g s e c, MonadFail m) => Int ->
+                          [t] -> String ->
+                          (DeclInFormat, Bool, Bool) ->
+                          [SExpr Pos] -> m [(RoleDeclaration t)]
 loadPredefRoleDeclsAux _ _ _ _ [] = do return []
 loadPredefRoleDeclsAux height vars tag (fmt,areq,False) exprs =
     do (tg,insts) <- loadPredefRoleDecls height vars tag "" fmt areq exprs
@@ -178,9 +185,10 @@
 loadPredefRoleDeclsAux _ _ tag _ (x:_) =
     fail (shows (annotation x) ("Malformed declaration: subtag required " ++ tag))
 
-loadPredefSkelDeclsAux :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> String ->
-                       (DeclInFormat, Bool, Bool) ->
-                       [SExpr Pos] -> m [(SkelDeclaration t)]
+loadPredefSkelDeclsAux :: (Algebra t p g s e c, MonadFail m) => [Int] ->
+                          [t] -> String ->
+                          (DeclInFormat, Bool, Bool) ->
+                          [SExpr Pos] -> m [(SkelDeclaration t)]
 loadPredefSkelDeclsAux _ _ _ _ [] = do return []
 loadPredefSkelDeclsAux height vars tag (fmt,areq,False) exprs =
     do (tg,insts) <- loadPredefSkelDecls height vars tag "" fmt areq exprs
@@ -204,7 +212,7 @@
      fail (shows (annotation x) ("Malformed declaration: subtag required " ++ tag))
 -- loadPredefSkelDeclsAux _ _ _ (_,_,True) _ = do return []
 
-loadPredefRoleDecls :: (Algebra t p g s e c, Monad m) => Int -> [t] -> String ->
+loadPredefRoleDecls :: (Algebra t p g s e c, MonadFail m) => Int -> [t] -> String ->
                        String -> DeclInFormat -> Bool ->
                        [SExpr Pos] -> m (RoleDeclaration t)
 -- Anything with no expressions: not present, return an empty list of instances.
@@ -252,7 +260,7 @@
        then fail ("[ASSERT FAILED] Input format not supported")
        else fail (shows (annotation (head xs)) "[ASSERT FAILED] Input format not supported")
 
-loadPredefSkelDecls :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> String ->
+loadPredefSkelDecls :: (Algebra t p g s e c, MonadFail m) => [Int] -> [t] -> String ->
                        String -> DeclInFormat -> Bool ->
                        [SExpr Pos] -> m (SkelDeclaration t)
 -- Anything with no expressions: not present, return an empty list of instances.
@@ -297,7 +305,7 @@
        then fail ("[ASSERT FAILED] Input format not supported")
        else fail (shows (annotation (head xs)) "[ASSERT FAILED] Input format not supported")
 
-loadRoleTermPairPlusMaybeOneLoc :: (Algebra t p g s e c, Monad m) => Int ->
+loadRoleTermPairPlusMaybeOneLoc :: (Algebra t p g s e c, MonadFail m) => Int ->
                                    [t] -> String ->
                                    SExpr Pos -> m (RoleDeclInst t)
 loadRoleTermPairPlusMaybeOneLoc _ vars stag (L _ [x1, x2]) =
@@ -314,7 +322,7 @@
 loadRoleTermPairPlusMaybeOneLoc _ _ _ x = fail
                         (shows (annotation x) "Malformed pair of terms")
 
-loadSkelTermPair :: (Algebra t p g s e c, Monad m) => [t] -> String ->
+loadSkelTermPair :: (Algebra t p g s e c, MonadFail m) => [t] -> String ->
                                    SExpr Pos -> m (SkelDeclInst t)
 loadSkelTermPair vars stag (L _ [x1, x2]) =
     do
@@ -324,7 +332,7 @@
 loadSkelTermPair _ _ x = fail
                         (shows (annotation x) "Malformed pair of terms")
 
-loadRolePriority :: Monad m => Int -> SExpr Pos -> m (Int, Int)
+loadRolePriority :: MonadFail m => Int -> SExpr Pos -> m (Int, Int)
 loadRolePriority n (L _ [N _ i, N _ p])
     | 0 <= i && i < n = return (i, p)
 loadRolePriority _ x = fail (shows (annotation x) "Malformed priority")
@@ -340,7 +348,8 @@
 
 -- This is the only place a role is generated with an empty name.
 -- This is what marks a strand as a listener.
-mkListenerRole :: (Algebra t p g s e c, Monad m) => Pos -> g -> m (g, Role t)
+mkListenerRole :: (Algebra t p g s e c, MonadFail m) => Pos -> g ->
+                  m (g, Role t)
 mkListenerRole pos g =
   do
     (g, xs) <- loadVars g [L pos [S pos "x", S pos "mesg"]]
@@ -350,7 +359,7 @@
 
 -- Protocol Rules
 
-loadRules :: (Algebra t p g s e c, Monad m) => Prot t g -> g ->
+loadRules :: (Algebra t p g s e c, MonadFail m) => Prot t g -> g ->
              [SExpr Pos] -> m (g, [Rule t], [SExpr ()])
 loadRules prot g (L pos (S _ "defrule" : x) : xs) =
     do
@@ -365,7 +374,7 @@
       comment <- alist [] xs    -- Ensure remaining is an alist
       return (g, [], comment)
 
-loadRule :: (Algebra t p g s e c, Monad m) => Prot t g -> g ->
+loadRule :: (Algebra t p g s e c, MonadFail m) => Prot t g -> g ->
             Pos -> [SExpr Pos] -> m (g, Rule t)
 loadRule prot g pos (S _ name : x : xs) =
   do
@@ -381,7 +390,7 @@
 -- Make an association list into a comment.  The first argument is the
 -- set of keys of key-value pairs to be dropped from the comment.
 
-alist :: Monad m => [String] -> [SExpr Pos] -> m [SExpr ()]
+alist :: MonadFail m => [String] -> [SExpr Pos] -> m [SExpr ()]
 alist _ [] = return []
 alist keys (a@(L _ (S _ key : _)) : xs)
     | elem key keys = alist keys xs
@@ -418,18 +427,18 @@
       f _ = False
 
 -- Complain if alist has a bad key
-badKey :: Monad m => [String] -> [SExpr Pos] -> m ()
+badKey :: MonadFail m => [String] -> [SExpr Pos] -> m ()
 badKey keys (L _ (S pos key : _) : xs)
     | elem key keys =
       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] ->
+loadTrace :: (Algebra t p g s e c, MonadFail m) => [t] ->
              [SExpr Pos] -> m [Event t]
 loadTrace vars xs = mapM (loadEvt vars) xs
 
-loadEvt :: (Algebra t p g s e c, Monad m) => [t] ->
+loadEvt :: (Algebra t p g s e c, MonadFail m) => [t] ->
           SExpr Pos -> m (Event t)
 loadEvt vars (L _ [S _ "recv", t]) =
     do
@@ -456,7 +465,7 @@
     fail (shows pos $ "Malformed direction: " ++ dir)
 loadEvt _ x = fail (shows (annotation x) "Malformed event")
 
-loadBaseTerms :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [t]
+loadBaseTerms :: (Algebra t p g s e c, MonadFail m) => [t] -> [SExpr Pos] -> m [t]
 loadBaseTerms _ [] = return []
 loadBaseTerms vars (x : xs) =
     do
@@ -464,7 +473,8 @@
       ts <- loadBaseTerms vars xs
       return (adjoin t ts)
 
-maybeLoadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m (Maybe t)
+maybeLoadBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] ->
+                     SExpr Pos -> m (Maybe t)
 maybeLoadBaseTerm vars x =
     do
       t <- loadTerm vars False x
@@ -472,7 +482,7 @@
          True -> return (Just t)
          False -> return Nothing
 
-loadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t
+loadBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m t
 loadBaseTerm vars x =
     do
       mt <- maybeLoadBaseTerm vars x
@@ -480,7 +490,7 @@
         Just t -> return t
         Nothing -> fail (shows (annotation x) "Expecting an atom")
 
-loadPosBaseTerms :: (Algebra t p g s e c, Monad m) => [t] ->
+loadPosBaseTerms :: (Algebra t p g s e c, MonadFail m) => [t] ->
                     [SExpr Pos] -> m [(Maybe Int, t)]
 loadPosBaseTerms _ [] = return []
 loadPosBaseTerms vars (x : xs) =
@@ -489,7 +499,7 @@
       ts <- loadPosBaseTerms vars xs
       return (t:ts)
 
-loadPosBaseTerm :: (Algebra t p g s e c, Monad m) => [t] ->
+loadPosBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] ->
                    SExpr Pos -> m (Maybe Int, t)
 loadPosBaseTerm vars x'@(L _ [x, N _ opos])
     | opos < 0 =
@@ -506,7 +516,7 @@
         True -> return (Nothing, t)
         False -> fail (shows (annotation x) "Expecting an atom")
 
-loadPositions :: Monad m => Int -> [SExpr Pos] -> m [Int]
+loadPositions :: MonadFail m => Int -> [SExpr Pos] -> m [Int]
 loadPositions _ [] = return []
 loadPositions height (x : xs) =
     do
@@ -514,7 +524,7 @@
       ps <- loadPositions height xs
       return (p:ps)
 
-loadPosition :: Monad m => Int -> SExpr Pos -> m Int
+loadPosition :: MonadFail m => Int -> SExpr Pos -> m Int
 loadPosition height x@(N _ pos)
     | pos < 0 = fail (shows (annotation x) "Expecting a non-negative height")
     | pos >= height = fail (shows (annotation x) "Height out of range")
@@ -523,7 +533,7 @@
 
 -- Find protocol and then load a preskeleton.
 
-findPreskel :: (Algebra t p g s e c, Monad m) => Pos ->
+findPreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->
                [Prot t g] -> [SExpr Pos] ->
                m (Preskel t g s e)
 findPreskel pos ps (S _ name : xs) =
@@ -532,7 +542,7 @@
       Just p -> loadPreskel pos p xs
 findPreskel pos _ _ = fail (shows pos "Malformed skeleton")
 
-loadPreskel :: (Algebra t p g s e c, Monad m) => Pos ->
+loadPreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->
                Prot t g -> [SExpr Pos] ->
                m (Preskel t g s e)
 loadPreskel pos p (L _ (S _ "vars" : vars) : xs) =
@@ -541,7 +551,7 @@
       loadInsts pos p kvars gen [] xs
 loadPreskel pos _ _ = fail (shows pos "Malformed skeleton")
 
-loadInsts :: (Algebra t p g s e c, Monad m) => Pos ->
+loadInsts :: (Algebra t p g s e c, MonadFail m) => Pos ->
              Prot t g -> [t] -> g -> [Instance t e] ->
              [SExpr Pos] -> m (Preskel t g s e)
 loadInsts top p kvars gen insts (L pos (S _ "defstrand" : x) : xs) =
@@ -587,7 +597,7 @@
 loadComment key comment =
   [L () (S () key : map strip comment)]
 
-loadPriorities :: (Algebra t p g s e c, Monad m) => [SExpr Pos] ->
+loadPriorities :: (Algebra t p g s e c, MonadFail m) => [SExpr Pos] ->
                   [Instance t e] -> m [((Int,Int),Int)]
 loadPriorities [] _ = return []
 loadPriorities ((L pos [L _ [N _ s, N _ i], N _ p]) : rest) insts
@@ -612,7 +622,7 @@
     where
       keys = [ key | L _ (S _ head : (S _ key : _)) <- alist, head=="decl" ]
 
-loadInst :: (Algebra t p g s e c, Monad m) => Pos ->
+loadInst :: (Algebra t p g s e c, MonadFail m) => Pos ->
             Prot t g -> [t] -> g -> String -> Int ->
             [SExpr Pos] -> m (g, Instance t e)
 loadInst pos p kvars gen role height env =
@@ -626,7 +636,7 @@
               (gen', env') <- foldM (loadMaplet kvars vars) (gen, emptyEnv) env
               return (mkInstance gen' r env' height)
 
-lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t)
+lookupRole :: MonadFail m => Pos -> Prot t g -> String -> m (Role t)
 lookupRole _ p role  | role == "" =
     return $ listenerRole p
 lookupRole pos p role =
@@ -635,7 +645,7 @@
           fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname p)
       Just r -> return r
 
-loadMaplet :: (Algebra t p g s e c, Monad m) => [t] -> [t] ->
+loadMaplet :: (Algebra t p g s e c, MonadFail m) => [t] -> [t] ->
               (g, e) -> SExpr Pos -> m (g, e)
 loadMaplet kvars vars env (L pos [domain, range]) =
     do
@@ -646,14 +656,14 @@
         [] -> fail (shows pos "Domain does not match range")
 loadMaplet _ _ _ x = fail (shows (annotation x) "Malformed maplet")
 
-loadListener :: (Algebra t p g s e c, Monad m) => Prot t g ->
+loadListener :: (Algebra t p g s e c, MonadFail m) => Prot t g ->
                 [t] -> g -> SExpr Pos -> m (g, Instance t e)
 loadListener p kvars gen x =
     do
       t <- loadTerm kvars False x
       return $ mkListener p gen t
 
-loadRest :: (Algebra t p g s e c, Monad m) => Pos -> [t] ->
+loadRest :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] ->
             Prot t g -> [Goal t] -> g -> [Instance t e] ->
             [SExpr Pos] -> [SExpr Pos] -> SkelDeclList t ->
             [SExpr Pos] -> [SExpr ()] -> [((Int,Int),Int)] ->
@@ -682,7 +692,7 @@
       where
         termsInDlist olist = concat $ map dterms (concatMap snd olist)
 
-loadGenSkelDecls :: (Algebra t p g s e c, Monad m) => [Int] -> [t] ->
+loadGenSkelDecls :: (Algebra t p g s e c, MonadFail m) => [Int] -> [t] ->
                     [(String,[SExpr Pos])] -> m [SkelDeclaration t]
 loadGenSkelDecls _ _ [] = return []
 loadGenSkelDecls heights vars ((name,rawds):b) =
@@ -691,7 +701,8 @@
       b' <- loadGenSkelDecls heights vars b
       return ((name,a'):b')
 
-loadGenSkelDeclList :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> [SExpr Pos] ->
+loadGenSkelDeclList :: (Algebra t p g s e c, MonadFail m) => [Int] ->
+                       [t] -> [SExpr Pos] ->
                        m (SkelDeclInstList t)
 loadGenSkelDeclList _ _ [] = return []
 loadGenSkelDeclList heights vars (a:b) =
@@ -700,7 +711,8 @@
       b' <- loadGenSkelDeclList heights vars b
       return (a':b')
 
-loadGenSkelDecl :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> String ->
+loadGenSkelDecl :: (Algebra t p g s e c, MonadFail m) => [Int] ->
+                   [t] -> String ->
                    SExpr Pos -> m (SkelDeclInst t)
 loadGenSkelDecl heights vars stag (L _ (tlist:llist)) =
     do
@@ -712,7 +724,7 @@
 loadGenSkelDecl _ _ _ x =
     fail (shows (annotation x) "Malformed declaration: expecting a list")
 
-loadGenRoleDecls :: (Algebra t p g s e c, Monad m) => Int -> [t] ->
+loadGenRoleDecls :: (Algebra t p g s e c, MonadFail m) => Int -> [t] ->
                     [(String,[SExpr Pos])] -> m [RoleDeclaration t]
 loadGenRoleDecls _ _ [] = return []
 loadGenRoleDecls height vars ((name,rawds):b) =
@@ -721,7 +733,8 @@
       b' <- loadGenRoleDecls height vars b
       return ((name,a'):b')
 
-loadGenRoleDeclList :: (Algebra t p g s e c, Monad m) => Int -> [t] -> [SExpr Pos] ->
+loadGenRoleDeclList :: (Algebra t p g s e c, MonadFail m) => Int ->
+                       [t] -> [SExpr Pos] ->
                        m (RoleDeclInstList t)
 loadGenRoleDeclList _ _ [] = return []
 loadGenRoleDeclList height vars (a:b) =
@@ -730,7 +743,7 @@
       b' <- loadGenRoleDeclList height vars b
       return (a':b')
 
-loadGenRoleDecl :: (Algebra t p g s e c, Monad m) => Int -> [t] -> String ->
+loadGenRoleDecl :: (Algebra t p g s e c, MonadFail m) => Int -> [t] -> String ->
                    SExpr Pos -> m (RoleDeclInst t)
 loadGenRoleDecl height vars stag (L _ (tlist:llist)) =
     do
@@ -742,7 +755,7 @@
 loadGenRoleDecl _ _ _ x =
     fail (shows (annotation x) "Malformed declaration: expecting a list")
 
-loadOrderings :: Monad m => [Int] -> [SExpr Pos] -> Bool -> m [Pair]
+loadOrderings :: MonadFail m => [Int] -> [SExpr Pos] -> Bool -> m [Pair]
 loadOrderings heights x strict =
     foldM f [] x
     where
@@ -751,7 +764,7 @@
             np <- loadPair heights x strict
             return (adjoin np ns)
 
-loadPair :: Monad m => [Int] -> SExpr Pos -> Bool -> m Pair
+loadPair :: MonadFail m => [Int] -> SExpr Pos -> Bool -> m Pair
 loadPair heights (L pos [x0, x1]) strict =
     do
       n0 <- loadNode heights x0
@@ -761,7 +774,7 @@
         False -> return (n0, n1)
 loadPair _ x _ = fail (shows (annotation x) "Malformed pair")
 
-loadTerms :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m [t]
+loadTerms :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m [t]
 loadTerms _ (L _ []) = return []
 loadTerms vars (L pos (head:rest)) =
     do
@@ -770,7 +783,7 @@
       return (a:b)
 loadTerms _ x = fail (shows (annotation x) "Malformed list of terms")
 
-loadNodes :: Monad m => [Int] -> [SExpr Pos] -> m [Node]
+loadNodes :: MonadFail m => [Int] -> [SExpr Pos] -> m [Node]
 loadNodes _ [] = return []
 loadNodes heights (head:rest) =
     do
@@ -778,7 +791,7 @@
       a <- loadNode heights head
       return (a:b)
 
-loadIntsMax :: Monad m => Int -> [SExpr Pos] -> m [Int]
+loadIntsMax :: MonadFail m => Int -> [SExpr Pos] -> m [Int]
 loadIntsMax _ [] = return []
 loadIntsMax max (a:b) =
     do
@@ -786,14 +799,14 @@
       b <- loadIntsMax max b
       return (a:b)
 
-loadIntMax :: Monad m => Int -> SExpr Pos -> m Int
+loadIntMax :: MonadFail m => Int -> SExpr Pos -> m Int
 loadIntMax max (N pos x)
     | x < 0 = fail (shows pos "Malformed declaration: Negative position in role")
     | x >= max = fail (shows pos "Malformed declaration: Bad position in role")
     | otherwise = return x
 loadIntMax _ x = fail (shows (annotation x) "Malformed declaration: position")
 
-loadNode :: Monad m => [Int] -> SExpr Pos -> m Node
+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node
 loadNode heights (L pos [N _ s, N _ p])
     | s < 0 = fail (shows pos "Malformed node: Negative strand in node")
     | p < 0 = fail (shows pos "Malformed node: Negative position in node")
@@ -809,7 +822,7 @@
           | otherwise = height xs (s - 1)
 loadNode _ x = fail (shows (annotation x) "Malformed node")
 
-loadFact :: (Algebra t p g s e c, Monad m) =>
+loadFact :: (Algebra t p g s e c, MonadFail m) =>
             [Int] -> [t] -> SExpr Pos -> m (Fact t)
 loadFact heights vars (L _ (S _ name : fs)) =
   do
@@ -818,7 +831,7 @@
 loadFact _ _ x =
   fail (shows (annotation x) "Malformed fact")
 
-loadFterm :: (Algebra t p g s e c, Monad m) =>
+loadFterm :: (Algebra t p g s e c, MonadFail m) =>
              [Int] -> [t] -> SExpr Pos -> m (FTerm t)
 loadFterm heights _ (N pos s)
   | 0 <= s && s < length heights = return $ FSid s
@@ -828,7 +841,7 @@
     t <- loadTerm vars False x
     return $ FTerm t
 
-loadPov :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadPov :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
            [SExpr Pos] -> m (Maybe (Preskel t g s e), [Sid])
 loadPov _ _ [] = return (Nothing, [])
 loadPov pos p [L _ xs, x] =
@@ -838,18 +851,18 @@
     return (Just k, prob)
 loadPov pos _ _ = fail (shows pos "Bad POV within a skeleton")
 
-loadInt :: Monad m => SExpr Pos -> m Int
+loadInt :: MonadFail m => SExpr Pos -> m Int
 loadInt (N _ n) = return n
 loadInt x = fail (shows (annotation x) "Expecting an integer")
 
-loadPovPreskel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadPovPreskel :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                   SExpr Pos -> m (Preskel t g s e)
 loadPovPreskel _ p (L pos (S _ "defskeleton" : S _ name : xs))
   | pname p == name = loadPreskel pos p xs
   | otherwise = fail (shows pos $ "Protocol " ++ name ++ " mismatch")
 loadPovPreskel pos _ _ = fail (shows pos "Malformed defskeleton")
 
-checkProb :: Monad m => Pos -> Int -> [Sid] -> m ()
+checkProb :: MonadFail m => Pos -> Int -> [Sid] -> m ()
 checkProb pos nstrands prob =
   mapM_ f prob
   where
@@ -859,7 +872,7 @@
 -- Security Goals
 
 -- Load a defgoal form
-findGoal :: (Algebra t p g s e c, Monad m) => Pos ->
+findGoal :: (Algebra t p g s e c, MonadFail m) => Pos ->
             [Prot t g] -> [SExpr Pos] -> m (Preskel t g s e)
 findGoal pos ps (S _ name : x : xs) =
     case L.find (\p -> name == pname p) ps of
@@ -889,7 +902,7 @@
 
 --- Load a sequence of security goals
 
-loadGoals :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadGoals :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
              g -> [SExpr Pos] -> m (g, [Goal t])
 loadGoals _ _ g [] = return (g, [])
 loadGoals pos prot g (x : xs) =
@@ -905,7 +918,7 @@
 -- Load a single security goal, a universally quantified formula
 -- Returns the goal and the antecedent with position information.
 
-loadSentence :: (Algebra t p g s e c, Monad m) => Mode -> Pos ->
+loadSentence :: (Algebra t p g s e c, MonadFail m) => Mode -> Pos ->
                 Prot t g -> g -> SExpr Pos -> m (g, Goal t, Conj t)
 loadSentence md _ prot g (L pos [S _ "forall", L _ vs, x]) =
   do
@@ -915,7 +928,8 @@
 
 -- Load the top-level implication of a security goal
 
-loadImplication :: (Algebra t p g s e c, Monad m) => Mode -> Pos -> Prot t g ->
+loadImplication :: (Algebra t p g s e c, MonadFail m) => Mode ->
+                   Pos -> Prot t g ->
                    g -> [t] -> SExpr Pos -> m (g, Goal t, Conj t)
 loadImplication md _ prot g vars (L pos [S _ "implies", a, c]) =
   do
@@ -934,7 +948,7 @@
 -- The conclusion must be a disjunction.  Each disjunct may introduce
 -- existentially quantified variables.
 
-loadConclusion :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadConclusion :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                   g -> [t] -> SExpr Pos -> m (g, [([t], Conj t)])
 loadConclusion _ _ g _ (L _ [S _ "false"]) = return (g, [])
 loadConclusion _ prot g vars (L pos (S _ "or" : xs)) =
@@ -944,7 +958,7 @@
     (g, a) <- loadExistential pos prot g vars x
     return (g, [a])
 
-loadDisjuncts :: (Algebra t p g s e c, Monad m) => Pos ->
+loadDisjuncts :: (Algebra t p g s e c, MonadFail m) => Pos ->
                  Prot t g -> g -> [t] -> [SExpr Pos] ->
                  [([t], Conj t)] -> m (g, [([t], Conj t)])
 loadDisjuncts _ _ g _ [] rest = return (g, reverse rest)
@@ -953,7 +967,7 @@
     (g, a) <- loadExistential pos prot g vars x
     loadDisjuncts pos prot g vars xs (a : rest)
 
-loadExistential :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadExistential :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                    g -> [t] -> SExpr Pos -> m (g, ([t], Conj t))
 loadExistential _ prot g vars (L pos [S _ "exists", L _ vs, x]) =
   do
@@ -968,7 +982,7 @@
 -- Load a conjunction and check the result as determined by the mode
 -- md.
 
-loadCheckedConj :: (Algebra t p g s e c, Monad m) => Mode -> Pos ->
+loadCheckedConj :: (Algebra t p g s e c, MonadFail m) => Mode -> Pos ->
                    Prot t g -> [t] -> [t] -> SExpr Pos -> m (Conj t)
 loadCheckedConj RoleSpec pos prot vars unbound x =
   loadRoleSpecific pos prot vars unbound x
@@ -978,7 +992,7 @@
 --- Load a conjunction of atomic formulas and ensure the formula is
 --- role specific.
 
-loadRoleSpecific :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadRoleSpecific :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                     [t] -> [t] -> SExpr Pos -> m (Conj t)
 loadRoleSpecific pos prot vars unbound x =
   do
@@ -996,7 +1010,7 @@
 -- Load a conjuction of atomic formulas and ensure that all declared
 -- variables are used.
 
-loadUsedVars :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadUsedVars :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                 [t] -> [t] -> SExpr Pos -> m (Conj t)
 loadUsedVars pos prot vars unbound x =
   do
@@ -1009,7 +1023,7 @@
 
 -- Load a conjunction of atomic formulas
 
-loadConjunction :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadConjunction :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                    [t] -> SExpr Pos -> m (Conj t)
 loadConjunction _ p kvars (L pos (S _ "and" : xs)) =
   loadConjuncts pos p kvars xs []
@@ -1018,7 +1032,7 @@
     (pos, a) <- loadPrimary top p kvars x
     return [(pos, a)]
 
-loadConjuncts :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadConjuncts :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                  [t] -> [SExpr Pos] -> Conj t -> m (Conj t)
 loadConjuncts _ _ _ [] rest = return (reverse rest)
 loadConjuncts top p kvars (x : xs) rest =
@@ -1028,7 +1042,7 @@
 
 -- Load the atomic formulas
 
-loadPrimary :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
+loadPrimary :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->
                [t] -> SExpr Pos -> m (Pos, AForm t)
 loadPrimary _ _ kvars (L pos [S _ "=", x, y]) =
   do
@@ -1105,7 +1119,7 @@
 
 -- Load a term and make sure it has sort strd
 
-loadStrdTerm :: (Algebra t p g s e c, Monad m) =>
+loadStrdTerm :: (Algebra t p g s e c, MonadFail  m) =>
                 [t] -> SExpr Pos -> m t
 loadStrdTerm ts x =
   do
@@ -1116,7 +1130,7 @@
 
 -- Load a term and make sure it describes a node
 
-loadNodeTerm :: (Algebra t p g s e c, Monad m) =>
+loadNodeTerm :: (Algebra t p g s e c, MonadFail m) =>
                 [t] -> SExpr Pos -> SExpr Pos -> m (NodeTerm t)
 loadNodeTerm ts x (N _ i) | i >= 0 =
   do
@@ -1127,7 +1141,7 @@
 
 -- Load a term and make sure it does not have sort node
 
-loadAlgTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t
+loadAlgTerm :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m t
 loadAlgTerm _ x@(L _ [N _ _, N _ _]) =
   fail (shows (annotation x) "Expecting an algebra term")
 loadAlgTerm ts x =
@@ -1148,7 +1162,7 @@
 
 -- Returns variables in unbound that are not role specific
 
-roleSpecific :: (Algebra t p g s e c, Monad m) =>
+roleSpecific :: (Algebra t p g s e c, MonadFail m) =>
                 [t] -> (Pos, AForm t) -> m [t]
 roleSpecific unbound (_, Length _ z _) =
   return $ L.delete z 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
@@ -6,6 +6,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Lib.Protocol (Event (..), evtTerms, evtMesgTerms, evtMap, evt,
     recvTerm, Trace, stripSync, tterms, originates,
     originationPos, gainedPos, genGainedPos, firstOccurs,
@@ -344,7 +350,7 @@
 -- the trace, and every variable that occurs in each atom
 -- declared to be non-originating occurs in some term in the trace,
 -- and the atom must never be carried by any term in the trace.
-roleWellFormed :: (Monad m, Algebra t p g s e c) => Role t -> m ()
+roleWellFormed :: (MonadFail m, Algebra t p g s e c) => Role t -> m ()
 roleWellFormed role =
     do
       failwith "[ASSERT FAILED] invalid declaration"
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
@@ -6,6 +6,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener,
     role, env, trace, height, listenerTerm, Sid, Node, mkPreskel,
     firstSkeleton, Pair, Preskel, gen, protocol, kgoals, insts,
@@ -1250,7 +1256,7 @@
 thinManyStrands prs ps =
   [ prs' | prs' <- compressMany prs ps,
            prs'' <- compressMany prs (swap ps),
-           isomorphic (gist (skel prs')) (gist (skel prs''))]
+           probIsomorphic (skel prs') (skel prs'')]
 
 compressMany :: Algebra t p g s e c => PRS t p g s e c ->
                 [(Sid, Sid)] -> [PRS t p g s e c]
@@ -2136,7 +2142,7 @@
                             (filter (\(t, _) -> not (isNum t)) (kugen k)))
 
 -- Do notation friendly preskeleton well formed check.
-wellFormedPreskel :: (Monad m, Algebra t p g s e c) =>
+wellFormedPreskel :: (MonadFail m, Algebra t p g s e c) =>
                      Preskel t g s e -> m (Preskel t g s e)
 wellFormedPreskel k
     | preskelWellFormed k = return k
@@ -2145,7 +2151,7 @@
 -- Exported
 -- A version of preskelWellFormed that explains why a preskeleton is
 -- not well formed.
-verbosePreskelWellFormed :: (Monad m, Algebra t p g s e c) =>
+verbosePreskelWellFormed :: (MonadFail m, Algebra t p g s e c) =>
                             Preskel t g s e -> m ()
 verbosePreskelWellFormed k =
     do
@@ -2189,14 +2195,14 @@
           (null ts)
 
 -- Do notation friendly preskeleton well formed check.
-reducedWellFormed :: Monad m => Preskel t g s e -> m ()
+reducedWellFormed :: MonadFail m => Preskel t g s e -> m ()
 reducedWellFormed k
   | reducedWellOrdered k = return ()
   | otherwise = fail "reduced preskeleton not well formed"
 
 -- A transition or an observer node should have at most one transition
 -- node immediately after it.
-noStateSplit :: Monad m => Preskel t g s e -> m ()
+noStateSplit :: MonadFail m => Preskel t g s e -> m ()
 noStateSplit k
   | loop (leadsto k) S.empty = return ()
   | otherwise = fail "reduced preskeleton has a state split"
diff --git a/src/CPSA/Lib/Utilities.hs b/src/CPSA/Lib/Utilities.hs
--- a/src/CPSA/Lib/Utilities.hs
+++ b/src/CPSA/Lib/Utilities.hs
@@ -7,6 +7,8 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
 module CPSA.Lib.Utilities where
 
 import qualified Data.Set as S
@@ -30,8 +32,14 @@
 instance Monad ReturnFail where
     Fail l >>= _   = Fail l
     Return r >>= k = k r
-    fail s = Fail s             -- This must be moved to MonadFail
 
+#if (MIN_VERSION_base(4,13,0))
+instance MonadFail ReturnFail where
+#else
+#define MonadFail Monad
+#endif
+    fail s         = Fail s
+
 adjoin :: Eq a => a -> [a] -> [a]
 adjoin x xs
     | x `elem` xs = xs
@@ -62,7 +70,7 @@
 nats n = [0..(n - 1)]
 
 {-# INLINE assert #-}
-assert :: Monad m => (a -> Bool) -> a -> m a
+assert :: MonadFail m => (a -> Bool) -> a -> m a
 assert pred x
     | pred x = return x
     | otherwise = fail "assertion failed"
@@ -114,7 +122,7 @@
       (Just n, Just n') -> n >= n'
       _ -> True
 
-failwith :: Monad m => String -> Bool -> m ()
+failwith :: MonadFail m => String -> Bool -> m ()
 failwith msg test =
     case test of
       True -> return ()
diff --git a/src/CPSA/Match/Match.hs b/src/CPSA/Match/Match.hs
--- a/src/CPSA/Match/Match.hs
+++ b/src/CPSA/Match/Match.hs
@@ -4,6 +4,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Match.Match (testMatcher) where
 
 import CPSA.Lib.SExpr
@@ -31,7 +37,7 @@
     return $ L () $ map (showSubst vs) (absenceSubst g a)
 go _ x = fail (shows (annotation x) "Malformed input!")
 
-loadMatch :: (Algebra t p g s e c, Monad m) =>
+loadMatch :: (Algebra t p g s e c, MonadFail m) =>
               [t] -> SExpr Pos -> m (t, t)
 loadMatch vs (L _ [r, n]) =
   do
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
@@ -6,6 +6,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.SAS.SAS (State, sas) where
 
 import Control.Monad (foldM)
@@ -31,7 +37,7 @@
 
 type State t g c = ([Prot t g c], [Preskel t g c])
 
-sas :: (Algebra t p g s e c, Monad m) => String -> g ->
+sas :: (Algebra t p g s e c, MonadFail m) => String -> g ->
          State t g c -> Maybe (SExpr Pos) ->
          m (State t g c, Maybe (SExpr ()))
 sas _ _ (ps, ks) Nothing =    -- Nothing signifies end-of-file
@@ -41,7 +47,7 @@
 sas name gen (ps, ks) (Just sexpr) = -- Looking for shapes
     loadOtherPreskel name gen ps ks sexpr
 
-loadPOV :: (Algebra t p g s e c, Monad m) => String -> g ->
+loadPOV :: (Algebra t p g s e c, MonadFail m) => String -> g ->
            [Prot t g c] -> SExpr Pos ->
            m (State t g c, Maybe (SExpr ()))
 loadPOV name origin ps (L pos (S _ "defprotocol" : xs)) =
@@ -60,7 +66,7 @@
         _ -> return ((ps, []), Nothing) -- Not POV
 loadPOV _ _ ps _ = return ((ps, []), Nothing)
 
-loadOtherPreskel :: (Algebra t p g s e c, Monad m) => String -> g ->
+loadOtherPreskel :: (Algebra t p g s e c, MonadFail m) => String -> g ->
                     [Prot t g c] -> [Preskel t g c] ->
                     SExpr Pos -> m (State t g c, Maybe (SExpr ()))
 loadOtherPreskel name origin ps ks (L pos (S _ "defprotocol" : xs)) =
@@ -81,7 +87,7 @@
 loadOtherPreskel _ _ ps ks _ = return ((ps, ks), Nothing)
 
 -- Ensure every uniq originates
-origCheck :: (Algebra t p g s e c, Monad m) =>
+origCheck :: (Algebra t p g s e c, MonadFail m) =>
              Pos -> Preskel t g c -> m ()
 origCheck pos k =
   mapM_ f (uniqs k)
@@ -114,7 +120,7 @@
 
 -- Load a protocol.  On success, returns a Prot record.
 
-loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->
+loadProt :: (Algebra t p g s e c, MonadFail m) => String -> g ->
             Pos -> [SExpr Pos] -> m (Prot t g c)
 loadProt nom origin pos (S _ name : S _ alg : x : xs)
     | alg /= nom =
@@ -132,7 +138,7 @@
 -- every variable that occurs in a preskeleton never occurs in one of
 -- its roles.
 
-loadRoles :: (Algebra t p g s e c, Monad m) => g ->
+loadRoles :: (Algebra t p g s e c, MonadFail m) => g ->
              [SExpr Pos] -> m (g, [Role t c])
 loadRoles origin xs =
     mapAccumLM loadRole origin $ stripComments xs
@@ -154,7 +160,7 @@
       (z'', ys) <- mapAccumLM f z' xs
       return (z'', y : ys)
 
-loadRole :: (Algebra t p g s e c, Monad m) => g ->
+loadRole :: (Algebra t p g s e c, MonadFail m) => g ->
             SExpr Pos -> m (g, Role t c)
 loadRole gen (L _ (S _ "defrole" :
                      S _ name :
@@ -174,7 +180,7 @@
 listenerName :: String
 listenerName = ""
 
-makeListenerRole :: (Algebra t p g s e c, Monad m) => Pos -> g ->
+makeListenerRole :: (Algebra t p g s e c, MonadFail m) => Pos -> g ->
                     m (g, Role t c)
 makeListenerRole pos gen =
     do
@@ -184,7 +190,7 @@
       let r = Role { rname = listenerName, vars = vars, ctx = ctx }
       return (gen', r)
 
-makeVar :: (Algebra t p g s e c, Monad m) => Pos -> g -> String -> m (g, t)
+makeVar :: (Algebra t p g s e c, MonadFail m) => Pos -> g -> String -> m (g, t)
 makeVar pos gen name =
     do
       (gen', ts) <- loadVars gen [L pos [S pos name, S pos "mesg"]]
@@ -202,7 +208,7 @@
 type GVM g t = (g, VM t)
 
 -- Add a variable for a node if the mapping does not already exist.
-addVar :: (Algebra t p g s e c, Monad m) =>
+addVar :: (Algebra t p g s e c, MonadFail m) =>
           Pos -> GVM g t -> Strand -> m (GVM g t)
 addVar pos (gen, vm) z =
   case M.lookup z vm of
@@ -224,7 +230,7 @@
 
 -- Find a protocol
 
-findProt :: Monad m => Pos -> [Prot t g c] -> [SExpr Pos] -> m (Prot t g c)
+findProt :: MonadFail m => Pos -> [Prot t g c] -> [SExpr Pos] -> m (Prot t g c)
 findProt pos ps (S _ name : _) =
     case L.find (\p -> name == pname p) ps of
       Nothing -> fail (shows pos $ "Protocol " ++ name ++ " unknown")
@@ -269,7 +275,7 @@
       homomorphisms :: [SExpr Pos], -- Loaded later
       varmap :: VM t }
 
-loadPreskel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->
+loadPreskel :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g c ->
                g -> [SExpr Pos] -> m (Preskel t g c)
 loadPreskel pos prot gen (S _ _ : L _ (S _ "vars" : vars) : xs) =
     do
@@ -304,7 +310,7 @@
                         varmap = varmap})
 loadPreskel pos _ _ _ = fail (shows pos "Malformed skeleton")
 
-loadInsts :: (Algebra t p g s e c, Monad m) => Prot t g c ->
+loadInsts :: (Algebra t p g s e c, MonadFail m) => Prot t g c ->
              [t] -> [Instance t c] -> [SExpr Pos] -> m [Instance t c]
 loadInsts prot kvars insts (L pos (S _ "defstrand" : x) : xs) =
     case x of
@@ -325,7 +331,7 @@
 loadInsts _ _ insts _ =
     return (reverse insts)
 
-loadInst :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->
+loadInst :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g c ->
             [t] -> String -> Int -> [SExpr Pos] -> m (Instance t c)
 loadInst pos prot kvars role height env =
     do
@@ -334,14 +340,14 @@
       return (Instance { pos = pos, role = r,
                          env = env, height = height })
 
-lookupRole :: Monad m => Pos -> Prot t g c -> String -> m (Role t c)
+lookupRole :: MonadFail m => Pos -> Prot t g c -> String -> m (Role t c)
 lookupRole pos prot role =
     case L.find (\r -> role == rname r) (roles prot) of
       Nothing ->
           fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname prot)
       Just r -> return r
 
-loadMaplet :: (Algebra t p g s e c, Monad m) =>
+loadMaplet :: (Algebra t p g s e c, MonadFail m) =>
               [t] -> [t] -> SExpr Pos -> m (t, t)
 loadMaplet kvars vars (L _ [domain, range]) =
     do
@@ -350,7 +356,7 @@
       return (t, t')
 loadMaplet _ _ x = fail (shows (annotation x) "Malformed maplet")
 
-loadListener :: (Algebra t p g s e c, Monad m) => Pos ->
+loadListener :: (Algebra t p g s e c, MonadFail m) => Pos ->
                 Prot t g c -> [t] -> SExpr Pos -> m (Instance t c)
 loadListener pos prot kvars x =
     do
@@ -361,7 +367,7 @@
 
 -- Load the node orderings
 
-loadOrderings :: Monad m => Strands -> [SExpr Pos] -> m [Pair]
+loadOrderings :: MonadFail m => Strands -> [SExpr Pos] -> m [Pair]
 loadOrderings _ [] = return []
 loadOrderings strands (x : xs) =
     do
@@ -369,7 +375,7 @@
       nps <- loadOrderings strands xs
       return (adjoin np nps)
 
-loadPair :: Monad m => [Int] -> SExpr Pos -> m Pair
+loadPair :: MonadFail m => [Int] -> SExpr Pos -> m Pair
 loadPair heights (L pos [x0, x1]) =
     do
       n0 <- loadNode heights x0
@@ -381,7 +387,7 @@
       sameStrands (s0, _) (s1, _) = s0 == s1
 loadPair _ x = fail (shows (annotation x) "Malformed pair")
 
-loadNode :: Monad m => [Int] -> SExpr Pos -> m Node
+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node
 loadNode heights (L pos [N _ s, N _ p])
     | s < 0 = fail (shows pos "Negative strand in node")
     | p < 0 = fail (shows pos "Negative position in node")
@@ -397,7 +403,8 @@
           | otherwise = height xs (s - 1)
 loadNode _ x = fail (shows (annotation x) "Malformed node")
 
-loadBaseTerms :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [t]
+loadBaseTerms :: (Algebra t p g s e c, MonadFail m) => [t] ->
+                 [SExpr Pos] -> m [t]
 loadBaseTerms _ [] = return []
 loadBaseTerms vars (x : xs) =
     do
@@ -405,7 +412,7 @@
       ts <- loadBaseTerms vars xs
       return (adjoin t ts)
 
-loadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t
+loadBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m t
 loadBaseTerm vars x =
     do
       t <- loadTerm vars False x
@@ -413,7 +420,7 @@
         True -> return t
         False -> fail (shows (annotation x) "Expecting an atom")
 
-loadOrigs :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->
+loadOrigs :: (Algebra t p g s e c, MonadFail m) => [t] -> Strands ->
              [SExpr Pos] -> m [(t, Node)]
 loadOrigs _ _ [] = return []
 loadOrigs vars heights (x : xs) =
@@ -422,7 +429,7 @@
       os <- loadOrigs vars heights xs
       return (adjoin o os)
 
-loadOrig :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->
+loadOrig :: (Algebra t p g s e c, MonadFail m) => [t] -> Strands ->
             SExpr Pos -> m (t, Node)
 loadOrig vars heights (L _ [x, y]) =
     do
@@ -433,12 +440,12 @@
     fail (shows (annotation x) "Malformed origination")
 
 -- Make a variable for each strand
-makeVarmap :: (Algebra t p g s e c, Monad m) =>
+makeVarmap :: (Algebra t p g s e c, MonadFail m) =>
               Pos -> g -> [Strand] -> m (GVM g t)
 makeVarmap pos g strands =
   foldM (addVar pos) (g, M.empty) strands
 
-loadFact :: (Algebra t p g s e c, Monad m) => [t] ->
+loadFact :: (Algebra t p g s e c, MonadFail m) => [t] ->
             VM t -> SExpr Pos -> m (Fact t)
 loadFact vars varmap (L _ (S _ name : ft)) =
   do
@@ -447,7 +454,7 @@
 loadFact _ _ x =
   fail (shows (annotation x) "Malformed fact")
 
-loadFactTerm :: (Algebra t p g s e c, Monad m) =>
+loadFactTerm :: (Algebra t p g s e c, MonadFail m) =>
                 [t] -> VM t -> SExpr Pos -> m t
 loadFactTerm _ varmap (N pos z) =
   case M.lookup z varmap of
@@ -464,12 +471,12 @@
 
 type Homo t = ([(t, t)], [(t, t)])
 
-loadMaps :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
+loadMaps :: (Algebra t p g s e c, MonadFail m) => Preskel t g c ->
             Preskel t g c -> [SExpr Pos] -> m [Homo t]
 loadMaps pov k maps =
     mapM (loadMap pov k) maps
 
-loadMap :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
+loadMap :: (Algebra t p g s e c, MonadFail m) => Preskel t g c ->
             Preskel t g c -> SExpr Pos -> m (Homo t)
 loadMap pov k (L _ [L _ strandMap, L _ algebraMap]) =
     do
@@ -480,18 +487,19 @@
       return (nh, ah)
 loadMap _ _ x = fail (shows (annotation x) "Malformed map")
 
-loadPerm :: Monad m => SExpr Pos -> m Int
+loadPerm :: MonadFail m => SExpr Pos -> m Int
 loadPerm (N _ n) | n >= 0 = return n
 loadPerm x = fail (shows (annotation x) "Expecting a natural number")
 
 -- Applies a strand permutation to a strand.
-loadStrandEq :: Monad m => Preskel t g c -> [Int] -> (Strand, t) -> m (t, t)
+loadStrandEq :: MonadFail m => Preskel t g c -> [Int] ->
+                (Strand, t) -> m (t, t)
 loadStrandEq k perm (z, v) =
   do
     z <- index perm z
     return (v, slookup z (varmap k))
 
-index :: Monad m => [a] -> Int -> m a
+index :: MonadFail m => [a] -> Int -> m a
 index (x : _) 0 = return x
 index (_ : xs) i | i > 0 = index xs (i - 1)
 index _ _ = fail "Bad strand map"
@@ -552,7 +560,7 @@
 
 type Analysis t g c = (Preskel t g c, [(Homo t, Preskel t g c)])
 
-loadAnalysis :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
+loadAnalysis :: (Algebra t p g s e c, MonadFail m) => Preskel t g c ->
                 [Preskel t g c] -> m (Analysis t g c)
 loadAnalysis pov ks =
   do
@@ -642,7 +650,7 @@
 
 -- Formula printing
 
-displayFormula :: (Algebra t p g s e c, Monad m) =>
+displayFormula :: (Algebra t p g s e c, MonadFail m) =>
                   [Prot t g c] -> [Preskel t g c] ->
                   m (State t g c, Maybe (SExpr ()))
 displayFormula ps [] =
diff --git a/src/CPSA/Shapes/Shapes.hs b/src/CPSA/Shapes/Shapes.hs
--- a/src/CPSA/Shapes/Shapes.hs
+++ b/src/CPSA/Shapes/Shapes.hs
@@ -6,6 +6,12 @@
 -- modify it under the terms of the BSD License as published by the
 -- University of California.
 
+{-# LANGUAGE CPP #-}
+
+#if !(MIN_VERSION_base(4,13,0))
+#define MonadFail Monad
+#endif
+
 module CPSA.Shapes.Shapes (Map, empty, shape) where
 
 import qualified Data.IntMap as I
@@ -24,7 +30,7 @@
 -- skeleton is changed to reflect omitted skeletons, and its seen
 -- children are deleted.
 
-shape :: Monad m => Map -> SExpr Pos -> m (Map, Maybe (SExpr Pos))
+shape :: MonadFail m => Map -> SExpr Pos -> m (Map, Maybe (SExpr Pos))
 shape map x@(L _ (S _ "defskeleton" : _ : _ : strands)) =
     do
       label <- nassoc "label" xs
@@ -71,7 +77,7 @@
       extend x (Just y) = Just (x ++ y)
 
 -- Look up a value known to be an Int
-nassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe Int)
+nassoc :: MonadFail m => String -> [SExpr Pos] -> m (Maybe Int)
 nassoc key xs =
     case assoc key xs of
       Nothing -> return Nothing
@@ -82,7 +88,7 @@
       Just (x:_) -> fail (shows (annotation x) "Expecting one number")
       Just [] -> fail (shows (annotation (head xs)) "Expecting one number")
 
-num :: Monad m => SExpr Pos -> m Int
+num :: MonadFail m => SExpr Pos -> m Int
 num (N _ n) = return n
 num x = fail (shows (annotation x) "Expecting a number")
 
diff --git a/tst/aik.scm b/tst/aik.scm
--- a/tst/aik.scm
+++ b/tst/aik.scm
@@ -28,4 +28,3 @@
   (vars (i x mf pc name) (ek k akey) (srk skey))
   (deflistener (enc "aic" i k x (privk pc)))
   (non-orig (privk pc)))
-
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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from aik.scm")
 
 (defprotocol aikprot basic
diff --git a/tst/attest.scm b/tst/attest.scm
new file mode 100644
--- /dev/null
+++ b/tst/attest.scm
@@ -0,0 +1,106 @@
+(herald attest-door)
+
+(defprotocol attest-door basic
+  (defrole appraise
+    (vars (d p a akey) (n text))
+    (trace
+     (recv (enc (enc d n (invk p)) a))
+     (send (enc n a p)))
+    (comment "The appraiser for the door"))
+  (defrole person
+    (vars (d p a akey) (k skey) (n t text))
+    (trace
+     (send (enc (enc d n (invk p)) a))
+     (recv (enc n a p))
+     (send (enc (enc k (invk p)) d))
+     (recv (enc t k))
+     (send t))
+    (uniq-orig n k)
+    (comment "Person requesting door entry"))
+  (defrole door
+    (vars (d p akey) (k skey) (t text))
+    (trace
+     (recv (enc (enc k (invk p)) d))
+     (send (enc t k))
+     (recv t))
+    (uniq-orig t))
+  (defrole squealer
+    (vars (d p akey) (k skey) (t text))
+    (trace
+     (recv (enc (enc k (invk p)) d))
+     (send k))
+    (comment "Fake door"))
+  (defrule yes
+    (forall ((z strd) (a akey))
+	    (implies
+	     (and (p "appraise" z 2)
+		  (p "appraise" "a" z a)
+		  (non (invk a)))
+	     (exists ((d akey))
+		     (and (p "appraise" "d" z d)
+			  (non (invk d))))))
+    (comment "Appraisal succeeded"))
+  (comment "Door attestations protocol"))
+
+(defskeleton attest-door
+  (vars (p a akey))
+  (defstrand person 5 (p p) (a a))
+  (non-orig (invk p) (invk a))
+  (comment "Analyze from the person's perspective"))
+
+(defprotocol attest-door-trust basic
+  (defrole appraise
+    (vars (d p a akey) (n text))
+    (trace
+     (recv (enc (enc d n (invk p)) a))
+     (send (enc n a p)))
+    (comment "The appraiser for the door"))
+  (defrole person
+    (vars (d p a akey) (k skey) (n t text))
+    (trace
+     (send (enc (enc d n (invk p)) a))
+     (recv (enc n a p))
+     (send (enc (enc k (invk p)) d))
+     (recv (enc t k))
+     (send t))
+    (uniq-orig n k)
+    (comment "Person requesting door entry"))
+  (defrole door
+    (vars (d p akey) (k skey) (t text))
+    (trace
+     (recv (enc (enc k (invk p)) d))
+     (send (enc t k))
+     (recv t))
+    (uniq-orig t))
+  (defrole squealer
+    (vars (d p akey) (k skey) (t text))
+    (trace
+     (recv (enc (enc k (invk p)) d))
+     (send k))
+    (comment "Fake door"))
+  (defrule yes
+    (forall ((z strd) (a akey))
+	    (implies
+	     (and (p "appraise" z 2)
+		  (p "appraise" "a" z a)
+		  (non (invk a)))
+	     (exists ((d akey))
+		     (and (p "appraise" "d" z d)
+			  (non (invk d))))))
+    (comment "Appraisal succeeded"))
+  (defrule trust
+    (forall ((z w strd) (d akey))
+	    (implies
+	     (and (p "appraise" z 2)
+		  (p "appraise" "d" z d)
+		  (p "squealer" w 2)
+		  (p "squealer" "d" w d))
+	     (false)))
+    (comment "Squealer prohibited due to attestation"))
+  (comment "Door attestations protocol with attestation"))
+
+(defskeleton attest-door-trust
+  (vars (p a akey))
+  (defstrand person 5 (p p) (a a))
+  (non-orig (invk p) (invk a))
+  (comment "Analyze from the person's perspective"))
diff --git a/tst/attest.tst b/tst/attest.tst
new file mode 100644
--- /dev/null
+++ b/tst/attest.tst
@@ -0,0 +1,325 @@
+(herald attest-door)
+
+(comment "CPSA 3.6.4")
+(comment "All input read from attest.scm")
+
+(defprotocol attest-door basic
+  (defrole appraise
+    (vars (d p a akey) (n text))
+    (trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    (comment "The appraiser for the door"))
+  (defrole person
+    (vars (d p a akey) (k skey) (n t text))
+    (trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    (uniq-orig n k)
+    (comment "Person requesting door entry"))
+  (defrole door
+    (vars (d p akey) (k skey) (t text))
+    (trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
+    (uniq-orig t))
+  (defrole squealer
+    (vars (d p akey) (k skey))
+    (trace (recv (enc (enc k (invk p)) d)) (send k))
+    (comment "Fake door"))
+  (defrule yes
+    (forall ((z strd) (a akey))
+      (implies
+        (and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
+        (exists ((d akey))
+          (and (p "appraise" "d" z d) (non (invk d))))))
+    (comment "Appraisal succeeded"))
+  (comment "Door attestations protocol"))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (non-orig (invk p) (invk a))
+  (uniq-orig n k)
+  (comment "Analyze from the person's perspective")
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))
+  (label 0)
+  (unrealized (0 1))
+  (origs (n (0 0)) (k (0 2)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n k)
+  (rule yes)
+  (operation nonce-test (added-strand appraise 2) n (0 1)
+    (enc (enc d n (invk p)) a))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p))))
+  (label 1)
+  (parent 0)
+  (unrealized (0 3))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d d-0 p-0 akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (defstrand door 2 (t t) (k k) (d d-0) (p p-0))
+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n t k)
+  (operation encryption-test (added-strand door 2) (enc t k) (0 3))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv (enc (enc k (invk p-0)) d-0)) (send (enc t k))))
+  (label 2)
+  (parent 1)
+  (unrealized (2 0))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (deflistener k)
+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n k)
+  (operation encryption-test (added-listener k) (enc t k) (0 3))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv k) (send k)))
+  (label 3)
+  (parent 1)
+  (unrealized (2 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (defstrand door 2 (t t) (k k) (d d) (p p))
+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n t k)
+  (operation nonce-test (contracted (d-0 d) (p-0 p)) k (2 0)
+    (enc (enc k (invk p)) d))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv (enc (enc k (invk p)) d)) (send (enc t k))))
+  (label 4)
+  (parent 2)
+  (unrealized)
+  (shape)
+  (maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))
+  (origs (t (2 1)) (n (0 0)) (k (0 2))))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d d-0 p-0 akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (defstrand door 2 (t t) (k k) (d d-0) (p p-0))
+  (defstrand squealer 2 (k k) (d d) (p p))
+  (precedes ((0 0) (1 0)) ((0 2) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))
+    ((3 1) (2 0)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n t k)
+  (operation nonce-test (added-strand squealer 2) k (2 0)
+    (enc (enc k (invk p)) d))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv (enc (enc k (invk p-0)) d-0)) (send (enc t k)))
+    ((recv (enc (enc k (invk p)) d)) (send k)))
+  (label 5)
+  (parent 2)
+  (unrealized)
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (deflistener k)
+  (defstrand squealer 2 (k k) (d d) (p p))
+  (precedes ((0 0) (1 0)) ((0 2) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))
+    ((3 1) (2 0)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n k)
+  (operation nonce-test (added-strand squealer 2) k (2 0)
+    (enc (enc k (invk p)) d))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv k) (send k)) ((recv (enc (enc k (invk p)) d)) (send k)))
+  (label 6)
+  (parent 3)
+  (seen 7)
+  (unrealized)
+  (comment "1 in cohort - 0 not yet seen"))
+
+(defskeleton attest-door
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (defstrand squealer 2 (k k) (d d) (p p))
+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n k)
+  (operation generalization deleted (2 0))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv (enc (enc k (invk p)) d)) (send k)))
+  (label 7)
+  (parent 5)
+  (unrealized)
+  (shape)
+  (maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))
+  (origs (n (0 0)) (k (0 2))))
+
+(comment "Nothing left to do")
+
+(defprotocol attest-door-trust basic
+  (defrole appraise
+    (vars (d p a akey) (n text))
+    (trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    (comment "The appraiser for the door"))
+  (defrole person
+    (vars (d p a akey) (k skey) (n t text))
+    (trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    (uniq-orig n k)
+    (comment "Person requesting door entry"))
+  (defrole door
+    (vars (d p akey) (k skey) (t text))
+    (trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
+    (uniq-orig t))
+  (defrole squealer
+    (vars (d p akey) (k skey))
+    (trace (recv (enc (enc k (invk p)) d)) (send k))
+    (comment "Fake door"))
+  (defrule yes
+    (forall ((z strd) (a akey))
+      (implies
+        (and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
+        (exists ((d akey))
+          (and (p "appraise" "d" z d) (non (invk d))))))
+    (comment "Appraisal succeeded"))
+  (defrule trust
+    (forall ((z w strd) (d akey))
+      (implies
+        (and (p "appraise" z 2) (p "appraise" "d" z d)
+          (p "squealer" w 2) (p "squealer" "d" w d))
+        (false)))
+    (comment "Squealer prohibited due to attestation"))
+  (comment "Door attestations protocol with attestation"))
+
+(defskeleton attest-door-trust
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (non-orig (invk p) (invk a))
+  (uniq-orig n k)
+  (comment "Analyze from the person's perspective")
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))
+  (label 8)
+  (unrealized (0 1))
+  (origs (n (0 0)) (k (0 2)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton attest-door-trust
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n k)
+  (rule yes)
+  (operation nonce-test (added-strand appraise 2) n (0 1)
+    (enc (enc d n (invk p)) a))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p))))
+  (label 9)
+  (parent 8)
+  (unrealized (0 3))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton attest-door-trust
+  (vars (n t text) (k skey) (p a d d-0 p-0 akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (defstrand door 2 (t t) (k k) (d d-0) (p p-0))
+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n t k)
+  (operation encryption-test (added-strand door 2) (enc t k) (0 3))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv (enc (enc k (invk p-0)) d-0)) (send (enc t k))))
+  (label 10)
+  (parent 9)
+  (unrealized (2 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton attest-door-trust
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (deflistener k)
+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n k)
+  (operation encryption-test (added-listener k) (enc t k) (0 3))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv k) (send k)))
+  (label 11)
+  (parent 9)
+  (unrealized (2 0))
+  (dead)
+  (comment "empty cohort"))
+
+(defskeleton attest-door-trust
+  (vars (n t text) (k skey) (p a d akey))
+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))
+  (defstrand appraise 2 (n n) (d d) (p p) (a a))
+  (defstrand door 2 (t t) (k k) (d d) (p p))
+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
+  (non-orig (invk p) (invk a) (invk d))
+  (uniq-orig n t k)
+  (operation nonce-test (contracted (d-0 d) (p-0 p)) k (2 0)
+    (enc (enc k (invk p)) d))
+  (traces
+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
+    ((recv (enc (enc k (invk p)) d)) (send (enc t k))))
+  (label 12)
+  (parent 10)
+  (unrealized)
+  (shape)
+  (maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))
+  (origs (t (2 1)) (n (0 0)) (k (0 2))))
+
+(comment "Nothing left to do")
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from blanchet.scm")
 
 (defprotocol blanchet basic
diff --git a/tst/bltk_test.scm b/tst/bltk_test.scm
--- a/tst/bltk_test.scm
+++ b/tst/bltk_test.scm
@@ -71,5 +71,3 @@
   (vars (a b name))
   (defstrand recvr 2 (a a) (b b))
   (non-orig (bltk a b)))
-
-
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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from bltk_test.scm")
 
 (defprotocol test diffie-hellman
diff --git a/tst/comp_test.scm b/tst/comp_test.scm
new file mode 100644
--- /dev/null
+++ b/tst/comp_test.scm
@@ -0,0 +1,156 @@
+(herald "Main Example")
+
+(defprotocol main-ex-src basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+     (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+     (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i text) (k skey) (x mesg))
+    (trace
+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+     (send (enc "sorry" a b k))))
+  (defrole ay
+    (vars (a b c akey) (i d text) (k skey) (x mesg))
+    (trace
+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+     (send (enc "data" d k)))
+    (uniq-orig d)))
+
+(defprotocol main-ex-tgt basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+     (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+     (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i y n text) (k skey) (x mesg))
+    (trace
+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+     (send (enc y n i a x c))
+     (recv n)
+     (send (enc "sorry" a b k)))
+    (uniq-orig y n))
+  (defrole ay
+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))
+    (trace
+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+     (send (enc y n i a x c))
+     (recv y)
+     (send (enc "data" d k)))
+    (uniq-orig d y n))
+  (defrole sn
+    (vars (a b c akey) (i ssn y n text))
+    (trace
+     (recv (enc y n i a (enc a b i ssn c) c))
+     (send n)))
+  (defrole sy
+    (vars (a b c akey) (i ssn y n text))
+    (trace
+     (recv (enc y n i a (enc a b i ssn c) c))
+     (send y))))
+
+(defprotocol main-ex-tgt-rule basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+     (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+     (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i y n text) (k skey) (x mesg))
+    (trace
+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+     (send (enc y n i a x c))
+     (recv n)
+     (send (enc "sorry" a b k)))
+    (uniq-orig y n))
+  (defrole ay
+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))
+    (trace
+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+     (send (enc y n i a x c))
+     (recv y)
+     (send (enc "data" d k)))
+    (uniq-orig d y n))
+  (defrole sn
+    (vars (a b c akey) (i ssn y n text))
+    (trace
+     (recv (enc y n i a (enc a b i ssn c) c))
+     (send n)))
+  (defrole sy
+    (vars (a b c akey) (i ssn y n text))
+    (trace
+     (recv (enc y n i a (enc a b i ssn c) c))
+     (send y)))
+  (defrule src
+    (forall ((z strd) (i ssn text) (k skey) (a b c akey))
+	    (implies
+	     (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)
+		  (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)
+		  (p "qn" "c" z c) (non (invk a)) (non (invk b)) (non (invk c))
+		  (uniq k))
+	     (exists ((z-0 strd) (x mesg))
+		     (and (p "an" z-0 4) (p "an" "x" z-0 x)
+			  (p "an" "i" z-0 i) (p "an" "k" z-0 k)
+			  (p "an" "a" z-0 a) (p "an" "b" z-0 b)
+			  (p "an" "c" z-0 c) (prec z 0 z-0 0)
+			  (prec z-0 3 z 1)))))))
+
+(defskeleton main-ex-src
+  (vars (a b c akey))
+  (defstrand qn 2 (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c))
+  (comment
+   (defgoal main-ex-src
+     (forall ((i ssn text) (k skey) (a b c akey) (z strd))
+	     (implies
+	      (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)
+		   (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)
+		   (p "qn" "c" z c) (non (invk a)) (non (invk b)) (non (invk c))
+		   (uniq-at k z 0))
+	      (exists ((x mesg) (z-0 strd))
+		      (and (p "an" z-0 2) (p "an" "x" z-0 x) (p "an" "i" z-0 i)
+			   (p "an" "k" z-0 k) (p "an" "a" z-0 a) (p "an" "b" z-0 b)
+			   (p "an" "c" z-0 c) (prec z 0 z-0 0) (prec z-0 1 z 1))))))))
+
+(defskeleton main-ex-src
+  (vars (a b c akey))
+  (defstrand qy 2 (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c)))
+
+(defskeleton main-ex-tgt
+  (vars (a b c akey))
+  (defstrand qn 2 (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c)))
+
+(defskeleton main-ex-tgt
+  (vars (a b c akey))
+  (defstrand qy 2 (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c)))
+
+(defskeleton main-ex-tgt-rule
+  (vars (a b c akey))
+  (defstrand qn 2 (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c)))
diff --git a/tst/comp_test.tst b/tst/comp_test.tst
new file mode 100644
--- /dev/null
+++ b/tst/comp_test.tst
@@ -0,0 +1,604 @@
+(herald "Main Example")
+
+(comment "CPSA 3.6.4")
+(comment "All input read from comp_test.scm")
+
+(defprotocol main-ex-src basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc "sorry" a b k))))
+  (defrole ay
+    (vars (a b c akey) (i d text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc "data" d k)))
+    (uniq-orig d)))
+
+(defskeleton main-ex-src
+  (vars (i ssn text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (comment
+    (defgoal main-ex-src
+      (forall ((i ssn text) (k skey) (a b c akey) (z strd))
+        (implies
+          (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)
+            (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)
+            (p "qn" "c" z c) (non (invk a)) (non (invk b))
+            (non (invk c)) (uniq-at k z 0))
+          (exists ((x mesg) (z-0 strd))
+            (and (p "an" z-0 2) (p "an" "x" z-0 x) (p "an" "i" z-0 i)
+              (p "an" "k" z-0 k) (p "an" "a" z-0 a) (p "an" "b" z-0 b)
+              (p "an" "c" z-0 c) (prec z 0 z-0 0) (prec z-0 1 z 1)))))))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k))))
+  (label 0)
+  (unrealized (0 1))
+  (origs (k (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton main-ex-src
+  (vars (x mesg) (i ssn i-0 text) (k skey) (a b c c-0 akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (defstrand an 2 (x x) (i i-0) (k k) (a a) (b b) (c c-0))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (operation encryption-test (added-strand an 2) (enc "sorry" a b k)
+    (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    ((recv (cat i-0 a (enc (enc k b c-0 i-0 (invk a)) b) x))
+      (send (enc "sorry" a b k))))
+  (label 1)
+  (parent 0)
+  (unrealized (1 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton main-ex-src
+  (vars (i ssn text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (deflistener k)
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (operation encryption-test (added-listener k) (enc "sorry" a b k)
+    (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k))) ((recv k) (send k)))
+  (label 2)
+  (parent 0)
+  (unrealized (1 0))
+  (dead)
+  (comment "empty cohort"))
+
+(defskeleton main-ex-src
+  (vars (x mesg) (i ssn text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (defstrand an 2 (x x) (i i) (k k) (a a) (b b) (c c))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (operation encryption-test (displaced 2 0 qy 1)
+    (enc k b c-0 i-0 (invk a)) (1 0))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc "sorry" a b k))))
+  (label 3)
+  (parent 1)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (k k))))
+  (origs (k (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol main-ex-src basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc "sorry" a b k))))
+  (defrole ay
+    (vars (a b c akey) (i d text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc "data" d k)))
+    (uniq-orig d)))
+
+(defskeleton main-ex-src
+  (vars (i ssn d text) (k skey) (a b c akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k))))
+  (label 4)
+  (unrealized (0 1))
+  (origs (k (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton main-ex-src
+  (vars (x mesg) (i ssn d i-0 text) (k skey) (a b c a-0 b-0 c-0 akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (defstrand ay 2 (x x) (i i-0) (d d) (k k) (a a-0) (b b-0) (c c-0))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig d k)
+  (operation encryption-test (added-strand ay 2) (enc "data" d k) (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    ((recv (cat i-0 a-0 (enc (enc k b-0 c-0 i-0 (invk a-0)) b-0) x))
+      (send (enc "data" d k))))
+  (label 5)
+  (parent 4)
+  (unrealized (1 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton main-ex-src
+  (vars (i ssn d text) (k skey) (a b c akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (deflistener k)
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (operation encryption-test (added-listener k) (enc "data" d k) (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k))) ((recv k) (send k)))
+  (label 6)
+  (parent 4)
+  (unrealized (1 0))
+  (dead)
+  (comment "empty cohort"))
+
+(defskeleton main-ex-src
+  (vars (x mesg) (i ssn d text) (k skey) (a b c akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (defstrand ay 2 (x x) (i i) (d d) (k k) (a a) (b b) (c c))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig d k)
+  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (i-0 i)) k
+    (1 0) (enc (enc k b c i (invk a)) b))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc "data" d k))))
+  (label 7)
+  (parent 5)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (d d) (k k))))
+  (origs (d (1 1)) (k (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol main-ex-tgt basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i y n text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k)))
+    (uniq-orig y n))
+  (defrole ay
+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k)))
+    (uniq-orig y n d))
+  (defrole sn
+    (vars (a b c akey) (i ssn y n text))
+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send n)))
+  (defrole sy
+    (vars (a b c akey) (i ssn y n text))
+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send y))))
+
+(defskeleton main-ex-tgt
+  (vars (i ssn text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k))))
+  (label 8)
+  (unrealized (0 1))
+  (origs (k (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton main-ex-tgt
+  (vars (x mesg) (i ssn i-0 y n text) (k skey) (a b c c-0 akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (defstrand an 4 (x x) (i i-0) (y y) (n n) (k k) (a a) (b b) (c c-0))
+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig y n k)
+  (operation encryption-test (added-strand an 4) (enc "sorry" a b k)
+    (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    ((recv (cat i-0 a (enc (enc k b c-0 i-0 (invk a)) b) x))
+      (send (enc y n i-0 a x c-0)) (recv n) (send (enc "sorry" a b k))))
+  (label 9)
+  (parent 8)
+  (unrealized (1 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton main-ex-tgt
+  (vars (i ssn text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (deflistener k)
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (operation encryption-test (added-listener k) (enc "sorry" a b k)
+    (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k))) ((recv k) (send k)))
+  (label 10)
+  (parent 8)
+  (unrealized (1 0))
+  (dead)
+  (comment "empty cohort"))
+
+(defskeleton main-ex-tgt
+  (vars (x mesg) (i ssn y n text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (defstrand an 4 (x x) (i i) (y y) (n n) (k k) (a a) (b b) (c c))
+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig y n k)
+  (operation encryption-test (displaced 2 0 qy 1)
+    (enc k b c-0 i-0 (invk a)) (1 0))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k))))
+  (label 11)
+  (parent 9)
+  (unrealized (1 2))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton main-ex-tgt
+  (vars (i ssn y n ssn-0 text) (k skey) (a b c b-0 akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (defstrand an 4 (x (enc a b-0 i ssn-0 c)) (i i) (y y) (n n) (k k)
+    (a a) (b b) (c c))
+  (defstrand sn 2 (i i) (ssn ssn-0) (y y) (n n) (a a) (b b-0) (c c))
+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig y n k)
+  (operation nonce-test (added-strand sn 2) n (1 2)
+    (enc y n i a (enc a b-0 i ssn-0 c) c))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    ((recv
+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))
+      (send (enc y n i a (enc a b-0 i ssn-0 c) c)) (recv n)
+      (send (enc "sorry" a b k)))
+    ((recv (enc y n i a (enc a b-0 i ssn-0 c) c)) (send n)))
+  (label 12)
+  (parent 11)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (k k))))
+  (origs (k (0 0)) (y (1 1)) (n (1 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol main-ex-tgt basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i y n text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k)))
+    (uniq-orig y n))
+  (defrole ay
+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k)))
+    (uniq-orig y n d))
+  (defrole sn
+    (vars (a b c akey) (i ssn y n text))
+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send n)))
+  (defrole sy
+    (vars (a b c akey) (i ssn y n text))
+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send y))))
+
+(defskeleton main-ex-tgt
+  (vars (i ssn d text) (k skey) (a b c akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k))))
+  (label 13)
+  (unrealized (0 1))
+  (origs (k (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton main-ex-tgt
+  (vars (x mesg) (i ssn d i-0 y n text) (k skey)
+    (a b c a-0 b-0 c-0 akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (defstrand ay 4 (x x) (i i-0) (y y) (n n) (d d) (k k) (a a-0) (b b-0)
+    (c c-0))
+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig d y n k)
+  (operation encryption-test (added-strand ay 4) (enc "data" d k) (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    ((recv (cat i-0 a-0 (enc (enc k b-0 c-0 i-0 (invk a-0)) b-0) x))
+      (send (enc y n i-0 a-0 x c-0)) (recv y) (send (enc "data" d k))))
+  (label 14)
+  (parent 13)
+  (unrealized (1 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton main-ex-tgt
+  (vars (i ssn d text) (k skey) (a b c akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (deflistener k)
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (operation encryption-test (added-listener k) (enc "data" d k) (0 1))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k))) ((recv k) (send k)))
+  (label 15)
+  (parent 13)
+  (unrealized (1 0))
+  (dead)
+  (comment "empty cohort"))
+
+(defskeleton main-ex-tgt
+  (vars (x mesg) (i ssn d y n text) (k skey) (a b c akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (defstrand ay 4 (x x) (i i) (y y) (n n) (d d) (k k) (a a) (b b) (c c))
+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig d y n k)
+  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (i-0 i)) k
+    (1 0) (enc (enc k b c i (invk a)) b))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k))))
+  (label 16)
+  (parent 14)
+  (unrealized (1 2))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton main-ex-tgt
+  (vars (x mesg) (i ssn d n text) (k skey) (a b c akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (defstrand ay 4 (x x) (i i) (y n) (n n) (d d) (k k) (a a) (b b) (c c))
+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig d n k)
+  (operation nonce-test (displaced 2 1 ay 2) y (1 2) (enc y n i a x c))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc n n i a x c)) (recv n) (send (enc "data" d k))))
+  (label 17)
+  (parent 16)
+  (unrealized (1 2))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton main-ex-tgt
+  (vars (i ssn d y n ssn-0 text) (k skey) (a b c b-0 akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (defstrand ay 4 (x (enc a b-0 i ssn-0 c)) (i i) (y y) (n n) (d d)
+    (k k) (a a) (b b) (c c))
+  (defstrand sy 2 (i i) (ssn ssn-0) (y y) (n n) (a a) (b b-0) (c c))
+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig d y n k)
+  (operation nonce-test (added-strand sy 2) y (1 2)
+    (enc y n i a (enc a b-0 i ssn-0 c) c))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    ((recv
+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))
+      (send (enc y n i a (enc a b-0 i ssn-0 c) c)) (recv y)
+      (send (enc "data" d k)))
+    ((recv (enc y n i a (enc a b-0 i ssn-0 c) c)) (send y)))
+  (label 18)
+  (parent 16)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (d d) (k k))))
+  (origs (y (1 1)) (n (1 1)) (d (1 3)) (k (0 0))))
+
+(defskeleton main-ex-tgt
+  (vars (i ssn d n ssn-0 text) (k skey) (a b c b-0 akey))
+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))
+  (defstrand ay 4 (x (enc a b-0 i ssn-0 c)) (i i) (y n) (n n) (d d)
+    (k k) (a a) (b b) (c c))
+  (defstrand sy 2 (i i) (ssn ssn-0) (y n) (n n) (a a) (b b-0) (c c))
+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig d n k)
+  (operation nonce-test (added-strand sy 2) n (1 2)
+    (enc n n i a (enc a b-0 i ssn-0 c) c))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    ((recv
+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))
+      (send (enc n n i a (enc a b-0 i ssn-0 c) c)) (recv n)
+      (send (enc "data" d k)))
+    ((recv (enc n n i a (enc a b-0 i ssn-0 c) c)) (send n)))
+  (label 19)
+  (parent 17)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (d d) (k k))))
+  (origs (n (1 1)) (d (1 3)) (k (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol main-ex-tgt-rule basic
+  (defrole qn
+    (vars (a b c akey) (i ssn text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    (uniq-orig k))
+  (defrole qy
+    (vars (a b c akey) (i ssn d text) (k skey))
+    (trace
+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "data" d k)))
+    (uniq-orig k))
+  (defrole an
+    (vars (a b c akey) (i y n text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k)))
+    (uniq-orig y n))
+  (defrole ay
+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))
+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k)))
+    (uniq-orig y n d))
+  (defrole sn
+    (vars (a b c akey) (i ssn y n text))
+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send n)))
+  (defrole sy
+    (vars (a b c akey) (i ssn y n text))
+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send y)))
+  (defrule src
+    (forall ((z strd) (i ssn text) (k skey) (a b c akey))
+      (implies
+        (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)
+          (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)
+          (p "qn" "c" z c) (non (invk a)) (non (invk b)) (non (invk c))
+          (uniq k))
+        (exists ((z-0 strd) (x mesg))
+          (and (p "an" z-0 4) (p "an" "x" z-0 x) (p "an" "i" z-0 i)
+            (p "an" "k" z-0 k) (p "an" "a" z-0 a) (p "an" "b" z-0 b)
+            (p "an" "c" z-0 c) (prec z 0 z-0 0) (prec z-0 3 z 1)))))))
+
+(defskeleton main-ex-tgt-rule
+  (vars (i ssn text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig k)
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k))))
+  (label 20)
+  (unrealized (0 1))
+  (origs (k (0 0)))
+  (comment "Not closed under rules"))
+
+(defskeleton main-ex-tgt-rule
+  (vars (x mesg) (ssn i y n text) (k skey) (a b c akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (defstrand an 4 (x x) (i i) (y y) (n n) (k k) (a a) (b b) (c c))
+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig y n k)
+  (rule src)
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))
+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k))))
+  (label 21)
+  (parent 20)
+  (unrealized (1 2))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton main-ex-tgt-rule
+  (vars (ssn i y n ssn-0 text) (k skey) (a b c b-0 akey))
+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))
+  (defstrand an 4 (x (enc a b-0 i ssn-0 c)) (i i) (y y) (n n) (k k)
+    (a a) (b b) (c c))
+  (defstrand sn 2 (i i) (ssn ssn-0) (y y) (n n) (a a) (b b-0) (c c))
+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))
+  (non-orig (invk a) (invk b) (invk c))
+  (uniq-orig y n k)
+  (operation nonce-test (added-strand sn 2) n (1 2)
+    (enc y n i a (enc a b-0 i ssn-0 c) c))
+  (traces
+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))
+      (recv (enc "sorry" a b k)))
+    ((recv
+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))
+      (send (enc y n i a (enc a b-0 i ssn-0 c) c)) (recv n)
+      (send (enc "sorry" a b k)))
+    ((recv (enc y n i a (enc a b-0 i ssn-0 c) c)) (send n)))
+  (label 22)
+  (parent 21)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (k k))))
+  (origs (y (1 1)) (n (1 1)) (k (0 0))))
+
+(comment "Nothing left to do")
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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from dh-ca.scm")
 
 (defprotocol dhca diffie-hellman
diff --git a/tst/dh_mim.scm b/tst/dh_mim.scm
--- a/tst/dh_mim.scm
+++ b/tst/dh_mim.scm
@@ -2,9 +2,9 @@
 
 ; In this example, the initiator and responder roles participate in a
 ; Diffie-Hellman exchange, and then a nonce is transmitted by the
-; initiator and received by the responder.  
+; initiator and received by the responder.
 
-; A man-in-the-middle attack is possible, because there is no 
+; A man-in-the-middle attack is possible, because there is no
 ; attempt made to authenticate either of the parties.  Therefore, the
 ; adversary may emulate the responder to the initator and vice versa.
 
@@ -28,7 +28,6 @@
     (uniq-gen y))
   (comment "Diffie-hellman key exchange followed by an encryption"))
 
-
 (defskeleton dh_mim
   (vars (n text) (x0 y0 expt) (x y rndx))
   (defstrand init 3 (n n) (y y0) (x x))
@@ -37,4 +36,3 @@
   (uniq-orig n)
   (pen-non-orig x y)
   (comment "Agreement on the encrypted text only"))
-
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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from dh_mim.scm")
 
 (defprotocol dh_mim diffie-hellman
diff --git a/tst/dh_mim2.scm b/tst/dh_mim2.scm
--- a/tst/dh_mim2.scm
+++ b/tst/dh_mim2.scm
@@ -32,4 +32,3 @@
   (pen-non-orig x y)
   (comment "Agreement on the encrypted text only"))
 ;)
-
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from dh_test.scm")
 (comment "Strand count bounded at 20")
 
diff --git a/tst/dhnsl_basic.scm b/tst/dhnsl_basic.scm
--- a/tst/dhnsl_basic.scm
+++ b/tst/dhnsl_basic.scm
@@ -9,7 +9,7 @@
      (recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
-     
+
      )
     (absent (y (exp (gen) x)))
 ;    (uniq-gen y)
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from ffgg.scm")
 
 (defprotocol ffgg basic
diff --git a/tst/fluffy_draft03_gske.scm b/tst/fluffy_draft03_gske.scm
new file mode 100644
--- /dev/null
+++ b/tst/fluffy_draft03_gske.scm
@@ -0,0 +1,114 @@
+(herald "GSKE, part of Fluffy: Simplified Key Exchange for Constrained Environments draft-hardjono-ace-fluffy-03"
+ (comment "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt"))
+
+;; This model does not include timestamps or optional fields.
+(defprotocol fluffy basic
+ (defrole sp
+  (vars (b s name) (nb g text) (gk skey))
+  (trace
+   (send (cat "req" s g (enc b nb (ltk s b))))
+   (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+ (defrole keyserv
+  (vars (a b s name) (nb na g text) (gk skey))
+  (trace
+   (recv (cat "req" s g (enc b nb (ltk s b))))
+   (send (cat "resp" b (enc s g nb gk (ltk s b))))
+   (recv (cat "fetch" s g (enc a na (ltk s a))))
+   (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+  (uniq-gen gk))
+ (defrole client
+  (vars (a b s name) (na g text) (gk skey))
+  (trace
+   (send (cat "fetch" s g (enc a na (ltk s a))))
+   (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))
+
+;; Service principal's (sp) point-of-view
+(defskeleton fluffy
+ (vars (b s name) (nb text) (gk skey))
+ (defstrand sp 2 (b b) (s s) (nb nb) (gk gk))
+ (non-orig (ltk s b))
+ (uniq-orig nb)
+ (comment "Service Principal's point-of-view"))
+
+;; Simple key distribution center's (skdc) point-of-view
+(defskeleton fluffy
+ (vars (a b s name) (nb na text) (gk skey))
+ (defstrand keyserv 4 (a a) (b b) (s s) (nb nb) (na na) (gk gk))
+ (non-orig (ltk s b) (ltk s a))
+ (uniq-gen gk)
+ (comment "SKDC's point-of-view"))
+
+;; Client's point-of-view
+(defskeleton fluffy
+ (vars (a s name) (na text) (gk skey))
+ (defstrand client 2 (a a) (s s) (na na) (gk gk))
+ (non-orig (ltk s a))
+ (uniq-orig na)
+ (comment "Clients's point-of-view"))
+
+(defprotocol fluffy-rule basic
+  (defrole sp
+    (vars (b s name) (nb g text) (gk skey))
+    (trace
+     (send (cat "req" s g (enc b nb (ltk s b))))
+     (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (defrole keyserv
+    (vars (a b s name) (nb na g text) (gk skey))
+    (trace
+     (recv (cat "req" s g (enc b nb (ltk s b))))
+     (send (cat "resp" b (enc s g nb gk (ltk s b))))
+     (recv (cat "fetch" s g (enc a na (ltk s a))))
+     (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    (uniq-gen gk))
+  (defrole client
+    (vars (a b s name) (na g text) (gk skey))
+    (trace
+     (send (cat "fetch" s g (enc a na (ltk s a))))
+     (recv (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (defrule client-no-request
+    (forall ((a s name) (y z strd))
+	    (implies
+	     (and
+	      (p "client" z 1)
+	      (p "client" "s" z s)
+	      (p "client" "a" z a)
+	      (p "keyserv" y 1)
+	      (p "keyserv" "s" y s)
+	      (p "keyserv" "b" y a))
+	     (false))))
+  (defrule sp-no-fetch
+    (forall ((b s name) (y z strd))
+	    (implies
+	     (and
+	      (p "sp" z 1)
+	      (p "sp" "s" z s)
+	      (p "sp" "b" z b)
+	      (p "keyserv" y 3)
+	      (p "keyserv" "s" y s)
+	      (p "keyserv" "a" y b))
+	     (false))))
+  )
+
+;; Service principal's (sp) point-of-view
+(defskeleton fluffy-rule
+ (vars (b s name) (nb text) (gk skey))
+ (defstrand sp 2 (b b) (s s) (nb nb) (gk gk))
+ (non-orig (ltk s b))
+ (uniq-orig nb)
+ (comment "Service Principal's point-of-view"))
+
+;; Simple key distribution center's (skdc) point-of-view
+(defskeleton fluffy-rule
+ (vars (a b s name) (nb na text) (gk skey))
+ (defstrand keyserv 4 (a a) (b b) (s s) (nb nb) (na na) (gk gk))
+ (non-orig (ltk s b) (ltk s a))
+ (uniq-gen gk)
+ (comment "SKDC's point-of-view"))
+
+;; Client's point-of-view
+(defskeleton fluffy-rule
+ (vars (a s name) (na text) (gk skey))
+ (defstrand client 2 (a a) (s s) (na na) (gk gk))
+ (non-orig (ltk s a))
+ (uniq-orig na)
+ (comment "Clients's point-of-view"))
diff --git a/tst/fluffy_draft03_gske.tst b/tst/fluffy_draft03_gske.tst
new file mode 100644
--- /dev/null
+++ b/tst/fluffy_draft03_gske.tst
@@ -0,0 +1,608 @@
+(herald
+  "GSKE, part of Fluffy: Simplified Key Exchange for Constrained Environments draft-hardjono-ace-fluffy-03"
+  (comment
+    "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt"))
+
+(comment "CPSA 3.6.4")
+(comment "All input read from fluffy_draft03_gske.scm")
+
+(defprotocol fluffy basic
+  (defrole sp
+    (vars (b s name) (nb g text) (gk skey))
+    (trace (send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (defrole keyserv
+    (vars (a b s name) (nb na g text) (gk skey))
+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    (uniq-gen gk))
+  (defrole client
+    (vars (a s name) (na g text) (gk skey))
+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))
+
+(defskeleton fluffy
+  (vars (nb g text) (b s name) (gk skey))
+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))
+  (non-orig (ltk s b))
+  (uniq-orig nb)
+  (comment "Service Principal's point-of-view")
+  (traces
+    ((send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (label 0)
+  (unrealized (0 1))
+  (origs (nb (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton fluffy
+  (vars (nb g nb-0 text) (b s b-0 name) (gk skey))
+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))
+  (defstrand keyserv 4 (nb nb-0) (na nb) (g g) (a b) (b b-0) (s s)
+    (gk gk))
+  (precedes ((0 0) (1 2)) ((1 3) (0 1)))
+  (non-orig (ltk s b))
+  (uniq-gen gk)
+  (uniq-orig nb)
+  (operation encryption-test (added-strand keyserv 4)
+    (enc s g nb gk (ltk s b)) (0 1))
+  (traces
+    ((send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b)))))
+    ((recv (cat "req" s g (enc b-0 nb-0 (ltk s b-0))))
+      (send (cat "resp" b-0 (enc s g nb-0 gk (ltk s b-0))))
+      (recv (cat "fetch" s g (enc b nb (ltk s b))))
+      (send (cat "deliver" b (enc s g nb gk (ltk s b))))))
+  (label 1)
+  (parent 0)
+  (unrealized)
+  (shape)
+  (maps ((0) ((b b) (s s) (nb nb) (gk gk) (g g))))
+  (origs (nb (0 0))))
+
+(defskeleton fluffy
+  (vars (nb g text) (b s name) (gk skey))
+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))
+  (defstrand keyserv 2 (nb nb) (g g) (b b) (s s) (gk gk))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (ltk s b))
+  (uniq-gen gk)
+  (uniq-orig nb)
+  (operation encryption-test (added-strand keyserv 2)
+    (enc s g nb gk (ltk s b)) (0 1))
+  (traces
+    ((send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b)))))
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (label 2)
+  (parent 0)
+  (unrealized)
+  (shape)
+  (maps ((0) ((b b) (s s) (nb nb) (gk gk) (g g))))
+  (origs (nb (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol fluffy basic
+  (defrole sp
+    (vars (b s name) (nb g text) (gk skey))
+    (trace (send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (defrole keyserv
+    (vars (a b s name) (nb na g text) (gk skey))
+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    (uniq-gen gk))
+  (defrole client
+    (vars (a s name) (na g text) (gk skey))
+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))
+
+(defskeleton fluffy
+  (vars (nb na g text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (comment "SKDC's point-of-view")
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (label 3)
+  (unrealized (0 0) (0 2))
+  (origs)
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton fluffy
+  (vars (nb na g g-0 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))
+  (precedes ((1 0) (0 0)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand sp 1) (enc b nb (ltk s b))
+    (0 0))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "req" s g-0 (enc b nb (ltk s b))))))
+  (label 4)
+  (parent 3)
+  (unrealized (0 2))
+  (comment "3 in cohort - 3 not yet seen"))
+
+(defskeleton fluffy
+  (vars (nb na g g-0 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))
+  (precedes ((1 0) (0 0)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand client 1)
+    (enc b nb (ltk s b)) (0 0))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b))))))
+  (label 5)
+  (parent 3)
+  (unrealized (0 2))
+  (comment "3 in cohort - 3 not yet seen"))
+
+(defskeleton fluffy
+  (vars (nb g g-0 text) (b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na nb) (g g) (a b) (b b) (s s) (gk gk))
+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))
+  (precedes ((1 0) (0 0)))
+  (non-orig (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (displaced 2 1 sp 1) (enc a na (ltk s a))
+    (0 2))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc b nb (ltk s b))))
+      (send (cat "deliver" b (enc s g nb gk (ltk s b)))))
+    ((send (cat "req" s g-0 (enc b nb (ltk s b))))))
+  (label 6)
+  (parent 4)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a b) (b b) (s s) (nb nb) (na nb) (gk gk) (g g))))
+  (origs))
+
+(defskeleton fluffy
+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))
+  (defstrand sp 1 (nb na) (g g-1) (b a) (s s))
+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand sp 1) (enc a na (ltk s a))
+    (0 2))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "req" s g-0 (enc b nb (ltk s b)))))
+    ((send (cat "req" s g-1 (enc a na (ltk s a))))))
+  (label 7)
+  (parent 4)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))
+  (origs))
+
+(defskeleton fluffy
+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))
+  (defstrand client 1 (na na) (g g-1) (a a) (s s))
+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand client 1)
+    (enc a na (ltk s a)) (0 2))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "req" s g-0 (enc b nb (ltk s b)))))
+    ((send (cat "fetch" s g-1 (enc a na (ltk s a))))))
+  (label 8)
+  (parent 4)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))
+  (origs))
+
+(defskeleton fluffy
+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))
+  (defstrand sp 1 (nb na) (g g-1) (b a) (s s))
+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand sp 1) (enc a na (ltk s a))
+    (0 2))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b)))))
+    ((send (cat "req" s g-1 (enc a na (ltk s a))))))
+  (label 9)
+  (parent 5)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))
+  (origs))
+
+(defskeleton fluffy
+  (vars (nb g g-0 text) (b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na nb) (g g) (a b) (b b) (s s) (gk gk))
+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))
+  (precedes ((1 0) (0 0)))
+  (non-orig (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (displaced 2 1 client 1)
+    (enc a na (ltk s a)) (0 2))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc b nb (ltk s b))))
+      (send (cat "deliver" b (enc s g nb gk (ltk s b)))))
+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b))))))
+  (label 10)
+  (parent 5)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a b) (b b) (s s) (nb nb) (na nb) (gk gk) (g g))))
+  (origs))
+
+(defskeleton fluffy
+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))
+  (defstrand client 1 (na na) (g g-1) (a a) (s s))
+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand client 1)
+    (enc a na (ltk s a)) (0 2))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b)))))
+    ((send (cat "fetch" s g-1 (enc a na (ltk s a))))))
+  (label 11)
+  (parent 5)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))
+  (origs))
+
+(comment "Nothing left to do")
+
+(defprotocol fluffy basic
+  (defrole sp
+    (vars (b s name) (nb g text) (gk skey))
+    (trace (send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (defrole keyserv
+    (vars (a b s name) (nb na g text) (gk skey))
+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    (uniq-gen gk))
+  (defrole client
+    (vars (a s name) (na g text) (gk skey))
+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))
+
+(defskeleton fluffy
+  (vars (na g text) (a s name) (gk skey))
+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))
+  (non-orig (ltk s a))
+  (uniq-orig na)
+  (comment "Clients's point-of-view")
+  (traces
+    ((send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (label 12)
+  (unrealized (0 1))
+  (origs (na (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton fluffy
+  (vars (na g nb text) (a s b name) (gk skey))
+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (precedes ((0 0) (1 2)) ((1 3) (0 1)))
+  (non-orig (ltk s a))
+  (uniq-gen gk)
+  (uniq-orig na)
+  (operation encryption-test (added-strand keyserv 4)
+    (enc s g na gk (ltk s a)) (0 1))
+  (traces
+    ((send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (label 13)
+  (parent 12)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (s s) (na na) (gk gk) (g g))))
+  (origs (na (0 0))))
+
+(defskeleton fluffy
+  (vars (na g text) (a s name) (gk skey))
+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))
+  (defstrand keyserv 2 (nb na) (g g) (b a) (s s) (gk gk))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (ltk s a))
+  (uniq-gen gk)
+  (uniq-orig na)
+  (operation encryption-test (added-strand keyserv 2)
+    (enc s g na gk (ltk s a)) (0 1))
+  (traces
+    ((send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((recv (cat "req" s g (enc a na (ltk s a))))
+      (send (cat "resp" a (enc s g na gk (ltk s a))))))
+  (label 14)
+  (parent 12)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (s s) (na na) (gk gk) (g g))))
+  (origs (na (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol fluffy-rule basic
+  (defrole sp
+    (vars (b s name) (nb g text) (gk skey))
+    (trace (send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (defrole keyserv
+    (vars (a b s name) (nb na g text) (gk skey))
+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    (uniq-gen gk))
+  (defrole client
+    (vars (a s name) (na g text) (gk skey))
+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (defrule client-no-request
+    (forall ((a s name) (y z strd))
+      (implies
+        (and (p "client" z 1) (p "client" "s" z s) (p "client" "a" z a)
+          (p "keyserv" y 1) (p "keyserv" "s" y s) (p "keyserv" "b" y a))
+        (false))))
+  (defrule sp-no-fetch
+    (forall ((b s name) (y z strd))
+      (implies
+        (and (p "sp" z 1) (p "sp" "s" z s) (p "sp" "b" z b)
+          (p "keyserv" y 3) (p "keyserv" "s" y s) (p "keyserv" "a" y b))
+        (false)))))
+
+(defskeleton fluffy-rule
+  (vars (nb g text) (b s name) (gk skey))
+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))
+  (non-orig (ltk s b))
+  (uniq-orig nb)
+  (comment "Service Principal's point-of-view")
+  (traces
+    ((send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (label 15)
+  (unrealized (0 1))
+  (origs (nb (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton fluffy-rule
+  (vars (nb g text) (b s name) (gk skey))
+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))
+  (defstrand keyserv 2 (nb nb) (g g) (b b) (s s) (gk gk))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (ltk s b))
+  (uniq-gen gk)
+  (uniq-orig nb)
+  (operation encryption-test (added-strand keyserv 2)
+    (enc s g nb gk (ltk s b)) (0 1))
+  (traces
+    ((send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b)))))
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (label 16)
+  (parent 15)
+  (unrealized)
+  (shape)
+  (maps ((0) ((b b) (s s) (nb nb) (gk gk) (g g))))
+  (origs (nb (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol fluffy-rule basic
+  (defrole sp
+    (vars (b s name) (nb g text) (gk skey))
+    (trace (send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (defrole keyserv
+    (vars (a b s name) (nb na g text) (gk skey))
+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    (uniq-gen gk))
+  (defrole client
+    (vars (a s name) (na g text) (gk skey))
+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (defrule client-no-request
+    (forall ((a s name) (y z strd))
+      (implies
+        (and (p "client" z 1) (p "client" "s" z s) (p "client" "a" z a)
+          (p "keyserv" y 1) (p "keyserv" "s" y s) (p "keyserv" "b" y a))
+        (false))))
+  (defrule sp-no-fetch
+    (forall ((b s name) (y z strd))
+      (implies
+        (and (p "sp" z 1) (p "sp" "s" z s) (p "sp" "b" z b)
+          (p "keyserv" y 3) (p "keyserv" "s" y s) (p "keyserv" "a" y b))
+        (false)))))
+
+(defskeleton fluffy-rule
+  (vars (nb na g text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (comment "SKDC's point-of-view")
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (label 17)
+  (unrealized (0 0) (0 2))
+  (origs)
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton fluffy-rule
+  (vars (nb na g g-0 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))
+  (precedes ((1 0) (0 0)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand sp 1) (enc b nb (ltk s b))
+    (0 0))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "req" s g-0 (enc b nb (ltk s b))))))
+  (label 18)
+  (parent 17)
+  (unrealized (0 2))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton fluffy-rule
+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))
+  (defstrand client 1 (na na) (g g-1) (a a) (s s))
+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))
+  (non-orig (ltk s a) (ltk s b))
+  (uniq-gen gk)
+  (operation encryption-test (added-strand client 1)
+    (enc a na (ltk s a)) (0 2))
+  (traces
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((send (cat "req" s g-0 (enc b nb (ltk s b)))))
+    ((send (cat "fetch" s g-1 (enc a na (ltk s a))))))
+  (label 19)
+  (parent 18)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))
+  (origs))
+
+(comment "Nothing left to do")
+
+(defprotocol fluffy-rule basic
+  (defrole sp
+    (vars (b s name) (nb g text) (gk skey))
+    (trace (send (cat "req" s g (enc b nb (ltk s b))))
+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))
+  (defrole keyserv
+    (vars (a b s name) (nb na g text) (gk skey))
+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))
+    (uniq-gen gk))
+  (defrole client
+    (vars (a s name) (na g text) (gk skey))
+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (defrule client-no-request
+    (forall ((a s name) (y z strd))
+      (implies
+        (and (p "client" z 1) (p "client" "s" z s) (p "client" "a" z a)
+          (p "keyserv" y 1) (p "keyserv" "s" y s) (p "keyserv" "b" y a))
+        (false))))
+  (defrule sp-no-fetch
+    (forall ((b s name) (y z strd))
+      (implies
+        (and (p "sp" z 1) (p "sp" "s" z s) (p "sp" "b" z b)
+          (p "keyserv" y 3) (p "keyserv" "s" y s) (p "keyserv" "a" y b))
+        (false)))))
+
+(defskeleton fluffy-rule
+  (vars (na g text) (a s name) (gk skey))
+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))
+  (non-orig (ltk s a))
+  (uniq-orig na)
+  (comment "Clients's point-of-view")
+  (traces
+    ((send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (label 20)
+  (unrealized (0 1))
+  (origs (na (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton fluffy-rule
+  (vars (na g nb text) (a s b name) (gk skey))
+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))
+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))
+  (precedes ((0 0) (1 2)) ((1 3) (0 1)))
+  (non-orig (ltk s a))
+  (uniq-gen gk)
+  (uniq-orig na)
+  (operation encryption-test (added-strand keyserv 4)
+    (enc s g na gk (ltk s a)) (0 1))
+  (traces
+    ((send (cat "fetch" s g (enc a na (ltk s a))))
+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))
+    ((recv (cat "req" s g (enc b nb (ltk s b))))
+      (send (cat "resp" b (enc s g nb gk (ltk s b))))
+      (recv (cat "fetch" s g (enc a na (ltk s a))))
+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))
+  (label 21)
+  (parent 20)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (s s) (na na) (gk gk) (g g))))
+  (origs (na (0 0))))
+
+(comment "Nothing left to do")
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from goals.scm")
 
 (defprotocol ns basic
diff --git a/tst/iadh_um.scm b/tst/iadh_um.scm
--- a/tst/iadh_um.scm
+++ b/tst/iadh_um.scm
@@ -47,7 +47,6 @@
     (fn-of ("principal-of" (l self))))
   )
 
-
 ;; Implicit authentication: participants will agree on the resulting key
 ;; foo(key).  Therefore they should agree on the names A and B.
  (defskeleton iadh-um
@@ -60,7 +59,7 @@
   (comment "Implicit authentication")
 )
 
- ;; Security: 
+ ;; Security:
 (defskeleton iadh-um
   (vars (e1 e2 l rndx) (lp expt) (A B name))
   (defstrand participant 5 (e e1) (l l) (ep e2) (lp lp) (self A) (peer B))
@@ -68,6 +67,3 @@
   (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul e1 e2))))
   (non-orig (privk A) (privk B))
 )
-
-
- 
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from or.scm")
 
 (defprotocol or basic
diff --git a/tst/ordered.scm b/tst/ordered.scm
new file mode 100644
--- /dev/null
+++ b/tst/ordered.scm
@@ -0,0 +1,26 @@
+(herald ordered)
+
+(defprotocol ordered basic
+
+  (defrole dec
+    (vars (t text) (k akey))
+    (trace (recv (enc t k)) (send t)))
+
+  (defrule neq
+    (forall ((x mesg))
+	    (implies (fact neq x x) (false))))
+
+  (defrule order
+    (forall ((y z strd))
+	    (implies
+	     (and (p "dec" y 2)
+		  (p "dec" z 2))
+	     (or (prec y 1 z 0)
+		 (prec z 1 y 0)
+		 (= y z))))))
+
+(defskeleton ordered
+  (vars (a b text))
+  (defstrand dec 2 (t a))
+  (defstrand dec 2 (t b))
+  (facts (neq a b)))
diff --git a/tst/ordered.tst b/tst/ordered.tst
new file mode 100644
--- /dev/null
+++ b/tst/ordered.tst
@@ -0,0 +1,58 @@
+(herald ordered)
+
+(comment "CPSA 3.6.4")
+(comment "All input read from ordered.scm")
+
+(defprotocol ordered basic
+  (defrole dec
+    (vars (t text) (k akey))
+    (trace (recv (enc t k)) (send t)))
+  (defrule neq (forall ((x mesg)) (implies (fact neq x x) (false))))
+  (defrule order
+    (forall ((y z strd))
+      (implies
+        (and (p "dec" y 2) (p "dec" z 2))
+        (or (prec y 1 z 0) (prec z 1 y 0) (= y z))))))
+
+(defskeleton ordered
+  (vars (a b text) (k k-0 akey))
+  (defstrand dec 2 (t a) (k k))
+  (defstrand dec 2 (t b) (k k-0))
+  (facts (neq a b))
+  (traces ((recv (enc a k)) (send a)) ((recv (enc b k-0)) (send b)))
+  (label 0)
+  (unrealized)
+  (origs)
+  (comment "Not closed under rules"))
+
+(defskeleton ordered
+  (vars (a b text) (k k-0 akey))
+  (defstrand dec 2 (t a) (k k))
+  (defstrand dec 2 (t b) (k k-0))
+  (precedes ((0 1) (1 0)))
+  (facts (neq a b))
+  (rule order)
+  (traces ((recv (enc a k)) (send a)) ((recv (enc b k-0)) (send b)))
+  (label 1)
+  (parent 0)
+  (unrealized)
+  (shape)
+  (maps ((0 1) ((a a) (b b) (k k) (k-0 k-0))))
+  (origs))
+
+(defskeleton ordered
+  (vars (a b text) (k k-0 akey))
+  (defstrand dec 2 (t a) (k k))
+  (defstrand dec 2 (t b) (k k-0))
+  (precedes ((1 1) (0 0)))
+  (facts (neq a b))
+  (rule order)
+  (traces ((recv (enc a k)) (send a)) ((recv (enc b k-0)) (send b)))
+  (label 2)
+  (parent 0)
+  (unrealized)
+  (shape)
+  (maps ((0 1) ((a a) (b b) (k k) (k-0 k-0))))
+  (origs))
+
+(comment "Nothing left to do")
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from priority_test.scm")
 
 (defprotocol priority_test basic
diff --git a/tst/prottrans.scm b/tst/prottrans.scm
new file mode 100644
--- /dev/null
+++ b/tst/prottrans.scm
@@ -0,0 +1,107 @@
+(herald "Protocol Transformations With Rules")
+
+;; Basic Needham-Schroeder using asymmetric keys
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b akey) (na nb text))
+    (trace
+     (send (enc na a b))
+     (recv (enc na nb a))
+     (send (enc nb b))))
+  (defrole resp
+    (vars (b a akey) (nb na text))
+    (trace
+     (recv (enc na a b))
+     (send (enc na nb a))
+     (recv (enc nb b))))
+  (comment "Needham-Schroeder without rules"))
+
+;;; The initiator point-of-view
+(defskeleton ns
+  (vars (a b akey) (na text))
+  (defstrand init 3 (a a) (b b) (na na))
+  (non-orig (invk a) (invk b))
+  (uniq-orig na)
+  (comment "Initiator point-of-view"))
+
+;;; The responder point-of-view
+(defskeleton ns
+  (vars (a akey) (nb text))
+  (defstrand resp 3 (a a) (nb nb))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (comment "Responder point-of-view"))
+
+;;; Unilateral protocol
+(defprotocol unilateral basic
+  (defrole init
+     (vars (n text) (k akey))
+     (trace
+      (send (enc n k))
+      (recv n)))
+  (defrole resp
+     (vars (n text) (k akey))
+     (trace
+      (recv (enc n k))
+      (send n))))
+
+(defskeleton unilateral
+  (vars (k akey) (n text))
+  (defstrand init 2 (n n) (k k))
+  (non-orig (invk k))
+  (uniq-orig n)
+  (comment "The shape analysis sentence for this problem:"
+    (defgoal unilateral
+      (forall ((n text) (k akey) (z strd))
+        (implies
+          (and (p "init" z 2) (p "init" "n" z n) (p "init" "k" z k)
+            (non (invk k)) (uniq-at n z 0))
+          (exists ((z-0 strd))
+            (and (p "resp" z-0 2) (p "resp" "n" z-0 n)
+              (p "resp" "k" z-0 k) (prec z 0 z-0 0)
+              (prec z-0 1 z 1))))))))
+
+(defprotocol ns-with-rule basic
+  (defrole init
+    (vars (a b akey) (na nb text))
+    (trace
+     (send (enc na a b))
+     (recv (enc na nb a))
+     (send (enc nb b))))
+  (defrole resp
+    (vars (b a akey) (nb na text))
+    (trace
+     (recv (enc na a b))
+     (send (enc na nb a))
+     (recv (enc nb b))))
+  (defrule unilateral
+    (forall ((r strd) (a akey) (nb text))
+	    (implies
+	     (and (p "resp" r 3)
+		  (p "resp" "a" r a)
+		  (p "resp" "nb" r nb)
+		  (non (invk a))
+		  (uniq nb))
+	     (exists ((i strd))
+		     (and (p "init" i 3)
+			  (p "init" "a" i a)
+			  (p "init" "nb" i nb)
+			  (prec r 1 i 1)
+			  (prec i 2 r 2)))))
+    (comment "Unilateral sas under the predicate mapping:")
+    (comment (p "init" 2) "->" (p "resp" 3) "and")
+    (comment (p "init" "n") "->" (p "resp" "nb") "and")
+    (comment (p "init" "k") "->" (p "resp" "a") "and")
+    (comment (p "resp" 2) "->" (p "init" 3) "and")
+    (comment (p "resp" "n") "->" (p "init" "nb"))
+    (comment (p "resp" "k") "->" (p "init" "a")))
+  (comment "Needham-Schroeder with rule"))
+
+;;; The responder point-of-view
+(defskeleton ns-with-rule
+  (vars (a akey) (nb text))
+  (defstrand resp 3 (a a) (nb nb))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (comment "Responder point-of-view"))
diff --git a/tst/prottrans.tst b/tst/prottrans.tst
new file mode 100644
--- /dev/null
+++ b/tst/prottrans.tst
@@ -0,0 +1,236 @@
+(herald "Protocol Transformations With Rules")
+
+(comment "CPSA 3.6.4")
+(comment "All input read from prottrans.scm")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b akey) (na nb text))
+    (trace (send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))
+  (defrole resp
+    (vars (b a akey) (nb na text))
+    (trace (recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))
+  (comment "Needham-Schroeder without rules"))
+
+(defskeleton ns
+  (vars (na nb text) (a b akey))
+  (defstrand init 3 (na na) (nb nb) (a a) (b b))
+  (non-orig (invk a) (invk b))
+  (uniq-orig na)
+  (comment "Initiator point-of-view")
+  (traces ((send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))
+  (label 0)
+  (unrealized (0 1))
+  (origs (na (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (na nb nb-0 text) (a b akey))
+  (defstrand init 3 (na na) (nb nb) (a a) (b b))
+  (defstrand resp 2 (nb nb-0) (na na) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b))
+  (uniq-orig na)
+  (operation nonce-test (added-strand resp 2) na (0 1) (enc na a b))
+  (traces ((send (enc na a b)) (recv (enc na nb a)) (send (enc nb b)))
+    ((recv (enc na a b)) (send (enc na nb-0 a))))
+  (label 1)
+  (parent 0)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (na nb text) (a b akey))
+  (defstrand init 3 (na na) (nb nb) (a a) (b b))
+  (defstrand resp 2 (nb nb) (na na) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk a) (invk b))
+  (uniq-orig na)
+  (operation nonce-test (contracted (nb-0 nb)) na (0 1) (enc na nb a)
+    (enc na a b))
+  (traces ((send (enc na a b)) (recv (enc na nb a)) (send (enc nb b)))
+    ((recv (enc na a b)) (send (enc na nb a))))
+  (label 2)
+  (parent 1)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (na na) (nb nb))))
+  (origs (na (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b akey) (na nb text))
+    (trace (send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))
+  (defrole resp
+    (vars (b a akey) (nb na text))
+    (trace (recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))
+  (comment "Needham-Schroeder without rules"))
+
+(defskeleton ns
+  (vars (nb na text) (a b akey))
+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (comment "Responder point-of-view")
+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))
+  (label 3)
+  (unrealized (0 2))
+  (origs (nb (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (nb na text) (a b b-0 akey))
+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))
+  (defstrand init 3 (na na) (nb nb) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (operation nonce-test (added-strand init 3) nb (0 2) (enc na nb a))
+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))
+    ((send (enc na a b-0)) (recv (enc na nb a)) (send (enc nb b-0))))
+  (label 4)
+  (parent 3)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (nb nb) (b b) (na na))))
+  (origs (nb (0 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol unilateral basic
+  (defrole init
+    (vars (n text) (k akey))
+    (trace (send (enc n k)) (recv n)))
+  (defrole resp
+    (vars (n text) (k akey))
+    (trace (recv (enc n k)) (send n))))
+
+(defskeleton unilateral
+  (vars (n text) (k akey))
+  (defstrand init 2 (n n) (k k))
+  (non-orig (invk k))
+  (uniq-orig n)
+  (comment "The shape analysis sentence for this problem:"
+    (defgoal unilateral
+      (forall ((n text) (k akey) (z strd))
+        (implies
+          (and (p "init" z 2) (p "init" "n" z n) (p "init" "k" z k)
+            (non (invk k)) (uniq-at n z 0))
+          (exists ((z-0 strd))
+            (and (p "resp" z-0 2) (p "resp" "n" z-0 n)
+              (p "resp" "k" z-0 k) (prec z 0 z-0 0)
+              (prec z-0 1 z 1)))))))
+  (traces ((send (enc n k)) (recv n)))
+  (label 5)
+  (unrealized (0 1))
+  (origs (n (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton unilateral
+  (vars (n text) (k akey))
+  (defstrand init 2 (n n) (k k))
+  (defstrand resp 2 (n n) (k k))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk k))
+  (uniq-orig n)
+  (operation nonce-test (added-strand resp 2) n (0 1) (enc n k))
+  (traces ((send (enc n k)) (recv n)) ((recv (enc n k)) (send n)))
+  (label 6)
+  (parent 5)
+  (unrealized)
+  (shape)
+  (maps ((0) ((k k) (n n))))
+  (origs (n (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns-with-rule basic
+  (defrole init
+    (vars (a b akey) (na nb text))
+    (trace (send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))
+  (defrole resp
+    (vars (b a akey) (nb na text))
+    (trace (recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))
+  (defrule unilateral
+    (forall ((r strd) (a akey) (nb text))
+      (implies
+        (and (p "resp" r 3) (p "resp" "a" r a) (p "resp" "nb" r nb)
+          (non (invk a)) (uniq nb))
+        (exists ((i strd))
+          (and (p "init" i 3) (p "init" "a" i a) (p "init" "nb" i nb)
+            (prec r 1 i 1) (prec i 2 r 2)))))
+    (comment "Unilateral sas under the predicate mapping:")
+    (comment (p "init" 2) "->" (p "resp" 3) "and")
+    (comment (p "init" "n") "->" (p "resp" "nb") "and")
+    (comment (p "init" "k") "->" (p "resp" "a") "and")
+    (comment (p "resp" 2) "->" (p "init" 3) "and")
+    (comment (p "resp" "n") "->" (p "init" "nb"))
+    (comment (p "resp" "k") "->" (p "init" "a")))
+  (comment "Needham-Schroeder with rule"))
+
+(defskeleton ns-with-rule
+  (vars (nb na text) (a b akey))
+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (comment "Responder point-of-view")
+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))
+  (label 7)
+  (unrealized (0 2))
+  (origs (nb (0 1)))
+  (comment "Not closed under rules"))
+
+(defskeleton ns-with-rule
+  (vars (na na-0 nb text) (b a b-0 akey))
+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))
+  (defstrand init 3 (na na-0) (nb nb) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (rule unilateral)
+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))
+    ((send (enc na-0 a b-0)) (recv (enc na-0 nb a))
+      (send (enc nb b-0))))
+  (label 8)
+  (parent 7)
+  (unrealized (1 1))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton ns-with-rule
+  (vars (na nb text) (b a b-0 akey))
+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))
+  (defstrand init 3 (na na) (nb nb) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (operation nonce-test (contracted (na-0 na)) nb (1 1) (enc na nb a))
+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))
+    ((send (enc na a b-0)) (recv (enc na nb a)) (send (enc nb b-0))))
+  (label 9)
+  (parent 8)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (nb nb) (b b) (na na))))
+  (origs (nb (0 1))))
+
+(defskeleton ns-with-rule
+  (vars (na na-0 nb text) (b a b-0 b-1 akey))
+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))
+  (defstrand init 3 (na na-0) (nb nb) (a a) (b b-0))
+  (defstrand init 3 (na na) (nb nb) (a a) (b b-1))
+  (precedes ((0 1) (2 1)) ((1 2) (0 2)) ((2 2) (1 1)))
+  (non-orig (invk a))
+  (uniq-orig nb)
+  (operation nonce-test (added-strand init 3) nb (1 1) (enc na nb a))
+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))
+    ((send (enc na-0 a b-0)) (recv (enc na-0 nb a)) (send (enc nb b-0)))
+    ((send (enc na a b-1)) (recv (enc na nb a)) (send (enc nb b-1))))
+  (label 10)
+  (parent 8)
+  (seen 9)
+  (unrealized)
+  (comment "1 in cohort - 0 not yet seen"))
+
+(comment "Nothing left to do")
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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from reflect.scm")
 
 (defprotocol reflect basic
diff --git a/tst/role_uniq.scm b/tst/role_uniq.scm
new file mode 100644
--- /dev/null
+++ b/tst/role_uniq.scm
@@ -0,0 +1,56 @@
+(herald "Role Unique Origination")
+
+(defprotocol blanchet basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (send (enc (enc s (invk a)) b))
+     (recv (enc d s)))
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (recv (enc (enc s (invk a)) b))
+     (send (enc d s))))
+  (comment "Blanchet's protocol using unnamed asymmetric keys"))
+
+(defskeleton blanchet
+  (vars (a b akey) (s skey) (d data))
+  (defstrand init 2 (a a) (b b) (s s) (d d))
+  (non-orig (invk b))
+  (comment "Analyze from the initiator's perspective"))
+
+(defskeleton blanchet
+  (vars (a b akey) (s skey) (d data))
+  (defstrand resp 2 (a a) (b b) (s s) (d d))
+  (non-orig (invk a) (invk b))
+  (comment "Analyze from the responder's perspective"))
+
+(defprotocol blanchet basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (send (enc (enc s (invk a)) b))
+     (recv (enc d s))))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (recv (enc (enc s (invk a)) b))
+     (send (enc d s))))
+  (defrule role-uniq
+    (forall ((z strd) (s skey))
+	    (implies (p "init" "s" z s)
+		     (uniq s))))
+  (comment "Blanchet's protocol using unnamed asymmetric keys"))
+
+(defskeleton blanchet
+  (vars (a b akey) (s skey) (d data))
+  (defstrand init 2 (a a) (b b) (s s) (d d))
+  (non-orig (invk b))
+  (comment "Analyze from the initiator's perspective"))
+
+(defskeleton blanchet
+  (vars (a b akey) (s skey) (d data))
+  (defstrand resp 2 (a a) (b b) (s s) (d d))
+  (non-orig (invk a) (invk b))
+  (comment "Analyze from the responder's perspective"))
diff --git a/tst/role_uniq.tst b/tst/role_uniq.tst
new file mode 100644
--- /dev/null
+++ b/tst/role_uniq.tst
@@ -0,0 +1,247 @@
+(herald "Role Unique Origination")
+
+(comment "CPSA 3.6.4")
+(comment "All input read from role_uniq.scm")
+
+(defprotocol blanchet basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (comment "Blanchet's protocol using unnamed asymmetric keys"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (comment "Analyze from the initiator's perspective")
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))
+  (label 0)
+  (unrealized (0 1))
+  (origs (s (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b a-0 b-0 akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    ((recv (enc (enc s (invk a-0)) b-0)) (send (enc d s))))
+  (label 1)
+  (parent 0)
+  (unrealized (1 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (deflistener s)
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (operation encryption-test (added-listener s) (enc d s) (0 1))
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    ((recv s) (send s)))
+  (label 2)
+  (parent 0)
+  (unrealized (1 0))
+  (dead)
+  (comment "empty cohort"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (defstrand resp 2 (d d) (s s) (a a) (b b))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)
+    (enc (enc s (invk a)) b))
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    ((recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (label 3)
+  (parent 1)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (d d))))
+  (origs (s (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol blanchet basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (comment "Blanchet's protocol using unnamed asymmetric keys"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand resp 2 (d d) (s s) (a a) (b b))
+  (non-orig (invk a) (invk b))
+  (comment "Analyze from the responder's perspective")
+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (label 4)
+  (unrealized (0 0))
+  (origs)
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b b-0 akey))
+  (defstrand resp 2 (d d) (s s) (a a) (b b))
+  (defstrand init 1 (s s) (a a) (b b-0))
+  (precedes ((1 0) (0 0)))
+  (non-orig (invk a) (invk b))
+  (uniq-orig s)
+  (operation encryption-test (added-strand init 1) (enc s (invk a))
+    (0 0))
+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))
+    ((send (enc (enc s (invk a)) b-0))))
+  (label 5)
+  (parent 4)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (d d))))
+  (origs (s (1 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol blanchet basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (defrule role-uniq
+    (forall ((z strd) (s skey)) (implies (p "init" "s" z s) (uniq s))))
+  (comment "Blanchet's protocol using unnamed asymmetric keys"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (non-orig (invk b))
+  (comment "Analyze from the initiator's perspective")
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))
+  (label 6)
+  (unrealized)
+  (origs)
+  (comment "Not closed under rules"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (rule role-uniq)
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))
+  (label 7)
+  (parent 6)
+  (unrealized (0 1))
+  (origs (s (0 0)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b a-0 b-0 akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    ((recv (enc (enc s (invk a-0)) b-0)) (send (enc d s))))
+  (label 8)
+  (parent 7)
+  (unrealized (1 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (deflistener s)
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (operation encryption-test (added-listener s) (enc d s) (0 1))
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    ((recv s) (send s)))
+  (label 9)
+  (parent 7)
+  (unrealized (1 0))
+  (dead)
+  (comment "empty cohort"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand init 2 (d d) (s s) (a a) (b b))
+  (defstrand resp 2 (d d) (s s) (a a) (b b))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (invk b))
+  (uniq-orig s)
+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)
+    (enc (enc s (invk a)) b))
+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
+    ((recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (label 10)
+  (parent 8)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (d d))))
+  (origs (s (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol blanchet basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (defrule role-uniq
+    (forall ((z strd) (s skey)) (implies (p "init" "s" z s) (uniq s))))
+  (comment "Blanchet's protocol using unnamed asymmetric keys"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b akey))
+  (defstrand resp 2 (d d) (s s) (a a) (b b))
+  (non-orig (invk a) (invk b))
+  (comment "Analyze from the responder's perspective")
+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s))))
+  (label 11)
+  (unrealized (0 0))
+  (origs)
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton blanchet
+  (vars (d data) (s skey) (a b b-0 akey))
+  (defstrand resp 2 (d d) (s s) (a a) (b b))
+  (defstrand init 1 (s s) (a a) (b b-0))
+  (precedes ((1 0) (0 0)))
+  (non-orig (invk a) (invk b))
+  (uniq-orig s)
+  (rule role-uniq)
+  (operation encryption-test (added-strand init 1) (enc s (invk a))
+    (0 0))
+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))
+    ((send (enc (enc s (invk a)) b-0))))
+  (label 12)
+  (parent 11)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (s s) (d d))))
+  (origs (s (1 0))))
+
+(comment "Nothing left to do")
diff --git a/tst/rule-order.scm b/tst/rule-order.scm
new file mode 100644
--- /dev/null
+++ b/tst/rule-order.scm
@@ -0,0 +1,21 @@
+(herald rule-order)
+
+(defprotocol rule-order basic
+  (defrole init
+    (vars (s t text))
+    (trace
+     (send (cat s t))))
+
+  (defrule ge
+    (forall ((x y text))
+	    (implies
+	     (fact le x y)
+	     (or
+	      (= x y)
+	      (fact lt x y)))))
+  )
+
+(defskeleton rule-order
+  (vars (s t text))
+  (defstrand init 1 (s s) (t t))
+  (facts (le s t)))
diff --git a/tst/rule-order.tst b/tst/rule-order.tst
new file mode 100644
--- /dev/null
+++ b/tst/rule-order.tst
@@ -0,0 +1,48 @@
+(herald rule-order)
+
+(comment "CPSA 3.6.4")
+(comment "All input read from rule-order.scm")
+
+(defprotocol rule-order basic
+  (defrole init (vars (s t text)) (trace (send (cat s t))))
+  (defrule ge
+    (forall ((x y text))
+      (implies (fact le x y) (or (= x y) (fact lt x y))))))
+
+(defskeleton rule-order
+  (vars (s t text))
+  (defstrand init 1 (s s) (t t))
+  (facts (le s t))
+  (traces ((send (cat s t))))
+  (label 0)
+  (unrealized)
+  (origs)
+  (comment "Not closed under rules"))
+
+(defskeleton rule-order
+  (vars (t text))
+  (defstrand init 1 (s t) (t t))
+  (facts (le t t))
+  (rule ge)
+  (traces ((send (cat t t))))
+  (label 1)
+  (parent 0)
+  (unrealized)
+  (shape)
+  (maps ((0) ((s t) (t t))))
+  (origs))
+
+(defskeleton rule-order
+  (vars (s t text))
+  (defstrand init 1 (s s) (t t))
+  (facts (lt s t) (le s t))
+  (rule ge)
+  (traces ((send (cat s t))))
+  (label 2)
+  (parent 0)
+  (unrealized)
+  (shape)
+  (maps ((0) ((s s) (t t))))
+  (origs))
+
+(comment "Nothing left to do")
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from test_small.scm")
 
 (defprotocol test diffie-hellman
diff --git a/tst/trust-anchor.scm b/tst/trust-anchor.scm
new file mode 100644
--- /dev/null
+++ b/tst/trust-anchor.scm
@@ -0,0 +1,19 @@
+(herald trust-anchor
+	(comment "Tests rule application on initial skeleton"))
+
+(defprotocol trust-anchor basic
+  ;;; trust-anchor property guarantees non
+  (defrule trust-anchor-inverse-is-non
+    (forall ((k akey))
+	    (implies (fact trust-anchor k)
+		     (non (invk k))))))
+
+(defskeleton trust-anchor
+  (vars (f ca name))
+  (deflistener (enc f (pubk f) (privk ca)))
+  (non-orig (privk ca)))
+
+(defskeleton trust-anchor
+  (vars (f ca name))
+  (deflistener (enc f (pubk f) (privk ca)))
+  (facts (trust-anchor (pubk ca))))
diff --git a/tst/trust-anchor.tst b/tst/trust-anchor.tst
new file mode 100644
--- /dev/null
+++ b/tst/trust-anchor.tst
@@ -0,0 +1,58 @@
+(herald trust-anchor
+  (comment "Tests rule application on initial skeleton"))
+
+(comment "CPSA 3.6.4")
+(comment "All input read from trust-anchor.scm")
+
+(defprotocol trust-anchor basic
+  (defrule trust-anchor-inverse-is-non
+    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k))))))
+
+(defskeleton trust-anchor
+  (vars (f ca name))
+  (deflistener (enc f (pubk f) (privk ca)))
+  (non-orig (privk ca))
+  (traces
+    ((recv (enc f (pubk f) (privk ca)))
+      (send (enc f (pubk f) (privk ca)))))
+  (label 0)
+  (unrealized (0 0))
+  (dead)
+  (origs)
+  (comment "empty cohort"))
+
+(comment "Nothing left to do")
+
+(defprotocol trust-anchor basic
+  (defrule trust-anchor-inverse-is-non
+    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k))))))
+
+(defskeleton trust-anchor
+  (vars (f ca name))
+  (deflistener (enc f (pubk f) (privk ca)))
+  (facts (trust-anchor (pubk ca)))
+  (traces
+    ((recv (enc f (pubk f) (privk ca)))
+      (send (enc f (pubk f) (privk ca)))))
+  (label 1)
+  (unrealized)
+  (origs)
+  (comment "Not closed under rules"))
+
+(defskeleton trust-anchor
+  (vars (f ca name))
+  (deflistener (enc f (pubk f) (privk ca)))
+  (non-orig (privk ca))
+  (facts (trust-anchor (pubk ca)))
+  (rule trust-anchor-inverse-is-non)
+  (traces
+    ((recv (enc f (pubk f) (privk ca)))
+      (send (enc f (pubk f) (privk ca)))))
+  (label 2)
+  (parent 1)
+  (unrealized (0 0))
+  (dead)
+  (origs)
+  (comment "empty cohort"))
+
+(comment "Nothing left to do")
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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (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.3")
+(comment "CPSA 3.6.4")
 (comment "All input read from yahalom.scm")
 
 (defprotocol yahalom diffie-hellman