diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,26 @@
+2016-06-03  Moses D. Liskov <mliskov@mitre.org>
+
+	* doc/examples/IKE_variants.tar.gz: Added this compressed archive
+	of IKEv1 and IKEv2 variant input files.
+	
+2016-03-30  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/SAS/SAS.hs: Added support for fringe skeletons so that
+	cpassas makes use of depth limited output.  When a tree depth
+	limit is exceeded, a fringe labeled skeleton is printed.  cpsasas
+	produces a sentence with a right-hand-side that encodes both the
+	shapes and the fringe.  Thus, when cpsa is running the a tree
+	depth limit of one, cpsasas computes a cohort analysis sentence.
+
+2016-03-29  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Reduction.hs (LPreskel): Added a depth field, so
+	that CPSA aborts when the depth of one branch exceeds a bound.
+
+	* src/CPSA/Lib/Algebra.hs: Added escapeSet to Term class and remove
+	protectors, thus computing the escape set in a more
+	straightforward way.
+
 2015-11-23  John D. Ramsdell  <ramsdell@mitre.org>
 
 	* src/CPSA/SAS/Main.hs (main): Changed start up so that the herald
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,18 @@
 CPSA NEWS
 
+  June, 2016:
+
+* New feature: depth limit.  When a depth limit is specified, analysis of
+  skeletons will proceed as long as the skeleton's depth in the search tree
+  is below the limit.  Skeletons not analyzed are marked as "(fringe)" to
+  indicate the incomplete nature of those branches of the analysis.  Unlike
+  hitting a strand bound, the tool does not exit with an error when the depth
+  limit is reached.
+
+* IKE_variants.tar.gz added: This is an archive of over 30 variants of
+  IKEv1 and IKEv2 protocols modeled in CPSA.  The archive can be found in the
+  doc/examples directory.
+
   February, 2016: CPSA version 3 released to the public.
 
 Version 3 of CPSA is a major update to the tool including many new features.
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,5 +1,5 @@
 Name:			cpsa
-Version:		3.3.0
+Version:		3.3.1
 Maintainer:		mliskov@mitre.org
 Cabal-Version:		>= 1.6
 License:		BSD3
@@ -60,7 +60,7 @@
   examples/plaindh.scm examples/plaindh.xhtml examples/priority_test.scm
   examples/priority_test.xhtml examples/station.scm examples/station.xhtml
   examples/subsort_test.scm examples/woolam.scm examples/yahalom.scm
-  examples/yahalom.xhtml
+  examples/yahalom.xhtml examples/IKE_variants.tar.gz
 Data-Dir:	    	doc
 Extra-Source-Files:
   Makefile ChangeLog README.txt NEWS ghci cpsatst setup.bat
diff --git a/doc/cpsamanual.pdf b/doc/cpsamanual.pdf
Binary files a/doc/cpsamanual.pdf and b/doc/cpsamanual.pdf differ
diff --git a/doc/examples/IKE_variants.tar.gz b/doc/examples/IKE_variants.tar.gz
new file mode 100644
Binary files /dev/null and b/doc/examples/IKE_variants.tar.gz differ
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
@@ -423,28 +423,17 @@
           | x `elem` xs = xs
           | otherwise = x : xs
 
