packages feed

cpsa 2.3.5 → 2.4.0

raw patch · 86 files changed

+1168/−980 lines, 86 filesnew-component:exe:cpsasas

Files

ChangeLog view
@@ -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
NEWS view
@@ -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
cpsa.cabal view
@@ -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
doc/Make.hs view
@@ -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"
doc/cpsa.mk view
@@ -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
doc/cpsadesign.pdf view

binary file changed (273516 → 273796 bytes)

doc/cpsaintroslides.pdf view

binary file changed (93144 → 93145 bytes)

doc/cpsaintroslides.tex view
@@ -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}
doc/cpsaoverview.pdf view

binary file changed (129002 → 129002 bytes)

doc/cpsaprimer.pdf view

binary file changed (273733 → 273720 bytes)

doc/cpsaprimer.tex view
@@ -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
doc/cpsaspec.pdf view

binary file changed (388817 → 387594 bytes)

doc/cpsaspec.tex view
@@ -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}
doc/cpsauser.html view
@@ -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)
doc/index.html view
@@ -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>
doc/macros.tex view
@@ -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)}
src/CPSA/Lib/Reduction.hs view
@@ -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
− src/CPSA/Logic/Logic.hs 
@@ -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]
− src/CPSA/Logic/Main.hs 
@@ -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
+ src/CPSA/SAS/Main.hs view
@@ -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
+ src/CPSA/SAS/SAS.hs view
@@ -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]
src/prover9.pl view
@@ -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),
tst/DH_hack.tst view
@@ -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")
tst/Make.hs view
@@ -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"
tst/Makefile view
@@ -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
tst/blanchet.tst view
@@ -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
tst/completeness-test.tst view
@@ -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
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from crushing.scm")  (defprotocol crushing basic
tst/dass_simple.tst view
@@ -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
tst/denning-sacco.tst view
@@ -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
tst/deorig_contract.tst view
@@ -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
tst/deorig_mesg.tst view
@@ -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
tst/deorig_simple.tst view
@@ -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
tst/dy.tst view
@@ -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
tst/encsig.tst view
@@ -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
tst/epmo-hash.tst view
@@ -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
tst/epmo-key-hash.tst view
@@ -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
tst/epmo.tst view
@@ -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
tst/epmo_acctnum-key-hash.tst view
@@ -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
tst/ffgg.tst view
@@ -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
tst/fragile_pruning.tst view
@@ -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
tst/hashtest-key-hash.tst view
@@ -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
tst/hashtest.tst view
@@ -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
tst/incompleteness_example.tst view
@@ -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
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from isoreject.scm")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from kelly1.scm")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from kerberos.scm")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from mass.lsp")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from mass2.lsp")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -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
tst/neuman-stubblebine-reauth.tst view
@@ -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
tst/neuman-stubblebine.tst view
@@ -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
tst/no_contraction.tst view
@@ -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
tst/non_transforming.tst view
@@ -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
tst/nonaug-prune.tst view
@@ -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
tst/ns-l.tst view
@@ -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
tst/ns.tst view
@@ -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
tst/nsl3.tst view
@@ -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
tst/nsl4cm1.tst view

file too large to diff

tst/nslsk.tst view
@@ -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
tst/or.tst view
@@ -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
tst/pca.tst view
@@ -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")
tst/pen-non-orig-test.tst view
@@ -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
tst/pkinit.tst view
@@ -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
tst/preprocess.tst view
@@ -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
tst/print.tst view
@@ -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
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from pruning1.scm")  (defprotocol prune basic
tst/sigenc.tst view
@@ -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
tst/sorted_epmo_acctnum.tst view
@@ -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")
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from targetterms2.scm")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from targetterms6.scm")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from targetterms8.scm")  (defprotocol targetterms8 basic
tst/timestamping.tst view
@@ -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
tst/uncarried_keys.tst view
@@ -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
tst/uo.tst view
@@ -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
tst/wang-hash.tst view
@@ -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")
tst/wang-key-hash.tst view
@@ -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")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from weird.scm")  (defprotocol weird basic
tst/wide-mouth-frog-scyther.tst view
@@ -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
tst/wide-mouth-frog.tst view
@@ -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
tst/wonthull.tst view
@@ -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")
tst/wonthull2.tst view
@@ -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")
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.5")+(comment "CPSA 2.4.0") (comment "All input read from wonthull3.scm")  (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -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
tst/yahalom-6.3.6.tst view
@@ -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")
tst/yahalom.tst view
@@ -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")