diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,26 @@
+2015-07-08  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* cpsa.cabal (Version): Tagged as version 2.5.1
+
+2015-06-30  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Basic/Algebra.hs (occursIn): Restricted first argument
+	of occursIn to variables as the implementation returns incorrect
+	answers for other cases.  The code was called with a variable in
+	its first argument, so this correction does not change any
+	results.
+
+2015-06-25  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Strand.hs (geq): Removed dynamic role specific test
+	because it erroneously reports violations.  The existing static
+	role specific test correctly does the job.
+
+2015-06-18  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* doc/{cpsaprimer,cpsagoals}.tex: Repaired errors and made
+	improvements in response to a review of this document.
+
 2015-05-21  John D. Ramsdell  <ramsdell@mitre.org>
 
 	* cpsa.cabal (Version): Tagged as version 2.5.0
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,9 @@
 CPSA NEWS -- history of user-visible changes.
 
+* Changes in version 2.5.1
+
+** CPSA Goals document updated
+
 * Changes in version 2.5.0
 
 ** Added support for security goals
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,5 +1,5 @@
 Name:			cpsa
-Version:		2.5.0
+Version:		2.5.1
 Maintainer:		ramsdell@mitre.org
 Cabal-Version:		>= 1.6
 License:		BSD3
diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf
Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ
diff --git a/doc/cpsagoals.pdf b/doc/cpsagoals.pdf
Binary files a/doc/cpsagoals.pdf and b/doc/cpsagoals.pdf differ
diff --git a/doc/cpsagoals.tex b/doc/cpsagoals.tex
--- a/doc/cpsagoals.tex
+++ b/doc/cpsagoals.tex
@@ -137,7 +137,7 @@
   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
   (non-orig (privk b))
   (uniq-orig n1)
-  (satisfied yes))
+  (satisfies yes))
 \end{verbatim}
 \caption{Needham-Schroeder Initiator Point of View}
 \label{fig:ns init}
@@ -168,12 +168,13 @@
 
 To be precise, a security goal is an order-sorted first-order logic
 sentence in a restricted form.  The sentence in Figure~\ref{fig:ns
-  init} has the form shared by all security goals.  It is a universally
-quantified implication.  The antecedent is a conjunction of atomic
-formulas.  For this sentence, the conclusion is an existentially
-quantified conjunction of atomic formulas, but in general, the
-conclusion is a disjunction of existentially quantified conjunctions
-of atomic formulas.  \sym{(false)} is a synonym for \sym{(or)}.
+  init} has the form shared by all security goals.  It is a
+universally quantified implication.  The antecedent is a conjunction
+of atomic formulas.  For this sentence, the conclusion is an
+existentially quantified conjunction of atomic formulas, but in
+general, the conclusion is a disjunction of existentially quantified
+conjunctions of atomic formulas.  In what follows, \sym{(false)} is a
+synonym for \sym{(or)}.
 
 \begin{center}\scshape
   \begin{tabular}{rcl}
@@ -194,17 +195,30 @@
 implication.
 
 The predicates used to construct an atomic formula (\textsc{atomic})
-are listed in Table~\ref{tab:predicates}.  The first line gives the
-syntax of a role position predicate.  It contains three tokens,
-\texttt{p}, a string that names a role, and an integer that specifies
-a position within the trace of the role.  That is, for role~$r$ with a
-trace of length~$n$, there are~$n$ role position predicates,
-\mbox{\texttt{p} $r$ $i$}, for $0\leq i < n$.  The second line gives
-the syntax of a role parameter predicate.  It contains three tokens,
-\texttt{p}, a string that names a role, and a string that names a role
-variable.  For role~$r$, there is role parameter predicate for each
-variable declared by~$r$.
+are listed in Table~\ref{tab:predicates}.  There are two classes of
+predicates, protocol specific and protocol independent predicates, and
+two kinds of protocol specific predicates, role position and role
+parameter predicates.  Protocol specific predicates are distinguished
+from protocol independent predicates by being composed of three
+tokens, the first of which is \texttt{p}.
 
+The first line of the table gives the syntax of a role position
+predicate.  It contains three tokens, \texttt{p}, a string that names
+a role, and an integer that specifies a position within the trace of
+the role.  That is, for role~$r$ with a trace of length~$n$, there
+are~$n$ role position predicates, \mbox{\texttt{p} $r$ $i$}, for
+$0\leq i < n$.  Thus \verb|(p "init" 2 z0)| is an atomic formula using
+the role position predicate for position 2 in the \texttt{init} role
+of the protocol in Figure~\ref{fig:ns roles}.
+
+The second line gives the syntax of a role parameter predicate.  It
+contains three tokens, \texttt{p}, a string that names a role, and a
+string that names a role variable.  For role~$r$, there is role
+parameter predicate for each variable declared by~$r$.  Thus
+\verb|(p "init" 2 "n1" z0 n1)| is an atomic formula using the role
+parameter predicate for parameter \text{n1} in the \texttt{init} role
+of the protocol.
+
 The empty string names the listener role of a protocol.  The role
 has the variable \texttt{x} of sort \texttt{mesg} as its only role
 variable.  There are two positions in the listener role.
@@ -437,8 +451,9 @@
 \end{quote}
 The annotation includes a variable mapping for the shape that
 satisfies the antecedent of the goal but does not satisfy its
-conclusion.  The mapping \texttt{(b b)} is the reason the shape does
-not satisfy the goal.
+conclusion.  The reason the shape does not satisfy the goal is because
+the mapping \texttt{(b b)} maps the initiator's \texttt{b} parameter
+to \texttt{b}, not \texttt{b-0} as is required to model the shape.
 
 Galvin Lowe identified this authentication failure in
 Needham-Schroeder and provided a fix.  In the Needham-Schroeder-Lowe
@@ -467,7 +482,7 @@
 
 Figure~\ref{fig:ns secrecy} contains an analysis of Needham-Schroeder
 from the point of view of a complete run of the initiator under the
-assumption that the responder's and its peer's private key are
+assumption that the responder's and its peer's private keys are
 uncompromised and the nonce~\texttt{n1} it generates uniquely
 originates.  Futhermore, the point of view asserts that the nonce is
 leaked using a listener.
@@ -486,7 +501,7 @@
 this example, process the sample file \texttt{goal.scm} with {\cpsa}
 and display its output in a browser.
 
-The protocol and its goal is shown in Figure~\ref{fig:unilateral}.
+The protocol and its goal are shown in Figure~\ref{fig:unilateral}.
 The goal asserts that if a realized skeleton contains a full length
 initiator strand that uniquely generates \texttt{n1}, and
 peer~\texttt{a}'s private key is uncompromised, then the skeleton will
@@ -594,7 +609,7 @@
 {\cpsa} has demonstrated two ways in which Needham-Schroeder achieves
 the goals of the Unilateral Protocol.
 
-\section{The Whole Story}\label{sec:whole story}
+\section{The Rest of the Story}\label{sec:whole story}
 
 The examples in the previous section demonstrate the typical way
 security goals are analyzed with {\cpsa}.  However, there are more
@@ -608,7 +623,7 @@
 It is wise to ensure that the antecedent in every sentence is
 identical.  When {\cpsa} performs satisfaction-checking on
 sentence~$\Phi$, it only determines if each shape it finds is
-satisfied.  If the point of view skeleton in not the characteristic
+satisfied.  If the point of view skeleton is not the characteristic
 skeleton of the antecedent of~$\Phi$, the fact that all skeletons
 satisfy~$\Phi$ cannot be used to conclude that~$\Phi$ is true in all
 executions of the protocol.
@@ -649,7 +664,7 @@
 \end{quote}
 
 The program \texttt{cpsasas}, discussed in the next section, can be
-used to generate an formula with an antecedent such that the input
+used to generate a formula with an antecedent such that the input
 skeleton is the characteristic skeleton of the antecedent.
 
 \subsection{Shape Analysis Sentences}\label{sec:sas}
diff --git a/doc/cpsaintroslides.pdf b/doc/cpsaintroslides.pdf
Binary files a/doc/cpsaintroslides.pdf and b/doc/cpsaintroslides.pdf differ
diff --git a/doc/cpsaintroslides.tex b/doc/cpsaintroslides.tex
--- a/doc/cpsaintroslides.tex
+++ b/doc/cpsaintroslides.tex
@@ -221,7 +221,7 @@
 \begin{mitreslide}{Blanchet Problem Statement}
 \begin{itemize}
 \item Analyze from the point-of-view of a full length responder
-\item Assume $\privk{B}$ is uncompromised
+\item Assume $\privk{A}$ and $\privk{B}$ are uncompromised
 \item Assume symmetric key~$S$ is freshly generated
 \hfill\raisebox{0ex}[0ex]{\includegraphics{blanchet-5.mps}}
 \end{itemize}
@@ -230,7 +230,7 @@
 (defskeleton blanchet
   (vars (a b name) (s skey) (d data))
   (defstrand resp 2 (a a) (b b) (s s) (d d))
-  (non-orig (privk b))
+  (non-orig (privk a) (privk b))
   (uniq-orig s))
 \end{verbatim}
 \end{quote}
diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf
Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ
diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf
Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ
diff --git a/doc/cpsaprimer.tex b/doc/cpsaprimer.tex
--- a/doc/cpsaprimer.tex
+++ b/doc/cpsaprimer.tex
@@ -84,7 +84,7 @@
 tools used to interpret the results.  The analyzer, \texttt{cpsa},
 provides support for several algebras, one of which is the Basic
 Crypto Algebra.  Programs that assist in the interpretation of results
-are \texttt{cpsashape} and \texttt{cpsagraph}.  The analyzer prints
+are \texttt{cpsashapes} and \texttt{cpsagraph}.  The analyzer prints
 the steps it used to solve each problem.  The \texttt{cpsashapes}
 program extracts the shapes discovered by an analyzer run.  The
 \texttt{cpsagraph} program graphs both forms of output using Scalable
@@ -145,7 +145,7 @@
 \section{BCA Messages}
 
 Each message exchanged in a protocol is represented by a term.  Terms
-represent atomic values such text objects, principal names, and
+represent atomic values such as text objects, principal names, and
 asymmetric and symmetric keys.  They also represent values composed
 from other values via encryption and concatenation.
 
@@ -890,7 +890,7 @@
 
 For each skeleton, a {\cpsa} analyzer computes a set of skeletons that
 refine it using a fixed set of operations based on authentication
-tests.  The immediate descendants of a skeleton is called its
+tests.  The immediate descendants of a skeleton are called its
 \index{cohort}\emph{cohort.}  A member of the cohort that is
 equivalent to a previously seen skeleton is replaced by that skeleton.
 Thus the skeletons in an analysis form a directed acyclic graph.  All
@@ -1146,7 +1146,7 @@
 This section contains advice derived from using {\cpsa}.  When
 specifying {\cpsa} input, one must decide when to specify terms as
 uniquely originating or non-originating in a role, and when to
-specifying them in the initial skeleton.  If a flesh value is
+specifying them in the initial skeleton.  If a fresh value is
 generated by all programs that implement a role in a protocol, the
 term that represents the fresh value should be assumed to be uniquely
 originating in the role.  Otherwise, unique origination assumptions
diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf
Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ
diff --git a/doc/macros.tex b/doc/macros.tex
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -1,5 +1,5 @@
 \newcommand{\cpsa}{\textsc{cpsa}}
