packages feed

cpsa 2.2.12 → 2.2.13

raw patch · 24 files changed

+215/−161 lines, 24 files

Files

ChangeLog view
@@ -1,3 +1,25 @@+2013-02-28  John D. Ramsdell  <ramsdell@mitre.org>++	* doc/*.html:  Convert to HTML 5 mainly by eliminating the DOCTYPE+	element.++	* cpsa.cabal (Version):  Tagged as version 2.2.13++2013-02-12  Paul D. Rowe  <prowe@mitre.org>++	* src/perm.pl:  Fix permutation bug.++2013-01-22  John D. Ramsdell  <ramsdell@mitre.org>++	* tst/Makefile ($EXE): Added optional extension for Cygwin users.+	On Cygwin, put "export EXE=.exe" in a startup file.++2012-11-13  John D. Ramsdell  <ramsdell@mitre.org>++	* doc/cpsaspec.tex (chapter{Generalization}): Corrected the+	definition of a location in the text describing variable+	separation.+ 2012-11-09  John D. Ramsdell  <ramsdell@mitre.org>  	* cpsa.cabal (Version):  Tagged as version 2.2.12.
NEWS view
@@ -1,5 +1,13 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.13++** Better support for Cygwin users+   Added optional extension for Cygwin users.  On Cygwin, put "export+   EXE=.exe" in a startup file.++** Bug fixed in src/perm.pl+ * Changes in version 2.2.12  ** Documentation improved
README view
@@ -11,6 +11,10 @@ Find the documentation directory by typing "cpsa -h" in a command shell, and view index.html in a browser. +Cabal installation options are listed with:++$ cabal help install+ INSTALLING FROM A TARBALL  If Haskell Platform is not available, install GHC and its parallel@@ -58,17 +62,18 @@  QUICK START (Windows) -The software has been tested on a Windows system on which neither-MinGW or Cygwin has been installed.  Install GHC and then from a-command prompt type:+Unless you are using Cygwin or MinGW, the cabal install above is your+best bet.  The software has been tested on a Windows system on which+neither MinGW or Cygwin has been installed.  Install GHC and then run+the "setup.bat" batch file with administrator privileges. -C:\...> runghc Setup.hs configure+If you do not have administrator privileges, run:++C:\...> runghc Setup.hs configure --user --prefix="DIRECTORY" C:\...> runghc Setup.hs build C:\...> runghc Setup.hs install -If you do not have administrator privileges, configure with:--C:\...> runghc Setup.hs configure --user+and place DIRECTORY\bin on your path.  Documentation and samples are in the directory given by C:\...> cpsa -h
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.2.12+Version:		2.2.13 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3
doc/cpsadesign.pdf view

binary file changed (203169 → 275306 bytes)

doc/cpsadesign.tex view
@@ -544,7 +544,7 @@ the reverse of the both communication ordering~$O$ and the implied strand succession orderings.  The edges are reversed because events in a node's past are of interest when analyzing a node.  When the graph-is acyclic, the transitive asymmetric relation~$\kprec{k}$ of~$k$ is the+is acyclic, the transitive irreflexive relation~$\kprec{k}$ of~$k$ is the transitive closure of the graph, and $n_0\kprec{k} n_1$ asserts that the message event at~$n_0$ precedes the one at~$n_1$.  (A preskeleton with a graph that contains cycles is not well-formed.)@@ -696,7 +696,7 @@  The second significant difference is that the precedes relation is represented by a list of ordered pairs in this document, but in the-specification, the precedes relation is always asymmetric and+specification, the precedes relation is always irreflexive and transitive.  In the code, the transitive reduction is performed on the precedes relation, and the output always contains the fewest number of ordered pairs possible without changing the transitive closure of the
doc/cpsadha.pdf view

binary file changed (131702 → 222454 bytes)

doc/cpsaintroslides.pdf view

binary file changed (68220 → 93151 bytes)

doc/cpsaoverview.pdf view

binary file changed (82385 → 129012 bytes)

doc/cpsaprimer.pdf view

binary file changed (194779 → 273723 bytes)

doc/cpsaprimer.tex view
@@ -383,12 +383,10 @@ Additionally, the following strand succession edges\index{strand   succession edges} are included: $$\{((s,p), (s, p+1))\mid s<|i|, p+1<\cn{height}(i(s))\}.$$ Executions with cyclic graphs are omitted-from consideration, because they violate causality.  Relation~$R$ on-set~$S$ is \emph{asymmetric}\index{asymmetric relation} iff-$x\mathbin{R}y$ implies not $y\mathbin{R}x$ for all distinct $x,y \in-S$.  The transitive asymmetric relation~$\prec$ is the transitive-closure of the graph's edges, and $n_0\prec n_1$ asserts that the-message event at~$n_0$ precedes the one at~$n_1$.+from consideration, because they violate causality.  The transitive+irreflexive~$\prec$ is the transitive closure of the graph's edges,+and $n_0\prec n_1$ asserts that the message event at~$n_0$ precedes+the one at~$n_1$.  The node relation of an execution satisfies one additional property. For each reception node in its sequence, there exists a unique
doc/cpsaspec.pdf view

binary file changed (329942 → 410823 bytes)

doc/cpsaspec.tex view
@@ -419,13 +419,11 @@ and~$\evt_\Theta(n_1)=\inbnd t$.  For each reception node~$n_1$, there is a unique transmission node~$n_0$ with $n_0\rightarrow n_1$. -Each acyclic graph has a transitive asymmetric relation~$\prec$ on its-vertices.  The relation specifies the causal ordering of nodes in a-bundle.  Relation~$R$ on set~$S$ is-\index{asymmetric relation}\emph{asymmetric} iff $x\mathbin{R}y$ implies not-$y\mathbin{R}x$ for all distinct $x,y \in S$.  An asymmetric-transitive binary relation is also called a \index{strict partial-  order}\index{partial order!strict}strict partial order.+Each acyclic graph has a transitive irreflexive relation~$\prec$ on+its vertices.  The relation specifies the causal ordering of nodes in+a bundle.  An transitive irreflexive binary relation is also called a+\index{strict partial order}\index{partial order!strict}strict partial+order.  An atom \index{uniquely originates}\emph{uniquely originates} in a bundle if it originates in the trace of exactly one strand.  An atom@@ -528,7 +526,7 @@   skeleton}\index{skeleton!realized}\emph{realizes} the bundle if $\rl'$ and $\Theta'_X$ are the truncations of $\rl$ and $\Theta_X$ respectively that omit penetrator strands from their domains, $\prec$-is the transitive asymmetric relation associated with the bundle+is the transitive irreflexive relation associated with the bundle without penetrator nodes, $N$ is the set of non-originating atoms with variables that occur in $\Theta'_X$, and $U$ is the set of atoms that uniquely originate and are carried by some regular event.@@ -538,7 +536,7 @@ \begin{enumerate} \item Sequence $\rl$ demonstrates that the strands in $\sdom(\Theta_X)$   satisfy the conditions for being a part of a run of protocol~$P$.-\item Relation $\prec$ is transitive, asymmetric, and includes the+\item Relation $\prec$ is transitive, irreflexive, and includes the   strand succession relation $(\Rightarrow)$. \item If $n\prec n'$, then either $n\Rightarrow n'$,   $\evt_{\Theta_X}(n)=\outbnd t$ and   $\evt_{\Theta_X}(n')=\inbnd@@ -1379,7 +1377,9 @@ $$\begin{array}{r@{}c@{}ll} \dctx{\{t\}\cup T_p}{T_a}&{}\to{}&\dctx{T_p}{T_a}\setminus\{t\} &\mbox{if $t$ is an atom or in $X_{\top}$}\\-\dctx{\{(t_0,t_1)\}\cup T_p}{T_a}&{}\to{}&\dctx{\{t_0,t_1\}\cup T_p}{T_a}\\+\dctx{\{(t_0,t_1)\}\cup T_p}{T_a}&{}\to{}+&\dctx{\{t_0,t_1,(t_0,t_1)\}\cup T_p}{T_a}+&\mbox{if $t_0,t_1\notin T_p$}\\ \dctx{\{\enc{t_0}{t_1}\}\cup T_p}{T_a}&{}\to{}&\dctx{\{t_0,\enc{t_0}{t_1}\}\cup T_p}{T_a} &\mbox{if $t_0\notin T_p$ and}\\@@ -1849,21 +1849,25 @@ Sometimes a more general skeleton can be found by replacing some occurrences of one variable by a fresh variable.  For variable separation, the location of an occurrence of a variable is defined-using a skeleton's instance sequence.+using a skeleton's instance.  Recall that in the external syntax,+strand~$s$ in skeleton~$k$ is described by an instance of the form+$\inst(r,h,\sigma)$.  (Instances are introduced in+Section~\ref{sec:instances}.)  \begin{defn}[Location]-Message~$t$ is at \emph{location} $(s,i,p)$ in~$k$ if-$\pm t=\Theta_k(s)(i)\termat p$.+Variable~$x$ is at \emph{location} $(s,y,p)$ in~$k$ if+the instance at $\Theta_k(s)$ is $\inst(r,h,\sigma)$ and+$x=\sigma(y)\termat p$. \end{defn}  \begin{defn}[Variable Separation] Skeleton~$k_0$ \index{variable separation}\emph{generalizes by   variable separation} skeleton~$k_1$, written $k_1\reduction{\ops{V}_t}_k k_0$, if $k_1\reduction{<}_k k_0$,-$k_2\reduction{\fn{skel}}k_0$, and~$k_2$ is~$k_1$ except ~$t$ is a+$k_2\reduction{\fn{skel}}k_0$, and~$k_2$ is~$k_1$ except~$t$ is a variable that occurs in multiple locations in~$k_1$, and~$k_2$ is the result of replacing~$t$ with a variable~$t_0$ of the same sort at a-subset of~$t$'s locations, where~$t_0$ occurs nowhere in~$k_1$.+proper subset of~$t$'s locations, where~$t_0$ occurs nowhere in~$k_1$. \end{defn}  When separating a non-originating term, both the term and its clone
doc/cpsauser.html view
@@ -1,6 +1,4 @@ <?xml version="1.0" encoding="UTF-8"?>-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"-      "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head>   <meta http-equiv="content-type"@@ -37,23 +35,23 @@ <p>The analyzer is designed to work well with other tools. S-expressions are used for both input and output. The analyzer reads all the problems in its input, writes out the solution to each problem, and then exits. This release-contains seven tools. The <a href="#cpsagraph"><tt>cpsagraph</tt></a> program+contains seven tools. The <a href="#cpsagraph"><code>cpsagraph</code></a> program provides a visualization of answers using Scalable Vector Graphics (<a href="http://www.w3.org/Graphics/SVG/">SVG</a>). The <a-href="#cpsashapes"><tt>cpsashapes</tt></a> program removes intermediate results+href="#cpsashapes"><code>cpsashapes</code></a> program removes intermediate results from analyzer runs making the shapes easy to identify. The <a-href="#cpsafiff"><tt>cpsadiff</tt></a> program compares CPSA output+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"><tt>cpsalogic</tt></a> program logical+The <a href="#cpsalogic"><code>cpsalogic</code></a> program logical   formula that can be used to ensure security goals are achieved. The <a-href="#cpsaannotations"><tt>cpsaannotations</tt></a> program uses protocol+href="#cpsaannotations"><code>cpsaannotations</code></a> program uses protocol annotations to annotate shapes and generate protocol soundness obligations. The-<a href="#cpsaparameters"><tt>cpsaparameters</tt></a> program detects some+<a href="#cpsaparameters"><code>cpsaparameters</code></a> program detects some specification errors by performing a data flow analysis on protocol roles. The-<a href="#cpsapp"><tt>cpsapp</tt></a> program pretty prints its input using a+<a href="#cpsapp"><code>cpsapp</code></a> program pretty prints its input using a CPSA specific algorithm.</p>  <p>The input syntax is essentially the same as the output syntax. A Lisp aware@@ -63,7 +61,7 @@ this information.</p>  <p>The typical pattern of usage is to enter the set of problems to be analyzed-into a file, in this example, <tt>prob.scm</tt>, analyze the problems, and if+into a file, in this example, <code>prob.scm</code>, analyze the problems, and if something interesting is produced, visualize the answers.</p>  <blockquote>@@ -81,7 +79,7 @@ </blockquote>  <p id="make">The distribution comes with the-file <a href="cpsa.mk"><tt>cpsa.mk</tt></a> for inclusion into your+file <a href="cpsa.mk"><code>cpsa.mk</code></a> for inclusion into your makefile. A sample makefile follows. If you cut-and-paste from a browser window, be sure to convert the leading spaces in the last line into a tab character.</p>@@ -102,14 +100,14 @@  <p>The CPSA program   is <a href="http://www.gnu.org/software/emacs/">Emacs</a> friendly.-  If you run the above <tt>makefile</tt> via &quot;<tt>M-x-  compile</tt>&quot;, the results will be displayed in a buffer in-  Compilation Mode.  The command &quot;<tt>C-x `</tt>&quot; will visit-  the locus of the next error message or match (<tt>next-error</tt>)+  If you run the above <code>makefile</code> via &quot;<kbd>M-x+  compile</kbd>&quot;, the results will be displayed in a buffer in+  Compilation Mode.  The command &quot;<kbd>C-x `</kbd>&quot; will visit+  the locus of the next error message or match (<code>next-error</code>)   in your CPSA input file.</p> -<p>For platforms without GNU <tt>make</tt>, the Haskell program <a-href="Make.hs"><tt>Make.hs</tt></a> can be loaded into a Haskell interpreter+<p>For platforms without GNU <code>make</code>, the Haskell program <a+href="Make.hs"><code>Make.hs</code></a> can be loaded into a Haskell interpreter and perform a similar function. Users are expected to copy the makefile or the Haskell program into the directory containing a set of analysis problems, and then modify the file so it specifies the command line flags appropriate for the@@ -121,7 +119,7 @@ symbol are allowed at various points in the grammar. Key-value pairs with unrecognized keys are ignored, and are available for use by other tools. On output, unrecognized key-value pairs are preserved when printing protocols, but-elided when printing skeletons, with the exception of the <tt>comment</tt>+elided when printing skeletons, with the exception of the <code>comment</code> key.</p>  <p>The input is an option herald form followed by a sequence of@@ -147,23 +145,23 @@ PROT-ALIST ::= ...</pre> </blockquote> -<p>The protocol <tt>ID</tt> is a symbol that names the protocol, and the role-<tt>ID</tt> is a symbol that names the role. The <tt>ALG</tt> symbol identifies+<p>The protocol <code>ID</code> is a symbol that names the protocol, and the role+<code>ID</code> is a symbol that names the role. The <code>ALG</code> symbol identifies the algebra used by the protocol. For the Basic Cryptographic Algebra, the-symbol is <tt>basic</tt>. For the Diffie-Hellman Algebra, the symbol is-<tt>diffie-hellman</tt>. The <tt>var</tt> form contains symbols that+symbol is <code>basic</code>. For the Diffie-Hellman Algebra, the symbol is+<code>diffie-hellman</code>. The <code>var</code> form contains symbols that declare the sort of the variables used in this role. The set of sort symbols is algebra specific. The protocol association list has no predefined keys, while the role association list has three. The value associated with both of these keys must be atoms in the-algebra. Each <tt>non-orig</tt> term must not be carried by any event+algebra. Each <code>non-orig</code> term must not be carried by any event in the role's trace, but each of its variables must occur in some-term.  A role non-origination assumption of the form <tt>(3 a)</tt>-asserts that atom <tt>a</tt> will not be mapped into an instance-unless its height is at least three.  For each <tt>pen-non-orig</tt>+term.  A role non-origination assumption of the form <code>(3 a)</code>+asserts that atom <code>a</code> will not be mapped into an instance+unless its height is at least three.  For each <code>pen-non-orig</code> term, each of its variables must occur in some term, but unlike a non-origination assumption, the term may be carried.-Each <tt>uniq-orig</tt> term must originate in the role's trace. Every+Each <code>uniq-orig</code> term must originate in the role's trace. Every non-atomic variable must be acquired by the role's trace.</p>  <p>The structure of sorts and terms in the Basic Cryptographic Algebra@@ -176,12 +174,12 @@       |  (pubk STRING ID) | (privk STRING ID)</pre> </blockquote> -<p>The form (<tt>cat</tt> a b c d e) is expands to (<tt>cat</tt> a (<tt>cat</tt>-b (<tt>cat</tt> c (<tt>cat</tt> d e)))).</p>+<p>The form (<code>cat</code> a b c d e) is expands to (<code>cat</code> a (<code>cat</code>+b (<code>cat</code> c (<code>cat</code> d e)))).</p>  <p>A term in the Basic Crypto Algebra is an atom if it is variable of a sort-other than <tt>mesg</tt>, or it if formed from one of the following operations:-<tt>pubk</tt>, <tt>privk</tt>, <tt>invk</tt>, and <tt>ltk</tt>.</p>+other than <code>mesg</code>, or it if formed from one of the following operations:+<code>pubk</code>, <code>privk</code>, <code>invk</code>, and <code>ltk</code>.</p>  <blockquote>   <pre>SKELETON   ::= (defskeleton ID VARS STRAND+ SKEL-ALIST)@@ -195,9 +193,9 @@ NODE       ::= (INT INT)</pre> </blockquote> -<p>The <tt>ID</tt> in the skeleton form names a protocol. It refers to the last+<p>The <code>ID</code> in the skeleton form names a protocol. It refers to the last protocol definition of that name which precedes the skeleton form. The-<tt>ID</tt> in the strand form names a role. The integer in the strand form+<code>ID</code> in the strand form names a role. The integer in the strand form gives the height of the strand. The sequence of pairs of terms in the strand form specify an environment used to construct the messages in a strand from its role's trace. The first term is interpreted using the role's variables and the@@ -216,31 +214,31 @@ specify how to map every role variable. The reader inserts missing mappings, and renames every skeleton variable that also occurs in a role of its protocol. The sort of every skeleton variable that occurs-in the <tt>non-orig</tt>, <tt>pen-non-orig</tt>, or <tt>uniq-orig</tt>+in the <code>non-orig</code>, <code>pen-non-orig</code>, or <code>uniq-orig</code> list or in a maplet must be declared.</p>  <p>On output, key-value pairs are added to all skeleton's association list. Every skeleton in the output is labeled with a unique identifier with-<tt>(label INT)</tt> A skeleton has <tt>(parent INT)</tt> if it is a member of-the cohort of the identified parent. A skeleton has <tt>(seen INT+)</tt> when+<code>(label INT)</code> A skeleton has <code>(parent INT)</code> if it is a member of+the cohort of the identified parent. A skeleton has <code>(seen INT+)</code> when members of its cohort are isomorphic to previously seen skeletons. A skeleton-lists its unrealized nodes with <tt>(unrealized NODE*)</tt>. The traces-associated with each strand is given by the <tt>(traces ...)</tt> form.+lists its unrealized nodes with <code>(unrealized NODE*)</code>. The traces+associated with each strand is given by the <code>(traces ...)</code> form. Finally, the operation used to derive this skeleton from its parent is recorded-with <tt>(operation TEST KIND TERM NODE TERM*)</tt>, where <tt>TEST</tt> is the-authentication test <tt>encryption-test</tt> or <tt>nonce</tt>, <tt>KIND</tt>-is <tt>(added-strand ID INT)</tt>, <tt>(contracted MAPLET*)</tt>, or-<tt>(added-listener TERM)</tt>, <tt>TERM</tt> is the critical term,-<tt>NODE</tt> in the test node, and the remaining terms specify the escape set.+with <code>(operation TEST KIND TERM NODE TERM*)</code>, where <code>TEST</code> is the+authentication test <code>encryption-test</code> or <code>nonce</code>, <code>KIND</code>+is <code>(added-strand ID INT)</code>, <code>(contracted MAPLET*)</code>, or+<code>(added-listener TERM)</code>, <code>TERM</code> is the critical term,+<code>NODE</code> in the test node, and the remaining terms specify the escape set. When the operation kind is augmenting, the instance's role name and height are provided. For kind listening, a term is provided. For kind contracting, the substitution is provided. When a substitution refers to a variable not in the skeleton, its name is unpredictable. For generalization, the operation is-recorded as <tt>(operation generalization METHOD)</tt>, where <tt>METHOD</tt>-is one of <tt>deleted NODE</tt>, <tt>weakened NODE-PAIR</tt>, <tt>separated-TERM</tt> and <tt>forgot TERM</tt>. Generalization is used to find shapes from+recorded as <code>(operation generalization METHOD)</code>, where <code>METHOD</code>+is one of <code>deleted NODE</code>, <code>weakened NODE-PAIR</code>, <code>separated+TERM</code> and <code>forgot TERM</code>. Generalization is used to find shapes from realized skeletons. For shape collapsing, the operation is recorded as-<tt>(operation collapsed INT INT)</tt>, where the two <tt>INT</tt>s identify+<code>(operation collapsed INT INT)</code>, where the two <code>INT</code>s identify the strands merged. Shape collapsing is used to find related shapes.</p>  <p>The current Diffie-Hellman support is experimental and known to@@ -252,13 +250,13 @@ TERM ::= ... | (gen) | (exp TERM TERM)</pre> </blockquote> -<p>Given exponent <tt>x</tt>, <tt>(gen)</tt> is the group+<p>Given exponent <code>x</code>, <code>(gen)</code> is the group generator constant, and-given <tt>g</tt> and <tt>x</tt>, <tt>(exp g x)</tt>-is <tt>g</tt> raised to the <tt>x</tt> power.  Terms of the-form <tt>(gen)</tt> or <tt>(exp g x)</tt> are of sort <tt>base</tt>,-and <tt>x</tt> is of sort <tt>expn</tt>.  Terms of-sort <tt>expn</tt> are atoms, but terms of sort <tt>base</tt> are+given <code>g</code> and <code>x</code>, <code>(exp g x)</code>+is <code>g</code> raised to the <code>x</code> power.  Terms of the+form <code>(gen)</code> or <code>(exp g x)</code> are of sort <code>base</code>,+and <code>x</code> is of sort <code>expn</code>.  Terms of+sort <code>expn</code> are atoms, but terms of sort <code>base</code> are not.</p>  <p>Reasoning about the commutativity of exponents is supported via@@ -272,29 +270,29 @@  <h3>Macros and Includes</h3> -<p>After reading the input, <tt>cpsa</tt> expands macros before in analyzing+<p>After reading the input, <code>cpsa</code> expands macros before in analyzing the results. A macro definition is a top-level form.</p>  <blockquote>   <pre>(defmacro (NAME ARG*) BODY)</pre> </blockquote> -<p>The <tt>cpsa</tt> program expands all calls to macros in non-macro defining+<p>The <code>cpsa</code> program expands all calls to macros in non-macro defining S-expressions using the macros that have been defined previously. A macro definition can be used to expand a call if the first element of a list matches the name of the macro, and the length of the remaining elements in the list matches the length of the macro's argument list. When two macros definitions-are applicable, the last definition takes precedence. The <tt>cpsa</tt> program+are applicable, the last definition takes precedence. The <code>cpsa</code> program omits macro definitions from its output.</p>  <p>A source file can be included within another with the top-level-include form,<p>+include form,</p>  <blockquote>   <pre>(include FILE)</pre> </blockquote> -<p>where <tt>FILE</tt> is a string. The <tt>cpsa</tt> program+<p>where <code>FILE</code> is a string. The <code>cpsa</code> program includes files while it does macro expansion.</p>  <h3 id="usage">Usage of CPSA</h3>@@ -323,10 +321,10 @@ skeleton with too many strands. The strand count bound option is used to override the default strand count bound. Another way to limit resources used by the program is to limit the amount of memory it may use. The command-line-option <tt>+RTS -M512m -RTS</tt> limits memory usage to 512m.</p>+option <code>+RTS -M512m -RTS</code> limits memory usage to 512m.</p>  <p>The herald form can be used to specify options within a file.  The-  grammar for a herald form follows, where <tt>ALIST</tt> is an+  grammar for a herald form follows, where <code>ALIST</code> is an   association list with symbols as keys.</p>  <blockquote>@@ -334,29 +332,29 @@ TITLE  ::= SYMBOL | STRING</pre> </blockquote> -<p>The title is used by <tt>cpsagraph</tt> when generating XHTML.+<p>The title is used by <code>cpsagraph</code> when generating XHTML.   In the following example, the herald form specifies a strand bound   of 12 in a way that is equivalent to the command line-  option <tt>--bound=12</tt>.</p>+  option <code>--bound=12</code>.</p>  <blockquote>   <pre>(herald "Needham-Schroeder Public-Key Protocol" (bound 12))</pre> </blockquote> -<p>The herald form is only interpreted by the <tt>cpsa</tt> program,+<p>The herald form is only interpreted by the <code>cpsa</code> program,   and is treated as a comment by all other programs.  In particular,-  specifying a <tt>margin</tt> option effects <tt>cpsa</tt> only.</p>+  specifying a <code>margin</code> option effects <code>cpsa</code> only.</p>  <p>For long running problems, SMP parallelism is available. For example, on a-quad-core machine, we would probably use <tt>+RTS -N4 -RTS</tt>.</p>+quad-core machine, we would probably use <code>+RTS -N4 -RTS</code>.</p>  <p>In addition to the options provided on the command line or a herald   form, one can influence the order in which test nodes are sought.-  When a role includes <tt>(reverse-search)</tt> in its association+  When a role includes <code>(reverse-search)</code> in its association   list as a comment, the nodes in its instances will be searched in   reverse order.</p> -<p>When run with isomorphism checks disabled (<tt>--noisochk</tt>), CPSA+<p>When run with isomorphism checks disabled (<code>--noisochk</code>), CPSA searches for realized skeletons, not shapes. It attempts to speed up analysis by not identifying duplicate skeletons or generalizing realized skeletons, however in many cases, run times increase. It is used when normal analysis@@ -366,14 +364,14 @@ <p>In no isomorphism checking mode output, every realized skeleton is labeled a shape even when it is not. This allows the extraction of every realized skeletons from the output using the <a-href="#cpsashapes"><tt>cpsashapes</tt></a> program.</p>+href="#cpsashapes"><code>cpsashapes</code></a> program.</p>  <p>An error message that begins with "No test for unrealized node" identifies a severe error that should be reported as a bug.</p>  <h2 id="cpsagraph">Visualization</h2> -<p>The <tt>cpsagraph</tt> program produces a graphical rendering of the output+<p>The <code>cpsagraph</code> program produces a graphical rendering of the output or input of an analyzer using SVG. It is viewable only with a standards-compliant web browser such as FireFox.</p> @@ -390,29 +388,29 @@ transmission at the source of the edge happened before message reception at the destination edge. The edge is solid if the transmitting term is syntactically identical to the receiving term, otherwise the edge is dashed. Thus in an-algebra with a commutative operation <tt>*</tt>, the graphing program sometimes-draws a dashed line between <tt>(send (* a b))</tt> and <tt>(recv (* b-a))</tt>.</p>+algebra with a commutative operation <code>*</code>, the graphing program sometimes+draws a dashed line between <code>(send (* a b))</code> and <code>(recv (* b+a))</code>.</p>  <p>In the tree drawing, the label of a shape is blue. For dead skeletons, the label is red, unless it has been seen before, in which case it is orange. Otherwise the label is green for skeletons seen before. Seen skeleton labels are rendered in an italic font.</p> -<p>By the default, <tt>cpsagraph</tt> generates a view of CPSA S-expressions as+<p>By the default, <code>cpsagraph</code> generates a view of CPSA S-expressions as a compound document that contains SVG within XHTML. This view integrates graphics with the input text.</p> -<p>In compact mode, <tt>cpsagraph</tt> generates an SVG document. The tree is+<p>In compact mode, <code>cpsagraph</code> generates an SVG document. The tree is displayed immediately to the left of skeleton drawings. When there is more than one tree, the left-hand-side of the drawing contains a vertical listing of the trees. Compact mode output should never be used as a replacement for studying the text version of the output. The text version contains strictly more information, and should be displayed next to its graphical rendition.</p> -<p>In LaTeX mode, <tt>cpsagraph</tt> generates LaTeX source. XY-pic is used for+<p>In LaTeX mode, <code>cpsagraph</code> generates LaTeX source. XY-pic is used for drawings of skeletons. The margin specified in <a-href="cpsa.mk"><tt>cpsa.mk</tt></a> produces good results. </p>+href="cpsa.mk"><code>cpsa.mk</code></a> produces good results. </p>  <h3>Usage</h3> @@ -433,7 +431,7 @@  <h2 id="cpsadiff">Output Comparisons</h2> -<p>The <tt>cpsadiff</tt> program compares CPSA output files+<p>The <code>cpsadiff</code> program compares CPSA output files S-expression by S-expression, and prints the first skeleton that differs.</p> @@ -450,7 +448,7 @@  <h2 id="cpsashapes">Shape Extraction</h2> -<p>The <tt>cpsashapes</tt> program extracts the original problems and the+<p>The <code>cpsashapes</code> program extracts the original problems and the shapes from the output of a CPSA run. The shapes are linked to their problem so the output can be graphed.</p> @@ -467,7 +465,7 @@  <h2 id="cpsalogic">Formula Extraction</h2> -<p>The <tt>cpsalogic</tt> program extracts a formula in the language+<p>The <code>cpsalogic</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@@ -488,7 +486,7 @@  <h2 id="cpsaannotations">Annotations</h2> -<p>The <tt>cpsaannotations</tt> program uses protocol annotations to annotate+<p>The <code>cpsaannotations</code> program uses protocol annotations to annotate shapes and generate protocol soundness obligations.</p>  <h3>Usage</h3>@@ -506,8 +504,8 @@  <h3>Syntax</h3> -<p>To be analyzed, each role in a protocol must include an <tt>annotations</tt>-form. The <tt>TERM</tt> is a role atom that when instantiated, is the name of a+<p>To be analyzed, each role in a protocol must include an <code>annotations</code>+form. The <code>TERM</code> is a role atom that when instantiated, is the name of a principal in the shape. What follows is sequences of pairs. The integer gives the position of the event in the trace that is annotated by the formula. Zero-based indexing is used.</p>@@ -528,12 +526,12 @@ FTERM      ::= TERM | (ID FTERM*)</pre> </blockquote> -<p>Use <tt>(and)</tt> for truth and <tt>(or)</tt> for falsehood.</p>+<p>Use <code>(and)</code> for truth and <code>(or)</code> for falsehood.</p>  <h3>Output</h3> -<p>On output, each shape contains an <tt>annotations</tt> form and a-<tt>obligations</tt> form. The annotations form presents every non-trivial+<p>On output, each shape contains an <code>annotations</code> form and a+<code>obligations</code> form. The annotations form presents every non-trivial formula derived from the protocol. The obligations form presents every non-trivial soundness obligation.</p> @@ -560,7 +558,7 @@  <h3>Output</h3> -<p>On output, each role contains a <tt>parameters</tt> form with a list of sets+<p>On output, each role contains a <code>parameters</code> form with a list of sets of atoms.</p>  <blockquote>@@ -577,12 +575,12 @@ <p>In this example, the second parameter set is what is expected for a responder role in this version of the Needham-Schroeder protocol.</p> -<p>Macro expansion is not performed by this program. Use the <tt>-e</tt> option-with <tt>cpsa</tt> to preprocess input that contains macro definitions.</p>+<p>Macro expansion is not performed by this program. Use the <code>-e</code> option+with <code>cpsa</code> to preprocess input that contains macro definitions.</p>  <h2 id="cpsapp">Pretty Printing</h2> -<p>The <tt>cpsapp</tt> program program pretty prints its input using the CPSA+<p>The <code>cpsapp</code> program program pretty prints its input using the CPSA specific algorithm.</p>  <h3>Usage</h3>@@ -605,12 +603,12 @@ quoting. Every list is proper. An atom is either a symbol, an integer, or a string. The characters that make up a symbol are the letters, the digits, and the special characters in-"<tt>-*/&lt;=&gt;!?:$%_&amp;~^</tt>". A symbol may not begin with a+"<code>-*/&lt;=&gt;!?:$%_&amp;~^</code>". A symbol may not begin with a digit or a sign followed by a digit. The characters that make up a string are the printing characters omitting double quote and backslash. Double quotes delimit a string. A comment begins with a semicolon, or is an S-expression list at top-level that starts with-the <tt>comment</tt> symbol. </p>+the <code>comment</code> symbol. </p>  <hr />
doc/index.html view
@@ -1,6 +1,4 @@ <?xml version="1.0" encoding="UTF-8"?>-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"-      "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head>   <meta http-equiv="content-type" content="application/xhtml+xml; charset=UTF-8" />@@ -42,26 +40,25 @@   <pre>$ echo build | ghci Make.hs</pre> </blockquote> -<p>In Windows, click on <tt>Make.hs</tt> and type <tt>build</tt> at-  the <tt>GHCi</tt>-  prompt <tt>*Make&gt;</tt>. The <a href="cpsauser.html#make">CPSA User-  Guide</a> describes a better way to analyze protocols when GNU Make-  is available.</p>+<p>In Windows, click on <code>Make.hs</code> and type <code>build</code> at+  the <code>GHCi</code> prompt <code>*Make&gt;</code>.+  The <a href="cpsauser.html#make">CPSA User Guide</a> describes a+  better way to analyze protocols when GNU Make is available.</p>  <p>After running the analysis, you will note files with the extension-<tt>.xhtml</tt>. These are XHTML/SVG compound documents that can be viewed by+<code>.xhtml</code>. These are XHTML/SVG compound documents that can be viewed by standards compliant browsers such as Firefox, Chrome, Safari, and later versions of Internet Explorer.  See the section on <a href="cpsauser.html#cpsagraph">visualization</a> in the user guide for help interpreting these documents.</p>  <p>New users should study CPSA's analysis of the following protocols-  in order, Blanchet (<tt>blanchet.xhtml</tt>), Needham-Schroeder-  (<tt>ns.xhtml</tt>), Woo-Lam (<tt>woolam.xhtml</tt>), Yahalom-  (<tt>yahalom.xhtml</tt>), ffgg (<tt>ffgg.xhtml</tt>), and finally-  Otway-Rees (<tt>or.xhtml</tt>). When studying the full output,+  in order, Blanchet (<code>blanchet.xhtml</code>), Needham-Schroeder+  (<code>ns.xhtml</code>), Woo-Lam (<code>woolam.xhtml</code>), Yahalom+  (<code>yahalom.xhtml</code>), ffgg (<code>ffgg.xhtml</code>), and finally+  Otway-Rees (<code>or.xhtml</code>). When studying the full output,   simultaneously display the extracted shapes. The shapes file has an-  extension of <tt>_shapes.xhtml</tt>.</p>+  extension of <code>_shapes.xhtml</code>.</p>  <p>To make effective use of CPSA, new users should scan the   <a href="cpsauser.html">user guide</a> to get a flavor of its@@ -79,27 +76,27 @@   suite with many examples.  The README in the top-level directory of   the source distribution contains the installation instructions and   is essential reading for its effective use.  Serious users should-  favor the source distribution.</p>+  favor the source distribution if on a Unix-like platform.</p>  <p>Authentication tests guide the search for new skeletons in CPSA.   The authentication test solved at each step of the search is-  described by the <tt>operation</tt> form in CPSA output.  When CPSA+  described by the <code>operation</code> form in CPSA output.  When CPSA   generates unexpected output, find the first skeleton in the   derivation tree that exhibits the problem and read-  the <tt>operation</tt> form to find out what happened.+  the <code>operation</code> form to find out what happened.   Authentication tests are introduced in   the <a href="cpsaprimer.pdf">primer</a> and described in full   detail in the <a href="cpsaspec.pdf">The CPSA   Specification</a>.</p>  <p>An origination assumption-  (<tt>non-orig</tt>, <tt>pen-non-orig</tt>, and <tt>unig-orig</tt>),+  (<code>non-orig</code>, <code>pen-non-orig</code>, and <code>unig-orig</code>),   can be specified in a role or in a skeleton.  Be sure to read the   advice in the <a href="cpsaprimer.pdf">primer</a> on the proper   placement of origination assumptions.</p>  <p>Variables of sort message unify with any message.  See Otway-Rees-  (<tt>or.xhtml</tt>) for an example of the use of variables of this+  (<code>or.xhtml</code>) for an example of the use of variables of this   sort.</p>  <p>A quoted string is a constant of sort message and is called a tag.@@ -107,15 +104,15 @@   structure in the case where the implementation of the protocol   contains protections against message conflation.</p> -<p>Lisp-like macros in <tt>cpsa</tt> input can be used to replace+<p>Lisp-like macros in <code>cpsa</code> input can be used to replace   multiple occurrences of a message with one named definition of it.   Macros are described in the <a href="cpsaprimer.pdf">primer</a>.</p> -<p>When the <tt>cpsagraph</tt> program is given the <tt>--zoom</tt>+<p>When the <code>cpsagraph</code> program is given the <code>--zoom</code>   option, it produces diagrams that scale.  This is useful when   viewing large diagrams.</p> -<p>When the <tt>cpsapp</tt> program is given the <tt>--json</tt>+<p>When the <code>cpsapp</code> program is given the <code>--json</code>   option, it translates S-expressions into JavaScript Object   Notation.</p>
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.2.12}+\newcommand{\version}{2.2.13} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
doc/readme.html view
@@ -1,6 +1,4 @@ <?xml version="1.0" encoding="UTF-8"?>-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"-      "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head>   <meta http-equiv="REFRESH" content="0;url=index.html" />
setup.bat view
@@ -1,8 +1,8 @@ @setlocal enableextensions
 @cd /d "%~dp0"
 runghc Setup.hs configure 
