diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,28 @@
+2014-11-15  John D.  Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/SAS/SAS.hs (nodeForm): Fixed bug where some role
+	predicates were mistakenly omitted.
+
+2014-11-13  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* doc/cpsaspec.tex: Updated the appendix of shape analysis
+	sentences to agree with what is produced by cpsasas.
+
+2014-11-04  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/SAS/SAS.hs (reduce): Added a function that eliminates
+	trivial homomorphism equations by substituting equivalent
+	variables and simplifying.
+
+2014-10-31  John D. Ramsdell  <ramsdell@.mitre.org>
+
+	* cpsasas: Added a program that produces shape analysis sentences
+	using the goal language used with protocol transformations.  This
+	language is superior to the one used by the cpsalogic program.
+
+	* cpsalogic: Removed this program as it has been replaced with
+	cpsasas.
+
 2014-09-05  John D. Ramsdell  <ramsdell@mitre.org>
 
 	* cpsa.cabal (Version): Tagged as version 2.3.5
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,24 @@
 CPSA NEWS -- history of user-visible changes.
 
+* Changes in version 2.4.0
+
+** Added program cpsasas
+   The cpsasas program extracts a formula in the language of
+   order-sorted first-order logic for each problem and its shapes from
+   a CPSA run. The formula is called a shape analysis sentence. The
+   formula is modeled by all realized skeletons when CPSA finds all
+   the shapes for the problem.  The sentence can be use with an
+   automated first-order theorem prover to verify security goals
+   associated with a protocol.
+
+   This formula extractor uses a node-oriented language, rather than a
+   strand-orient language.  The new language integrates well with
+   other work on security goals and better supports protocol
+   transformations.
+
+** Program cpsalogic removed
+   The strand-oriented formula extractor has been removed.
+
 * Changes in version 2.3.5
 
 ** Added a translator from JSON to CPSA S-Expressions
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,5 +1,5 @@
 Name:			cpsa
-Version:		2.3.5
+Version:		2.4.0
 Maintainer:		ramsdell@mitre.org
 Cabal-Version:		>= 1.6
 License:		BSD3
@@ -219,8 +219,8 @@
     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Lib.CPSA
 
-Executable cpsalogic
-  Main-Is:		CPSA/Logic/Main.hs
+Executable cpsasas
+  Main-Is:		CPSA/SAS/Main.hs
   Build-Depends:	base >= 3 && < 5, containers
   GHC-Options:
     -Wall -fno-warn-name-shadowing -fwarn-unused-imports
@@ -230,5 +230,5 @@
     CPSA.Lib.Printer CPSA.Lib.Notation CPSA.Lib.Entry CPSA.Lib.Algebra
     CPSA.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader
     CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.CPSA
-    CPSA.Logic.Logic
+    CPSA.SAS.SAS
     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra
diff --git a/doc/Make.hs b/doc/Make.hs
--- a/doc/Make.hs
+++ b/doc/Make.hs
@@ -1,6 +1,6 @@
 -- A simple, CPSA specific make system
 