--- Returns the encryptions that carry the target.  If the target is
--- carried outside all encryptions, or is exposed because a decription
--- key is derivable, Nothing is returned.
-protectors :: Set Term -> Set Term -> Term -> Term -> Maybe [Term]
-protectors avoid sent target source =
-    do
-      ts <- bare source S.empty
-      return $ S.elems ts
-    where
-      bare source _
-           | source == target = Nothing
-      bare (F Cat [t, t']) acc =
-          maybe Nothing (bare t') (bare t acc)
-      bare t@(F Enc [t', key]) acc =
-          if target `carriedBy` t' then
-              if (derivable avoid sent) (inv key) then
-                  bare t' acc
-              else
-                  Just (S.insert t acc)
-          else
-              Just acc
-      bare _ acc = Just acc
+escapeSet :: Set Term -> Set Term -> Term -> Maybe (Set Term)
+escapeSet ts a ct =
+    if buildable ts a ct then
+        Nothing
+    else
+        Just $ S.filter f ts
+        where
+          f (F Enc [t, key]) =
+              carriedBy ct t &&
+              not (buildable ts a (inv key))
+          f _ = False
 
 instance C.Term Term where
     derivable = derivable
@@ -466,7 +455,7 @@
     decompose = decompose
     buildable = buildable
     encryptions = encryptions
-    protectors = protectors
+    escapeSet = escapeSet
     loadTerm = loadTerm2
 
 -- Places
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
@@ -958,37 +958,17 @@
     indicatorBasis = S.fold mul M.empty numAvoid
 indicator _ t = error ("Algebra.hs: indicator called on a non-base " ++ show t)
 
--- Returns the encryptions that carry something relevant to the target.
--- If something relevant to the target is carried outside all encryptions,
--- or is exposed because a decription key is derivable, Nothing is returned.
-protectors :: Set Term -> Set Term -> Term -> Term -> Maybe [Term]
-protectors avoid sent target source =
---  z ("protectors", avoid, sent, target, source) $
-    do
-      ts <- bare source S.empty
-      return $ S.elems ts
-    where
-      bare source acc
-          | source == target = Nothing
-          | relevant avoid source target =
-            case (getBase source == getBase target) of
-                 True -> Nothing
-                 False -> Just (S.insert source acc)
-      bare (F Cat [t, t']) acc =
-          maybe Nothing (bare t') (bare t acc)
-      bare t@(F Enc [t', key]) acc =
-          if relevantCarriedBy avoid target t' then
-              if (derivable avoid sent) (inv key) then
-                  bare t' acc
-              else
-                  Just (S.insert t acc)
-          else
-              Just acc
-      bare t acc =
-        if relevant avoid target t then
-          Just (S.insert t acc)
-        else
-          Just acc
+escapeSet :: Set Term -> Set Term -> Term -> Maybe (Set Term)
+escapeSet ts a ct =
+    if buildable ts a ct then
+        Nothing
+    else
+        Just $ S.filter f ts
+        where
+          f (F Enc [t, key]) =
+              relevantCarriedBy a ct t &&
+              not (buildable ts a (inv key))
+          f t = relevant a ct t
 
 instance C.Term Term where
     derivable = derivable
@@ -1010,7 +990,7 @@
     decompose = decompose
     buildable = buildable
     encryptions = encryptions
-    protectors = protectors
+    escapeSet = escapeSet
     loadTerm = loadTerm
 
 -- Places
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
@@ -81,16 +81,12 @@
     -- later in the list.
     encryptions :: t -> [(t,[t])]
 
-    -- protectors derivable target source returns Nothing if target is
-    -- carried by the source outside of an encryption, where derivable
-    -- is used to determine if a decryption key can be used to expose
-    -- the target.  Otherwise, it returns the list of encryptions in
-    -- the source that carry the target and have underivable
-    -- decryption keys, with duplicates eliminated.  If two
-    -- encryptions protect the target, only the outside one is
-    -- returned.  The inside encryption is the one that is carried by
-    -- the outside encryption.
-    protectors :: Set t -> Set t -> t -> t -> Maybe [t]
+    -- Assume (ts, a) is the output of decomposable, that is ts is a
+    -- set of encriptions and a is the reduced avoidance set.
+    -- escapeSet ts a ct = Nothing if buildable ts a ct = True.
+    -- Otherwise, escapeSet ts a ct = Just es, where es is the escape
+    -- set.
+    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
diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs
--- a/src/CPSA/Lib/Cohort.hs
+++ b/src/CPSA/Lib/Cohort.hs
@@ -8,7 +8,6 @@
 
 module CPSA.Lib.Cohort (Mode(..), reduce, unrealized, minPriority) where
 
-import Control.Monad
 import qualified Data.Set as S
 import Data.Set (Set)
 import qualified Data.List as L
@@ -215,9 +214,10 @@
 testNode mode k a n =
    case event n of
      In t ->
-       let ts = transmissionsBefore S.empty n in -- Public messages
-       if derivable a ts t then Nothing
-       else Just $ solveNode mode k a ts (graphNode n) t
+       let ts = transmissionsBefore S.empty n -- Public messages
+           (ts', a') = decompose ts a in
+       if buildable ts' a' t then Nothing
+       else Just $ solveNode mode k a' ts' (graphNode n) t
      Sync t | not (explainable k n (leadsto k)) ->
        Just $ solveSyncNode mode k (graphNode n) (now t)
      _ -> Nothing
@@ -231,7 +231,7 @@
     where
       loop [] = assertError ("Cohort.solveNode missing test at " ++ show n)
       loop ((ct, eks) : cts) =
-          case escapeSet a ts ct of
+          case escapeSet ts a ct of
             Nothing -> loop cts
             Just escape ->
                 places (carriedPlaces ct t)
@@ -256,22 +256,11 @@
       g (_, []) = False         -- An encryption test must have
       g _ = True                -- at least one non-derivable key
       -- Dump derivable encryption keys
-      h (ct, eks) = (ct, filter (not . (derivable a ts)) eks)
+      h (ct, eks) = (ct, filter (not . (buildable ts a)) eks)
       ff a (t, _) = any (nonTrivIndicator t) (S.elems a)
       nonTrivIndicator t e = case indicator t e of
         Just n -> n /= 0
         Nothing -> False
-
--- Compute the relevant escape set
-escapeSet :: Algebra t p g s e c => Set t ->
-             Set t -> t -> Maybe (Set t)
-escapeSet a ts ct =
-    foldM f S.empty (S.toList ts)
-    where
-      f e t =
-          do
-            es <- protectors a ts ct t
-            return (foldl (flip S.insert) e es)
 
 --carriedOnlyWithin :: Algebra t p g s e c => t -> Set t -> t -> Bool
 --carriedOnlyWithin target escape source =
diff --git a/src/CPSA/Lib/Entry.hs b/src/CPSA/Lib/Entry.hs
--- a/src/CPSA/Lib/Entry.hs
+++ b/src/CPSA/Lib/Entry.hs
@@ -80,6 +80,7 @@
       optGoalsSat :: Bool , -- True when goals satisfied stops tree expansion
       optLimit :: Int,          -- Step count limit
       optBound :: Int,          -- Strand cound bound
+      optDepth :: Int,          -- Tree depth bound
       optMargin :: Int,         -- Output line length
       optIndent :: Int }        -- Pretty printing indent
     deriving Show
@@ -96,6 +97,7 @@
   optGoalsSat = False,
   optLimit = 2000,
   optBound = 12,
+  optDepth = 32,
   optMargin = 72,
   optIndent = 2 }
 
diff --git a/src/CPSA/Lib/Main.hs b/src/CPSA/Lib/Main.hs
--- a/src/CPSA/Lib/Main.hs
+++ b/src/CPSA/Lib/Main.hs
@@ -30,6 +30,10 @@
 defaultStrandBound :: Int
 defaultStrandBound = optBound defaultOptions
 
+-- Default limit on the number of depths is a skeleton.
+defaultDepthBound :: Int
+defaultDepthBound = optDepth defaultOptions
+
 -- Default algebra
 defaultAlgebra :: String
 defaultAlgebra = optAlg defaultOptions
@@ -136,6 +140,10 @@
                 True -> writeComment h m $
                         "Strand count bounded at " ++ show (optBound opts)
                 False -> return ()
+              case optDepth opts /= defaultDepthBound of
+                True -> writeComment h m $
+                        "Tree depth bounded at " ++ show (optDepth opts)
+                False -> return ()
               case optCheckNoncesFirst opts of
                 True -> writeComment h m "Nonces checked first"
                 False -> return ()
@@ -168,6 +176,7 @@
     = Output String             -- Output file name
     | Limit String              -- Step count limit
     | Bound String              -- Strand count bound
+    | Depth String              -- Tree depth bound
     | Margin String             -- Output line length
     | Expand                    -- Expand macros only
     | NoIsoChk                  -- Disable isomorphism checks
@@ -188,6 +197,8 @@
       ("step count limit (default " ++ show defaultStepLimit ++ ")"),
       Option ['b'] ["bound"]    (ReqArg Bound "INT")
       ("strand count bound (default " ++ show defaultStrandBound ++ ")"),
+      Option ['d'] ["depth"]    (ReqArg Depth "INT")
+      ("tree depth bound (default " ++ show defaultDepthBound ++ ")"),
       Option ['m'] ["margin"]   (ReqArg Margin "INT")
       ("set output margin (default " ++ show (optMargin defaultOptions) ++ ")"),
       Option ['e'] ["expand"]   (NoArg Expand)
@@ -232,6 +243,14 @@
             _ ->
                 do
                   msg <- usage options ["Bad value for strand bound\n"]
+                  abort msg
+      loop (Depth value : flags) opts =
+          case readDec value of
+            [(depth, "")] ->
+                loop flags $ opts { optDepth = depth }
+            _ ->
+                do
+                  msg <- usage options ["Bad value for depth bound\n"]
                   abort msg
       loop (Margin value : flags) opts =
           case readDec value of
diff --git a/src/CPSA/Lib/Reduction.hs b/src/CPSA/Lib/Reduction.hs
--- a/src/CPSA/Lib/Reduction.hs
+++ b/src/CPSA/Lib/Reduction.hs
@@ -38,9 +38,15 @@
 data LPreskel t g s e
     = LPreskel { content :: Preskel t g s e,
                  label :: Int,
+                 depth :: Int,
                  parent :: Maybe (LPreskel t g s e) }
       deriving Show
 
+withParent :: Algebra t p g s e c => Preskel t g s e ->
+              Int ->  LPreskel t g s e -> LPreskel t g s e
+withParent k label parent =
+    LPreskel k label (1 + depth parent) (Just parent)
+
 -- A skeleton that has been seen before need not be reanalyzed.
 -- Instead, one looks up the label of the skeleton seen before, and
 -- returns it.  What follows is the data structure used to store
@@ -85,7 +91,7 @@
 -- last position is used to hold the reverse of the labels of the
 -- seen children
 data Reduct t g s e  =
-    Reduct !(LPreskel t g s e) !Int !Bool ![Preskel t g s e] ![Int]
+    Reduct !(LPreskel t g s e) !Int ![Preskel t g s e] ![Int]
 
 parMap :: (a -> b) -> [a] -> [b]
 parMap _ [] = []
@@ -103,6 +109,7 @@
 -}
 
 -- Entry point for analysis
+-- n is the step count
 solve :: Algebra t p g s e c => Options -> Handle ->
          [Preskel t g s e] -> Int -> IO ()
 solve _ h [] _ =                -- Done
@@ -113,21 +120,21 @@
       case firstSkeleton k of
         [] ->                  -- Input cannot be made into a skeleton
             do
-              let lk = LPreskel k n Nothing
-              wrt p h (commentPreskel lk [] (unrealized k) False False
+              let lk = LPreskel k n 0 Nothing
+              wrt p h (commentPreskel lk [] (unrealized k) Ordinary
                        "Input cannot be made into a skeleton--nothing to do")
               solve p h ks (n + 1)
         [k'] ->
             if isomorphic (gist k) (gist k') then -- Input was a skeleton
-                let lk' = LPreskel k' n Nothing in
+                let lk' = LPreskel k' n 0 Nothing in
                 begin p h ks (n + optLimit p) (n + 1)
                          (hist (gist k', n)) [lk']
             else                -- Input was not a skeleton
                 do
-                  let lk = LPreskel k n Nothing
-                  wrt p h (commentPreskel lk [] (unrealized k) False False
+                  let lk = LPreskel k n (-1) Nothing
+                  wrt p h (commentPreskel lk [] (unrealized k) Ordinary
                            "Not a skeleton")
-                  let lk' = LPreskel k' (n + 1) (Just lk)
+                  let lk' = withParent k' (n + 1) lk
                   begin p h ks (n + optLimit p) (n + 2)
                            (hist (gist k', n + 1))  [lk']
         _ -> error "Main.solve: can't handle more than one skeleton"
@@ -209,25 +216,29 @@
         do
           wrt p h (comment "Step limit exceeded--aborting run")
           dump p h (mktodo reducts todo tobig) "Step limit exceeded"
-step p h ks m oseen n seen todo tobig (Reduct lk _ _  _  _ : reducts)
+step p h ks m oseen n seen todo tobig (Reduct lk _ _  _  : reducts)
     | nstrands (content lk) >= optBound p = -- Check strand count
         step p h ks m oseen n seen todo (lk : tobig) reducts
-step p h ks m oseen n seen todo tobig (Reduct lk size cols kids dups : reducts)
+step p h ks m oseen n seen todo tobig (Reduct lk size kids dups : reducts)
     | optGoalsSat p && satCheck lk = -- Stop if goals satisfied mode?
         do
           let ns = unrealized (content lk)
-          let shape = null ns
-          wrt p h (commentPreskel lk [] ns shape False
-                   "satisfies all")
+          let shape = if null ns then Shape else Fringe
+          wrt p h (commentPreskel lk [] ns shape "satisfies all")
           step p h ks m oseen n seen todo tobig reducts
     | size <= 0 =               -- Interpret empty reducts
         do
           let ns = unrealized (content lk)
-          let shape = null ns
+          let shape = if null ns then Shape else Ordinary
           let live = null $ thresholdUnrealized (content lk)
-          wrt p h (commentPreskel lk [] ns shape False
+          wrt p h (commentPreskel lk [] ns shape
                    (if live then "" else "empty cohort"))
           step p h ks m oseen n seen todo tobig reducts
+    | depth lk >= optDepth p =
+        do
+          let ns = unrealized (content lk)
+          wrt p h (commentPreskel lk [] ns Fringe "")
+          step p h ks m oseen n seen todo tobig reducts
     | otherwise =
         do
           let (n', seen', todo', dups') =
@@ -236,18 +247,17 @@
           let u = size - length dups'
           let msg = shows size $ showString " in cohort - " $
                          shows u " not yet seen"
-          wrt p h (commentPreskel lk (reverse dups') ns cols False msg)
+          wrt p h (commentPreskel lk (reverse dups') ns Ordinary msg)
           step p h ks m oseen n' seen' todo' tobig reducts
 
 -- Expands one branch in the derivation tree.
 branch :: Algebra t p g s e c => Options -> Seen t g s e ->
           LPreskel t g s e -> Reduct t g s e
 branch p seen lk =
-    Reduct lk (length kids) cols
+    Reduct lk (length kids)
                (seqList $ reverse unseen) (seqList dups)
     where
       kids = reduce (mkMode p) (content lk)
-      cols = all collapsed kids
       (unseen, dups) =
           foldl (duplicates seen) ([], []) kids
 
@@ -258,13 +268,6 @@
            visitOldStrandsFirst = optTryOldStrandsFirst p,
            reverseNodeOrder = optTryYoungNodesFirst p}
 
--- Is preskeleton the result of a collapsing operation?
-collapsed :: Algebra t p g s e c => Preskel t g s e -> Bool
-collapsed k =
-    case operation k of
-      Collapsed _ _ -> True
-      _ -> False
-
 duplicates :: Algebra t p g s e c => Seen t g s e ->
               ([Preskel t g s e], [Int]) ->
                   Preskel t g s e -> ([Preskel t g s e], [Int])
@@ -278,7 +281,7 @@
           [LPreskel t g s e] -> [LPreskel t g s e] ->
           [LPreskel t g s e]
 mktodo reducts todo tobig =
-    map (\(Reduct lk _ _ _ _) -> lk) reducts ++ reverse todo ++ reverse tobig
+    map (\(Reduct lk _ _ _) -> lk) reducts ++ reverse todo ++ reverse tobig
 
 type Next t p g s e c =
     (Int, Seen t g s e, [LPreskel t g s e], [Int])
@@ -295,7 +298,7 @@
       Nothing ->
           (n + 1, remember (g, n) seen, lk : todo, dups)
           where
-            lk = LPreskel k n (Just p) -- Label a preskeleton here
+            lk = withParent k n p -- Label a preskeleton here
 
 -- This function reduces without checking for isomorphisms
 fast :: Algebra t p g s e c => Options -> Handle ->
@@ -320,7 +323,8 @@
       let ns = unrealized (content lk)
       let ks' = reduce (mkMode p) (content lk)
       let msg = show (length ks') ++ " in cohort"
-      wrt p h (commentPreskel lk [] ns (null ns) False msg)
+      let shape = if null ns then Shape else Ordinary
+      wrt p h (commentPreskel lk [] ns shape msg)
       let (n', todo') = foldl (children lk) (n, []) ks'
       fast p h ks m n' (todo ++ reverse todo')
 
@@ -328,7 +332,7 @@
             (Int, [LPreskel t g s e]) ->
             Preskel t g s e -> (Int, [LPreskel t g s e])
 children p (n, todo) k =        -- Label a preskeleton here
-    (n + 1, LPreskel k n (Just p) : todo)
+    (n + 1, withParent k n p : todo)
 
 -- Print partial results in a form that works with analysis tools
 dump :: Algebra t p g s e c => Options -> Handle ->
@@ -340,32 +344,30 @@
 dump p h (lk : lks) msg =
     do
       let ns = unrealized $ content lk
-      wrt p h (commentPreskel lk [] ns False True "aborted")
+      wrt p h (commentPreskel lk [] ns Ordinary "aborted")
       dump p h lks msg
 
 -- Add a label, maybe a parent, a list of seen preskeletons isomorphic
 -- to some members of this skeleton's cohort, and a list of unrealized
 -- nodes.  If it's a shape, note this fact.  Add a comment if present.
 commentPreskel :: Algebra t p g s e c => LPreskel t g s e ->
-                  [Int] -> [Node] -> Bool -> Bool -> String -> SExpr ()
-commentPreskel lk seen unrealized shape _ msg =
+                  [Int] -> [Node] -> Kind -> String -> SExpr ()
+commentPreskel lk seen unrealized kind msg =
     displayPreskel k $
     addKeyValues "label" [N () (label lk)] $
     maybeAddVKeyValues "parent" (\p -> [N () (label p)]) (parent lk) $
     condAddKeyValues "seen" (not $ null seen)
                      (map (N ()) (L.sort (L.nub seen))) $
     addKeyValues "unrealized" (map displayNode $ L.sort unrealized) $
---    addKeyValues "unrealized-todo" (map displayNode $ L.sort (filter (\n -> priority k n >= minPriority) unrealized)) $
-    condAddKeyValues "shape" shape [] $
-    condAddKeyValues "satisfies" (shape && (not $ null $ kgoals k))
+    addKindKey kind $
+    condAddKeyValues "satisfies" (kind == Shape && (not $ null $ kgoals k))
     (satisfies k) $
     -- Structure preserving maps
     -- Added for cpsasas program
-    condAddKeyValues "maps" shape (maps k) $
+    condAddKeyValues "maps" fringe (maps k) $
     -- Nodes of origination
     -- Added for cpsasas program
-    condAddKeyValues "origs" (starter k || shape) (origs k) $
-    -- condAddKeyValues "ugens" (starter k || shape) (ugens k) $
+    condAddKeyValues "origs" (starter k || fringe) (origs k) $
     -- Messages
     case msg of
       "" -> []
@@ -373,6 +375,7 @@
       "Not a skeleton" -> addKeyValues "preskeleton" [] [comment msg]
       _ -> [comment msg]
     where
+      fringe = kind /= Ordinary
       k = content lk
       starter k =               -- True for the POV skeleton and
           case pov k of         -- just a few others
@@ -395,6 +398,17 @@
     rest
 maybeAddVKeyValues key f (Just x) rest =
     addKeyValues key (f x) rest
+
+data Kind
+    = Ordinary
+    | Shape
+    | Fringe
+      deriving (Eq, Show)
+
+addKindKey :: Kind -> [SExpr ()] -> [SExpr ()]
+addKindKey Ordinary xs = xs
+addKindKey Shape xs = addKeyValues "shape" [] xs
+addKindKey Fringe xs = addKeyValues "fringe" [] xs
 
 -- Variable assignments and security goals
 
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
@@ -46,7 +46,7 @@
     do
       p <- findProt pos ps xs
       k <- loadPreskel pos p (pgen p) xs
-      case (isSkeleton k, isShape k) of
+      case (isSkeleton k, isFringe k) of
         (True, False) ->
           do                    -- Found POV
             origCheck pos k     -- Ensure uniqs originate
@@ -66,7 +66,7 @@
       p <- findProt pos ps xs
       let g = kgen (last ks)      -- Make sure vars in skeleton are
       k <- loadPreskel pos p g xs -- distinct from the ones in the POV
-      case isShape k of
+      case isFringe k of
         True ->
           do                    -- Found shape
             origCheck pos k     -- Ensure uniqs originate
@@ -251,7 +251,7 @@
       uniqs :: [t],
       origs :: [(t, t)],
       isSkeleton :: Bool,
-      isShape :: !Bool,         -- Always looked at, so make it strict
+      isFringe :: !Bool,         -- Always looked at, so make it strict
       homomorphisms :: [SExpr Pos], -- Loaded later
       varmap :: VM t }
 
@@ -282,7 +282,7 @@
                         uniqs = uniqs,
                         origs = map g origs,
                         isSkeleton = not $ hasKey preskeletonKey xs,
-                        isShape = hasKey shapeKey xs,
+                        isFringe = hasKey shapeKey xs || hasKey fringeKey xs,
                         homomorphisms = assoc mapsKey xs,
                         varmap = varmap})
 loadPreskel pos _ _ _ = fail (shows pos "Malformed skeleton")
@@ -503,6 +503,10 @@
 -- The key used to identify a shape
 shapeKey :: String
 shapeKey = "shape"
+
+-- The key used to identify a non-shape fringe
+fringeKey :: String
+fringeKey = "fringe"
 
 -- The key used to extract the list of homomorphisms
 mapsKey :: String