-\newcommand{\version}{2.5.0}
+\newcommand{\version}{2.5.1}
 \newcommand{\cpsacopying}{\begingroup
   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The
     MITRE Corporation.  Permission to copy without fee all or part of
diff --git a/src/CPSA/Basic/Algebra.hs b/src/CPSA/Basic/Algebra.hs
--- a/src/CPSA/Basic/Algebra.hs
+++ b/src/CPSA/Basic/Algebra.hs
@@ -261,13 +261,17 @@
 isAtom (D _) = False
 isAtom (P _) = False
 
--- Does a term occur in another term?
+-- Does a variable occur in a term?
 occursIn :: Term -> Term -> Bool
-occursIn t t' =
-    t == t' ||
+occursIn t t' | isVar t =
+  recur (I $ varId t) t'
+  where
+    recur t t' =
+      t == t' ||
       case t' of
-        F _ u -> any (occursIn t) u
+        F _ u -> any (recur t) u
         _ -> False
+occursIn t _ = error $ "Algebra.occursIn: Bad variable " ++ show t
 
 -- Fold f through a term applying it to each variable in the term.
 foldVars :: (a -> Term -> a) -> a -> Term -> a
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
@@ -540,18 +540,20 @@
   s == Text || s == Data || s == Name || s == Skey || s == Akey
 isAtom (G x) = isBasisVar x
 
--- Does a term occur in another term?
+-- Does a variable occur in a term?
 
 -- This function is always called with a variable that answers true to
--- isAcquiredVar as its first argument, so the first case never gets used.
+-- isAcquiredVar as its first argument.
 occursIn :: Term -> Term -> Bool
-occursIn (G t) (G t') =
-  t == t'
-occursIn t t' =
-  t == t' ||
-  case t' of
-    F _ u -> any (occursIn t) u
-    _ -> False
+occursIn t t' | isVar t =
+  recur (I $ varId t) t'
+  where
+    recur t t' =
+      t == t' ||
+      case t' of
+        F _ u -> any (recur t) u
+        _ -> False
+occursIn t _ = error $ "Algebra.occursIn: Bad variable " ++ show t
 
 -- Fold f through a term applying it to each variable in the term.
 foldVars :: (a -> Term -> a) -> a -> Term -> a
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
@@ -36,7 +36,7 @@
     -- when applied to node variables.
     isNodeVar :: t -> Bool
 
-    -- Does a term occur in another term?
+    -- Does a variable occur in a term?
     occursIn :: t -> t -> Bool
 
     -- Check to see if a list of terms is well-formed.
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
@@ -210,8 +210,8 @@
         do
           let ns = unrealized (content lk)
           let shape = null ns
-          wrt p h  (commentPreskel lk [] ns shape
-                    (if shape then "" else "empty cohort"))
+          wrt p h (commentPreskel lk [] ns shape
+                   (if shape then "" else "empty cohort"))
           step p h ks m oseen n seen todo tobig reducts
     | otherwise =
         do
@@ -221,7 +221,7 @@
           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 msg)
+          wrt p h (commentPreskel lk (reverse dups') ns cols msg)
           step p h ks m oseen n' seen' todo' tobig reducts
 
 -- Expands one branch in the derivation tree.
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
@@ -1931,13 +1931,10 @@
 satisfy (RolePred r i n) = grole r i n
 satisfy (ParamPred r v n t) = gparam r v n t
 
--- Equality This isn't right.  Suppose t is a compound term which has
--- some unbound variable.  Need static role specific check to
--- eliminate this case.
+-- Equality assumes there has been a static role specific check to
+-- eliminate error cases.
 geq :: Algebra t p g s e c => t -> t -> Sem t g s e
 geq t t' _ (g, e)
-  | t == ti = error ("Strand.geq: " ++ show t ++ " unbound")
-  | t' == ti' = error ("Strand.geq: " ++ show t' ++ " unbound")
   | ti == ti' = [(g, e)]
   | otherwise = []
   where
@@ -2004,7 +2001,7 @@
 gprec n n' k (g, e) =
   case (nodeLookup e n, nodeLookup e n') of
     (Just p, Just p')
-      | inSkel k p && inSkel k p' && 
+      | inSkel k p && inSkel k p' &&
         (strandPrec p p' || elem (p, p') tc) -> [(g, e)]
     (Just _, Just _) -> []
     (_, Just _) ->
diff --git a/tst/DH_hack.tst b/tst/DH_hack.tst
--- a/tst/DH_hack.tst
+++ b/tst/DH_hack.tst
@@ -1,6 +1,6 @@
 (herald "DH Hack" (bound 15))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from DH_hack.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/blanchet.tst b/tst/blanchet.tst
--- a/tst/blanchet.tst
+++ b/tst/blanchet.tst
@@ -1,7 +1,7 @@
 (herald "Blanchet's Simple Example Protocol"
   (comment "There is a flaw in this protocol by design"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from blanchet.scm")
 
 (defprotocol blanchet basic
diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst
--- a/tst/completeness-test.tst
+++ b/tst/completeness-test.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from completeness-test.scm")
 
 (defprotocol completeness-test basic
diff --git a/tst/crushing.tst b/tst/crushing.tst
--- a/tst/crushing.tst
+++ b/tst/crushing.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from crushing.scm")
 
 (defprotocol crushing basic
diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst
--- a/tst/dass_simple.tst
+++ b/tst/dass_simple.tst
@@ -1,6 +1,6 @@
 (herald "Distributed Authentication Security Service Protocol Variants")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from dass_simple.scm")
 
 (defprotocol dass-simple basic
diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst
--- a/tst/denning-sacco.tst
+++ b/tst/denning-sacco.tst
@@ -1,6 +1,6 @@
 (herald "Denning-Sacco Protocol")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from denning-sacco.scm")
 
 (defprotocol denning-sacco basic
diff --git a/tst/deorig_contract.tst b/tst/deorig_contract.tst
--- a/tst/deorig_contract.tst
+++ b/tst/deorig_contract.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from deorig_contract.scm")
 
 (defprotocol deorig-contract basic
diff --git a/tst/deorig_mesg.tst b/tst/deorig_mesg.tst
--- a/tst/deorig_mesg.tst
+++ b/tst/deorig_mesg.tst
@@ -1,6 +1,6 @@
 (herald deorig-mesg)
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from deorig_mesg.scm")
 
 (defprotocol deorig-mesg basic
diff --git a/tst/deorig_simple.tst b/tst/deorig_simple.tst
--- a/tst/deorig_simple.tst
+++ b/tst/deorig_simple.tst
@@ -1,6 +1,6 @@
 (herald deorig-simple)
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from deorig_simple.scm")
 
 (defprotocol deorig-simple basic
diff --git a/tst/dy.tst b/tst/dy.tst
--- a/tst/dy.tst
+++ b/tst/dy.tst
@@ -1,6 +1,6 @@
 (herald "Example 1.3 from 1983 Dolev-Yao Paper")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from dy.lsp")
 
 (defprotocol dy basic
diff --git a/tst/encsig.tst b/tst/encsig.tst
--- a/tst/encsig.tst
+++ b/tst/encsig.tst
@@ -1,7 +1,7 @@
 (herald "Encrypted Signed Message Example"
   (comment "Shows examples of key usage of asymmetric keys"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from encsig.scm")
 
 (defprotocol mult-keys-enc-sig basic
diff --git a/tst/epmo-hash.tst b/tst/epmo-hash.tst
--- a/tst/epmo-hash.tst
+++ b/tst/epmo-hash.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol with Key Hashing"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from epmo-hash.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo-key-hash.tst b/tst/epmo-key-hash.tst
--- a/tst/epmo-key-hash.tst
+++ b/tst/epmo-key-hash.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol with Key Hashing"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from epmo-key-hash.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo.tst b/tst/epmo.tst
--- a/tst/epmo.tst
+++ b/tst/epmo.tst
@@ -1,7 +1,7 @@
 (herald "Electronic Purchase with Money Order Protocol"
   (comment "Annotated with trust management formulas"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from epmo.scm")
 
 (defprotocol epmo basic
diff --git a/tst/epmo_acctnum-key-hash.tst b/tst/epmo_acctnum-key-hash.tst
--- a/tst/epmo_acctnum-key-hash.tst
+++ b/tst/epmo_acctnum-key-hash.tst
@@ -2,7 +2,7 @@
   "Electronic Purchase with Money Order Protocol Variant with Key Hashing"
   (comment "This version includes account numbers in exchanges"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from epmo_acctnum-key-hash.scm")
 
 (defprotocol epmo_acctnum basic
diff --git a/tst/ffgg.tst b/tst/ffgg.tst
--- a/tst/ffgg.tst
+++ b/tst/ffgg.tst
@@ -1,7 +1,7 @@
 (herald "The ffgg Protocol"
   (comment "From A Necessarily Parallel Attack by Jon K. Millen"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from ffgg.scm")
 
 (defprotocol ffgg basic
diff --git a/tst/fragile_pruning.tst b/tst/fragile_pruning.tst
--- a/tst/fragile_pruning.tst
+++ b/tst/fragile_pruning.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from fragile_pruning.scm")
 
 (defprotocol fragile_pruning basic
diff --git a/tst/goals.scm b/tst/goals.scm
--- a/tst/goals.scm
+++ b/tst/goals.scm
@@ -1,89 +1,146 @@
 (herald goals)
 
-;;; Some authentication goals
+;;; Section 1 --- Examples from CPSA and Formal Security Goals
 
-;;; Unilateral authentication
+;;; Needham-Schroeder from Section 10 of the CPSA Primer
 
-(defprotocol unilateral basic
+(defprotocol ns basic
   (defrole init
-     (vars (a name) (n text))
-     (trace
-      (send (enc n (pubk a)))
-      (recv n)))
+    (vars (a b name) (n1 n2 text))
+    (trace
+     (send (enc n1 a (pubk b)))
+     (recv (enc n1 n2 (pubk a)))
+     (send (enc n2 (pubk b)))))
   (defrole resp
-     (vars (a name) (n text))
-     (trace
-      (recv (enc n (pubk a)))
-      (send n))))
+    (vars (b a name) (n2 n1 text))
+    (trace
+     (recv (enc n1 a (pubk b)))
+     (send (enc n1 n2 (pubk a)))
+     (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
 
-(defgoal unilateral
-  (forall ((a name) (n text) (z0 node))
-	  (implies
-	   (and 
-	    (p "init" 1 z0)
-	    (p "init" "n" z0 n)
-	    (p "init" "a" z0 a)
-	    (non (privk a))
-	    (uniq n))
-	   (exists ((z1 node))
-		   (and
-		    (p "resp" 1 z1)
-		    (p "resp" "a" z1 a)))))
-  (comment "Authentication goal"))
+(defgoal ns
+  (forall ((b name) (n1 text) (z0 node))
+    (implies
+     (and (p "init" 2 z0)
+      (p "init" "n1" z0 n1) (p "init" "b" z0 b)
+      (non (privk b)) (uniq n1))
+     (exists ((z1 node))
+	     (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))
+  (comment "Initiator point of view")
+  (comment "Authentication goal: agreement on name b"))
 
-(defprotocol ns basic
+(defgoal ns
+  (forall ((b name) (n1 text) (z0 node))
+    (implies
+     (and (p "init" 2 z0)
+      (p "init" "n1" z0 n1) (p "init" "b" z0 b)
+      (non (privk b)) (uniq n1))
+     (exists ((z1 node))
+	     (and (p "resp" 1 z1) (p "resp" "b" z1 b)
+	      (prec z1 z0)))))
+  (comment "Prec example"))
+
+(defgoal ns
+  (forall ((a b name) (n2 text) (z0 node))
+    (implies
+     (and (p "resp" 2 z0) (p "resp" "n2" z0 n2)
+      (p "resp" "a" z0 a) (p "resp" "b" z0 b)
+      (non (privk a)) (uniq n2))
+     (exists ((z1 node))
+      (and (p "init" 1 z1) (p "init" "b" z1 b)))))
+  (comment "Responder point of view")
+  (comment "Failed authentication goal: agreement on name b"))
+
+(defprotocol nsl basic
   (defrole init
     (vars (a b name) (n1 n2 text))
     (trace
      (send (enc n1 a (pubk b)))
-     (recv (enc n1 n2 (pubk a)))
+     (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))))
   (defrole resp
-    (vars (a b name) (n1 n2 text))
+    (vars (b a name) (n2 n1 text))
     (trace
      (recv (enc n1 a (pubk b)))
-     (send (enc n1 n2 (pubk a)))
+     (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
+  (comment "Needham-Schroeder-Lowe with no role origination assumptions"))
 
+(defgoal nsl
+  (forall ((a b name) (n2 text) (z0 node))
+    (implies
+     (and (p "resp" 2 z0) (p "resp" "n2" z0 n2)
+      (p "resp" "a" z0 a) (p "resp" "b" z0 b)
+      (non (privk a)) (uniq n2))
+     (exists ((z1 node))
+      (and (p "init" 1 z1) (p "init" "b" z1 b)))))
+  (comment "Responder point of view")
+  (comment "Authentication goal: agreement on name b"))
+
+(defgoal ns
+  (forall ((a b name) (n1 text) (z0 z1 node))
+    (implies
+     (and (p "init" 2 z0) (p "init" "n1" z0 n1)
+      (p "init" "a" z0 a) (p "init" "b" z0 b)
+      (p "" 0 z1) (p "" "x" z1 n1)
+      (non (privk a)) (non (privk b)) (uniq n1))
+     (false)))
+  (comment "Initiator point of view")
+  (comment "Secrecy goal: nonce n1 not revealed"))
+
+(defprotocol unilateral basic
+  (defrole init
+    (vars (a name) (n text))
+    (trace
+     (send (enc n (pubk a)))
+     (recv n)))
+  (defrole resp
+    (vars (a name) (n text))
+    (trace
+     (recv (enc n (pubk a)))
+     (send n)))
+  (comment "Unilateral authentication"))
+
+(defgoal unilateral
+  (forall ((a name) (n text)
+           (z0 node))
+   (implies
+    (and (p "init" 1 z0)
+     (p "init" "n" z0 n)
+     (p "init" "a" z0 a)
+     (non (privk a)) (uniq n))
+    (exists ((z1 node))
+     (and (p "resp" 1 z1)
+      (p "resp" "a" z1 a)))))
+  (comment "Unilateral authentication goal"))
+
 ;;; Does initiator satisfy the unilateral authentication goal?
 
 ;;; Note that the goal requires translation of some of the role
 ;;; specific predicates.
 (defgoal ns
   (forall ((a name) (n text) (z0 node))
-	  (implies
-	   (and 
-	    (p "init" 1 z0)
-	    (p "init" "n1" z0 n)
-	    (p "init" "b" z0 a)
-	    (non (privk a))
-	    (uniq n))
-	   (exists ((z1 node))
-		   (and
-		    (p "resp" 1 z1)
-		    (p "resp" "b" z1 a)))))
+   (implies
+    (and (p "init" 1 z0) (p "init" "n1" z0 n)
+     (p "init" "b" z0 a) (non (privk a)) (uniq n))
+    (exists ((z1 node))
+     (and (p "resp" 1 z1) (p "resp" "b" z1 a)))))
   (comment "Initiator authentication goal")
   (comment "Same as unilateral goal under the predicate mapping:")
   (comment (p "init" "n") "->" (p "init" "n1") "and")
   (comment (p "init" "a") "->" (p "init" "b") "and")
   (comment (p "resp" "a") "->" (p "resp" "b")))
-  
+
 ;;; Does responder satisfy the unilateral authentication goal?
 
 (defgoal ns
   (forall ((a name) (n text) (z0 node))
-	  (implies
-	   (and 
-	    (p "resp" 2 z0)
-	    (p "resp" "n2" z0 n)
-	    (p "resp" "a" z0 a)
-	    (non (privk a))
-	    (uniq n))
-	   (exists ((z1 node))
-		   (and
-		    (p "init" 2 z1)
-		    (p "init" "a" z1 a)))))
+   (implies
+    (and (p "resp" 2 z0) (p "resp" "n2" z0 n)
+     (p "resp" "a" z0 a) (non (privk a)) (uniq n))
+    (exists ((z1 node))
+     (and (p "init" 2 z1) (p "init" "a" z1 a)))))
   (comment "Responder authentication goal")
   (comment "Same as unilateral goal under the predicate mapping:")
   (comment (p "init" 1) "->" (p "resp" 2) "and")
@@ -94,172 +151,175 @@
 
 (defgoal ns
   (forall ((a b name) (n text) (z0 node))
-	  (implies
-	   (and 
-	    (p "init" 1 z0)
-	    (p "init" "n1" z0 n)
-	    (p "init" "a" z0 a)
-	    (p "init" "b" z0 b)
-	    (non (privk a))
-	    (non (privk b))
-	    (uniq n))
-	   (exists ((z1 node))
-		   (and
-		    (p "resp" 1 z1)
-		    (p "resp" "b" z1 b)))))
+    (implies
+     (and
+      (p "init" 1 z0) (p "init" "n1" z0 n)
+      (p "init" "a" z0 a) (p "init" "b" z0 b)
+      (non (privk a)) (non (privk b)) (uniq n))
+     (exists ((z1 node))
+      (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))
   (forall ((a b name) (n text) (z0 node))
-	  (implies
-	   (and 
-	    (p "init" 1 z0)
-	    (p "init" "n1" z0 n)
-	    (p "init" "a" z0 a)
-	    (p "init" "b" z0 b)
-	    (non (privk a))
-	    (non (privk b))
-	    (uniq n))
-	   (exists ((z1 node))
-		   (and
-		    (p "resp" 1 z1)
-		    (p "resp" "a" z1 a)))))
-  (comment "Double initiator authentication goal"))
-  
+   (implies
+     (and
+      (p "init" 1 z0) (p "init" "n1" z0 n)
+      (p "init" "a" z0 a) (p "init" "b" z0 b)
+      (non (privk a)) (non (privk b)) (uniq n))
+     (exists ((z1 node))
+      (and (p "resp" 1 z1) (p "resp" "a" z1 a)))))
+  (comment "Two initiator authentication goals"))
+
+;;; The shape analysis sentence as input (kind of useless)
+
 (defgoal ns
-  (forall ((a b name) (n text) (z0 node))
-	  (implies
-	   (and 
-	    (p "resp" 2 z0)
-	    (p "resp" "n2" z0 n)
-	    (p "resp" "a" z0 a)
-	    (p "resp" "b" z0 b)
-	    (non (privk a))
-	    (non (privk b))
-	    (uniq n))
-	   (exists ((z1 node))
-		   (and
-		    (p "init" 2 z1)
-		    (p "init" "a" z1 a)))))
-  (forall ((a b name) (n text) (z0 node))
-	  (implies
-	   (and 
-	    (p "resp" 2 z0)
-	    (p "resp" "n2" z0 n)
-	    (p "resp" "a" z0 a)
-	    (p "resp" "b" z0 b)
-	    (non (privk a))
-	    (non (privk b))
-	    (uniq n))
-	   (exists ((z1 node))
-		   (and
-		    (p "init" 2 z1)
-		    (p "init" "b" z1 b)))))
-  (comment "Double responder authentication goal"))
+  (forall ((n1 n2 text) (b a name) (z z-0 node))
+    (implies
+      (and (p "init" 0 z) (p "init" 2 z-0)
+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)
+        (str-prec z z-0) (non (privk b)) (uniq-at n1 z))
+      (exists ((n2-0 text) (z-1 z-2 z-3 node))
+        (and (p "init" 1 z-1) (p "resp" 0 z-2)
+          (p "resp" 1 z-3) (p "resp" "n2" z-3 n2-0)
+          (p "resp" "n1" z-3 n1) (p "resp" "b" z-3 b)
+          (p "resp" "a" z-3 a) (prec z z-2) (prec z-3 z-1)
+          (str-prec z z-1) (str-prec z-1 z-0)
+          (str-prec z-2 z-3)))))
+  (comment "Shape analysis sentence"))
 
-;;; Old stuff
+;;; Section 2 --- Additional Examples
 
-;;; The initiator point-of-view
+(defgoal ns
+  (forall ((a b name) (n2 text) (z0 z1 node))
+    (implies
+     (and
+      (p "resp" 2 z0) (p "resp" "n2" z0 n2)
+      (p "resp" "a" z0 a) (p "resp" "b" z0 b)
+      (p "" 0 z1) (p "" "x" z1 n2)
+      (non (privk a)) (non (privk b)) (uniq n2))
+     (false)))
+  (comment "Responder point of view")
+  (comment "Failed secrecy goal: nonce n2 not revealed"))
+
+;;; Double initiator point of view
 (defskeleton ns
-  (vars (a b name) (n1 text))
+  (vars (a b name) (n1 n1-0 text))
   (defstrand init 3 (a a) (b b) (n1 n1))
+  (defstrand init 3 (a a) (b b) (n1 n1-0))
   (non-orig (privk b) (privk a))
-  (uniq-orig n1)
+  (uniq-orig n1 n1-0)
   (goals
-   (forall ((a b name) (n1 text) (no nu node))
-	   (implies
-	    (and (p "init" 2 no)
-		 (p "init" "a" no a)
-		 (p "init" "b" no b)
-		 (p "init" "n1" no n1)
-		 (p "init" 0 nu)
-		 (str-prec nu no)
-		 (non (privk a))
-		 (non (privk b))
-		 (uniq-at n1 nu))
-	    (exists ((na nb node))
-		    (and (p "init" 2 na)
-			 (p "resp" 1 nb)
-			 (p "init" "b" na b)
-			 (p "resp" "b" nb b))))))
-  (comment "Initiator point-of-view"))
+   (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))
+    (implies
+     (and
+      (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)
+      (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
+      (p "init" "a" z-0 a) (p "init" "b" z-0 b)
+      (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)
+      (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)
+      (str-prec z-1 z-2) (non (privk a)) (non (privk b))
+      (uniq-at n1 z) (uniq-at n1-0 z-1))
+     (= z-1 z))))
+  (comment "Double initiator point of view"))
 
-(defgoal ns
-  (forall ((a b name) (n1 text) (no nu node))
-	  (implies
-	   (and (p "init" 2 no)
-		(p "init" "a" no a)
-		(p "init" "b" no b)
-		(p "init" "n1" no n1)
-		(p "init" 0 nu)
-		(str-prec nu no)
-		(non (privk a))
-		(non (privk b))
-		(uniq-at n1 nu))
-	   (exists ((na nb node))
-		   (and (p "init" 2 na)
-			(p "resp" 1 nb)
-			(p "init" "b" na b)
-			(p "resp" "b" nb b)))))
-  (comment "Initiator point-of-view"))
+(defprotocol nsl-typeless basic
+  (defrole init
+    (vars (a b name) (n1 text) (n2 mesg))
+    (trace
+     (send (enc a n1 (pubk b)))
+     (recv (enc n1 n2 b (pubk a)))
+     (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 text) (n1 mesg))
+    (trace
+     (recv (enc a n1 (pubk b)))
+     (send (enc n1 n2 b (pubk a)))
+     (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder-Lowe with untyped nonces"))
 
-;;; The responder point-of-view
+;;; The responder point of view
+(defgoal nsl-typeless
+  (forall ((n2 text) (a b name) (z z-0 node))
+    (implies
+      (and (p "resp" 1 z) (p "" 0 z-0)
+        (p "resp" "n2" z n2) (p "resp" "b" z b) (p "resp" "a" z a)
+        (p "" "x" z-0 n2) (non (privk a)) (non (privk b)) (uniq n2))
+      (false)))
+  (comment "Shows typeflaw in typeless NSL"))
+
 (defskeleton ns
   (vars (a name) (n2 text))
   (defstrand resp 3 (a a) (n2 n2))
   (non-orig (privk a))
   (uniq-orig n2)
   (goals
-  (forall ((n2 n1 text) (a b name) (z z-0 node))
+   (forall ((n1 n2 text) (a b name) (z z-0 node))
     (implies
-      (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)
-        (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b) (p "resp" "a" z-0 a)
-        (str-prec z z-0) (non (privk a)) (uniq-at n2 z))
-      (exists ((b-0 name) (z-1 z-2 node))
-        (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)
-          (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)
-          (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)
-          (str-prec z-1 z-2))))))
-  (comment "Responder point-of-view"))
+      (and (p "init" 0 z) (p "init" 2 z-0)
+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)
+        (str-prec z z-0) (non (privk a)) (non (privk b))
+        (uniq-at n1 z))
+      (exists ((z-1 z-2 z-3 node))
+        (and (p "init" 1 z-1) (p "resp" 0 z-2)
+          (p "resp" 1 z-3) (p "resp" "n2" z-3 n2)
+          (p "resp" "n1" z-3 n1) (p "resp" "b" z-3 b)
+          (p "resp" "a" z-3 a) (prec z z-2) (prec z-3 z-1)
+          (str-prec z z-1) (str-prec z-1 z-0)
+          (str-prec z-2 z-3))))))
+  (comment "Responder point of view with SAS"))
 
-;;; The responder point-of-view
 (defskeleton ns
   (vars (a name) (n2 text))
   (defstrand resp 3 (a a) (n2 n2))
   (non-orig (privk a))
   (uniq-orig n2)
   (goals
-   (forall ((n2 n1 text) (a b name) (z z-0 node))
+   (forall ((n1 n2 text) (a b name) (z z-0 node))
     (implies
-      (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)
-        (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b) (p "resp" "a" z-0 a)
-        (str-prec z z-0) (non (privk a)) (uniq-at n2 z))
-      (exists ((b-0 name) (z-1 z-2 node))
-        (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)
-          (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)
-          (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)
-          (str-prec z-1 z-2))))))
-  (comment "Responder point-of-view"))
+      (and (p "init" 0 z) (p "init" 2 z-0)
+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)
+        (str-prec z z-0) (non (privk a)) (non (privk b))
+        (uniq-at n1 z))
+      (false))))
+  (comment "Responder point of view with false as the conclusion"))
 
-;;; Double initiator point-of-view
 (defskeleton ns
-  (vars (a b name) (n1 n1-0 text))
+  (vars (a b name) (n1 text))
   (defstrand init 3 (a a) (b b) (n1 n1))
-  (defstrand init 3 (a a) (b b) (n1 n1-0))
   (non-orig (privk b) (privk a))
-  (uniq-orig n1 n1-0)
+  (uniq-orig n1)
   (goals
-   (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))
-	   (implies
-	    (and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)
-		 (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
-		 (p "init" "a" z-0 a) (p "init" "b" z-0 b)
-		 (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)
-		 (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)
-		 (str-prec z-1 z-2) (non (privk a)) (non (privk b))
-		 (uniq-at n1 z) (uniq-at n1-0 z-1))
-	    (= z-1 z))))
-  (comment "Double initiator point-of-view"))
+   (forall ((n1 n2 text) (a b name) (z z-0 node))
+    (implies
+      (and (p "init" 0 z) (p "init" 2 z-0)
+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)
+        (str-prec z z-0) (non (privk a)) (non (privk b))
+        (uniq-at n1 z))
+      (false))))
+  (comment "Initiator point of view with false as the conclusion"))
 
+(defgoal ns
+  (forall ((a b name) (n text) (z0 node))
+   (implies
+    (and
+     (p "resp" 2 z0) (p "resp" "n2" z0 n)
+     (p "resp" "a" z0 a) (p "resp" "b" z0 b)
+     (non (privk a)) (non (privk b)) (uniq n))
+    (exists ((z1 node))
+     (and (p "init" 2 z1) (p "init" "a" z1 a)))))
+  (forall ((a b name) (n text) (z0 node))
+   (implies
+    (and
+     (p "resp" 2 z0) (p "resp" "n2" z0 n)
+     (p "resp" "a" z0 a) (p "resp" "b" z0 b)
+     (non (privk a)) (non (privk b)) (uniq n))
+    (exists ((z1 node))
+     (and (p "init" 2 z1) (p "init" "b" z1 b)))))
+  (comment "Two responder authentication goals"))
+
 ;;; Needham-Schroeder Protocol with origination assumptions on roles
-;;; This
 
 (defprotocol ns-role-origs basic
   (defrole init
@@ -280,12 +340,12 @@
     (uniq-orig n2))
   (comment "Needham-Schroeder with role assumptions that are too strong"))
 
-;;; The initiator point-of-view
+;;; The initiator point of view
 (defskeleton ns-role-origs
   (vars)
   (defstrand init 3))
 
-;;; The responder point-of-view
+;;; The responder point of view
 (defskeleton ns-role-origs
   (vars)
   (defstrand resp 3))
@@ -329,27 +389,3 @@
   (non-orig (privk a))
   (uniq-orig n1)
   (precedes ((1 1) (0 1))))
-
-(defprotocol nsl-typeless basic
-  (defrole init
-    (vars (a b name) (n1 text) (n2 mesg))
-    (trace
-     (send (enc a n1 (pubk b)))
-     (recv (enc n1 n2 b (pubk a)))
-     (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (b a name) (n2 text) (n1 mesg))
-    (trace
-     (recv (enc a n1 (pubk b)))
-     (send (enc n1 n2 b (pubk a)))
-     (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder-Lowe with untyped nonces"))
-
-;;; The responder point-of-view
-(defskeleton nsl-typeless
-  (vars (a b name) (n2 text))
-  (defstrand resp 2 (a a) (n2 n2) (b b))
-  (deflistener n2)
-  (non-orig (privk a) (privk b))
-  (uniq-orig n2)
-  (comment "Shows typeflaw in typeless NSL"))
diff --git a/tst/goals.tst b/tst/goals.tst
--- a/tst/goals.tst
+++ b/tst/goals.tst
@@ -1,1117 +1,1645 @@
 (herald goals)
 
-(comment "CPSA 2.5.0")
-(comment "All input read from goals.scm")
-
-(defprotocol unilateral basic
-  (defrole init
-    (vars (a name) (n text))
-    (trace (send (enc n (pubk a))) (recv n)))
-  (defrole resp
-    (vars (a name) (n text))
-    (trace (recv (enc n (pubk a))) (send n))))
-
-(defskeleton unilateral
-  (vars (n text) (a name))
-  (defstrand init 2 (n n) (a a))
-  (non-orig (privk a))
-  (uniq-orig n)
-  (goals
-    (forall ((a name) (n text) (z0 node))
-      (implies
-        (and (p "init" 1 z0) (p "init" "n" z0 n) (p "init" "a" z0 a)
-          (non (privk a)) (uniq n))
-        (exists ((z1 node))
-          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
-  (comment "Authentication goal")
-  (traces ((send (enc n (pubk a))) (recv n)))
-  (label 0)
-  (unrealized (0 1))
-  (origs (n (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton unilateral
-  (vars (n text) (a name))
-  (defstrand init 2 (n n) (a a))
-  (defstrand resp 2 (n n) (a a))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a))
-  (uniq-orig n)
-  (operation nonce-test (added-strand resp 2) n (0 1) (enc n (pubk a)))
-  (traces ((send (enc n (pubk a))) (recv n))
-    ((recv (enc n (pubk a))) (send n)))
-  (label 1)
-  (parent 0)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0) ((a a) (n n))))
-  (origs (n (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n n2 text) (a a-0 name))
-  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
-  (non-orig (privk a))
-  (uniq-orig n)
-  (goals
-    (forall ((a name) (n text) (z0 node))
-      (implies
-        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "b" z0 a)
-          (non (privk a)) (uniq n))
-        (exists ((z1 node))
-          (and (p "resp" 1 z1) (p "resp" "b" z1 a))))))
-  (comment "Initiator authentication goal"
-    "Same as unilateral goal under the predicate mapping:"
-    (p "init" "n") "->" (p "init" "n1") "and" (p "init" "a") "->"
-    (p "init" "b") "and" (p "resp" "a") "->" (p "resp" "b"))
-  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0)))))
-  (label 2)
-  (unrealized (0 1))
-  (origs (n (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n n2 n2-0 text) (a a-0 name))
-  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
-  (defstrand resp 2 (n1 n) (n2 n2-0) (a a-0) (b a))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a))
-  (uniq-orig n)
-  (operation nonce-test (added-strand resp 2) n (0 1)
-    (enc n a-0 (pubk a)))
-  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0))))
-    ((recv (enc n a-0 (pubk a))) (send (enc n n2-0 (pubk a-0)))))
-  (label 3)
-  (parent 2)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0) ((a a) (n n) (a-0 a-0) (n2 n2))))
-  (origs (n (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n n1 text) (a b name))
-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))
-  (non-orig (privk a))
-  (uniq-orig n)
-  (goals
-    (forall ((a name) (n text) (z0 node))
-      (implies
-        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
-          (non (privk a)) (uniq n))
-        (exists ((z1 node))
-          (and (p "init" 2 z1) (p "init" "a" z1 a))))))
-  (comment "Responder authentication goal"
-    "Same as unilateral goal under the predicate mapping:" (p "init" 1)
-    "->" (p "resp" 2) "and" (p "init" "n") "->" (p "resp" "n2") "and"
-    (p "init" "a") "->" (p "resp" "a") "and" (p "resp" 1) "->"
-    (p "init" 2) "and" (p "resp" "a") "->" (p "init" "a"))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
-      (recv (enc n (pubk b)))))
-  (label 4)
-  (unrealized (0 2))
-  (origs (n (0 1)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n n1 text) (a b b-0 name))
-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))
-  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
-  (non-orig (privk a))
-  (uniq-orig n)
-  (operation nonce-test (added-strand init 3) n (0 2)
-    (enc n1 n (pubk a)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
-      (recv (enc n (pubk b))))
-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))
-      (send (enc n (pubk b-0)))))
-  (label 5)
-  (parent 4)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0) ((a a) (n n) (b b) (n1 n1))))
-  (origs (n (0 1))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n n2 text) (a b name))
-  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n)
-  (goals
-    (forall ((a b name) (n text) (z0 node))
-      (implies
-        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
-          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
-        (exists ((z1 node)) (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))
-    (forall ((a b name) (n text) (z0 node))
-      (implies
-        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
-          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
-        (exists ((z1 node))
-          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
-  (comment "Double initiator authentication goal")
-  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a)))))
-  (label 6)
-  (unrealized (0 1))
-  (origs (n (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n n2 n2-0 text) (a b name))
-  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n) (n2 n2-0) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n)
-  (operation nonce-test (added-strand resp 2) n (0 1)
-    (enc n a (pubk b)))
-  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))
-    ((recv (enc n a (pubk b))) (send (enc n n2-0 (pubk a)))))
-  (label 7)
-  (parent 6)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n n2 text) (a b name))
-  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n) (n2 n2) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n)
-  (operation nonce-test (contracted (n2-0 n2)) n (0 1)
-    (enc n n2 (pubk a)) (enc n a (pubk b)))
-  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))
-    ((recv (enc n a (pubk b))) (send (enc n n2 (pubk a)))))
-  (label 8)
-  (parent 7)
-  (unrealized)
-  (shape)
-  (satisfies yes yes)
-  (maps ((0) ((a a) (b b) (n n) (n2 n2))))
-  (origs (n (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n n1 text) (a b name))
-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n)
-  (goals
-    (forall ((a b name) (n text) (z0 node))
-      (implies
-        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
-          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
-        (exists ((z1 node)) (and (p "init" 2 z1) (p "init" "a" z1 a)))))
-    (forall ((a b name) (n text) (z0 node))
-      (implies
-        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
-          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
-        (exists ((z1 node))
-          (and (p "init" 2 z1) (p "init" "b" z1 b))))))
-  (comment "Double responder authentication goal")
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
-      (recv (enc n (pubk b)))))
-  (label 9)
-  (unrealized (0 2))
-  (origs (n (0 1)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n n1 text) (a b b-0 name))
-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))
-  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n)
-  (operation nonce-test (added-strand init 3) n (0 2)
-    (enc n1 n (pubk a)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
-      (recv (enc n (pubk b))))
-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))
-      (send (enc n (pubk b-0)))))
-  (label 10)
-  (parent 9)
-  (unrealized)
-  (shape)
-  (satisfies yes (no (a a) (b b) (n n) (z0 (0 2))))
-  (maps ((0) ((a a) (b b) (n n) (n1 n1))))
-  (origs (n (0 1))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (goals
-    (forall ((a b name) (n1 text) (no nu node))
-      (implies
-        (and (p "init" 2 no) (p "init" "a" no a) (p "init" "b" no b)
-          (p "init" "n1" no n1) (p "init" 0 nu) (str-prec nu no)
-          (non (privk a)) (non (privk b)) (uniq-at n1 nu))
-        (exists ((na nb node))
-          (and (p "init" 2 na) (p "resp" 1 nb) (p "init" "b" na b)
-            (p "resp" "b" nb b))))))
-  (comment "Initiator point-of-view")
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (label 11)
-  (unrealized (0 1))
-  (origs (n1 (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n2 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (operation nonce-test (added-strand resp 2) n1 (0 1)
-    (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
-  (label 12)
-  (parent 11)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
-  (label 13)
-  (parent 12)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
-  (origs (n1 (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (goals
-    (forall ((a b name) (n1 text) (no nu node))
-      (implies
-        (and (p "init" 2 no) (p "init" "a" no a) (p "init" "b" no b)
-          (p "init" "n1" no n1) (p "init" 0 nu) (str-prec nu no)
-          (non (privk a)) (non (privk b)) (uniq-at n1 nu))
-        (exists ((na nb node))
-          (and (p "init" 2 na) (p "resp" 1 nb) (p "init" "b" na b)
-            (p "resp" "b" nb b))))))
-  (comment "Initiator point-of-view")
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (label 14)
-  (unrealized (0 1))
-  (origs (n1 (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n2 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (operation nonce-test (added-strand resp 2) n1 (0 1)
-    (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
-  (label 15)
-  (parent 14)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
-  (label 16)
-  (parent 15)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
-  (origs (n1 (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n2 n1 text) (a b name))
-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))
-  (non-orig (privk a))
-  (uniq-orig n2)
-  (goals
-    (forall ((n2 n1 text) (a b name) (z z-0 node))
-      (implies
-        (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)
-          (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b)
-          (p "resp" "a" z-0 a) (str-prec z z-0) (non (privk a))
-          (uniq-at n2 z))
-        (exists ((b-0 name) (z-1 z-2 node))
-          (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)
-            (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)
-            (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)
-            (str-prec z-1 z-2))))))
-  (comment "Responder point-of-view")
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (label 17)
-  (unrealized (0 2))
-  (origs (n2 (0 1)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n2 n1 text) (a b b-0 name))
-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
-  (non-orig (privk a))
-  (uniq-orig n2)
-  (operation nonce-test (added-strand init 3) n2 (0 2)
-    (enc n1 n2 (pubk a)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b-0)))))
-  (label 18)
-  (parent 17)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
-  (origs (n2 (0 1))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n2 n1 text) (a b name))
-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))
-  (non-orig (privk a))
-  (uniq-orig n2)
-  (goals
-    (forall ((n2 n1 text) (a b name) (z z-0 node))
-      (implies
-        (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)
-          (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b)
-          (p "resp" "a" z-0 a) (str-prec z z-0) (non (privk a))
-          (uniq-at n2 z))
-        (exists ((b-0 name) (z-1 z-2 node))
-          (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)
-            (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)
-            (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)
-            (str-prec z-1 z-2))))))
-  (comment "Responder point-of-view")
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (label 19)
-  (unrealized (0 2))
-  (origs (n2 (0 1)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n2 n1 text) (a b b-0 name))
-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
-  (non-orig (privk a))
-  (uniq-orig n2)
-  (operation nonce-test (added-strand init 3) n2 (0 2)
-    (enc n1 n2 (pubk a)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b-0)))))
-  (label 20)
-  (parent 19)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
-  (origs (n2 (0 1))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n1 n1-0 n2 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1 n1-0)
-  (goals
-    (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))
-      (implies
-        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)
-          (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
-          (p "init" "a" z-0 a) (p "init" "b" z-0 b)
-          (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)
-          (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)
-          (str-prec z-1 z-2) (non (privk a)) (non (privk b))
-          (uniq-at n1 z) (uniq-at n1-0 z-1)) (= z-1 z))))
-  (comment "Double initiator point-of-view")
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
-      (send (enc n2-0 (pubk b)))))
-  (label 21)
-  (unrealized (0 1) (1 1))
-  (origs (n1 (0 0)) (n1-0 (1 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (operation collapsed 1 0)
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (label 22)
-  (parent 21)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
-  (defstrand resp 2 (n1 n1-0) (n2 n2-1) (a a) (b b))
-  (precedes ((1 0) (2 0)) ((2 1) (1 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1 n1-0)
-  (operation nonce-test (added-strand resp 2) n1-0 (1 1)
-    (enc n1-0 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
-      (send (enc n2-0 (pubk b))))
-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-1 (pubk a)))))
-  (label 23)
-  (parent 21)
-  (unrealized (0 1) (1 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n2 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (operation nonce-test (added-strand resp 2) n1 (0 1)
-    (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
-  (label 24)
-  (parent 22)
-  (unrealized (0 1))
-  (origs (n1 (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n1-0 n2 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
-  (defstrand resp 2 (n1 n1-0) (n2 n2-0) (a a) (b b))
-  (precedes ((1 0) (2 0)) ((2 1) (1 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1 n1-0)
-  (operation nonce-test (contracted (n2-1 n2-0)) n1-0 (1 1)
-    (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
-      (send (enc n2-0 (pubk b))))
-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a)))))
-  (label 25)
-  (parent 23)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
-  (label 26)
-  (parent 24)
-  (unrealized)
-  (shape)
-  (satisfies yes)
-  (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))
-  (origs (n1 (0 0))))
-
-(defskeleton ns
-  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
-  (defstrand resp 2 (n1 n1-0) (n2 n2-0) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2-1) (a a) (b b))
-  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1 n1-0)
-  (operation nonce-test (added-strand resp 2) n1 (0 1)
-    (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
-      (send (enc n2-0 (pubk b))))
-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-1 (pubk a)))))
-  (label 27)
-  (parent 25)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns
-  (vars (n1 n1-0 n2 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))
-  (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1-0) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))
-  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1 n1-0)
-  (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1)
-    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 (pubk a)))
-      (send (enc n2-0 (pubk b))))
-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2 (pubk a))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
-  (label 28)
-  (parent 27)
-  (unrealized)
-  (shape)
-  (satisfies
-    (no (n1-0 n1) (n1 n1-0) (n2-0 n2-0) (n2 n2) (a a) (b b) (z-2 (0 0))
-      (z-1 (0 2)) (z-0 (1 0)) (z (1 2))))
-  (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2))))
-  (origs (n1 (0 0)) (n1-0 (1 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns-role-origs basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    (non-orig (privk b))
-    (uniq-orig n1))
-  (defrole resp
-    (vars (b a name) (n2 n1 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    (non-orig (privk a))
-    (uniq-orig n2))
-  (comment
-    "Needham-Schroeder with role assumptions that are too strong"))
-
-(defskeleton ns-role-origs
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (non-orig (privk b))
-  (uniq-orig n1)
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (label 29)
-  (unrealized (0 1))
-  (origs (n1 (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns-role-origs
-  (vars (n1 n2 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1 n2-0)
-  (operation nonce-test (added-strand resp 2) n1 (0 1)
-    (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
-  (label 30)
-  (parent 29)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns-role-origs
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1 n2)
-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
-  (label 31)
-  (parent 30)
-  (unrealized)
-  (shape)
-  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
-  (origs (n2 (1 1)) (n1 (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns-role-origs basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    (non-orig (privk b))
-    (uniq-orig n1))
-  (defrole resp
-    (vars (b a name) (n2 n1 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    (non-orig (privk a))
-    (uniq-orig n2))
-  (comment
-    "Needham-Schroeder with role assumptions that are too strong"))
-
-(defskeleton ns-role-origs
-  (vars (n2 n1 text) (b a name))
-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
-  (non-orig (privk a))
-  (uniq-orig n2)
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (label 32)
-  (unrealized (0 2))
-  (origs (n2 (0 1)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns-role-origs
-  (vars (n2 n1 text) (b a b-0 name))
-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
-  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
-  (non-orig (privk a) (privk b-0))
-  (uniq-orig n2 n1)
-  (operation nonce-test (added-strand init 3) n2 (0 2)
-    (enc n1 n2 (pubk a)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b-0)))))
-  (label 33)
-  (parent 32)
-  (unrealized (0 0) (0 2))
-  (comment "2 in cohort - 2 not yet seen"))
-
-(defskeleton ns-role-origs
-  (vars (n2 n1 text) (a b name))
-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n2 n1)
-  (operation nonce-test (contracted (b-0 b)) n1 (0 0)
-    (enc n1 a (pubk b)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (label 34)
-  (parent 33)
-  (unrealized)
-  (shape)
-  (maps ((0) ((b b) (a a) (n2 n2) (n1 n1))))
-  (origs (n1 (1 0)) (n2 (0 1))))
-
-(defskeleton ns-role-origs
-  (vars (n2 n1 n2-0 text) (b a b-0 name))
-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
-  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b-0) (a a))
-  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
-  (non-orig (privk a) (privk b-0))
-  (uniq-orig n2 n1 n2-0)
-  (operation nonce-test (added-strand resp 2) n1 (0 0)
-    (enc n1 a (pubk b-0)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b-0))))
-    ((recv (enc n1 a (pubk b-0))) (send (enc n1 n2-0 (pubk a)))))
-  (label 35)
-  (parent 33)
-  (unrealized (0 0) (0 2))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns-role-origs
-  (vars (n2 n1 n2-0 text) (a b name))
-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
-  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n2 n1 n2-0)
-  (operation nonce-test (contracted (b-0 b)) n1 (0 0)
-    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
-  (traces
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
-  (label 36)
-  (parent 35)
-  (seen 34)
-  (unrealized)
-  (comment "1 in cohort - 0 not yet seen"))
-
-(comment "Nothing left to do")
-
-(defprotocol ns2 basic
-  (defrole init
-    (vars (a b name) (n1 n2 n3 text))
-    (trace (send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (b a name) (n2 n1 text))
-    (trace (recv (enc n1 n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b))))
-    (note doubled nonce in the first message))
-  (note that this protocol is derived from Needham-Schroeder))
-
-(defskeleton ns2
-  (vars (n1 n2 n3 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (traces
-    ((send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (label 37)
-  (unrealized (0 1))
-  (origs (n1 (0 0)))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns2
-  (vars (n2 n3 n2-0 text) (a b name))
-  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))
-  (defstrand resp 2 (n2 n2-0) (n1 n3) (b b) (a a))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n3)
-  (operation nonce-test (added-strand resp 2) n3 (0 1)
-    (enc n3 n3 a (pubk b)))
-  (traces
-    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2-0 (pubk a)))))
-  (label 38)
-  (parent 37)
-  (unrealized (0 1))
-  (comment "1 in cohort - 1 not yet seen"))
-
-(defskeleton ns2
-  (vars (n3 n2 text) (a b name))
-  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))
-  (defstrand resp 2 (n2 n2) (n1 n3) (b b) (a a))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n3)
-  (operation nonce-test (contracted (n2-0 n2)) n3 (0 1)
-    (enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)))
-  (traces
-    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2 (pubk a)))))
-  (label 39)
-  (parent 38)
-  (unrealized)
-  (shape)
-  (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3))))
-  (origs (n3 (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol ns basic
-  (defrole init
-    (vars (a b name) (n1 n2 text))
-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (a b name) (n1 n2 text))
-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder"))
-
-(defskeleton ns
-  (vars (n1 n2 text) (a b name))
-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))
-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n1)
-  (traces
-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
-      (send (enc n2 (pubk b))))
-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
-  (label 40)
-  (unrealized)
-  (shape)
-  (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b))))
-  (origs (n1 (0 0))))
-
-(comment "Nothing left to do")
-
-(defprotocol nsl-typeless basic
-  (defrole init
-    (vars (a b name) (n1 text) (n2 mesg))
-    (trace (send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (defrole resp
-    (vars (b a name) (n2 text) (n1 mesg))
-    (trace (recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))
-      (recv (enc n2 (pubk b)))))
-  (comment "Needham-Schroeder-Lowe with untyped nonces"))
-
-(defskeleton nsl-typeless
-  (vars (n1 mesg) (n2 text) (a b name))
-  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
-  (deflistener n2)
-  (non-orig (privk a) (privk b))
-  (uniq-orig n2)
-  (comment "Shows typeflaw in typeless NSL")
-  (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))
-    ((recv n2) (send n2)))
-  (label 41)
-  (unrealized (1 0))
-  (preskeleton)
-  (comment "Not a skeleton"))
-
-(defskeleton nsl-typeless
-  (vars (n1 mesg) (n2 text) (a b name))
-  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
-  (deflistener n2)
-  (precedes ((0 1) (1 0)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n2)
-  (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))
-    ((recv n2) (send n2)))
-  (label 42)
-  (parent 41)
-  (unrealized (1 0))
-  (origs (n2 (0 1)))
-  (comment "2 in cohort - 2 not yet seen"))
-
-(defskeleton nsl-typeless
-  (vars (n2 n1 text) (a b name))
-  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
-  (deflistener n2)
-  (defstrand init 3 (n2 n2) (n1 n1) (a a) (b b))
-  (precedes ((0 1) (2 1)) ((2 2) (1 0)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n2)
-  (operation nonce-test (added-strand init 3) n2 (1 0)
-    (enc n1 n2 b (pubk a)))
-  (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))
-    ((recv n2) (send n2))
-    ((send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))
-      (send (enc n2 (pubk b)))))
-  (label 43)
-  (parent 42)
-  (unrealized (1 0))
-  (comment "empty cohort"))
-
-(defskeleton nsl-typeless
-  (vars (n2 n2-0 text) (a b a-0 name))
-  (defstrand resp 2 (n1 a-0) (n2 n2) (b b) (a a))
-  (deflistener n2)
-  (defstrand resp 2 (n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0))
-  (precedes ((0 1) (2 0)) ((2 1) (1 0)))
-  (non-orig (privk a) (privk b))
-  (uniq-orig n2)
-  (operation nonce-test (added-strand resp 2) n2 (1 0)
-    (enc a-0 n2 b (pubk a)))
-  (traces ((recv (enc a a-0 (pubk b))) (send (enc a-0 n2 b (pubk a))))
-    ((recv n2) (send n2))
-    ((recv (enc a-0 n2 b (pubk a)))
-      (send (enc (cat n2 b) n2-0 a (pubk a-0)))))
-  (label 44)
-  (parent 42)
-  (unrealized)
-  (shape)
-  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 a-0))))
-  (origs (n2 (0 1))))
+(comment "CPSA 2.5.1")
+(comment "All input read from goals.scm")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (b a name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (non-orig (privk b))
+  (uniq-orig n1)
+  (goals
+    (forall ((b name) (n1 text) (z0 node))
+      (implies
+        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)
+          (non (privk b)) (uniq n1))
+        (exists ((z1 node))
+          (and (p "resp" 1 z1) (p "resp" "b" z1 b))))))
+  (comment "Initiator point of view"
+    "Authentication goal: agreement on name b")
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 0)
+  (unrealized (0 1))
+  (origs (n1 (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (b a name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (0 1)
+    (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 1)
+  (parent 0)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))
+  (origs (n1 (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (b a name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (non-orig (privk b))
+  (uniq-orig n1)
+  (goals
+    (forall ((b name) (n1 text) (z0 node))
+      (implies
+        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)
+          (non (privk b)) (uniq n1))
+        (exists ((z1 node))
+          (and (p "resp" 1 z1) (p "resp" "b" z1 b) (prec z1 z0))))))
+  (comment "Prec example")
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 2)
+  (unrealized (0 1))
+  (origs (n1 (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (b a name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (0 1)
+    (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 3)
+  (parent 2)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))
+  (origs (n1 (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (goals
+    (forall ((a b name) (n2 text) (z0 node))
+      (implies
+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
+          (p "resp" "b" z0 b) (non (privk a)) (uniq n2))
+        (exists ((z1 node))
+          (and (p "init" 1 z1) (p "init" "b" z1 b))))))
+  (comment "Responder point of view"
+    "Failed authentication goal: agreement on name b")
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (label 4)
+  (unrealized (0 2))
+  (origs (n2 (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b b-0 name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand init 3) n2 (0 2)
+    (enc n1 n2 (pubk a)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0)))))
+  (label 5)
+  (parent 4)
+  (unrealized)
+  (shape)
+  (satisfies (no (a a) (b b) (n2 n2) (z0 (0 2))))
+  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
+  (origs (n2 (0 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol nsl basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment
+    "Needham-Schroeder-Lowe with no role origination assumptions"))
+
+(defskeleton nsl
+  (vars (n2 n1 text) (a b name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (goals
+    (forall ((a b name) (n2 text) (z0 node))
+      (implies
+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
+          (p "resp" "b" z0 b) (non (privk a)) (uniq n2))
+        (exists ((z1 node))
+          (and (p "init" 1 z1) (p "init" "b" z1 b))))))
+  (comment "Responder point of view"
+    "Authentication goal: agreement on name b")
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (label 6)
+  (unrealized (0 2))
+  (origs (n2 (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton nsl
+  (vars (n2 n1 text) (a b name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand init 3) n2 (0 2)
+    (enc n1 n2 b (pubk a)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 7)
+  (parent 6)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
+  (origs (n2 (0 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (deflistener n1)
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (goals
+    (forall ((a b name) (n1 text) (z0 z1 node))
+      (implies
+        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "a" z0 a)
+          (p "init" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n1)
+          (non (privk a)) (non (privk b)) (uniq n1)) (false))))
+  (comment "Initiator point of view"
+    "Secrecy goal: nonce n1 not revealed")
+  (traces ((recv n1))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 8)
+  (unrealized (0 0) (1 1))
+  (preskeleton)
+  (comment "Not a skeleton"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (deflistener n1)
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (precedes ((1 0) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (traces ((recv n1))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 9)
+  (parent 8)
+  (unrealized (0 0) (1 1))
+  (origs (n1 (1 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (a b name))
+  (deflistener n1)
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (1 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (1 1)
+    (enc n1 a (pubk b)))
+  (traces ((recv n1))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 10)
+  (parent 9)
+  (unrealized (0 0) (1 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (deflistener n1)
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (1 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (contracted (n2-0 n2)) n1 (1 1)
+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
+  (traces ((recv n1))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
+  (label 11)
+  (parent 10)
+  (unrealized (0 0))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (deflistener n1)
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (precedes ((1 0) (2 0)) ((2 1) (0 0)) ((2 1) (1 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (displaced 3 2 resp 2) n1 (0 0)
+    (enc n1 a (pubk b)))
+  (traces ((recv n1))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
+  (label 12)
+  (parent 11)
+  (unrealized (0 0))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (a b name))
+  (deflistener n1)
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((1 0) (2 0)) ((1 0) (3 0)) ((2 1) (1 1)) ((3 1) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (0 0)
+    (enc n1 a (pubk b)))
+  (traces ((recv n1))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 13)
+  (parent 11)
+  (seen 15)
+  (unrealized (0 0))
+  (comment "1 in cohort - 0 not yet seen"))
+
+(defskeleton ns
+  (vars (n2 text) (a b name))
+  (deflistener n2)
+  (defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))
+  (precedes ((1 0) (2 0)) ((1 2) (0 0)) ((2 1) (1 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (operation nonce-test (displaced 3 1 init 3) n2 (0 0)
+    (enc n2 n2 (pubk a)) (enc n2 a (pubk b)))
+  (traces ((recv n2))
+    ((send (enc n2 a (pubk b))) (recv (enc n2 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n2 a (pubk b))) (send (enc n2 n2 (pubk a)))))
+  (label 14)
+  (parent 12)
+  (unrealized (0 0))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (a b name))
+  (deflistener n1)
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((1 0) (2 0)) ((1 0) (3 0)) ((2 1) (0 0)) ((2 1) (1 1))
+    ((3 1) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (0 0)
+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
+  (traces ((recv n1))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 15)
+  (parent 12)
+  (seen 16)
+  (unrealized (0 0))
+  (comment "1 in cohort - 0 not yet seen"))
+
+(defskeleton ns
+  (vars (n2 n2-0 text) (a b name))
+  (deflistener n2)
+  (defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))
+  (defstrand resp 2 (n2 n2-0) (n1 n2) (b b) (a a))
+  (precedes ((1 0) (2 0)) ((1 0) (3 0)) ((1 2) (0 0)) ((2 1) (1 1))
+    ((3 1) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand resp 2) n2 (0 0) (enc n2 (pubk b))
+    (enc n2 n2 (pubk a)) (enc n2 a (pubk b)))
+  (traces ((recv n2))
+    ((send (enc n2 a (pubk b))) (recv (enc n2 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n2 a (pubk b))) (send (enc n2 n2 (pubk a))))
+    ((recv (enc n2 a (pubk b))) (send (enc n2 n2-0 (pubk a)))))
+  (label 16)
+  (parent 14)
+  (unrealized (0 0))
+  (comment "empty cohort"))
+
+(comment "Nothing left to do")
+
+(defprotocol unilateral basic
+  (defrole init
+    (vars (a name) (n text))
+    (trace (send (enc n (pubk a))) (recv n)))
+  (defrole resp
+    (vars (a name) (n text))
+    (trace (recv (enc n (pubk a))) (send n)))
+  (comment "Unilateral authentication"))
+
+(defskeleton unilateral
+  (vars (n text) (a name))
+  (defstrand init 2 (n n) (a a))
+  (non-orig (privk a))
+  (uniq-orig n)
+  (goals
+    (forall ((a name) (n text) (z0 node))
+      (implies
+        (and (p "init" 1 z0) (p "init" "n" z0 n) (p "init" "a" z0 a)
+          (non (privk a)) (uniq n))
+        (exists ((z1 node))
+          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
+  (comment "Unilateral authentication goal")
+  (traces ((send (enc n (pubk a))) (recv n)))
+  (label 17)
+  (unrealized (0 1))
+  (origs (n (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton unilateral
+  (vars (n text) (a name))
+  (defstrand init 2 (n n) (a a))
+  (defstrand resp 2 (n n) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a))
+  (uniq-orig n)
+  (operation nonce-test (added-strand resp 2) n (0 1) (enc n (pubk a)))
+  (traces ((send (enc n (pubk a))) (recv n))
+    ((recv (enc n (pubk a))) (send n)))
+  (label 18)
+  (parent 17)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((a a) (n n))))
+  (origs (n (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n n2 text) (a a-0 name))
+  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
+  (non-orig (privk a))
+  (uniq-orig n)
+  (goals
+    (forall ((a name) (n text) (z0 node))
+      (implies
+        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "b" z0 a)
+          (non (privk a)) (uniq n))
+        (exists ((z1 node))
+          (and (p "resp" 1 z1) (p "resp" "b" z1 a))))))
+  (comment "Initiator authentication goal"
+    "Same as unilateral goal under the predicate mapping:"
+    (p "init" "n") "->" (p "init" "n1") "and" (p "init" "a") "->"
+    (p "init" "b") "and" (p "resp" "a") "->" (p "resp" "b"))
+  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0)))))
+  (label 19)
+  (unrealized (0 1))
+  (origs (n (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n n2 n2-0 text) (a a-0 name))
+  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
+  (defstrand resp 2 (n2 n2-0) (n1 n) (b a) (a a-0))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a))
+  (uniq-orig n)
+  (operation nonce-test (added-strand resp 2) n (0 1)
+    (enc n a-0 (pubk a)))
+  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0))))
+    ((recv (enc n a-0 (pubk a))) (send (enc n n2-0 (pubk a-0)))))
+  (label 20)
+  (parent 19)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((a a) (n n) (a-0 a-0) (n2 n2))))
+  (origs (n (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n n1 text) (a b name))
+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
+  (non-orig (privk a))
+  (uniq-orig n)
+  (goals
+    (forall ((a name) (n text) (z0 node))
+      (implies
+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
+          (non (privk a)) (uniq n))
+        (exists ((z1 node))
+          (and (p "init" 2 z1) (p "init" "a" z1 a))))))
+  (comment "Responder authentication goal"
+    "Same as unilateral goal under the predicate mapping:" (p "init" 1)
+    "->" (p "resp" 2) "and" (p "init" "n") "->" (p "resp" "n2") "and"
+    (p "init" "a") "->" (p "resp" "a") "and" (p "resp" 1) "->"
+    (p "init" 2) "and" (p "resp" "a") "->" (p "init" "a"))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
+      (recv (enc n (pubk b)))))
+  (label 21)
+  (unrealized (0 2))
+  (origs (n (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n n1 text) (a b b-0 name))
+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (privk a))
+  (uniq-orig n)
+  (operation nonce-test (added-strand init 3) n (0 2)
+    (enc n1 n (pubk a)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
+      (recv (enc n (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))
+      (send (enc n (pubk b-0)))))
+  (label 22)
+  (parent 21)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((a a) (n n) (b b) (n1 n1))))
+  (origs (n (0 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n n2 text) (a b name))
+  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n)
+  (goals
+    (forall ((a b name) (n text) (z0 node))
+      (implies
+        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
+          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
+        (exists ((z1 node)) (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))
+    (forall ((a b name) (n text) (z0 node))
+      (implies
+        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
+          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
+        (exists ((z1 node))
+          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
+  (comment "Two initiator authentication goals")
+  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a)))))
+  (label 23)
+  (unrealized (0 1))
+  (origs (n (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n n2 n2-0 text) (a b name))
+  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n)
+  (operation nonce-test (added-strand resp 2) n (0 1)
+    (enc n a (pubk b)))
+  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))
+    ((recv (enc n a (pubk b))) (send (enc n n2-0 (pubk a)))))
+  (label 24)
+  (parent 23)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n n2 text) (a b name))
+  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n)
+  (operation nonce-test (contracted (n2-0 n2)) n (0 1)
+    (enc n n2 (pubk a)) (enc n a (pubk b)))
+  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))
+    ((recv (enc n a (pubk b))) (send (enc n n2 (pubk a)))))
+  (label 25)
+  (parent 24)
+  (unrealized)
+  (shape)
+  (satisfies yes yes)
+  (maps ((0) ((a a) (b b) (n n) (n2 n2))))
+  (origs (n (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (b a name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (non-orig (privk b))
+  (uniq-orig n1)
+  (goals
+    (forall ((n1 n2 text) (b a name) (z z-0 node))
+      (implies
+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk b))
+          (uniq-at n1 z))
+        (exists ((n2-0 text) (z-1 z-2 z-3 node))
+          (and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)
+            (p "resp" "n2" z-3 n2-0) (p "resp" "n1" z-3 n1)
+            (p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)
+            (prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)
+            (str-prec z-2 z-3))))))
+  (comment "Shape analysis sentence")
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 26)
+  (unrealized (0 1))
+  (origs (n1 (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (b a name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (0 1)
+    (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 27)
+  (parent 26)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((n1 n1) (n2 n2) (b b) (a a))))
+  (origs (n1 (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b name))
+  (deflistener n2)
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (goals
+    (forall ((a b name) (n2 text) (z0 z1 node))
+      (implies
+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
+          (p "resp" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n2)
+          (non (privk a)) (non (privk b)) (uniq n2)) (false))))
+  (comment "Responder point of view"
+    "Failed secrecy goal: nonce n2 not revealed")
+  (traces ((recv n2))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (label 28)
+  (unrealized (0 0) (1 2))
+  (preskeleton)
+  (comment "Not a skeleton"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b name))
+  (deflistener n2)
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (precedes ((1 1) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (traces ((recv n2))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (label 29)
+  (parent 28)
+  (unrealized (0 0) (1 2))
+  (origs (n2 (1 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b b-0 name))
+  (deflistener n2)
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (precedes ((1 1) (0 0)) ((1 1) (2 1)) ((2 2) (1 2)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand init 3) n2 (1 2)
+    (enc n1 n2 (pubk a)))
+  (traces ((recv n2))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0)))))
+  (label 30)
+  (parent 29)
+  (unrealized (0 0))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b b-0 name))
+  (deflistener n2)
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (precedes ((1 1) (2 1)) ((2 2) (0 0)) ((2 2) (1 2)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (operation nonce-test (displaced 3 2 init 3) n2 (0 0)
+    (enc n1 n2 (pubk a)))
+  (traces ((recv n2))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0)))))
+  (label 31)
+  (parent 30)
+  (unrealized)
+  (shape)
+  (satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))
+  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))
+  (origs (n2 (1 1))))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b b-0 b-1 name))
+  (deflistener n2)
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-1))
+  (precedes ((1 1) (2 1)) ((1 1) (3 1)) ((2 2) (1 2)) ((3 2) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand init 3) n2 (0 0)
+    (enc n1 n2 (pubk a)))
+  (traces ((recv n2))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0))))
+    ((send (enc n1 a (pubk b-1))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-1)))))
+  (label 32)
+  (parent 30)
+  (unrealized)
+  (shape)
+  (satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))
+  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))
+  (origs (n2 (1 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n1 n1-0 n2 n2-0 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1 n1-0)
+  (goals
+    (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))
+      (implies
+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)
+          (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
+          (p "init" "a" z-0 a) (p "init" "b" z-0 b)
+          (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)
+          (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)
+          (str-prec z-1 z-2) (non (privk a)) (non (privk b))
+          (uniq-at n1 z) (uniq-at n1-0 z-1)) (= z-1 z))))
+  (comment "Double initiator point of view")
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
+      (send (enc n2-0 (pubk b)))))
+  (label 33)
+  (unrealized (0 1) (1 1))
+  (origs (n1 (0 0)) (n1-0 (1 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation collapsed 1 0)
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 34)
+  (parent 33)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
+  (defstrand resp 2 (n2 n2-1) (n1 n1-0) (b b) (a a))
+  (precedes ((1 0) (2 0)) ((2 1) (1 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1 n1-0)
+  (operation nonce-test (added-strand resp 2) n1-0 (1 1)
+    (enc n1-0 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
+      (send (enc n2-0 (pubk b))))
+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-1 (pubk a)))))
+  (label 35)
+  (parent 33)
+  (unrealized (0 1) (1 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (0 1)
+    (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 36)
+  (parent 34)
+  (unrealized (0 1))
+  (origs (n1 (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n1-0 n2 n2-0 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a))
+  (precedes ((1 0) (2 0)) ((2 1) (1 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1 n1-0)
+  (operation nonce-test (contracted (n2-1 n2-0)) n1-0 (1 1)
+    (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
+      (send (enc n2-0 (pubk b))))
+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a)))))
+  (label 37)
+  (parent 35)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
+  (label 38)
+  (parent 36)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))
+  (origs (n1 (0 0))))
+
+(defskeleton ns
+  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a))
+  (defstrand resp 2 (n2 n2-1) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1 n1-0)
+  (operation nonce-test (added-strand resp 2) n1 (0 1)
+    (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))
+      (send (enc n2-0 (pubk b))))
+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-1 (pubk a)))))
+  (label 39)
+  (parent 37)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n1-0 n2 n2-0 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))
+  (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1-0) (b b) (a a))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1 n1-0)
+  (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1)
+    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 (pubk a)))
+      (send (enc n2-0 (pubk b))))
+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2 (pubk a))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 40)
+  (parent 39)
+  (unrealized)
+  (shape)
+  (satisfies
+    (no (n1-0 n1) (n1 n1-0) (n2-0 n2-0) (n2 n2) (a a) (b b) (z-2 (0 0))
+      (z-1 (0 2)) (z-0 (1 0)) (z (1 2))))
+  (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2))))
+  (origs (n1 (0 0)) (n1-0 (1 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol nsl-typeless basic
+  (defrole init
+    (vars (a b name) (n1 text) (n2 mesg))
+    (trace (send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 text) (n1 mesg))
+    (trace (recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder-Lowe with untyped nonces"))
+
+(defskeleton nsl-typeless
+  (vars (n1 mesg) (n2 text) (a b name))
+  (deflistener n2)
+  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (goals
+    (forall ((n2 text) (a b name) (z z-0 node))
+      (implies
+        (and (p "resp" 1 z) (p "" 0 z-0) (p "resp" "n2" z n2)
+          (p "resp" "b" z b) (p "resp" "a" z a) (p "" "x" z-0 n2)
+          (non (privk a)) (non (privk b)) (uniq n2)) (false))))
+  (comment "Shows typeflaw in typeless NSL")
+  (traces ((recv n2))
+    ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))))
+  (label 41)
+  (unrealized (0 0))
+  (preskeleton)
+  (comment "Not a skeleton"))
+
+(defskeleton nsl-typeless
+  (vars (n1 mesg) (n2 text) (a b name))
+  (deflistener n2)
+  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
+  (precedes ((1 1) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (traces ((recv n2))
+    ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))))
+  (label 42)
+  (parent 41)
+  (unrealized (0 0))
+  (origs (n2 (1 1)))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton nsl-typeless
+  (vars (n2 n1 text) (a b name))
+  (deflistener n2)
+  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
+  (defstrand init 3 (n2 n2) (n1 n1) (a a) (b b))
+  (precedes ((1 1) (2 1)) ((2 2) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand init 3) n2 (0 0)
+    (enc n1 n2 b (pubk a)))
+  (traces ((recv n2))
+    ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))
+    ((send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 43)
+  (parent 42)
+  (unrealized (0 0))
+  (comment "empty cohort"))
+
+(defskeleton nsl-typeless
+  (vars (n2 n2-0 text) (a b a-0 name))
+  (deflistener n2)
+  (defstrand resp 2 (n1 a-0) (n2 n2) (b b) (a a))
+  (defstrand resp 2 (n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0))
+  (precedes ((1 1) (2 0)) ((2 1) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand resp 2) n2 (0 0)
+    (enc a-0 n2 b (pubk a)))
+  (traces ((recv n2))
+    ((recv (enc a a-0 (pubk b))) (send (enc a-0 n2 b (pubk a))))
+    ((recv (enc a-0 n2 b (pubk a)))
+      (send (enc (cat n2 b) n2-0 a (pubk a-0)))))
+  (label 44)
+  (parent 42)
+  (unrealized)
+  (shape)
+  (satisfies (no (n2 n2) (a a) (b b) (z-0 (1 1)) (z (0 0))))
+  (maps ((0 1) ((n2 n2) (a a) (b b) (n1 a-0))))
+  (origs (n2 (1 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (goals
+    (forall ((n1 n2 text) (a b name) (z z-0 node))
+      (implies
+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
+          (non (privk b)) (uniq-at n1 z))
+        (exists ((z-1 z-2 z-3 node))
+          (and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)
+            (p "resp" "n2" z-3 n2) (p "resp" "n1" z-3 n1)
+            (p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)
+            (prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)
+            (str-prec z-2 z-3))))))
+  (comment "Responder point of view with SAS")
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (label 45)
+  (unrealized (0 2))
+  (origs (n2 (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b b-0 name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand init 3) n2 (0 2)
+    (enc n1 n2 (pubk a)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0)))))
+  (label 46)
+  (parent 45)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
+  (origs (n2 (0 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (goals
+    (forall ((n1 n2 text) (a b name) (z z-0 node))
+      (implies
+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
+          (non (privk b)) (uniq-at n1 z)) (false))))
+  (comment "Responder point of view with false as the conclusion")
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (label 47)
+  (unrealized (0 2))
+  (origs (n2 (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n2 n1 text) (a b b-0 name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (operation nonce-test (added-strand init 3) n2 (0 2)
+    (enc n1 n2 (pubk a)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0)))))
+  (label 48)
+  (parent 47)
+  (unrealized)
+  (shape)
+  (satisfies yes)
+  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
+  (origs (n2 (0 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (goals
+    (forall ((n1 n2 text) (a b name) (z z-0 node))
+      (implies
+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
+          (non (privk b)) (uniq-at n1 z)) (false))))
+  (comment "Initiator point of view with false as the conclusion")
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 49)
+  (unrealized (0 1))
+  (origs (n1 (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 n2-0 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (added-strand resp 2) n1 (0 1)
+    (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 50)
+  (parent 49)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
+  (label 51)
+  (parent 50)
+  (unrealized)
+  (shape)
+  (satisfies (no (n1 n1) (n2 n2) (a a) (b b) (z-0 (0 0)) (z (0 2))))
+  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
+  (origs (n1 (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n n1 text) (a b name))
+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n)
+  (goals
+    (forall ((a b name) (n text) (z0 node))
+      (implies
+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
+          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
+        (exists ((z1 node)) (and (p "init" 2 z1) (p "init" "a" z1 a)))))
+    (forall ((a b name) (n text) (z0 node))
+      (implies
+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
+          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
+        (exists ((z1 node))
+          (and (p "init" 2 z1) (p "init" "b" z1 b))))))
+  (comment "Two responder authentication goals")
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
+      (recv (enc n (pubk b)))))
+  (label 52)
+  (unrealized (0 2))
+  (origs (n (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns
+  (vars (n n1 text) (a b b-0 name))
+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n)
+  (operation nonce-test (added-strand init 3) n (0 2)
+    (enc n1 n (pubk a)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))
+      (recv (enc n (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))
+      (send (enc n (pubk b-0)))))
+  (label 53)
+  (parent 52)
+  (unrealized)
+  (shape)
+  (satisfies yes (no (a a) (b b) (n n) (z0 (0 2))))
+  (maps ((0) ((a a) (b b) (n n) (n1 n1))))
+  (origs (n (0 1))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns-role-origs basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    (non-orig (privk b))
+    (uniq-orig n1))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    (non-orig (privk a))
+    (uniq-orig n2))
+  (comment
+    "Needham-Schroeder with role assumptions that are too strong"))
+
+(defskeleton ns-role-origs
+  (vars (n1 n2 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (non-orig (privk b))
+  (uniq-orig n1)
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 54)
+  (unrealized (0 1))
+  (origs (n1 (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns-role-origs
+  (vars (n1 n2 n2-0 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1 n2-0)
+  (operation nonce-test (added-strand resp 2) n1 (0 1)
+    (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 55)
+  (parent 54)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns-role-origs
+  (vars (n1 n2 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1 n2)
+  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
+  (label 56)
+  (parent 55)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
+  (origs (n2 (1 1)) (n1 (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns-role-origs basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    (non-orig (privk b))
+    (uniq-orig n1))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    (non-orig (privk a))
+    (uniq-orig n2))
+  (comment
+    "Needham-Schroeder with role assumptions that are too strong"))
+
+(defskeleton ns-role-origs
+  (vars (n2 n1 text) (b a name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (non-orig (privk a))
+  (uniq-orig n2)
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (label 57)
+  (unrealized (0 2))
+  (origs (n2 (0 1)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns-role-origs
+  (vars (n2 n1 text) (b a b-0 name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
+  (non-orig (privk a) (privk b-0))
+  (uniq-orig n2 n1)
+  (operation nonce-test (added-strand init 3) n2 (0 2)
+    (enc n1 n2 (pubk a)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0)))))
+  (label 58)
+  (parent 57)
+  (unrealized (0 0) (0 2))
+  (comment "2 in cohort - 2 not yet seen"))
+
+(defskeleton ns-role-origs
+  (vars (n2 n1 text) (a b name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2 n1)
+  (operation nonce-test (contracted (b-0 b)) n1 (0 0)
+    (enc n1 a (pubk b)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 59)
+  (parent 58)
+  (unrealized)
+  (shape)
+  (maps ((0) ((b b) (a a) (n2 n2) (n1 n1))))
+  (origs (n1 (1 0)) (n2 (0 1))))
+
+(defskeleton ns-role-origs
+  (vars (n2 n1 n2-0 text) (b a b-0 name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b-0) (a a))
+  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
+  (non-orig (privk a) (privk b-0))
+  (uniq-orig n2 n1 n2-0)
+  (operation nonce-test (added-strand resp 2) n1 (0 0)
+    (enc n1 a (pubk b-0)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b-0))))
+    ((recv (enc n1 a (pubk b-0))) (send (enc n1 n2-0 (pubk a)))))
+  (label 60)
+  (parent 58)
+  (unrealized (0 0) (0 2))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns-role-origs
+  (vars (n2 n1 n2-0 text) (a b name))
+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
+  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n2 n1 n2-0)
+  (operation nonce-test (contracted (b-0 b)) n1 (0 0)
+    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
+  (traces
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
+  (label 61)
+  (parent 60)
+  (seen 59)
+  (unrealized)
+  (comment "1 in cohort - 0 not yet seen"))
+
+(comment "Nothing left to do")
+
+(defprotocol ns2 basic
+  (defrole init
+    (vars (a b name) (n1 n2 n3 text))
+    (trace (send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b))))
+    (note doubled nonce in the first message))
+  (note that this protocol is derived from Needham-Schroeder))
+
+(defskeleton ns2
+  (vars (n1 n2 n3 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (traces
+    ((send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (label 62)
+  (unrealized (0 1))
+  (origs (n1 (0 0)))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns2
+  (vars (n2 n3 n2-0 text) (a b name))
+  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))
+  (defstrand resp 2 (n2 n2-0) (n1 n3) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n3)
+  (operation nonce-test (added-strand resp 2) n3 (0 1)
+    (enc n3 n3 a (pubk b)))
+  (traces
+    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2-0 (pubk a)))))
+  (label 63)
+  (parent 62)
+  (unrealized (0 1))
+  (comment "1 in cohort - 1 not yet seen"))
+
+(defskeleton ns2
+  (vars (n3 n2 text) (a b name))
+  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n3) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n3)
+  (operation nonce-test (contracted (n2-0 n2)) n3 (0 1)
+    (enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)))
+  (traces
+    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2 (pubk a)))))
+  (label 64)
+  (parent 63)
+  (unrealized)
+  (shape)
+  (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3))))
+  (origs (n3 (0 0))))
+
+(comment "Nothing left to do")
+
+(defprotocol ns basic
+  (defrole init
+    (vars (a b name) (n1 n2 text))
+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b)))))
+  (defrole resp
+    (vars (b a name) (n2 n1 text))
+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
+      (recv (enc n2 (pubk b)))))
+  (comment "Needham-Schroeder with no role origination assumptions"))
+
+(defskeleton ns
+  (vars (n1 n2 text) (a b name))
+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
+  (non-orig (privk a) (privk b))
+  (uniq-orig n1)
+  (traces
+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
+      (send (enc n2 (pubk b))))
+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
+  (label 65)
+  (unrealized)
+  (shape)
+  (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b))))
+  (origs (n1 (0 0))))
 
 (comment "Nothing left to do")