-module Make (cpsa, shapes, logic, annos, params, cleanse, get, set,
+module Make (cpsa, shapes, sas, annos, params, cleanse, get, set,
              build, clean, roots) where
 
 {- Place a copy of this source file in the directory used to store
@@ -23,10 +23,10 @@
 
 If successful, the shapes are in the file prob_shapes.xhtml.
 
-*Make> logic "prob"
+*Make> sas "prob"
 
 If successful, the shape analysis sentences are in the file
-prob_logic.text.
+prob_sas.text.
 
 When the protocol is annotated with rely-guarantee formulas, type:
 
@@ -152,19 +152,19 @@
            inputExt = cpsaExt,
            outputExt = shapesRoot ++ cpsaExt }
 
--- Logic Rule
+-- SAS Rule
 
-logic :: FilePath -> IO ()
-logic root =
+sas :: FilePath -> IO ()
+sas root =
     do
       cpsaBasic root            -- Run CPSA if need be
-      make logicRule root
+      make sasRule root
 
-logicRule :: Rule
-logicRule =
-    Rule { prog = "cpsalogic",
+sasRule :: Rule
+sasRule =
+    Rule { prog = "cpsasas",
            inputExt = cpsaExt,
-           outputExt = logicExt }
+           outputExt = sasExt }
 
 -- Annotations Rule
 
@@ -203,7 +203,7 @@
       rm $ root ++ graphExt
       rm $ root ++ shapesRoot ++ cpsaExt
       rm $ root ++ shapesRoot ++ graphExt
-      rm $ root ++ logicExt
+      rm $ root ++ sasExt
       rm $ root ++ annosRoot ++ cpsaExt
       rm $ root ++ annosRoot ++ graphExt
       rm $ root ++ paramsRoot ++ cpsaExt
@@ -219,8 +219,8 @@
 shapesRoot :: String
 shapesRoot = "_shapes"
 
-logicExt :: String
-logicExt = "_logic.text"
+sasExt :: String
+sasExt = "_sas.text"
 
 annosRoot :: String
 annosRoot = "_annotations"
diff --git a/doc/cpsa.mk b/doc/cpsa.mk
--- a/doc/cpsa.mk
+++ b/doc/cpsa.mk
@@ -16,8 +16,8 @@
 	cpsashapes $(SHAPESFLAGS) -o $@ $<
 
 # Extract shape analysis sentences
-%_logic.text:	%.txt
-	cpsalogic $(LOGICFLAGS) -o $@ $<
+%_sas.text:	%.txt
+	cpsasas $(SASFLAGS) -o $@ $<
 
 # Annotate shapes
 %_annotations.txt:	%_shapes.txt
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/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
@@ -124,7 +124,7 @@
 \item \texttt{cpsagraph}: visualize output using XHTML and SVG
 \item \texttt{cpsadiff}: compare two \texttt{cpsa} output files
 \item \texttt{cpsaannotations}: support rely-guarantee method
-\item \texttt{cpsalogic}: produce shape analysis sentences
+\item \texttt{cpsasas}: produce shape analysis sentences
 \item \texttt{cpsapp}: pretty print input and output
 \item Build tools: GNU makefile template and a Haskell script
 \end{zitemize}
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
@@ -1190,7 +1190,7 @@
 
 \section{Formula Extraction}\label{sec:formulas}
 
-The \texttt{cpsalogic} program extracts a formula in the language of
+The \texttt{cpsasas} program extracts a formula in the language of
 order-sorted first-order logic for each problem and its shapes from a
 {\cpsa} run. The formula is called a shape analysis
 sentence~\cite{Ramsdell12}. The formula is satisfied in all realized
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/cpsaspec.tex b/doc/cpsaspec.tex
--- a/doc/cpsaspec.tex
+++ b/doc/cpsaspec.tex
@@ -2077,241 +2077,203 @@
 \chapter{Shape Analysis Sentences}\label{chp:logic}
 
 For each point-of-view skeleton and its shapes found by {\cpsa}, there
-is a formula in the language of order-sorted first-order logic called
-a \index{shape analysis sentence}\emph{shape analysis sentence,} often
-shortened to a shape sentence.  The sentence has a
-special form,
+is a formula in a language of order-sorted first-order logic called
+a \index{shape analysis sentence}\emph{shape analysis sentence}.  The
+sentence has a special form,
 $\all{X}(\Psi\supset\bigvee_i\some{Y_i}(\Delta_i\wedge\Phi_i))$,
-where~$\Psi$ and~$\Phi_i$ are conjunctions of atomic formulas and~$X$
-and~$Y_i$ are variable sets.  This fragment of first-order logic is
-called coherent logic.  Formula~$\Psi$ describes the point-of-view
-skeleton~$k_0$.  For each homomorphism to a shape,
+where~$\Psi$, $\Delta_i$, and~$\Phi_i$ are conjunctions of atomic
+formulas and~$X$ and~$Y_i$ are variable sets.  This fragment of
+first-order logic is called coherent logic.  Formula~$\Psi$ describes
+the point-of-view skeleton~$k_0$.  For each homomorphism to a shape,
 $k_0\homomorphism{\delta_i}k_i$, formula~$\Delta_i$ describes the
 structure preserving maps~$\delta_i$, and the shape~$k_i$ is described
 by~$\Phi_i$.
 
-An interpretation of a shape sentence is a skeleton.  If {\cpsa} finds
-all of the shapes and the homomorphisms associated with a
-point-of-view skeleton, the analysis' shape sentence is satisfied in
-all realized skeletons.  Shape sentences are closely related to
-security goals~\cite{guttman09}, and were motivated by that work.
-This material was extracted from~\cite{ramsdell12}, the paper that
+An interpretation of a shape analysis sentence is a skeleton.  If
+{\cpsa} finds all of the shapes and the homomorphisms associated with
+a point-of-view skeleton, the analysis' sentence is satisfied in all
+realized skeletons.  Let~$\Sigma$ be a shape analysis sentence
+and~$\Psi$ be a security goal.  If $\Sigma\supset\Psi$ is a theorem in
+order-sorted first-order logic, then~$\Psi$ is satisfied in all
+realized skeletons and its protocol achieves this goal.
+
+Shape analysis sentences are closely related to security goals
+in~\cite{guttman09}, and were motivated by that work.  This material
+was extracted from~\cite[Appendix~B]{ramsdell12}, the paper that
 introduced shape analysis sentences.
 
-\section{Shape Formulas}
+\section{Security Goals}
 
 The signature for terms extends the one used for the underlying
-message algebra with a sort $\dom{nat}$, the sort of natural numbers,
-and two new operations, constant $\cn{zero}\colon\dom{nat}$, and the
-successor function $\cn{succ}\colon\dom{nat}\to\dom{nat}$.  The text
-uses the usual numerals for natural numbers.  Variables of this sort
-will range over strands.
+message algebra with one new sort \dom{node}, the sort of nodes.  Sort
+\dom{node} has no subsorting relations with any other sort symbol.
 
-Shape formulas make use of protocol specific predicates and protocol
-independent predicates.  For each role $r=\role_Y(C,N,U)$ in
-protocol~$P$, there are protocol specific binary predicates
-$P[r,h,x]\colon\dom{nat}\times S$ for every $0\leq h<|C|$
-and~$x\colon\srt{S}$ that occurs in~$C|_h$.  The protocol independent
-predicate of arity four is $\cn{prec}\colon
-\dom{nat}\times\dom{nat}\times\dom{nat}\times\dom{nat}$.  The protocol
-independent unary predicates are $\cn{non}\colon B$ and
-$\cn{uniq}\colon B$ for each base sort~$B$, and the protocol
-independent ternary predicates are $\cn{orig}\colon
-B\times\dom{nat}\times\dom{nat}$.  The predicate \cn{false} has arity
-zero and, of course, equality is binary.
+Security goals make use of protocol specific and protocol independent
+predicates.  For each role $\role_Y(C,N,U)\in P$ and $i<|C|$, there is
+a protocol specific unary position predicate $P[r,i]:\dom{node}$.  For
+each role~$\role_Y(C,N,U)\in P$ and variable~$x:S$ that occurs in~$C$,
+there is a protocol specific binary parameter predicate
+$P[r,x]:\dom{node}\times{}S$.  The protocol independent unary
+predicates are $\mathsf{non}: B$ for each base sort~$B$.  The
+remaining protocol independent predicates are binary, and are
+$\mathsf{uniq}: B\times\dom{node}$,
+$\mathsf{sprec}:\dom{node}\times\dom{node}$,
+$\mathsf{prec}:\dom{node}\times\dom{node}$, and equality.
 
-We define~$\form(k)=(Y,\Phi)$, where~$\Phi$ is $k$'s skeleton formula,
-and~$Y$ is the formula's variable set.  Using the external syntax
-presented in Section~\ref{sec:instances}, let
-$k=\skel_X(P,I,\prec,N,U)$.  The variable set~$Y$ is~$X$ augmented
-with a variable~$z_s\colon\dom{nat}$ for each strand
-$s\in\sdom(I)$.  The formula~$\Phi$ is a conjunction of atomic
-formulas composed as follows.
+Soon we define~$\form(k)=(Y,\Phi)$, where~$\Phi$ is $k$'s skeleton
+formula, and~$Y$ is the formula's variable set, but first we define
+the relevant nodes of a skeleton~$N$.  Let $k=\skel_X(P,I,\prec,N,U)$
+and let~$\prec^-$ be the transitive reduction of~$\prec$.  Recall
+that~$\Theta_X$ is the strand space defined by~$I$, see
+Section~\ref{sec:instances}.  The \emph{relevant nodes} of~$k$ are
+$N=N_s\cup N_\prec\cup N_u$ where
 
+\[\renewcommand{\arraystretch}{1.5}
+\begin{array}{r@{{}={}}l}
+  N_s&\{(s,i)\mid s\in\sdom(\Theta_X)\land
+  i=|\Theta_X(s)|-1\}\\
+
+  N_\prec&\{(s,i)\mid
+  \renewcommand{\arraystretch}{1}
+  \begin{array}[t]{@{}l}
+    (s',i')\in\nodes(\Theta_X)\land s\neq s'\\
+    \quad\land((s,i)\prec^- (s',i')\lor(s',i')\prec^-(s,i))\}
+  \end{array}\\
+
+  N_u&\{(s,i)\mid t\in U,(s,i)\in\orig_k(t)\}
+\end{array}\]
+
+For~$\form(k)=(Y,\Phi)$, the variable set~$Y$ is~$X$ augmented with a
+fresh variable of sort~\dom{node} for each node in~$N$, and let $v(n)$ be
+the variable associated with node~$n$.
+
+The formula~$\Phi$ is a conjunction of atomic formulas composed as
+follows.
 \begin{itemize}
-\item For each $s\in\sdom(I)$, let $I(s)=\inst(r,h,\sigma)$.  For
-  each variable $x\in\sdom(\sigma)$ and term $t=\sigma(x)$, assert
-  $P[r,h,x](z_s,t)$.
-\item For each $(s,i)\prec(s',i')$, assert
-  $\cn{prec}(z_s,i,z_{s'},i')$.
+\item For each $(s,i)\in N$, assert $P[r,i](v(s,i))$,
+  where $I(s)=\cn{i}(r,h,\sigma$).
+\item For each $s\in\sdom(I)$, let
+  $I(s)=\cn{i}(r,h,\sigma)$.  For each variable
+  $x\in\svars(\prefix{r^c}{h})$ and term $t=\sigma(x)$, assert
+  $P[r,x](v(s,h-1),t)$,
+  where $r^c=C$ when $r=\role(C,N,U)$.
+\item For each $(s,i),(s,i')\in N$ such that $i<i'$, assert
+  $\cn{sprec}(v(s,i),v(s,i'))$.
+\item For each $(s,i)\prec^-(s',i')$ such that $s\neq s'$, assert
+  $\cn{prec}(v(s,i),v(s',i'))$.
 \item For each $t\in N$, assert $\cn{non}(t)$.
-\item For each $t\in U$, assert $\cn{uniq}(t)$.
-\item For each $t\in U$ and $(s,i)\in\orig_k(t)$, assert
-  $\cn{orig}(t,z_s, i)$.
+\item For each $t\in U$ and node~$n$ such that
+  $n\in\orig_k(t)$, assert $\cn{uniq}(t,v(n))$.
 \end{itemize}
 
-In the code that extracts a shape analysis sentence, the
-$\cn{prec}$ predicate is not asserted for strand succession, and
-only for communication when it is in the transitive reduction of
-the~$\prec$ relation.  The missing relations must be asserted as axioms
-for proper handling of a shape sentence.
-
-Given a set of homomorphisms $k_0\homomorphism{\delta_i}k_i$, its shape
-sentence is
-\begin{equation}
-\sent(k_0\homomorphism{\delta_i}k_i)=\all{X}(\Psi\supset
-\bigvee_i\some{Y_i}(\Delta_i\wedge\Phi_i)),\label{eq:shape sentence}
+Given a set of homomorphisms $\delta_i\colon k_0\mapsto k_i$, its shape
+analysis sentence is
+\begin{equation}\label{eqn:node-oriented shape sentence}
+\sent(\delta_i\colon k_0\mapsto k_i)=\all{X_0}(\Phi_0\supset
+\bigvee_i\some{X_i}(\Delta_i\wedge\Phi_i)),
 \end{equation}
-where $\form(k_0)=(X,\Psi)$.  The same procedure produces~$Y_i$
+where $\form(k_0)=(X_0,\Phi_0)$.  The same procedure produces~$X_i$
 and~$\Phi_i$ for shape~$k_i$ with one proviso---the variables in
-$Y_i$ that also occur in~$X$ must be renamed to avoid trouble while
+$X_i$ that also occur in~$X_0$ must be renamed to avoid trouble while
 encoding the structure preserving maps~$\delta_i$.
 
+The structure preserving maps~$\delta_i=(\phi_i,\sigma_i)$ are encoded
+in~$\Delta_i$ by a conjunction of equalities.  Map~$\sigma_i$ is coded
+as equalities between a message algebra variable in the domain
+of~$\sigma_i$ and the term it maps to.  Map~$\phi_i$ is coded as
+equalities between node variables in~$\Phi_0$ and node variables
+in~$\Phi_i$.  Let~$v_0$ be the node variables freshly generated
+for~$k_0$, and~$v_i$ be the ones generated for~$k_i$.  The
+strand mapping part of~$\Delta_i$ is
+\[\bigwedge_{(s,j)\in\sdom(v_0)}v_0(s,j)=v_i(\phi_i(s),j).\]
+
 \begin{figure}
 $$\begin{array}{l}
-\all{a_0,b_0\colon\srt{A}, s_0\colon\srt{S}, d_0\colon\srt{D}, z_0\colon\srt{N}}(\\
-\quad\init_{2,a}(z_0,a_0)\wedge
-\init_{2,b}(z_0,b_0)\wedge
-\init_{2,s}(z_0,s_0)\wedge
-\init_{2,d}(z_0,d_0)\wedge{}\\
-\quad\cn{non}(a_0^{-1})\wedge
-\cn{non}(b_0^{-1})\wedge
-\cn{uniq}(s_0)\wedge\cn{orig}(s_0,z_0,1)\\
+\all{a_0,b_0\colon\srt{A}, s_0\colon\srt{S}, d_0\colon\srt{D}, n_0\colon\srt{N}}(\\
+\quad\resp_1(n_0)\wedge\resp_{a}(n_0,a_0)\wedge
+\resp_{b}(n_0,b_0)\\
+\qquad{}\wedge
+\resp_{s}(n_0,s_0)\wedge
+\resp_{d}(n_0,d_0)\\
+\qquad{}\wedge\cn{non}(a_0^{-1})\wedge
+\cn{non}(b_0^{-1})\\
 \quad\supset\\
-\quad\some{a_1,b_1\colon\srt{A}, s_1\colon\srt{S}, d_1\colon\srt{D}, z_1,z_2\colon
-  N}(\\
-\qquad z_0=z_1\wedge a_0=a_1\wedge b_0=b_1\wedge s_0=s_1\wedge d_0=d_1\wedge{}\\
-\qquad\init_{2,a}(z_1,a_1)\wedge
-\init_{2,b}(z_1,b_1)\wedge
-\init_{2,s}(z_1,s_1)\wedge
-\init_{2,d}(z_1,d_1)\wedge{}\\
-\qquad\resp_{2,a}(z_1,a_1)\wedge
-\resp_{2,b}(z_1,b_1)\wedge
-\resp_{2,s}(z_1,s_1)\wedge
-\resp_{2,d}(z_1,d_1)\wedge{}\\
-\qquad\cn{prec}(z_1,1,z_2,1)\wedge
-\cn{prec}(z_2,2,z_1,2)\wedge{}\\
-\qquad\cn{non}(a_1^{-1})\wedge
-\cn{non}(b_1^{-1})\wedge
-\cn{uniq}(s_1)\wedge\cn{orig}(s_1,z_1,1)))
+\quad\some{a_1,b_1,b_2\colon\srt{A}, s_1\colon\srt{S},
+  d_1\colon\srt{D}, n_1,n_2,n_3\colon
+ \srt{N}}(\\
+\qquad n_0=n_1\wedge a_0=a_1\wedge b_0=b_1\wedge s_0=s_1\wedge
+d_0=d_1\\
+\qquad\quad\wedge\resp_1(n_1)\wedge
+\resp_{a}(n_1,a_1)\wedge
+\resp_{b}(n_1,b_1)\\
+\qquad\quad\wedge
+\resp_{s}(n_1,s_1)\wedge
+\resp_{d}(n_1,d_1)\wedge\resp_0(n_2)\\
+\qquad\quad\wedge\init_0(n_3)\wedge\init_a(n_3,a_1)\wedge
+\init_b(n_3,b_2)\wedge
+\init_s(n_3,s_1)\\
+\qquad\quad\wedge\cn{uniq}(s_1,n_2)\wedge
+\cn{prec}(n_3,n_2)\wedge\cn{sprec}(n_2,n_1)\\
+\qquad\quad\wedge\cn{non}(a_1^{-1})\wedge
+\cn{non}(b_1^{-1})))
 \end{array}$$
-\caption{A Shape Analysis Sentence for Blanchet's
+\caption{Shape Analysis Sentence for Blanchet's
   Protocol}\label{fig:blanchet's shape analysis sentence}
 \end{figure}
 
-The structure preserving maps~$\delta_i=(\phi_i,\sigma_i)$ are encoded
-in~$\Delta_i$ by a conjunction of equalities.  Map~$\sigma_i$ is coded
-as equalities between a message algebra variable in the domain
-of~$\sigma_i$ and the term it maps to.  Map~$\phi_i$ is coded as
-equalities between strand variables in~$\Psi$ and strand variables
-in~$\Phi_i$.  Let~$Z$ be the sequence of strand variables freshly
-generated for~$k_0$, and~$Z_i$ be the ones generated for~$k_i$.  The
-strand mapping part of~$\Delta_i$ is
-$\bigwedge_{j\in\sdom(\Theta)}Z(j)=Z_i(\phi_i(j))$.
-
-The shape analysis sentence for the first analysis of Blanchet's
+The shape analysis sentence for the second analysis of Blanchet's
 Simple Example Protocol in Section~\ref{sec:blanchet's simple example
   protocol} is displayed in Figure~\ref{fig:blanchet's shape analysis
-  sentence}.  The sort \dom{nat} is abbreviated as~\srt{N}, and the
-strand progress predicate $P[r,h,x](z,t)$ is written $r_{h,x}(z,t)$
-with the protocol left implicit.
-
-\section{Semantics of Shape Formulas}
+  sentence}.  The sort \dom{node} is abbreviated as~\srt{N}, and the
+parameter predicate $P[r,x](z,t)$ is written $r_x(z,t)$ with the
+protocol left implicit.
 
-Let $k=\skel_X(\rl,P,\Theta,\prec,N,U)$.  The universe of discourse is
-$\alg{D}=\nat\cup\alga_X$.  When formula~$\Psi$ is satisfied in
-skeleton~$k$ with variable assignment $\alpha\colon Y\to \alg{D}$, we
-write $k,\alpha\models\Psi$.  When sentence~$\Sigma$ is satisfied in
-skeleton~$k$, we write $k\models\Sigma$.
+\paragraph{Semantics of Skeleton Formulas.}
 
-For each protocol specific predicate $P[r,h,x]$, $k,\alpha\models
-P[r,h,x](y,z)$ iff $\alpha(y)\in\nat$, $\alpha(z)\in\alga$, and with
-$\alpha(y)=s$ and $r=\role(C,N,U)$,
+Let $k=\skel_X(P,I,\prec,N,U)$.  The universe of
+discourse is $\alg{D}=(\nat\times\nat)\cup\alga_X$.  When
+formula~$\Phi$ is satisfied in skeleton~$k$ with variable
+assignment $\alpha\colon Y\to \alg{D}$, we write
+$k,\alpha\models\Phi$.  We write~$\bar\alpha$ when~$\alpha$ is
+extended to terms in the obvious way.  When sentence~$\Gamma$ is
+satisfied in skeleton~$k$, we write $k\models\Gamma$.
 
-\begin{enumerate}
-\item $s\in\sdom(\Theta)$,
-\item $h\in\sdom(\Theta(s))$, and
-\item $\prefix{\Theta(s)}{h}=\sigma\circ\{x\mapsto\alpha(z)\}\circ\prefix{C}{h}$
-  for some~$\sigma$.
-\end{enumerate}
+\begin{itemize}
+\item $k,\alpha\models P[r,i](y)$ iff $\alpha(y)\in\nodes(\Theta_X)$,
+  $\alpha(y)=(s,i)$, and for some~$\sigma$,
+  \[\prefix{\Theta_X(s)}{i+1}=\sigma\circ\prefix{r^c}{i+1}.\]
+  Recall $r^c=C$ when $r=\role(C,N,U)$.
 
-In an interpretation, $\rl(s)$ need not be~$r$.  The events that make
-up a strand's trace is all that matters.  The protocol specific
-predicate $P[r,h,x]$ is called a \index{strand progress
-  predicate}\emph{strand progress predicate}, because it asserts a
-strand is associated with an instance of role~$r$ of height at
-least~$h$.
+\item $k,\alpha\models P[r,x](y,t)$ iff
+  $\alpha(y)\in\nodes(\Theta_X)$, $\bar\alpha(t)\in\alga_X$, and with
+  $\alpha(y)=(s, i)$ and for some~$\sigma$ with $\sigma(x)=\bar\alpha(t)$,
+  \[\prefix{\Theta_X(s)}{i+1}=\sigma\circ\prefix{r^c}{i+1}.\]
+\end{itemize}
 
 The interpretation of the protocol independent predicates is
 straightforward.
 \begin{itemize}
-\item $k,\alpha\models\cn{prec}(w,x,y,z)$ iff
-$(\alpha(w),\alpha(x))\prec(\alpha(y),\alpha(z))$.
-\item $k,\alpha\models\cn{non}(y)$ iff $\alpha(y)\in N$.
-\item $k,\alpha\models\cn{uniq}(y)$ iff $\alpha(y)\in U$.
-\item $k,\alpha\models\cn{orig}(x,y,z)$ iff $\alpha(x)\in U$ and
-  $(\alpha(y),\alpha(z))\in\orig_k(\alpha(x))$.
-\item $k,\alpha\models y=z$ iff $\alpha(y)=\alpha(z)$.
-\item $k,\alpha\not\models\cn{false}$.
+\item $k,\alpha\models\cn{prec}(y,z)$ iff
+  $\alpha(y)\prec\alpha(z)$.
+\item $k,\alpha\models\cn{sprec}(y,z)$ iff $\alpha(y)\prec\alpha(z)$,
+  $\alpha(y)=(s,i)$, and $\alpha(z)=(s,i')$.
+\item $k,\alpha\models\cn{non}(t)$ iff $\bar\alpha(t)\in\nu$.
+\item $k,\alpha\models\cn{uniq}(t,y)$ iff $\bar\alpha(t)\in\upsilon$ and
+  $\alpha(y)\in\orig_k(\bar\alpha(t))$.
+\item $k,\alpha\models y=z$ iff $\bar\alpha(y)=\bar\alpha(z)$.
 \end{itemize}
 
-\begin{thm}\label{thm:skeleton models}
-Let $\form(k_0)=(X,\Psi)$ and $\Phi=\some{X}\Psi$.  Formula~$\Phi$ is
-satisfied in~$k$ iff there is a homomorphism from~$k_0$ to
-$k$, i.e.\ $k\models\Phi$ iff
-$\some{\delta}k_0\homomorphism{\delta}k$.
-\end{thm}
-
-This theorem corrects the first of the two main results
-from~\cite{guttman09}, as that paper omits the \cn{orig} predicate.
-
-\begin{proof}
-For the forward direction, assume~$\alpha$ is a variable assignment
-for the variables in~$X$ such that $k,\alpha\models\Psi$, and let~$Z$
-be the sequence of strand variables constructed while
-generating~$\Psi$ from~$k_0$.  Then the pair of maps
-$\delta=(\comp{\alpha}{Z},\alpha)$ demonstrate a homomorphism from~$k_0$
-to~$k$, i.e.\ each item in the definition of a preskeleton
-homomorphism on Page~\pageref{def:preskeleton homomorphism} is
-satisfied.
-
-For the reverse direction, assume maps $\delta=(\phi,\sigma)$ are such
-that $k_0\homomorphism{\delta}k$.  Then the desired variable assigment is
-$$\alpha(x)=\left\{
-\begin{array}{ll}
-\phi(Z^{-1}(x))&x\in\sran(Z)\\
-\sigma(x)&x\in\sdom(\sigma).
-\end{array}\right.$$
-\end{proof}
-
-The set of bundles denoted by preskeleton~$k$, $\sembrack{k}$ is
-defined on Page~\pageref{def:preskeleton denotation}.
-
-\begin{thm}\label{thm:sentence implies}
-Let $k_0\homomorphism{\delta_i}k_i$ be a complete set of homomorphisms
-for shapes $k_i\in K$, and assume $\sembrack{k_0}=\bigcup_{k\in
-  K}\sembrack{k}$.  Then the shape analysis
-sentence~$\Sigma=\sent(k_0\homomorphism{\delta_i}k_i)$ is satisfied in
-all realized skeletons~$k$, i.e.\ $k\models\Sigma$.
-\end{thm}
-
-\begin{proof}
-Shapes are maximal among realized skeletons, so there is no realized
-skeleton in the image of~$k$ that is not in the image of one of the
-shapes.  Therefore, by Theorem~\ref{thm:skeleton models}, the negation
-of the hypothesis of the implication is satisfied in all realized
-skeletons that are not in the image of~$k_0$, and the disjunction is
-satisfied in the remaining realized skeletons.
-\end{proof}
-
-The security goals of a protocol can be formalized using the same
-language used to specify shape analysis sentences.  A security goal
-can express an authentication goal or a secrecy goal.
-
-Security goals and shape analysis sentences can be translated into the
-language of ordinary first-order logic and used with an automated
-first-order theorem prover.  If a theorem prover deduces security
-goal~$\Phi$ from shape analysis sentence~$\Sigma$, then $\Phi$ is
-satisfied in all realized skeletons.
+Let~$\Sigma$ be a shape analysis sentence and~$\Psi$ be a security
+goal.  If $\Sigma\supset\Psi$ is a theorem in order-sorted first-order
+logic, then~$\Psi$ is satisfied in all realized skeletons and its
+protocol achieves this goal.
 
-Security goals can be used to ensure essential properties of a
-protocol are preserved in the face of changes to the protocol.
-Suppose an initial version of a protocol is specified, and shape
-analysis sentences for it are produced.  The sentences can be edited
-to produce a formalization of security goals that should be preserved
-during any revision to the protocol.  After a revision, one can
-generate revised shape analysis sentences, and use them to make sure
-each security goal is still deducible.
+Since $\prec$ is transitive, transitivity of \fn{prec} can be used to
+prove a protocol achieves a goal.  That is,
+\[\cn{prec}(x,y)
+\land\cn{prec}(y,z)\supset
+\cn{prec}(x,z).\]
+Furthermore, $\cn{sprec}(x,y)\supset\cn{prec}(x,y)$.
 
 \bibliography{cpsa}
 \bibliographystyle{plain}
diff --git a/doc/cpsauser.html b/doc/cpsauser.html
--- a/doc/cpsauser.html
+++ b/doc/cpsauser.html
@@ -3,7 +3,7 @@
 <head>
   <meta http-equiv="content-type"
   content="application/xhtml+xml; charset=UTF-8" />
-  <title>CPSA 2.3 User Guide</title>
+  <title>CPSA 2.4 User Guide</title>
   <meta name="generator" content="Amaya 9.54, see http://www.w3.org/Amaya/" />
   <style type="text/css">
     h1 { text-align: center }
@@ -12,7 +12,7 @@
 </head>
 
 <body>
-<h1>CPSA 2.3 User Guide</h1>
+<h1>CPSA 2.4 User Guide</h1>
 
 <p>The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to enumerate all
 essentially different executions possible for a cryptographic protocol. We call
@@ -44,7 +44,7 @@
 href="#cpsafiff"><code>cpsadiff</code></a> program compares CPSA output
   files S-expression by S-expression, and prints the first skeleton
   that differs.
-The <a href="#cpsalogic"><code>cpsalogic</code></a> program logical
+The <a href="#cpsasas"><code>cpsasas</code></a> program logical
   formula that can be used to ensure security goals are achieved.
 The <a
 href="#cpsaannotations"><code>cpsaannotations</code></a> program uses protocol
@@ -148,6 +148,7 @@
             |  (uniq-orig TERM*) ROLE-ALIST
             |  (priority POS-INT*) ROLE-ALIST | ...
 POS-TERM    ::= TERM | (INT TERM)
+POS-INT    ::= (INT INT)
 PROT-ALIST ::= ...</pre>
 </blockquote>
 
@@ -501,9 +502,9 @@
   -v       --version      show version number</pre>
 </blockquote>
 
-<h2 id="cpsalogic">Formula Extraction</h2>
+<h2 id="cpsasas">Formula Extraction</h2>
 
-<p>The <code>cpsalogic</code> program extracts a formula in the language
+<p>The <code>cpsasas</code> program extracts a formula in the language
   of order-sorted first-order logic for each problem and its shapes
   from a CPSA run. The formula is called a shape analysis
   sentence. The formula is satisfied in all realized skeletons when
@@ -512,8 +513,8 @@
 <h3>Usage</h3>
 
 <blockquote>
-  <pre>$ cpsalogic -h
-Usage: cpsalogic [OPTIONS] [FILE]
+  <pre>$ cpsasas -h
+Usage: cpsasas [OPTIONS] [FILE]
   -o FILE    --output=FILE     output FILE
   -m INT     --margin=INT      set output margin (default 72)
   -a STRING  --algebra=STRING  algebra (default basic)
diff --git a/doc/index.html b/doc/index.html
--- a/doc/index.html
+++ b/doc/index.html
@@ -114,13 +114,22 @@
   option, it produces diagrams that scale.  This is useful when
   viewing large diagrams.</p>
 
-<p>When the <code>cpsapp</code> program is given the <code>--json</code>
-  option, it translates S-expressions into JavaScript Object
-  Notation.</p>
+<p>The <code>cpsasas</code> program translates a CPSA result into a
+  sentence in first-order logic that can be used with automated
+  theorem provers.  The formula is called a shape analysis sentence.
+  See <a href="http://arxiv.org/abs/1204.0480">Deducing Security Goals
+  From Shape Analysis Sentences</a> for more details.</p>
 
+<p>When the <code>cpsapp</code> program is given
+  the <code>--json</code> option, it translates S-expressions into
+  JavaScript Object Notation (JSON).  The <code>cpsajson</code>
+  program translates JSON into S-expressions.  These two programs
+  makes it easy to manipulate CPSA input and output using Python or
+  other languages with JSON libraries.</p>
+
 <p>The goal of CPSA is to automatically characterize the possible
   executions of a protocol compatible with a specified partial
-  execution. There is a rigorous 
+  execution. There is a rigorous
   <a href="http://www.mitre.org/publications/technical-papers/completeness-of-cpsa">proof</a>
   that the algorithm enumerates all of these characterizations.</p>
 
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.3.5}
+\newcommand{\version}{2.4.0}
 \newcommand{\cpsacopying}{\begingroup
   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The
     MITRE Corporation.  Permission to copy without fee all or part of
@@ -34,7 +34,7 @@
 \newcommand{\ith}{\imath^\mathrm{th}}
 \newcommand{\jth}{\jmath^\mathrm{th}}
 \newcommand{\append}{\mathbin{{}^\smallfrown}}
-\newcommand{\prefix}[2]{#1|_{#2}}
+\newcommand{\prefix}[2]{#1\dagger#2}
 \newcommand{\orig}{\mathcal{O}}
 \newcommand{\gain}{\mathcal{G}}
 %\newcommand{\pow}[1]{\mathcal{P}(#1)}
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
@@ -341,15 +341,15 @@
     addKeyValues "unrealized" (map displayNode $ L.sort unrealized) $
     condAddKeyValues "shape" shape [] $
     -- Structure preserving maps
-    -- Added for cpsalogic program
+    -- Added for cpsasas program
     condAddKeyValues "maps" shape (maps k) $
     -- Nodes of origination
-    -- Added for cpsalogic program
+    -- Added for cpsasas program
     condAddKeyValues "origs" (starter k || shape) (origs k) $
     -- Messages
     case msg of
       "" -> []
-      -- Preskeleton key added for cpsalogic program
+      -- Preskeleton key added for cpsasas program
       "Not a skeleton" -> addKeyValues "preskeleton" [] [comment msg]
       _ -> [comment msg]
     where
diff --git a/src/CPSA/Logic/Logic.hs b/src/CPSA/Logic/Logic.hs
deleted file mode 100644
--- a/src/CPSA/Logic/Logic.hs
+++ /dev/null
@@ -1,580 +0,0 @@
--- Converts a solution to a problem into a coherent logic formula
-
--- Copyright (c) 2011 The MITRE Corporation
---
--- This program is free software: you can redistribute it and/or
--- modify it under the terms of the BSD License as published by the
--- University of California.
-
-module CPSA.Logic.Logic (Prot, Preskel, State, logic) where
-
-import qualified Data.List as L
-import CPSA.Lib.CPSA
-
-{--
-import System.IO.Unsafe
-z :: Show a => a -> b -> b
-z x y = unsafePerformIO (print x >> return y)
---}
-
-type State t g c = ([Prot t g c], [Preskel t g c])
-
-logic :: (Algebra t p g s e c, Monad m) => String -> g ->
-         State t g c -> Maybe (SExpr Pos) ->
-         m (State t g c, Maybe (SExpr ()))
-logic _ _ (ps, ks) Nothing =    -- Nothing signifies end-of-file
-    displayFormula ps (reverse ks)
-logic name gen (ps, []) (Just sexpr) = -- Looking for POV skeleton
-    loadPOV name gen ps sexpr
-logic name gen (ps, ks) (Just sexpr) = -- Looking for shapes
-    loadOtherPreskel name gen ps ks sexpr
-
-loadPOV :: (Algebra t p g s e c, Monad m) => String -> g ->
-           [Prot t g c] -> SExpr Pos ->
-           m (State t g c, Maybe (SExpr ()))
-loadPOV name origin ps (L pos (S _ "defprotocol" : xs)) =
-    do
-      p <- loadProt name origin pos xs
-      return ((p : ps, []), Nothing)
-loadPOV _ _ ps (L pos (S _ "defskeleton" : xs)) =
-    do
-      p <- findProt pos ps xs
-      k <- loadPreskel pos p (pgen p) emptyContext xs
-      case (isSkeleton k, isShape k) of
-        (True, False) -> return ((ps, [k]), Nothing) -- Found POV
-        _ -> return ((ps, []), Nothing)              -- Not POV
-loadPOV _ _ ps _ = return ((ps, []), Nothing)
-
-loadOtherPreskel :: (Algebra t p g s e c, Monad m) => String -> g ->
-                    [Prot t g c] -> [Preskel t g c] ->
-                    SExpr Pos -> m (State t g c, Maybe (SExpr ()))
-loadOtherPreskel name origin ps ks (L pos (S _ "defprotocol" : xs)) =
-    do                     -- Found next protocol.  Print this formula
-      p <- loadProt name origin pos xs
-      displayFormula (p : ps) (reverse ks)
-loadOtherPreskel _ _ ps ks (L pos (S _ "defskeleton" : xs)) =
-    do
-      p <- findProt pos ps xs
-      let g = kgen (last ks)    -- Make sure vars in skeleton are
-      let c = kctx (last ks)    -- distinct from the ones in the POV
-      k <- loadPreskel pos p g c xs
-      case isShape k of
-        True -> return ((ps, k : ks), Nothing) -- Found shape
-        False -> return ((ps, ks), Nothing) -- Found intermediate skeleton
-loadOtherPreskel _ _ ps ks _ = return ((ps, ks), Nothing)
-
--- Load a protocol
-
--- The Prot record contains information extraced from protocols for
--- use when processing preskeletons.  A protocol includes a role for
--- all listeners.
-data Prot t g c = Prot
-    { pname :: String,          -- Protocol name
-      pgen :: g,                -- Generator for preskeletons
-      roles :: [Role t c] }
-    deriving Show
-
--- The Role record contains information extraced from roles for use
--- when processing preskeletons.
-data Role t c = Role
-    { rname :: String,          -- Role name
-      vars :: [t],
-      ctx :: c }
-    deriving Show
-
--- Load a protocol.  On success, returns a Prot record.
-
-loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->
-            Pos -> [SExpr Pos] -> m (Prot t g c)
-loadProt nom origin pos (S _ name : S _ alg : x : xs)
-    | alg /= nom =
-        fail (shows pos $ "Expecting terms in algebra " ++ nom)
-    | otherwise =
-        do
-          (gen, rs) <- loadRoles origin (x : xs)
-          (gen', r) <- makeListenerRole pos gen
-          return (Prot { pname = name, pgen = gen', roles = r : rs })
-loadProt _ _ pos _ =
-    fail (shows pos "Malformed protocol")
-
--- A generator is threaded thoughout the protocol loading process so
--- as to ensure no variable occurs in two roles.  It also ensures that
--- every variable that occurs in a preskeleton never occurs in one of
--- its roles.
-
-loadRoles :: (Algebra t p g s e c, Monad m) => g ->
-             [SExpr Pos] -> m (g, [Role t c])
-loadRoles origin xs =
-    mapAccumLM loadRole origin $ stripComments xs
-
-stripComments :: [SExpr Pos] -> [SExpr Pos]
-stripComments xs =
-    filter pred xs
-    where
-      pred (L _ (S _ sym : _)) = sym == "defrole"
-      pred _ = True             -- Catch bad entries
-
--- A monad version of map accumulation from the left
-mapAccumLM :: Monad m => (a -> b -> m (a, c)) -> a -> [b] -> m (a, [c])
-mapAccumLM _ z [] =
-    return (z, [])
-mapAccumLM f z (x : xs) =
-    do
-      (z', y) <- f z x
-      (z'', ys) <- mapAccumLM f z' xs
-      return (z'', y : ys)
-
-loadRole :: (Algebra t p g s e c, Monad m) => g ->
-            SExpr Pos -> m (g, Role t c)
-loadRole gen (L _ (S _ "defrole" :
-                     S _ name :
-	             L _ (S _ "vars" : vars) :
-                     L _ (S _ "trace" : _ : _) :
-                     _)) =
-    do
-      (gen, vars) <- loadVars gen vars
-      let ctx = addToContext emptyContext vars
-      let r = Role { rname = name, vars = vars, ctx = ctx }
-      return (gen, r)
-loadRole _ x =
-    fail (shows (annotation x) "Malformed role")
-
--- A protocol's listener role
-
-listenerName :: String
-listenerName = ""
-
-makeListenerRole :: (Algebra t p g s e c, Monad m) => Pos -> g ->
-                    m (g, Role t c)
-makeListenerRole pos gen =
-    do
-      (gen', t) <- makeVar pos gen "x"
-      let vars = [t]
-      let ctx = addToContext emptyContext vars
-      let r = Role { rname = listenerName, vars = vars, ctx = ctx }
-      return (gen', r)
-
-makeVar :: (Algebra t p g s e c, Monad m) => Pos -> g -> String -> m (g, t)
-makeVar pos gen name =
-    do
-      (gen', ts) <- loadVars gen [L pos [S pos name, S pos "mesg"]]
-      case ts of
-        [t] -> return (gen', t)
-        _ -> fail (shows pos "Bad variable generation")
-
--- Find a protocol
-
-findProt :: (Algebra t p g s e c, Monad m) => Pos ->
-            [Prot t g c] -> [SExpr Pos] -> m (Prot t g c)
-findProt pos ps (S _ name : _) =
-    case L.find (\p -> name == pname p) ps of
-      Nothing -> fail (shows pos $ "Protocol " ++ name ++ " unknown")
-      Just p -> return p
-findProt pos _ _ = fail (shows pos "Malformed skeleton")
-
--- Load a preskeleton
-
-data Instance t c = Instance
-    { pos :: Pos,               -- Instance position
-      role :: Role t c,         -- Role from which this was instantiated
-      env :: [(t, t)],          -- The environment
-      height :: Int,            -- Height of the instance
-      strand :: t }             -- Variable associated with the instance
-    deriving Show
-
-type Strands = [Int]            -- [Strand height]
-
-type Node = (Int, Int)          -- (Strand, Position)
-
-type Pair = (Node, Node)        -- Precedes relation
-
-data Preskel t g c = Preskel
-    { protocol :: Prot t g c,
-      kgen :: g,                -- Final generator
-      kvars :: [t],             -- Variables excluding strand vars
-      insts :: [Instance t c],
-      orderings :: [Pair],
-      nons :: [t],
-      uniqs :: [t],
-      origs :: [(t, Node)],
-      isSkeleton :: Bool,
-      isShape :: !Bool,         -- Always looked at, so make it strict
-      homomorphisms :: [SExpr Pos], -- Loaded later
-      kctx :: c }
-
-loadPreskel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->
-               g -> c -> [SExpr Pos] -> m (Preskel t g c)
-loadPreskel _ prot gen ctx (S _ _ : L _ (S _ "vars" : vars) : xs) =
-    do
-      (gen', kvars) <- loadVars gen vars
-      (gen'', insts) <- loadInsts prot gen' kvars [] xs
-      let strands = map strand insts
-      let heights = map height insts
-      orderings <- loadOrderings heights (assoc precedesKey xs)
-      nons <- loadBaseTerms kvars (assoc nonOrigKey xs)
-      uniqs <- loadBaseTerms kvars (assoc uniqOrigKey xs)
-      origs <- loadOrigs kvars heights (assoc origsKey xs)
-      let kctx = addToContext ctx (kvars ++ strands)
-      return (Preskel { protocol = prot,
-                        kgen = gen'',
-                        kvars = kvars,
-                        insts = insts,
-                        orderings = orderings,
-                        nons = nons,
-                        uniqs = uniqs,
-                        origs = origs,
-                        isSkeleton = not $ hasKey preskeletonKey xs,
-                        isShape = hasKey shapeKey xs,
-                        homomorphisms = assoc mapsKey xs,
-                        kctx = kctx })
-loadPreskel pos _ _ _ _ = fail (shows pos "Malformed skeleton")
-
-loadInsts :: (Algebra t p g s e c, Monad m) => Prot t g c ->
-             g -> [t] -> [Instance t c] -> [SExpr Pos] -> m (g, [Instance t c])
-loadInsts prot gen kvars insts (L pos (S _ "defstrand" : x) : xs) =
-    case x of
-      S _ role : N _ height : env ->
-          do
-            (gen', i) <- loadInst pos prot gen kvars role height env
-            loadInsts prot gen' kvars (i : insts) xs
-      _ ->
-          fail (shows pos "Malformed defstrand")
-loadInsts prot gen kvars insts (L pos (S _ "deflistener" : x) : xs) =
-    case x of
-      [term] ->
-          do
-            (gen', i) <- loadListener pos prot kvars gen term
-            loadInsts prot gen' kvars (i : insts) xs
-      _ ->
-          fail (shows pos "Malformed deflistener")
-loadInsts _ gen _ insts _ =
-    return (gen, reverse insts)
-
-loadInst :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->
-            g -> [t] -> String -> Int -> [SExpr Pos] -> m (g, Instance t c)
-loadInst pos prot gen kvars role height env =
-    do
-      r <- lookupRole pos prot role
-      env <- mapM (loadMaplet kvars (vars r)) env
-      (gen', t) <- makeVar pos gen "z" -- Make the strand variable
-      -- The sort of t will be fixed on output--see function skel.
-      return (gen', Instance { pos = pos, role = r,
-                               env = env, height = height,
-                               strand = t })
-
-lookupRole :: (Algebra t p g s e c, Monad m) => Pos ->
-              Prot t g c -> String -> m (Role t c)
-lookupRole pos prot role =
-    case L.find (\r -> role == rname r) (roles prot) of
-      Nothing ->
-          fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname prot)
-      Just r -> return r
-
-loadMaplet :: (Algebra t p g s e c, Monad m) =>
-              [t] -> [t] -> SExpr Pos -> m (t, t)
-loadMaplet kvars vars (L _ [domain, range]) =
-    do
-      t <- loadTerm vars domain
-      t' <- loadTerm kvars range
-      return (t, t')
-loadMaplet _ _ x = fail (shows (annotation x) "Malformed maplet")
-
-loadListener :: (Algebra t p g s e c, Monad m) => Pos ->
-                Prot t g c -> [t] -> g -> SExpr Pos -> m (g, Instance t c)
-loadListener pos prot kvars gen x =
-    do
-      r <- lookupRole pos prot listenerName
-      t <- loadTerm kvars x
-      (gen', z) <- makeVar pos gen "z" -- Make the strand variable
-      return (gen', Instance { pos = pos, role = r,
-                               env = [(head $ vars r, t)], height = 2,
-                               strand = z })
-
--- Load the node orderings
-
-loadOrderings :: Monad m => Strands -> [SExpr Pos] -> m [Pair]
-loadOrderings _ [] = return []
-loadOrderings strands (x : xs) =
-    do
-      np <- loadPair strands x
-      nps <- loadOrderings strands xs
-      return (adjoin np nps)
-
-loadPair :: Monad m => [Int] -> SExpr Pos -> m Pair
-loadPair heights (L pos [x0, x1]) =
-    do
-      n0 <- loadNode heights x0
-      n1 <- loadNode heights x1
-      case sameStrands n0 n1 of  -- Same strand
-        True -> fail (shows pos "Malformed pair -- nodes in same strand")
-        False -> return (n0, n1)
-    where
-      sameStrands (s0, _) (s1, _) = s0 == s1
-loadPair _ x = fail (shows (annotation x) "Malformed pair")
-
-loadNode :: Monad m => [Int] -> SExpr Pos -> m Node
-loadNode heights (L pos [N _ s, N _ p])
-    | s < 0 = fail (shows pos "Negative strand in node")
-    | p < 0 = fail (shows pos "Negative position in node")
-    | otherwise =
-        case height heights s of
-          Nothing -> fail (shows pos "Bad strand in node")
-          Just h | p < h -> return (s, p)
-          _ -> fail (shows pos "Bad position in node")
-    where
-      height [] _ = Nothing
-      height (x: xs) s          -- Assume s non-negative
-          | s == 0 = Just x
-          | otherwise = height xs (s - 1)
-loadNode _ x = fail (shows (annotation x) "Malformed node")
-
-loadBaseTerms :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [t]
-loadBaseTerms _ [] = return []
-loadBaseTerms vars (x : xs) =
-    do
-      t <- loadBaseTerm vars x
-      ts <- loadBaseTerms vars xs
-      return (adjoin t ts)
-
-loadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t
-loadBaseTerm vars x =
-    do
-      t <- loadTerm vars x
-      case isAtom t of
-        True -> return t
-        False -> fail (shows (annotation x) "Expecting an atom")
-
-loadOrigs :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->
-             [SExpr Pos] -> m [(t, Node)]
-loadOrigs _ _ [] = return []
-loadOrigs vars heights (x : xs) =
-    do
-      o <- loadOrig vars heights x
-      os <- loadOrigs vars heights xs
-      return (adjoin o os)
-
-loadOrig :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->
-            SExpr Pos -> m (t, Node)
-loadOrig vars heights (L _ [x, y]) =
-    do
-      t <- loadTerm vars x
-      n <- loadNode heights y
-      return (t, n)
-loadOrig _ _ x =
-    fail (shows (annotation x) "Malformed origination")
-
--- Homomorphisms
-
--- The maps entry in a preskeleton contains a list of homomorphisms.
--- A homomorphism is a list of length two, a strand map as a list of
--- natural numbers, and a substition.
-
-loadMaps :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
-            Preskel t g c -> [SExpr Pos] -> m [[SExpr ()]]
-loadMaps pov k maps =
-    mapM (loadMap pov k) maps
-
-loadMap :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
-            Preskel t g c -> SExpr Pos -> m [SExpr ()]
-loadMap pov k (L _ [L _ strandMap, L _ algebraMap]) =
-    do
-      let zs = map strand $ insts pov
-      perm <- mapM loadPerm strandMap -- Load the strand map
-      let zs' = map strand $ insts k
-      let zh = [(t, zs' !! p) | (t, p) <- zip zs perm]
-      -- Compute the strand part of the homomorphism
-      let eqs = map (displayEq $ kctx k) zh
-      -- Load the algebra part of the homomorphism
-      ah <- mapM (loadMaplet (kvars k) (kvars pov)) algebraMap
-      -- Compute the algebra part of the homomorphism
-      let eqa = map (displayEq $ kctx k) ah
-      return (eqs ++ eqa)
-loadMap _ _ x = fail (shows (annotation x) "Malformed map")
-
-loadPerm :: Monad m => SExpr Pos -> m Int
-loadPerm (N _ n) | n >= 0 = return n
-loadPerm x = fail (shows (annotation x) "Expecting a natural number")
-
-displayEq :: Algebra t p g s e c => c -> (t, t) -> SExpr ()
-displayEq ctx (x, y) =
-    L () [S () "equal", displayTerm ctx x, displayTerm ctx y]
-
--- Association lists
-
--- Lookup value in alist, appending values with the same key
-assoc :: String -> [SExpr a] -> [SExpr a]
-assoc key alist =
-    concat [ rest | L _ (S _ head : rest) <- alist, key == head ]
-
-keyPred :: String -> SExpr a -> Bool
-keyPred key (L _ (S _ head : _)) = key == head
-keyPred _ _ = False
-
-hasKey :: String -> [SExpr a] -> Bool
-hasKey key alist = any (keyPred key) alist
-
--- The key used to identify a non-skeleton
-preskeletonKey :: String
-preskeletonKey = "preskeleton"
-
--- The key used to identify a shape
-shapeKey :: String
-shapeKey = "shape"
-
--- The key used to extract the list of homomorphisms
-mapsKey :: String
-mapsKey = "maps"
-
--- The key used in preskeletons for communication orderings
-precedesKey :: String
-precedesKey = "precedes"
-
--- The key used in preskeletons for non-originating atoms
-nonOrigKey :: String
-nonOrigKey = "non-orig"
-
--- The key used in preskeletons for uniquely originating atoms
-uniqOrigKey :: String
-uniqOrigKey = "uniq-orig"
-
--- The key used to extract the nodes of origination
-origsKey :: String
-origsKey = "origs"
-
--- Formula printing
-
-displayFormula :: (Algebra t p g s e c, Monad m) =>
-                  [Prot t g c] -> [Preskel t g c] ->
-                  m (State t g c, Maybe (SExpr ()))
-displayFormula ps [] =
-    return ((ps, []), Nothing)
-displayFormula ps (k : ks) =
-    do
-      sexpr <- form k ks
-      return ((ps, []), Just sexpr)
-
-form :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
-        [Preskel t g c] -> m (SExpr ())
-form k ks =                     -- k is the POV skeleton
-    do                          -- ks is the list of shapes
-      (vars, conj) <- skel k
-      disj <- mapM (shape k) ks
-      return $ quantify "forall" vars
-                 (imply (conjoin conj) (disjoin disj))
-
--- Convert one skeleton into a declaration and a conjunction.  The
--- declaration is used as the bound variables in a quantifier.
-skel :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
-        m ([SExpr ()], [SExpr ()])
-skel k =
-    do
-      let vars = displayVars (kctx k) (kvars k)
-      let strands = displayVars (kctx k) (map strand $ insts k)
-      return (vars ++ listMap nat strands,
-              map (strandForm k) (insts k) ++
-              map (precForm k) (orderings k) ++
-              map (unary "non" $ kctx k) (nons k) ++
-              map (unary "uniq" $ kctx k) (uniqs k) ++
-              map (origForm k) (origs k))
-
-listMap :: ([SExpr ()] -> [SExpr ()]) -> [SExpr ()] -> [SExpr ()]
-listMap _ [] = []
-listMap f (L () xs : ys) = L () (f xs) : listMap f ys
-listMap f (y : ys) = y : listMap f ys
-
--- Replace "mesg" as the sort in the list with "nat"
-nat :: [SExpr ()] -> [SExpr ()]
-nat [] = error "Logic.nat: empty list as argument"
-nat [_] = [S () "nat"]
-nat (v : vs) = v : nat vs
-
--- Creates the atomic formulas used to describe an instance of a role
-strandForm :: Algebra t p g s e c => Preskel t g c ->
-              Instance t c -> SExpr ()
-strandForm k inst =
-    conjoin $ map f $ env inst
-    where
-      f (x, t) =
-          L () [S () "strand",
-                Q () $ pname $ protocol k, -- Name of the protocol
-                Q () $ rname $ role inst, -- Name of the role
-                N () $ height inst,
-                quote $ displayTerm (ctx $ role inst) x,
-                displayTerm (kctx k) (strand inst),
-                displayTerm (kctx k) t]
-
-quote :: SExpr () -> SExpr ()
-quote (S () str) = Q () str
-quote x = x
-
--- Creates the atomic formula used to describe a node ordering relation
-precForm :: Algebra t p g s e c => Preskel t g c -> Pair -> SExpr ()
-precForm k ((s, i), (s', i')) =
-    L () [S () "prec",
-          displayTerm (kctx k) t,
-          N () i,
-          displayTerm (kctx k) t',
-          N () i']
-    where
-      t = strand $ insts k !! s
-      t' = strand $ insts k !! s'
-
-origForm :: Algebra t p g s e c => Preskel t g c ->
-            (t, Node) -> SExpr ()
-origForm k (t, (s, i)) =
-    L () [S () "orig",
-          displayTerm (kctx k) t,
-          displayTerm (kctx k) z,
-          N () i]
-    where
-      z = strand $ insts k !! s
-
--- Creates a formula associated with a shape.  It is a disjunction of
--- existentially quantified formulas that describe the homomorphism
--- and the shape as a skeleton.
-shape :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
-         Preskel t g c -> m (SExpr ())
-shape pov k =
-    do
-      (vars, conj) <- skel k
-      case null $ homomorphisms k of
-        True -> fail "No homomorphism for shape"
-        False ->
-            do
-              hs <- loadMaps pov k (homomorphisms k)
-              let xs = [quantify "exists" vars $ conjoin (h ++ conj) | h <- hs]
-              return $ disjoin xs
-
--- Formula primitives
-
-unary :: Algebra t p g s e c => String -> c -> t -> SExpr ()
-unary pred ctx t =
-    L () [S () pred, displayTerm ctx t]
-
-quantify :: String -> [SExpr ()] -> SExpr () -> SExpr ()
-quantify _ [] form = form
-quantify name vars form =
-    L () [S () name, L () vars, form]
-
-conjoin :: [SExpr ()] -> SExpr ()
-conjoin conjuncts =
-    case concatMap f conjuncts of
-      [x] -> x
-      xs -> L () (S () "and" : xs)
-    where
-      f (L () (S () "and" : xs)) = xs
-      f x = [x]
-
-disjoin :: [SExpr ()] -> SExpr ()
-disjoin conjuncts =
-    case concatMap f conjuncts of
-      [x] -> x
-      xs -> L () (S () "or" : xs)
-    where
-      f (L () (S () "or" : xs)) = xs
-      f x = [x]
-
-imply :: SExpr () -> SExpr () -> SExpr ()
-imply (L () [S () "and"]) consequence = consequence
-imply antecedent consequence =
-    L () [S () "implies", antecedent, consequence]
diff --git a/src/CPSA/Logic/Main.hs b/src/CPSA/Logic/Main.hs
deleted file mode 100644
--- a/src/CPSA/Logic/Main.hs
+++ /dev/null
@@ -1,87 +0,0 @@
--- Summarize CPSA output as a formula in coherent logic
-
--- Copyright (c) 2011 The MITRE Corporation
---
--- This program is free software: you can redistribute it and/or
--- modify it under the terms of the BSD License as published by the
--- University of California.
-
-module Main (main) where
-
-import System.IO
-import CPSA.Lib.CPSA
-import CPSA.Lib.Entry
-import CPSA.Logic.Logic
-import qualified CPSA.Basic.Algebra
-import qualified CPSA.DiffieHellman.Algebra
-
--- Algebra names
-algs :: [String]
-algs = [CPSA.Basic.Algebra.name, CPSA.DiffieHellman.Algebra.name]
-
-main :: IO ()
-main =
-    do
-      let options = algOptions CPSA.Basic.Algebra.name
-      let interp = algInterp CPSA.Basic.Algebra.name algs
-      (p, (output, alg, margin)) <- start options interp
-      h <- outputHandle output
-      writeComment h margin cpsaVersion
-      writeComment h margin "Coherent logic"
-      case () of
-        _ | alg == CPSA.Basic.Algebra.name ->
-              go (step h alg CPSA.Basic.Algebra.origin margin)
-                 p ([], [])
-          | alg == CPSA.DiffieHellman.Algebra.name ->
-              go (step h alg CPSA.DiffieHellman.Algebra.origin margin)
-                 p ([], [])
-          | otherwise ->
-               abort ("Bad algebra: " ++ alg)
-      hClose h
-
-go :: (a -> Maybe (SExpr Pos) -> IO a) -> PosHandle -> a -> IO ()
-go f p a =
-    loop a
-    where
-      loop a =
-          do
-            x <- readSExpr p
-            case x of
-              Nothing ->
-                  do
-                    _ <- f a x
-                    return ()
-              Just _ ->
-                  do
-                    a <- f a x
-                    loop a
-
-step :: Algebra t p g s e c => Handle ->
-        String -> g -> Int -> State t g c ->
-        Maybe (SExpr Pos) -> IO (State t g c)
-step output _ _ margin state@([], []) (Just sexpr@(L _ (S _ cmt : _)))
-     | cmt == "herald" || cmt == "comment" =
-         do
-           writeLnSEexpr output margin sexpr
-           return state
-step output name origin margin state sexpr =
-    do
-      x <- tryIO (logic name origin state sexpr)
-      case x of
-        Right (acc, Nothing) ->
-            after output margin acc sexpr
-        Right (acc, Just x) ->
-            do
-              writeLnSEexpr output margin x
-              after output margin acc sexpr
-        Left err ->
-            abort (show err)
-
-after :: Algebra t p g s e c => Handle -> Int -> State t g c ->
-         Maybe (SExpr Pos) -> IO (State t g c)
-after output margin state (Just sexpr@(L _ (S _ "defprotocol" : _))) =
-    do
-      writeLnSEexpr output margin sexpr
-      return state
-after _ _ state _ =
-    return state
diff --git a/src/CPSA/SAS/Main.hs b/src/CPSA/SAS/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/CPSA/SAS/Main.hs
@@ -0,0 +1,87 @@
+-- Summarize CPSA output as a formula in coherent logic
+
+-- Copyright (c) 2011 The MITRE Corporation
+--
+-- This program is free software: you can redistribute it and/or
+-- modify it under the terms of the BSD License as published by the
+-- University of California.
+
+module Main (main) where
+
+import System.IO
+import CPSA.Lib.CPSA
+import CPSA.Lib.Entry
+import CPSA.SAS.SAS
+import qualified CPSA.Basic.Algebra
+import qualified CPSA.DiffieHellman.Algebra
+
+-- Algebra names
+algs :: [String]
+algs = [CPSA.Basic.Algebra.name, CPSA.DiffieHellman.Algebra.name]
+
+main :: IO ()
+main =
+    do
+      let options = algOptions CPSA.Basic.Algebra.name
+      let interp = algInterp CPSA.Basic.Algebra.name algs
+      (p, (output, alg, margin)) <- start options interp
+      h <- outputHandle output
+      writeComment h margin cpsaVersion
+      writeComment h margin "Coherent logic"
+      case () of
+        _ | alg == CPSA.Basic.Algebra.name ->
+              go (step h alg CPSA.Basic.Algebra.origin margin)
+                 p ([], [])
+          | alg == CPSA.DiffieHellman.Algebra.name ->
+              go (step h alg CPSA.DiffieHellman.Algebra.origin margin)
+                 p ([], [])
+          | otherwise ->
+               abort ("Bad algebra: " ++ alg)
+      hClose h
+
+go :: (a -> Maybe (SExpr Pos) -> IO a) -> PosHandle -> a -> IO ()
+go f p a =
+    loop a
+    where
+      loop a =
+          do
+            x <- readSExpr p
+            case x of
+              Nothing ->
+                  do
+                    _ <- f a x
+                    return ()
+              Just _ ->
+                  do
+                    a <- f a x
+                    loop a
+
+step :: Algebra t p g s e c => Handle ->
+        String -> g -> Int -> State t g c ->
+        Maybe (SExpr Pos) -> IO (State t g c)
+step output _ _ margin state@([], []) (Just sexpr@(L _ (S _ cmt : _)))
+     | cmt == "herald" || cmt == "comment" =
+         do
+           writeLnSEexpr output margin sexpr
+           return state
+step output name origin margin state sexpr =
+    do
+      x <- tryIO (sas name origin state sexpr)
+      case x of
+        Right (acc, Nothing) ->
+            after output margin acc sexpr
+        Right (acc, Just x) ->
+            do
+              writeLnSEexpr output margin x
+              after output margin acc sexpr
+        Left err ->
+            abort (show err)
+
+after :: Algebra t p g s e c => Handle -> Int -> State t g c ->
+         Maybe (SExpr Pos) -> IO (State t g c)
+after output margin state (Just sexpr@(L _ (S _ "defprotocol" : _))) =
+    do
+      writeLnSEexpr output margin sexpr
+      return state
+after _ _ state _ =
+    return state
diff --git a/src/CPSA/SAS/SAS.hs b/src/CPSA/SAS/SAS.hs
new file mode 100644
--- /dev/null
+++ b/src/CPSA/SAS/SAS.hs
@@ -0,0 +1,752 @@
+-- Converts a solution to a problem into a coherent logic formula
+
+-- Copyright (c) 2011 The MITRE Corporation
+--
+-- This program is free software: you can redistribute it and/or
+-- modify it under the terms of the BSD License as published by the
+-- University of California.
+
+module CPSA.SAS.SAS (Prot, Preskel, State, sas) where
+
+import Control.Monad (foldM)
+import qualified Data.List as L
+import qualified Data.Map as M
+import CPSA.Lib.CPSA
+
+{--
+import System.IO.Unsafe
+z :: Show a => a -> b -> b
+z x y = unsafePerformIO (print x >> return y)
+--}
+
+-- The root used for generated node names.
+root :: String
+root = "z"
+
+type State t g c = ([Prot t g c], [Preskel t g c])
+
+sas :: (Algebra t p g s e c, Monad m) => String -> g ->
+         State t g c -> Maybe (SExpr Pos) ->
+         m (State t g c, Maybe (SExpr ()))
+sas _ _ (ps, ks) Nothing =    -- Nothing signifies end-of-file
+    displayFormula ps (reverse ks)
+sas name gen (ps, []) (Just sexpr) = -- Looking for POV skeleton
+    loadPOV name gen ps sexpr
+sas name gen (ps, ks) (Just sexpr) = -- Looking for shapes
+    loadOtherPreskel name gen ps ks sexpr
+
+loadPOV :: (Algebra t p g s e c, Monad m) => String -> g ->
+           [Prot t g c] -> SExpr Pos ->
+           m (State t g c, Maybe (SExpr ()))
+loadPOV name origin ps (L pos (S _ "defprotocol" : xs)) =
+    do
+      p <- loadProt name origin pos xs
+      return ((p : ps, []), Nothing)
+loadPOV _ _ ps (L pos (S _ "defskeleton" : xs)) =
+    do
+      p <- findProt pos ps xs
+      k <- loadPreskel pos p (pgen p) xs
+      case (isSkeleton k, isShape k) of
+        (True, False) ->
+          do                    -- Found POV
+            origCheck pos k     -- Ensure uniqs originate
+            return ((ps, [k]), Nothing)
+        _ -> return ((ps, []), Nothing) -- Not POV
+loadPOV _ _ ps _ = return ((ps, []), Nothing)
+
+loadOtherPreskel :: (Algebra t p g s e c, Monad m) => String -> g ->
+                    [Prot t g c] -> [Preskel t g c] ->
+                    SExpr Pos -> m (State t g c, Maybe (SExpr ()))
+loadOtherPreskel name origin ps ks (L pos (S _ "defprotocol" : xs)) =
+    do                     -- Found next protocol.  Print this formula
+      p <- loadProt name origin pos xs
+      displayFormula (p : ps) (reverse ks)
+loadOtherPreskel _ _ ps ks (L pos (S _ "defskeleton" : xs)) =
+    do
+      p <- findProt pos ps xs
+      let g = kgen (last ks)      -- Make sure vars in skeleton are
+      k <- loadPreskel pos p g xs -- distinct from the ones in the POV
+      case isShape k of
+        True ->
+          do                    -- Found shape
+            origCheck pos k     -- Ensure uniqs originate
+            return ((ps, k : ks), Nothing)
+        False -> return ((ps, ks), Nothing) -- Found intermediate skeleton
+loadOtherPreskel _ _ ps ks _ = return ((ps, ks), Nothing)
+
+-- Ensure every uniq originates
+origCheck :: (Algebra t p g s e c, Monad m) =>
+             Pos -> Preskel t g c -> m ()
+origCheck pos k =
+  mapM_ f (uniqs k)
+  where
+    f t | any (\(t', _) -> t == t') (origs k) = return ()
+        | otherwise =
+      fail (shows pos "Uniq " ++ u ++ " has no origination point")
+      where
+        u = pp 0 0 (displayTerm ctx t)
+        ctx = addToContext emptyContext (kvars k)
+
+-- Load a protocol
+
+-- The Prot record contains information extraced from protocols for
+-- use when processing preskeletons.  A protocol includes a role for
+-- all listeners.
+data Prot t g c = Prot
+    { pname :: String,          -- Protocol name
+      pgen :: g,                -- Generator for preskeletons
+      roles :: [Role t c] }
+    deriving Show
+
+-- The Role record contains information extraced from roles for use
+-- when processing preskeletons.
+data Role t c = Role
+    { rname :: String,          -- Role name
+      vars :: [t],
+      ctx :: c }
+    deriving Show
+
+-- Load a protocol.  On success, returns a Prot record.
+
+loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->
+            Pos -> [SExpr Pos] -> m (Prot t g c)
+loadProt nom origin pos (S _ name : S _ alg : x : xs)
+    | alg /= nom =
+        fail (shows pos $ "Expecting terms in algebra " ++ nom)
+    | otherwise =
+        do
+          (gen, rs) <- loadRoles origin (x : xs)
+          (gen', r) <- makeListenerRole pos gen
+          return (Prot { pname = name, pgen = gen', roles = r : rs })
+loadProt _ _ pos _ =
+    fail (shows pos "Malformed protocol")
+
+-- A generator is threaded thoughout the protocol loading process so
+-- as to ensure no variable occurs in two roles.  It also ensures that
+-- every variable that occurs in a preskeleton never occurs in one of
+-- its roles.
+
+loadRoles :: (Algebra t p g s e c, Monad m) => g ->
+             [SExpr Pos] -> m (g, [Role t c])
+loadRoles origin xs =
+    mapAccumLM loadRole origin $ stripComments xs
+
+stripComments :: [SExpr Pos] -> [SExpr Pos]
+stripComments xs =
+    filter pred xs
+    where
+      pred (L _ (S _ sym : _)) = sym == "defrole"
+      pred _ = True             -- Catch bad entries
+
+-- A monad version of map accumulation from the left
+mapAccumLM :: Monad m => (a -> b -> m (a, c)) -> a -> [b] -> m (a, [c])
+mapAccumLM _ z [] =
+    return (z, [])
+mapAccumLM f z (x : xs) =
+    do
+      (z', y) <- f z x
+      (z'', ys) <- mapAccumLM f z' xs
+      return (z'', y : ys)
+
+loadRole :: (Algebra t p g s e c, Monad m) => g ->
+            SExpr Pos -> m (g, Role t c)
+loadRole gen (L _ (S _ "defrole" :
+                     S _ name :
+	             L _ (S _ "vars" : vars) :
+                     L _ (S _ "trace" : _ : _) :
+                     _)) =
+    do
+      (gen, vars) <- loadVars gen vars
+      let ctx = addToContext emptyContext vars
+      let r = Role { rname = name, vars = vars, ctx = ctx }
+      return (gen, r)
+loadRole _ x =
+    fail (shows (annotation x) "Malformed role")
+
+-- A protocol's listener role
+
+listenerName :: String
+listenerName = ""
+
+makeListenerRole :: (Algebra t p g s e c, Monad m) => Pos -> g ->
+                    m (g, Role t c)
+makeListenerRole pos gen =
+    do
+      (gen', t) <- makeVar pos gen "x"
+      let vars = [t]
+      let ctx = addToContext emptyContext vars
+      let r = Role { rname = listenerName, vars = vars, ctx = ctx }
+      return (gen', r)
+
+makeVar :: (Algebra t p g s e c, Monad m) => Pos -> g -> String -> m (g, t)
+makeVar pos gen name =
+    do
+      (gen', ts) <- loadVars gen [L pos [S pos name, S pos "mesg"]]
+      case ts of
+        [t] -> return (gen', t)
+        _ -> fail (shows pos "Bad variable generation")
+
+-- Node to variable maps
+
+-- A variable map maps nodes to variables
+
+type VM t = M.Map Node t
+
+-- A generator and a variable map
+type GVM g t = (g, VM t)
+
+-- Add a variable for a node if the mapping does not already exist.
+addVar :: (Algebra t p g s e c, Monad m) =>
+          Pos -> GVM g t -> Node -> m (GVM g t)
+addVar pos (gen, vm) n =
+  case M.lookup n vm of
+    Just _ -> return (gen, vm)
+    Nothing ->
+      do
+        (gen, t) <- makeVar pos gen root -- Make the variable
+        return (gen, M.insert n t vm)
+
+-- Node lookup assumes a node will always be found.
+nlookup :: Node -> VM t -> t
+nlookup n vm =
+  case M.lookup n vm of
+    Just t -> t
+    Nothing -> error ("SAS.lookup: cannot find " ++ show n)
+
+-- Find a protocol
+
+findProt :: (Algebra t p g s e c, Monad m) => Pos ->
+            [Prot t g c] -> [SExpr Pos] -> m (Prot t g c)
+findProt pos ps (S _ name : _) =
+    case L.find (\p -> name == pname p) ps of
+      Nothing -> fail (shows pos $ "Protocol " ++ name ++ " unknown")
+      Just p -> return p
+findProt pos _ _ = fail (shows pos "Malformed skeleton")
+
+-- Load a preskeleton
+
+data Instance t c = Instance
+    { pos :: Pos,               -- Instance position
+      role :: Role t c,         -- Role from which this was instantiated
+      env :: [(t, t)],          -- The environment
+      height :: Int }           -- Height of the instance
+    deriving Show
+
+type Strands = [Int]            -- [Strand height]
+
+type Node = (Int, Int)          -- (Strand, Position)
+
+type Pair = (Node, Node)        -- Precedes relation
+
+data Preskel t g c = Preskel
+    { protocol :: Prot t g c,
+      kgen :: g,                -- Final generator
+      kvars :: [t],             -- Algebra variables
+      knodes :: [t],            -- Node variables
+      insts :: [Instance t c],
+      strands :: [t],           -- A node for each instance
+      orderings :: [(t, t)],
+      succs :: [(t, t)],
+      nons :: [t],
+      uniqs :: [t],
+      origs :: [(t, t)],
+      isSkeleton :: Bool,
+      isShape :: !Bool,         -- Always looked at, so make it strict
+      homomorphisms :: [SExpr Pos], -- Loaded later
+      varmap :: VM t }
+
+loadPreskel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->
+               g -> [SExpr Pos] -> m (Preskel t g c)
+loadPreskel pos prot gen (S _ _ : L _ (S _ "vars" : vars) : xs) =
+    do
+      (gen, kvars) <- loadVars gen vars
+      insts <- loadInsts prot kvars [] xs
+      let heights = map height insts
+      orderings <- loadOrderings heights (assoc precedesKey xs)
+      nons <- loadBaseTerms kvars (assoc nonOrigKey xs)
+      uniqs <- loadBaseTerms kvars (assoc uniqOrigKey xs)
+      origs <- loadOrigs kvars heights (assoc origsKey xs)
+      let strands = map (\(s, h) -> (s, h - 1)) (zip [0..] heights)
+      (gen, varmap) <- makeVarmap pos gen strands orderings origs
+      let f (n0, n1) = (nlookup n0 varmap, nlookup n1 varmap)
+      let g (t, n) = (t, nlookup n varmap)
+      return (Preskel { protocol = prot,
+                        kgen = gen,
+                        kvars = kvars,
+                        knodes = M.elems varmap,
+                        insts = insts,
+                        strands = map (flip nlookup varmap) strands,
+                        orderings = map f orderings,
+                        succs = loadSuccs varmap,
+                        nons = nons,
+                        uniqs = uniqs,
+                        origs = map g origs,
+                        isSkeleton = not $ hasKey preskeletonKey xs,
+                        isShape = hasKey shapeKey xs,
+                        homomorphisms = assoc mapsKey xs,
+                        varmap = varmap})
+loadPreskel pos _ _ _ = fail (shows pos "Malformed skeleton")
+
+loadInsts :: (Algebra t p g s e c, Monad m) => Prot t g c ->
+             [t] -> [Instance t c] -> [SExpr Pos] -> m [Instance t c]
+loadInsts prot kvars insts (L pos (S _ "defstrand" : x) : xs) =
+    case x of
+      S _ role : N _ height : env ->
+          do
+            i <- loadInst pos prot kvars role height env
+            loadInsts prot kvars (i : insts) xs
+      _ ->
+          fail (shows pos "Malformed defstrand")
+loadInsts prot kvars insts (L pos (S _ "deflistener" : x) : xs) =
+    case x of
+      [term] ->
+          do
+            i <- loadListener pos prot kvars term
+            loadInsts prot kvars (i : insts) xs
+      _ ->
+          fail (shows pos "Malformed deflistener")
+loadInsts _ _ insts _ =
+    return (reverse insts)
+
+loadInst :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->
+            [t] -> String -> Int -> [SExpr Pos] -> m (Instance t c)
+loadInst pos prot kvars role height env =
+    do
+      r <- lookupRole pos prot role
+      env <- mapM (loadMaplet kvars (vars r)) env
+      return (Instance { pos = pos, role = r,
+                         env = env, height = height })
+
+lookupRole :: (Algebra t p g s e c, Monad m) => Pos ->
+              Prot t g c -> String -> m (Role t c)
+lookupRole pos prot role =
+    case L.find (\r -> role == rname r) (roles prot) of
+      Nothing ->
+          fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname prot)
+      Just r -> return r
+
+loadMaplet :: (Algebra t p g s e c, Monad m) =>
+              [t] -> [t] -> SExpr Pos -> m (t, t)
+loadMaplet kvars vars (L _ [domain, range]) =
+    do
+      t <- loadTerm vars domain
+      t' <- loadTerm kvars range
+      return (t, t')
+loadMaplet _ _ x = fail (shows (annotation x) "Malformed maplet")
+
+loadListener :: (Algebra t p g s e c, Monad m) => Pos ->
+                Prot t g c -> [t] -> SExpr Pos -> m (Instance t c)
+loadListener pos prot kvars x =
+    do
+      r <- lookupRole pos prot listenerName
+      t <- loadTerm kvars x
+      return (Instance { pos = pos, role = r,
+                         env = [(head $ vars r, t)], height = 2 })
+
+-- Load the node orderings
+
+loadOrderings :: Monad m => Strands -> [SExpr Pos] -> m [Pair]
+loadOrderings _ [] = return []
+loadOrderings strands (x : xs) =
+    do
+      np <- loadPair strands x
+      nps <- loadOrderings strands xs
+      return (adjoin np nps)
+
+loadPair :: Monad m => [Int] -> SExpr Pos -> m Pair
+loadPair heights (L pos [x0, x1]) =
+    do
+      n0 <- loadNode heights x0
+      n1 <- loadNode heights x1
+      case sameStrands n0 n1 of  -- Same strand
+        True -> fail (shows pos "Malformed pair -- nodes in same strand")
+        False -> return (n0, n1)
+    where
+      sameStrands (s0, _) (s1, _) = s0 == s1
+loadPair _ x = fail (shows (annotation x) "Malformed pair")
+
+loadNode :: Monad m => [Int] -> SExpr Pos -> m Node
+loadNode heights (L pos [N _ s, N _ p])
+    | s < 0 = fail (shows pos "Negative strand in node")
+    | p < 0 = fail (shows pos "Negative position in node")
+    | otherwise =
+        case height heights s of
+          Nothing -> fail (shows pos "Bad strand in node")
+          Just h | p < h -> return (s, p)
+          _ -> fail (shows pos "Bad position in node")
+    where
+      height [] _ = Nothing
+      height (x: xs) s          -- Assume s non-negative
+          | s == 0 = Just x
+          | otherwise = height xs (s - 1)
+loadNode _ x = fail (shows (annotation x) "Malformed node")
+
+loadBaseTerms :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [t]
+loadBaseTerms _ [] = return []
+loadBaseTerms vars (x : xs) =
+    do
+      t <- loadBaseTerm vars x
+      ts <- loadBaseTerms vars xs
+      return (adjoin t ts)
+
+loadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t
+loadBaseTerm vars x =
+    do
+      t <- loadTerm vars x
+      case isAtom t of
+        True -> return t
+        False -> fail (shows (annotation x) "Expecting an atom")
+
+-- Creates the atomic formulas used to describe the strand node orderings
+-- Must compute the transitive reduction of the within strand orderings
+loadSuccs :: Algebra t p g s e c => VM t -> [(t, t)]
+loadSuccs varmap =
+    concatMap f idx
+    where
+      ns = M.keys varmap               -- The set of nodes
+      ss = L.sort $ L.nub $ map fst ns -- The ordered set of strands
+      idx = [(s, is) | s <- ss,        -- The per strand indices
+                       let is = L.sort [i | (s', i) <- ns, s' == s]]
+      f (_, []) = error "SAS.loadSuccs: Bad index entry"
+      f (_, [_]) = []
+      f (s, i:i':is) =
+        (nlookup (s, i) varmap, nlookup (s, i') varmap):f(s, i':is)
+
+loadOrigs :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->
+             [SExpr Pos] -> m [(t, Node)]
+loadOrigs _ _ [] = return []
+loadOrigs vars heights (x : xs) =
+    do
+      o <- loadOrig vars heights x
+      os <- loadOrigs vars heights xs
+      return (adjoin o os)
+
+loadOrig :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->
+            SExpr Pos -> m (t, Node)
+loadOrig vars heights (L _ [x, y]) =
+    do
+      t <- loadTerm vars x
+      n <- loadNode heights y
+      return (t, n)
+loadOrig _ _ x =
+    fail (shows (annotation x) "Malformed origination")
+
+-- Homomorphisms
+
+-- The maps entry in a preskeleton contains a list of homomorphisms.
+-- A homomorphism is a list of length two, a strand map as a list of
+-- natural numbers, and a substition.
+
+type Homo t = ([(t, t)], [(t, t)])
+
+loadMaps :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
+            Preskel t g c -> [SExpr Pos] -> m [Homo t]
+loadMaps pov k maps =
+    mapM (loadMap pov k) maps
+
+loadMap :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
+            Preskel t g c -> SExpr Pos -> m (Homo t)
+loadMap pov k (L _ [L _ strandMap, L _ algebraMap]) =
+    do
+      perm <- mapM loadPerm strandMap -- Load the strand map
+      let nh = map (loadNodeEq k perm) (M.assocs $ varmap pov)
+      -- Load the algebra part of the homomorphism
+      ah <- mapM (loadMaplet (kvars k) (kvars pov)) algebraMap
+      return (nh, ah)
+loadMap _ _ x = fail (shows (annotation x) "Malformed map")
+
+loadPerm :: Monad m => SExpr Pos -> m Int
+loadPerm (N _ n) | n >= 0 = return n
+loadPerm x = fail (shows (annotation x) "Expecting a natural number")
+
+-- Applies a strand permutation to a node.
+-- Hope the strand map is valid, or !! will blow up.
+loadNodeEq :: Algebra t p g s e c => Preskel t g c ->
+              [Int] -> (Node, t) -> (t, t)
+loadNodeEq k perm ((s, i), v) =
+  (v, nlookup (perm !! s, i) (varmap k))
+
+-- Collect all the relevant nodes and make a variable for each one.
+makeVarmap :: (Algebra t p g s e c, Monad m) => Pos ->
+              g -> [Node] -> [Pair] -> [(t, Node)] -> m (GVM g t)
+makeVarmap pos g strands orderings origs =
+  do
+    gvm <- foldM fht (g, M.empty) strands
+    gvm <- foldM fodr gvm orderings
+    foldM forg  gvm origs
+  where
+    fht gvm n = addVar pos gvm n
+    fodr gvm (n0, n1) =
+      do
+        gvm <- addVar pos gvm n0
+        addVar pos gvm n1
+    forg gvm (_, n) = addVar pos gvm n
+
+-- Association lists
+
+-- Lookup value in alist, appending values with the same key
+assoc :: String -> [SExpr a] -> [SExpr a]
+assoc key alist =
+    concat [ rest | L _ (S _ head : rest) <- alist, key == head ]
+
+keyPred :: String -> SExpr a -> Bool
+keyPred key (L _ (S _ head : _)) = key == head
+keyPred _ _ = False
+
+hasKey :: String -> [SExpr a] -> Bool
+hasKey key alist = any (keyPred key) alist
+
+-- The key used to identify a non-skeleton
+preskeletonKey :: String
+preskeletonKey = "preskeleton"
+
+-- The key used to identify a shape
+shapeKey :: String
+shapeKey = "shape"
+
+-- The key used to extract the list of homomorphisms
+mapsKey :: String
+mapsKey = "maps"
+
+-- The key used in preskeletons for communication orderings
+precedesKey :: String
+precedesKey = "precedes"
+
+-- The key used in preskeletons for non-originating atoms
+nonOrigKey :: String
+nonOrigKey = "non-orig"
+
+-- The key used in preskeletons for uniquely originating atoms
+uniqOrigKey :: String
+uniqOrigKey = "uniq-orig"
+
+-- The key used to extract the nodes of origination
+origsKey :: String
+origsKey = "origs"
+
+type Analysis t g c = (Preskel t g c, [(Homo t, Preskel t g c)])
+
+loadAnalysis :: (Algebra t p g s e c, Monad m) => Preskel t g c ->
+                [Preskel t g c] -> m (Analysis t g c)
+loadAnalysis pov ks =
+  do
+    shapes <- mapM f ks
+    return (pov, concat shapes)
+  where
+    f k =
+      case null $ homomorphisms k of
+        True -> fail "No homomorphism for shape"
+        False ->
+            do
+              hs <- loadMaps pov k (homomorphisms k)
+              return [(h, k) | h <- hs]
+
+-- Eliminate trivial homomorphisms by substituting for the equality
+-- throughout the analysis.
+
+reduce :: Algebra t p g s e c => Analysis t g c -> Analysis t g c
+reduce (pov, shapes) =
+  (pov, map (reduceShape pov) shapes)
+
+reduceShape :: Algebra t p g s e c => Preskel t g c ->
+               (Homo t, Preskel t g c) -> (Homo t, Preskel t g c)
+reduceShape pov (homo, k) =
+  (mapHomo env homo, mapSkel env pov k)
+  where
+    env = snd $head $ homoEnv (kgen k) homo
+
+-- Compute a substition for equalities that equate two variables
+-- of the same sort.
+homoEnv :: Algebra t p g s e c => g -> Homo t -> [(g, e)]
+homoEnv g (a, n) = matchEqs (a ++ n) (g, emptyEnv)
+
+matchEqs :: Algebra t p g s e c => [(t, t)] -> (g, e) -> [(g, e)]
+matchEqs [] env = [env]
+matchEqs (eq:eqs) env =
+  do
+    e <- matchEq eq env
+    matchEqs eqs e
+
+matchEq :: Algebra t p g s e c => (t, t) -> (g, e) -> [(g, e)]
+matchEq (t, p) env
+  | isVar p =                   -- Match fails if there
+    case match p t env of       -- a sort mismatch
+      [] -> [env]
+      e -> e
+  | otherwise = [env]           -- Fail if p is not a variable
+
+-- Apply substitution and remove trival equations.
+mapHomo :: Algebra t p g s e c => e -> Homo t -> Homo t
+mapHomo env (a, n) =
+  (f a, f n)
+  where
+    f eqs = [(p, t1) |
+             (p, t0) <- eqs,
+             let t1 = instantiate env t0,
+             p /= t1]
+
+mapInst :: Algebra t p g s e c => e -> Instance t c -> Instance t c
+mapInst e inst =
+  inst { env = map f (env inst) }
+  where
+    f (p, x) = (p, instantiate e x)
+
+mapSkel :: Algebra t p g s e c => e -> Preskel t g c ->
+           Preskel t g c -> Preskel t g c
+mapSkel env pov k =
+  k { kvars = vs L.\\ kvars pov, -- Delete redundant POV variables
+      knodes = ns L.\\ knodes pov,
+      insts = map (mapInst env) (insts k),
+      strands = map (instantiate env) (strands k),
+      orderings = mapPair (instantiate env) (orderings k),
+      succs = mapPair (instantiate env) (succs k),
+      nons = map (instantiate env) (nons k),
+      uniqs = map (instantiate env) (uniqs k),
+      origs = mapPair (instantiate env) (origs k),
+      varmap = M.map (instantiate env) (varmap k) }
+  where
+    vs = map (instantiate env) (kvars k)
+    ns = map (instantiate env) (knodes k)
+    mapPair f l = map (\(a,b) -> (f a, f b)) l
+
+-- Formula printing
+
+displayFormula :: (Algebra t p g s e c, Monad m) =>
+                  [Prot t g c] -> [Preskel t g c] ->
+                  m (State t g c, Maybe (SExpr ()))
+displayFormula ps [] =
+    return ((ps, []), Nothing)
+displayFormula ps (k : ks) =
+    do
+      analysis <- loadAnalysis k ks
+      return ((ps, []), Just $ form $ reduce analysis)
+
+form :: Algebra t p g s e c => Analysis t g c -> SExpr ()
+form (pov, shapes) =
+  let (c, vars, conj) = skel emptyContext pov in
+  let disj = map (shape c conj) shapes in
+  quantify "forall" vars (imply (conjoin conj) (disjoin disj))
+
+-- Convert one skeleton into a declaration and a conjunction.  The
+-- declaration is used as the bound variables in a quantifier.  The
+-- context is extended so it can be used as input for another
+-- skeleton.
+skel :: Algebra t p g s e c => c -> Preskel t g c ->
+        (c, [SExpr ()], [SExpr ()])
+skel ctx k =
+  let vars = kvars k ++ knodes k in
+  let kctx = addToContext ctx vars in
+  let nodes = displayVars kctx (knodes k) in
+  (kctx,
+   displayVars kctx (kvars k) ++ listMap node nodes,
+   map (nodeForm kctx k) (M.assocs (varmap k)) ++
+   map (strandForm kctx k) (zip (strands k) $ insts k) ++
+   map (precForm kctx) (orderings k) ++
+   map (sprecForm kctx) (succs k) ++
+   map (unary "non" kctx) (nons k) ++
+   map (uniqForm kctx) (origs k))
+
+-- map through lists in an S-Expression.
+listMap :: ([SExpr ()] -> [SExpr ()]) -> [SExpr ()] -> [SExpr ()]
+listMap _ [] = []
+listMap f (L () xs : ys) = L () (f xs) : listMap f ys
+listMap f (y : ys) = y : listMap f ys
+
+-- Replace "mesg" as the sort in the list with "node"
+node :: [SExpr ()] -> [SExpr ()]
+node [] = error "SAS.node: empty list as argument"
+node [_] = [S () "node"]
+node (v : vs) = v : node vs
+
+-- Creates the atomic formulas used to describe an instance of a role
+nodeForm :: Algebra t p g s e c => c -> Preskel t g c ->
+            (Node, t) -> SExpr ()
+nodeForm c k ((s, i), n) =
+    L () [S () "p",
+          Q () $ pname $ protocol k, -- Name of the protocol
+          Q () $ rname $ role inst,  -- Name of the role
+          N () $ i,
+          displayTerm c n]
+    where
+      inst = insts k !! s
+
+quote :: SExpr () -> SExpr ()
+quote (S () str) = Q () str
+quote x = x
+
+-- Creates the atomic formulas used to describe an instance of a role
+strandForm :: Algebra t p g s e c => c -> Preskel t g c ->
+              (t, Instance t c) -> SExpr ()
+strandForm c k (s, inst) =
+    conjoin (map f (env inst))
+    where
+      f (x, t) =
+          L () [S () "p",
+                Q () $ pname $ protocol k, -- Name of the protocol
+                Q () $ rname $ role inst,  -- Name of the role
+                quote $ displayTerm (ctx $ role inst) x,
+                displayTerm c s,
+                displayTerm c t]
+
+-- Creates the atomic formula used to describe a node ordering relation
+precForm :: Algebra t p g s e c => c -> (t, t) -> SExpr ()
+precForm = binary "prec"
+
+-- Creates the atomic formula used to describe a strand node ordering
+sprecForm :: Algebra t p g s e c => c -> (t, t) -> SExpr ()
+sprecForm = binary "sprec"
+
+uniqForm :: Algebra t p g s e c => c -> (t, t) -> SExpr ()
+uniqForm = binary "uniq"
+
+-- Creates a formula associated with a shape.  It is a disjunction of
+-- existentially quantified formulas that describe the homomorphism
+-- and the shape as a skeleton.
+shape :: Algebra t p g s e c => c -> [SExpr ()] ->
+         (Homo t, Preskel t g c) -> SExpr ()
+shape c pov ((nh, ah), shape) =
+  let (ctx, vars, conj) = skel c shape in
+  let n = map (displayEq ctx) nh in
+  let a = map (displayEq ctx) ah in
+  quantify "exists" vars (conjoin (n ++ a ++ (conj L.\\ pov)))
+
+displayEq :: Algebra t p g s e c => c -> (t, t) -> SExpr ()
+displayEq = binary "equal"
+
+-- Formula primitives
+
+unary :: Algebra t p g s e c => String -> c -> t -> SExpr ()
+unary pred ctx t =
+    L () [S () pred, displayTerm ctx t]
+
+binary :: Algebra t p g s e c => String -> c -> (t, t) -> SExpr ()
+binary pred ctx (t0, t1) =
+    L () [S () pred, displayTerm ctx t0, displayTerm ctx t1]
+
+quantify :: String -> [SExpr ()] -> SExpr () -> SExpr ()
+quantify _ [] form = form
+quantify name vars form =
+    L () [S () name, L () vars, form]
+
+conjoin :: [SExpr ()] -> SExpr ()
+conjoin conjuncts =
+    case concatMap f conjuncts of
+      [x] -> x
+      xs -> L () (S () "and" : xs)
+    where
+      f (L () (S () "and" : xs)) = xs
+      f x = [x]
+
+disjoin :: [SExpr ()] -> SExpr ()
+disjoin conjuncts =
+    case concatMap f conjuncts of
+      [x] -> x
+      xs -> L () (S () "or" : xs)
+    where
+      f (L () (S () "or" : xs)) = xs
+      f x = [x]
+
+imply :: SExpr () -> SExpr () -> SExpr ()
+imply (L () [S () "and"]) consequence = consequence
+imply antecedent consequence =
+    L () [S () "implies", antecedent, consequence]
diff --git a/src/prover9.pl b/src/prover9.pl
--- a/src/prover9.pl
+++ b/src/prover9.pl
@@ -2,7 +2,7 @@
 
 %% CPSA tools in Prolog
 
-%% Translates the output of the cpsalogic program into the syntax of
+%% Translates the output of the cpsasas program into the syntax of
 %% Prover9.
 
 %% Known to work in SWI-Prolog, but not with GNU Prolog.
@@ -18,7 +18,7 @@
 :- use_module(pp).
 :- use_module(sexpr).
 
-%% prover9(+In, +Out) Translates cpsalogic program output in file In,
+%% prover9(+In, +Out) Translates cpsasas program output in file In,
 %% into the syntax of Prover9 and places it in file Out.
 prover9(In, Out) :-
 	sexpr:read_sexpr_list(In, Forms),
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.3.5")
+(comment "CPSA 2.4.0")
 (comment "All input read from DH_hack.scm")
 (comment "Strand count bounded at 15")
 
diff --git a/tst/Make.hs b/tst/Make.hs
--- a/tst/Make.hs
+++ b/tst/Make.hs
@@ -1,6 +1,6 @@
 -- A simple, CPSA specific make system
 
-module Make (cpsa, shapes, logic, annos, params, cleanse, get, set,
+module Make (cpsa, shapes, sas, annos, params, cleanse, get, set,
              build, clean, roots) where
 
 {- Place a copy of this source file in the directory used to store
@@ -23,10 +23,10 @@
 
 If successful, the shapes are in the file prob_shapes.xhtml.
 
-*Make> logic "prob"
+*Make> sas "prob"
 
 If successful, the shape analysis sentences are in the file
-prob_logic.text.
+prob_sas.text.
 
 When the protocol is annotated with rely-guarantee formulas, type:
 
@@ -152,19 +152,19 @@
            inputExt = cpsaExt,
            outputExt = shapesRoot ++ cpsaExt }
 
--- Logic Rule
+-- SAS Rule
 
-logic :: FilePath -> IO ()
-logic root =
+sas :: FilePath -> IO ()
+sas root =
     do
       cpsaBasic root            -- Run CPSA if need be
-      make logicRule root
+      make sasRule root
 
-logicRule :: Rule
-logicRule =
-    Rule { prog = "cpsalogic",
+sasRule :: Rule
+sasRule =
+    Rule { prog = "cpsasas",
            inputExt = cpsaExt,
-           outputExt = logicExt }
+           outputExt = sasExt }
 
 -- Annotations Rule
 
@@ -203,7 +203,7 @@
       rm $ root ++ graphExt
       rm $ root ++ shapesRoot ++ cpsaExt
       rm $ root ++ shapesRoot ++ graphExt
-      rm $ root ++ logicExt
+      rm $ root ++ sasExt
       rm $ root ++ annosRoot ++ cpsaExt
       rm $ root ++ annosRoot ++ graphExt
       rm $ root ++ paramsRoot ++ cpsaExt
@@ -219,8 +219,8 @@
 shapesRoot :: String
 shapesRoot = "_shapes"
 
-logicExt :: String
-logicExt = "_logic.text"
+sasExt :: String
+sasExt = "_sas.text"
 
 annosRoot :: String
 annosRoot = "_annotations"
diff --git a/tst/Makefile b/tst/Makefile
--- a/tst/Makefile
+++ b/tst/Makefile
@@ -7,7 +7,7 @@
 CPSA	= ../dist/build/cpsa/cpsa$(EXE)
 DIFF	= ../dist/build/cpsadiff/cpsadiff$(EXE)
 SHAPES	= ../dist/build/cpsashapes/cpsashapes$(EXE)
-LOGIC	= ../dist/build/cpsalogic/cpsalogic$(EXE)
+SAS	= ../dist/build/cpsasas/cpsasas$(EXE)
 ANNOTATIONS = ../dist/build/cpsaannotations/cpsaannotations$(EXE)
 GRAPH	= ../dist/build/cpsagraph/cpsagraph$(EXE)
 CPSAFLAGS = +RTS -M512m -RTS
@@ -29,8 +29,8 @@
 	$(SHAPES) $(SHAPESFLAGS) -o $@ $<
 
 # Extract shape analysis sentences
-%_logic.text:	%.txt
-	$(LOGIC) $(LOGICFLAGS) -o $@ $<
+%_sas.text:	%.txt
+	$(SAS) $(SASFLAGS) -o $@ $<
 
 # Annotate shapes
 %_annotations.txt:	%_shapes.txt
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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (comment "All input read from fragile_pruning.scm")
 
 (defprotocol fragile_pruning basic
diff --git a/tst/hashtest-key-hash.tst b/tst/hashtest-key-hash.tst
--- a/tst/hashtest-key-hash.tst
+++ b/tst/hashtest-key-hash.tst
@@ -1,6 +1,6 @@
 (herald "Hashtest")
 
-(comment "CPSA 2.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (comment "All input read from uncarried_keys.scm")
 
 (defprotocol uncarried-keys 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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (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.3.5")
+(comment "CPSA 2.4.0")
 (comment "All input read from yahalom.scm")
 (comment "Strand count bounded at 15")