-runghc Setup.hs build 
-+runghc Setup.hs build
+
 runghc Setup.hs install
--pause+
+pause
src/CPSA/DiffieHellman/Algebra.hs view
@@ -870,6 +870,19 @@  -- Unification and substitution +-- The rewrite rules used are:+--+-- (vars (h base) (x y expn))+--+-- 1.  ((exp h x) y) ==> (exp h (mul x y))+-- 2.  (exp h (one)) ==> h+-- 3.  unify((exp(h, x)), (exp(h, y)), s) ==>+--         unify(x, y, s)+-- 4   unify((exp(h, x)), (exp((gen), y)), s) ==>+--         unify(h, (exp gen (mul y (rec x))), s)+-- 5.  unify((exp((gen), x)), (exp(h, y)), s) ==>+--         unify((exp(h, x)), (exp((gen), y)), s)+ newtype Subst = Subst IdMap deriving (Eq, Ord)  instance Show Subst where
src/CPSA/Lib/Cohort.hs view
@@ -229,8 +229,7 @@             In t ->                 let ns = addSendingBefore S.empty n                     ts = S.map (evtTerm . event) ns -- Public messages-                    (ts', a') = decompose ts a -- Minimum decryption set-                    der = buildable ts' a' in -- Derivable before node+                    der = derivable a ts in -- Derivable before node                 if der t then                     loop nodes                 else
src/perm.pl view
@@ -66,4 +66,15 @@     perm_precedes(Perm, Precedes, OutPrecedes).  perm_node(Perm, (S, I), (OutS, I)) :--    nth0(S, Perm, OutS).+    index_of(Perm, S, OutS).++% Returns the index of the first occurence of Element in List+index_of(List, Element, Index) :-+    index_of(List, Element, 0, Index).+index_of([],_,_,_) :-+    print_message(error,'Element not found in list'),+    fail.+index_of([Element|_], Element, Curr, Curr) :- !.+index_of([_|List], Element, Curr, Index) :-+    Next is Curr + 1,+    index_of(List, Element, Next, Index).
tst/Makefile view
@@ -4,12 +4,12 @@  TSTS	:= $(patsubst %.scm,%.txt,$(wildcard *.scm)) \ 		$(patsubst %.lsp,%.txt,$(wildcard *.lsp))-CPSA	= ../dist/build/cpsa/cpsa-DIFF	= ../dist/build/cpsadiff/cpsadiff-SHAPES	= ../dist/build/cpsashapes/cpsashapes-LOGIC	= ../dist/build/cpsalogic/cpsalogic-ANNOTATIONS = ../dist/build/cpsaannotations/cpsaannotations-GRAPH	= ../dist/build/cpsagraph/cpsagraph+CPSA	= ../dist/build/cpsa/cpsa$(EXE)+DIFF	= ../dist/build/cpsadiff/cpsadiff$(EXE)+SHAPES	= ../dist/build/cpsashapes/cpsashapes$(EXE)+LOGIC	= ../dist/build/cpsalogic/cpsalogic$(EXE)+ANNOTATIONS = ../dist/build/cpsaannotations/cpsaannotations$(EXE)+GRAPH	= ../dist/build/cpsagraph/cpsagraph$(EXE) CPSAFLAGS = +RTS -M512m -RTS  # The expected answers are in files with the .tst extension.
tst/yahalom-6.3.6.scm view
@@ -2,7 +2,8 @@   (comment "A Survey of Authentication Protocol Literature:" 	   "Version 1.0, John Clark and Jeremy Jacob," 	   "Yahalom Protocol, Section 6.3.6, Page 49")-  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))+  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")+  (bound 15))  (defprotocol yahalom basic   (defrole init
tst/yahalom.scm view
@@ -1,4 +1,4 @@-(herald "Yahalom Protocol Without Forwarding")+(herald "Yahalom Protocol Without Forwarding" (bound 15))  (defprotocol yahalom basic   (defrole init