diff --git a/tst/hashtest-key-hash.tst b/tst/hashtest-key-hash.tst
--- a/tst/hashtest-key-hash.tst
+++ b/tst/hashtest-key-hash.tst
@@ -1,6 +1,6 @@
 (herald "Hashtest")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from hashtest-key-hash.scm")
 
 (defprotocol hashtest basic
diff --git a/tst/hashtest.tst b/tst/hashtest.tst
--- a/tst/hashtest.tst
+++ b/tst/hashtest.tst
@@ -1,6 +1,6 @@
 (herald "Hashtest")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from hashtest.scm")
 
 (defprotocol hashtest basic
diff --git a/tst/incompleteness_example.tst b/tst/incompleteness_example.tst
--- a/tst/incompleteness_example.tst
+++ b/tst/incompleteness_example.tst
@@ -1,7 +1,7 @@
 (herald incompleteness-example
   (comment "Shows a shape not found by CPSA"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from incompleteness_example.scm")
 
 (defprotocol incompleteness-example basic
diff --git a/tst/isoreject.tst b/tst/isoreject.tst
--- a/tst/isoreject.tst
+++ b/tst/isoreject.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from isoreject.scm")
 
 (defprotocol isoreject basic
diff --git a/tst/kelly1.tst b/tst/kelly1.tst
--- a/tst/kelly1.tst
+++ b/tst/kelly1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from kelly1.scm")
 
 (defprotocol kelly1 basic
diff --git a/tst/kerberos.tst b/tst/kerberos.tst
--- a/tst/kerberos.tst
+++ b/tst/kerberos.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from kerberos.scm")
 
 (defprotocol kerberos basic
diff --git a/tst/mass.tst b/tst/mass.tst
--- a/tst/mass.tst
+++ b/tst/mass.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from mass.lsp")
 
 (defprotocol mass basic
diff --git a/tst/mass2.tst b/tst/mass2.tst
--- a/tst/mass2.tst
+++ b/tst/mass2.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from mass2.lsp")
 
 (defprotocol mass2 basic
diff --git a/tst/missing_contraction.tst b/tst/missing_contraction.tst
--- a/tst/missing_contraction.tst
+++ b/tst/missing_contraction.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from missing_contraction.scm")
 
 (defprotocol missing-contraction basic
diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst
--- a/tst/neuman-stubblebine-reauth.tst
+++ b/tst/neuman-stubblebine-reauth.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from neuman-stubblebine-reauth.lsp")
 
 (defprotocol neuman-stubblebine-reauth basic
diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst
--- a/tst/neuman-stubblebine.tst
+++ b/tst/neuman-stubblebine.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from neuman-stubblebine.scm")
 
 (defprotocol neuman-stubblebine basic
diff --git a/tst/no_contraction.tst b/tst/no_contraction.tst
--- a/tst/no_contraction.tst
+++ b/tst/no_contraction.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from no_contraction.scm")
 
 (defprotocol no-contraction basic
diff --git a/tst/non_transforming.tst b/tst/non_transforming.tst
--- a/tst/non_transforming.tst
+++ b/tst/non_transforming.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from non_transforming.scm")
 
 (defprotocol non_transforming basic
diff --git a/tst/nonaug-prune.tst b/tst/nonaug-prune.tst
--- a/tst/nonaug-prune.tst
+++ b/tst/nonaug-prune.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from nonaug-prune.scm")
 
 (defprotocol nonaug-prune basic
diff --git a/tst/ns-l.tst b/tst/ns-l.tst
--- a/tst/ns-l.tst
+++ b/tst/ns-l.tst
@@ -1,7 +1,7 @@
 (herald "Needham-Schroeder-Low Public-Key Protocol"
   (comment "With deflistener's"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from ns-l.scm")
 
 (defprotocol ns basic
diff --git a/tst/ns.tst b/tst/ns.tst
--- a/tst/ns.tst
+++ b/tst/ns.tst
@@ -1,6 +1,6 @@
 (herald "Needham-Schroeder Public-Key Protocol Variants")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from ns.scm")
 
 (defprotocol ns basic
diff --git a/tst/nsl3.tst b/tst/nsl3.tst
--- a/tst/nsl3.tst
+++ b/tst/nsl3.tst
@@ -1,6 +1,6 @@
 (herald "Three Party Needham-Schroeder-Lowe Protocol")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from nsl3.scm")
 
 (defprotocol nsl3 basic
diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst
# file too large to diff: tst/nsl4cm1.tst
diff --git a/tst/nslsk.tst b/tst/nslsk.tst
--- a/tst/nslsk.tst
+++ b/tst/nslsk.tst
@@ -1,6 +1,6 @@
 (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from nslsk.scm")
 
 (defprotocol nslsk basic
diff --git a/tst/or.tst b/tst/or.tst
--- a/tst/or.tst
+++ b/tst/or.tst
@@ -1,7 +1,7 @@
 (herald "Otway-Rees Protocol"
   (comment "Standard version using variables of sort mesg"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from or.scm")
 
 (defprotocol or basic
diff --git a/tst/pca.tst b/tst/pca.tst
--- a/tst/pca.tst
+++ b/tst/pca.tst
@@ -1,7 +1,7 @@
 (herald "Privacy Certificate Authority" (bound 15)
   (comment "Generation of an Attestation Identity Certificate"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from pca.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/pen-non-orig-test.tst b/tst/pen-non-orig-test.tst
--- a/tst/pen-non-orig-test.tst
+++ b/tst/pen-non-orig-test.tst
@@ -1,6 +1,6 @@
 (herald "pen-non-orig test")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from pen-non-orig-test.scm")
 
 (defprotocol pennonorigtest basic
diff --git a/tst/pkinit.tst b/tst/pkinit.tst
--- a/tst/pkinit.tst
+++ b/tst/pkinit.tst
@@ -1,6 +1,6 @@
 (herald "Kerberos PK init")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from pkinit.scm")
 
 (defprotocol pkinit basic
diff --git a/tst/preprocess.tst b/tst/preprocess.tst
--- a/tst/preprocess.tst
+++ b/tst/preprocess.tst
@@ -1,6 +1,6 @@
 (herald "Pre-processing test example: modified NS with two responders")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from preprocess.scm")
 
 (defprotocol ns basic
diff --git a/tst/print.tst b/tst/print.tst
--- a/tst/print.tst
+++ b/tst/print.tst
@@ -1,7 +1,7 @@
 (herald "Print Test"
   (comment "See if read forms look like printed ones"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from print.scm")
 
 (defprotocol print-test basic
diff --git a/tst/pruning1.tst b/tst/pruning1.tst
--- a/tst/pruning1.tst
+++ b/tst/pruning1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from pruning1.scm")
 
 (defprotocol prune basic
diff --git a/tst/sigenc.tst b/tst/sigenc.tst
--- a/tst/sigenc.tst
+++ b/tst/sigenc.tst
@@ -1,7 +1,7 @@
 (herald "Signed Encrypted Message Example"
   (comment "Shows examples of key usage of asymmetric keys"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from sigenc.scm")
 
 (defprotocol mult-keys-sig-enc basic
diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst
--- a/tst/sorted_epmo_acctnum.tst
+++ b/tst/sorted_epmo_acctnum.tst
@@ -4,7 +4,7 @@
     "This version uses sorts to avoid confusion"
     "between a nonce and other data"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from sorted_epmo_acctnum.scm")
 (comment "Strand count bounded at 12")
 
diff --git a/tst/targetterms2.tst b/tst/targetterms2.tst
--- a/tst/targetterms2.tst
+++ b/tst/targetterms2.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from targetterms2.scm")
 
 (defprotocol targetterms2 basic
diff --git a/tst/targetterms6.tst b/tst/targetterms6.tst
--- a/tst/targetterms6.tst
+++ b/tst/targetterms6.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from targetterms6.scm")
 
 (defprotocol targetterms6 basic
diff --git a/tst/targetterms8.tst b/tst/targetterms8.tst
--- a/tst/targetterms8.tst
+++ b/tst/targetterms8.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from targetterms8.scm")
 
 (defprotocol targetterms8 basic
diff --git a/tst/timestamping.tst b/tst/timestamping.tst
--- a/tst/timestamping.tst
+++ b/tst/timestamping.tst
@@ -1,6 +1,6 @@
 (herald timestamping-service)
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from timestamping.scm")
 
 (defprotocol timestamping-service basic
diff --git a/tst/uncarried_keys.tst b/tst/uncarried_keys.tst
--- a/tst/uncarried_keys.tst
+++ b/tst/uncarried_keys.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from uncarried_keys.scm")
 
 (defprotocol uncarried-keys basic
diff --git a/tst/unilateral.tst b/tst/unilateral.tst
--- a/tst/unilateral.tst
+++ b/tst/unilateral.tst
@@ -1,6 +1,6 @@
 (herald unilateral)
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from unilateral.scm")
 
 (defprotocol unilateral basic
diff --git a/tst/uo.tst b/tst/uo.tst
--- a/tst/uo.tst
+++ b/tst/uo.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from uo.scm")
 
 (defprotocol uniq-orig basic
diff --git a/tst/wang-hash.tst b/tst/wang-hash.tst
--- a/tst/wang-hash.tst
+++ b/tst/wang-hash.tst
@@ -1,6 +1,6 @@
 (herald "Wang's Fair Exchange Protocol" (bound 10))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from wang-hash.scm")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/wang-key-hash.tst b/tst/wang-key-hash.tst
--- a/tst/wang-key-hash.tst
+++ b/tst/wang-key-hash.tst
@@ -1,6 +1,6 @@
 (herald "Wang's Fair Exchange Protocol" (bound 10))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from wang-key-hash.scm")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/weird.tst b/tst/weird.tst
--- a/tst/weird.tst
+++ b/tst/weird.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from weird.scm")
 
 (defprotocol weird basic
diff --git a/tst/wide-mouth-frog-scyther.tst b/tst/wide-mouth-frog-scyther.tst
--- a/tst/wide-mouth-frog-scyther.tst
+++ b/tst/wide-mouth-frog-scyther.tst
@@ -1,7 +1,7 @@
 (herald "Wide-Mouth Frog Protocol from Scyther"
   (comment "This protocol has an infinite number of shapes"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from wide-mouth-frog-scyther.lsp")
 
 (defprotocol wide-mouth-frog basic
diff --git a/tst/wide-mouth-frog.tst b/tst/wide-mouth-frog.tst
--- a/tst/wide-mouth-frog.tst
+++ b/tst/wide-mouth-frog.tst
@@ -1,7 +1,7 @@
 (herald "Wide-Mouth Frog Protocol"
   (comment "This protocol has an infinite number of shapes"))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from wide-mouth-frog.lsp")
 
 (defprotocol wide-mouth-frog basic
diff --git a/tst/wonthull.tst b/tst/wonthull.tst
--- a/tst/wonthull.tst
+++ b/tst/wonthull.tst
@@ -1,6 +1,6 @@
 (herald wonthull (bound 9))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from wonthull.scm")
 (comment "Strand count bounded at 9")
 
diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst
--- a/tst/wonthull2.tst
+++ b/tst/wonthull2.tst
@@ -1,6 +1,6 @@
 (herald wonthull2 (bound 9))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from wonthull2.scm")
 (comment "Strand count bounded at 9")
 
diff --git a/tst/wonthull3.tst b/tst/wonthull3.tst
--- a/tst/wonthull3.tst
+++ b/tst/wonthull3.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from wonthull3.scm")
 
 (defprotocol wonthull3 basic
diff --git a/tst/woolam.tst b/tst/woolam.tst
--- a/tst/woolam.tst
+++ b/tst/woolam.tst
@@ -1,6 +1,6 @@
 (herald "Woo-Lam Protocol")
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from woolam.scm")
 
 (defprotocol woolam basic
diff --git a/tst/yahalom-6.3.6.tst b/tst/yahalom-6.3.6.tst
--- a/tst/yahalom-6.3.6.tst
+++ b/tst/yahalom-6.3.6.tst
@@ -5,7 +5,7 @@
   (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")
   (bound 15))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from yahalom-6.3.6.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/yahalom.tst b/tst/yahalom.tst
--- a/tst/yahalom.tst
+++ b/tst/yahalom.tst
@@ -1,6 +1,6 @@
 (herald "Yahalom Protocol Without Forwarding" (bound 15))
 
-(comment "CPSA 2.5.0")
+(comment "CPSA 2.5.1")
 (comment "All input read from yahalom.scm")
 (comment "Strand count bounded at 15")