diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,25 @@ +2013-02-28 John D. Ramsdell + + * 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 + + * src/perm.pl: Fix permutation bug. + +2013-01-22 John D. Ramsdell + + * 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 + + * doc/cpsaspec.tex (chapter{Generalization}): Corrected the + definition of a location in the text describing variable + separation. + 2012-11-09 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 2.2.12. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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 diff --git a/README b/README --- a/README +++ b/README @@ -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 diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.2.12 +Version: 2.2.13 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ diff --git a/doc/cpsadesign.tex b/doc/cpsadesign.tex --- a/doc/cpsadesign.tex +++ b/doc/cpsadesign.tex @@ -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 diff --git a/doc/cpsadha.pdf b/doc/cpsadha.pdf Binary files a/doc/cpsadha.pdf and b/doc/cpsadha.pdf differ diff --git a/doc/cpsaintroslides.pdf b/doc/cpsaintroslides.pdf Binary files a/doc/cpsaintroslides.pdf and b/doc/cpsaintroslides.pdf differ diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ diff --git a/doc/cpsaprimer.tex b/doc/cpsaprimer.tex --- a/doc/cpsaprimer.tex +++ b/doc/cpsaprimer.tex @@ -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 diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ diff --git a/doc/cpsaspec.tex b/doc/cpsaspec.tex --- a/doc/cpsaspec.tex +++ b/doc/cpsaspec.tex @@ -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 diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -1,6 +1,4 @@ - 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 cpsagraph program +contains seven tools. The cpsagraph program provides a visualization of answers using Scalable Vector Graphics (SVG). The cpsashapes program removes intermediate results +href="#cpsashapes">cpsashapes program removes intermediate results from analyzer runs making the shapes easy to identify. The cpsadiff program compares CPSA output +href="#cpsafiff">cpsadiff program compares CPSA output files S-expression by S-expression, and prints the first skeleton that differs. -The cpsalogic program logical +The cpsalogic program logical formula that can be used to ensure security goals are achieved. The cpsaannotations program uses protocol +href="#cpsaannotations">cpsaannotations program uses protocol annotations to annotate shapes and generate protocol soundness obligations. The -cpsaparameters program detects some +cpsaparameters program detects some specification errors by performing a data flow analysis on protocol roles. The -cpsapp program pretty prints its input using a +cpsapp program pretty prints its input using a CPSA specific algorithm.

The input syntax is essentially the same as the output syntax. A Lisp aware @@ -63,7 +61,7 @@ this information.

The typical pattern of usage is to enter the set of problems to be analyzed -into a file, in this example, prob.scm, analyze the problems, and if +into a file, in this example, prob.scm, analyze the problems, and if something interesting is produced, visualize the answers.

@@ -81,7 +79,7 @@

The distribution comes with the -file cpsa.mk for inclusion into your +file cpsa.mk 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.

@@ -102,14 +100,14 @@

The CPSA program is Emacs friendly. - If you run the above makefile via "M-x - compile", the results will be displayed in a buffer in - Compilation Mode. The command "C-x `" will visit - the locus of the next error message or match (next-error) + If you run the above makefile via "M-x + compile", the results will be displayed in a buffer in + Compilation Mode. The command "C-x `" will visit + the locus of the next error message or match (next-error) in your CPSA input file.

-

For platforms without GNU make, the Haskell program Make.hs can be loaded into a Haskell interpreter +

For platforms without GNU make, the Haskell program Make.hs 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 comment +elided when printing skeletons, with the exception of the comment key.

The input is an option herald form followed by a sequence of @@ -147,23 +145,23 @@ PROT-ALIST ::= ... -

The protocol ID is a symbol that names the protocol, and the role -ID is a symbol that names the role. The ALG symbol identifies +

The protocol ID is a symbol that names the protocol, and the role +ID is a symbol that names the role. The ALG symbol identifies the algebra used by the protocol. For the Basic Cryptographic Algebra, the -symbol is basic. For the Diffie-Hellman Algebra, the symbol is -diffie-hellman. The var form contains symbols that +symbol is basic. For the Diffie-Hellman Algebra, the symbol is +diffie-hellman. The var 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 non-orig term must not be carried by any event +algebra. Each non-orig 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 (3 a) -asserts that atom a will not be mapped into an instance -unless its height is at least three. For each pen-non-orig +term. A role non-origination assumption of the form (3 a) +asserts that atom a will not be mapped into an instance +unless its height is at least three. For each pen-non-orig term, each of its variables must occur in some term, but unlike a non-origination assumption, the term may be carried. -Each uniq-orig term must originate in the role's trace. Every +Each uniq-orig term must originate in the role's trace. Every non-atomic variable must be acquired by the role's trace.

The structure of sorts and terms in the Basic Cryptographic Algebra @@ -176,12 +174,12 @@ | (pubk STRING ID) | (privk STRING ID) -

The form (cat a b c d e) is expands to (cat a (cat -b (cat c (cat d e)))).

+

The form (cat a b c d e) is expands to (cat a (cat +b (cat c (cat d e)))).

A term in the Basic Crypto Algebra is an atom if it is variable of a sort -other than mesg, or it if formed from one of the following operations: -pubk, privk, invk, and ltk.

+other than mesg, or it if formed from one of the following operations: +pubk, privk, invk, and ltk.

SKELETON   ::= (defskeleton ID VARS STRAND+ SKEL-ALIST)
@@ -195,9 +193,9 @@
 NODE       ::= (INT INT)
-

The ID in the skeleton form names a protocol. It refers to the last +

The ID in the skeleton form names a protocol. It refers to the last protocol definition of that name which precedes the skeleton form. The -ID in the strand form names a role. The integer in the strand form +ID 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 non-orig, pen-non-orig, or uniq-orig +in the non-orig, pen-non-orig, or uniq-orig list or in a maplet must be declared.

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 -(label INT) A skeleton has (parent INT) if it is a member of -the cohort of the identified parent. A skeleton has (seen INT+) when +(label INT) A skeleton has (parent INT) if it is a member of +the cohort of the identified parent. A skeleton has (seen INT+) when members of its cohort are isomorphic to previously seen skeletons. A skeleton -lists its unrealized nodes with (unrealized NODE*). The traces -associated with each strand is given by the (traces ...) form. +lists its unrealized nodes with (unrealized NODE*). The traces +associated with each strand is given by the (traces ...) form. Finally, the operation used to derive this skeleton from its parent is recorded -with (operation TEST KIND TERM NODE TERM*), where TEST is the -authentication test encryption-test or nonce, KIND -is (added-strand ID INT), (contracted MAPLET*), or -(added-listener TERM), TERM is the critical term, -NODE in the test node, and the remaining terms specify the escape set. +with (operation TEST KIND TERM NODE TERM*), where TEST is the +authentication test encryption-test or nonce, KIND +is (added-strand ID INT), (contracted MAPLET*), or +(added-listener TERM), TERM is the critical term, +NODE 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 (operation generalization METHOD), where METHOD -is one of deleted NODE, weakened NODE-PAIR, separated -TERM and forgot TERM. Generalization is used to find shapes from +recorded as (operation generalization METHOD), where METHOD +is one of deleted NODE, weakened NODE-PAIR, separated +TERM and forgot TERM. Generalization is used to find shapes from realized skeletons. For shape collapsing, the operation is recorded as -(operation collapsed INT INT), where the two INTs identify +(operation collapsed INT INT), where the two INTs identify the strands merged. Shape collapsing is used to find related shapes.

The current Diffie-Hellman support is experimental and known to @@ -252,13 +250,13 @@ TERM ::= ... | (gen) | (exp TERM TERM) -

Given exponent x, (gen) is the group +

Given exponent x, (gen) is the group generator constant, and -given g and x, (exp g x) -is g raised to the x power. Terms of the -form (gen) or (exp g x) are of sort base, -and x is of sort expn. Terms of -sort expn are atoms, but terms of sort base are +given g and x, (exp g x) +is g raised to the x power. Terms of the +form (gen) or (exp g x) are of sort base, +and x is of sort expn. Terms of +sort expn are atoms, but terms of sort base are not.

Reasoning about the commutativity of exponents is supported via @@ -272,29 +270,29 @@

Macros and Includes

-

After reading the input, cpsa expands macros before in analyzing +

After reading the input, cpsa expands macros before in analyzing the results. A macro definition is a top-level form.

(defmacro (NAME ARG*) BODY)
-

The cpsa program expands all calls to macros in non-macro defining +

The cpsa 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 cpsa program +are applicable, the last definition takes precedence. The cpsa program omits macro definitions from its output.

A source file can be included within another with the top-level -include form,

+include form,

(include FILE)
-

where FILE is a string. The cpsa program +

where FILE is a string. The cpsa program includes files while it does macro expansion.

Usage of CPSA

@@ -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 +RTS -M512m -RTS limits memory usage to 512m.

+option +RTS -M512m -RTS limits memory usage to 512m.

The herald form can be used to specify options within a file. The - grammar for a herald form follows, where ALIST is an + grammar for a herald form follows, where ALIST is an association list with symbols as keys.

@@ -334,29 +332,29 @@ TITLE ::= SYMBOL | STRING
-

The title is used by cpsagraph when generating XHTML. +

The title is used by cpsagraph 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 --bound=12.

+ option --bound=12.

(herald "Needham-Schroeder Public-Key Protocol" (bound 12))
-

The herald form is only interpreted by the cpsa program, +

The herald form is only interpreted by the cpsa program, and is treated as a comment by all other programs. In particular, - specifying a margin option effects cpsa only.

+ specifying a margin option effects cpsa only.

For long running problems, SMP parallelism is available. For example, on a -quad-core machine, we would probably use +RTS -N4 -RTS.

+quad-core machine, we would probably use +RTS -N4 -RTS.

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 (reverse-search) in its association + When a role includes (reverse-search) in its association list as a comment, the nodes in its instances will be searched in reverse order.

-

When run with isomorphism checks disabled (--noisochk), CPSA +

When run with isomorphism checks disabled (--noisochk), 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 @@

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 cpsashapes program.

+href="#cpsashapes">cpsashapes program.

An error message that begins with "No test for unrealized node" identifies a severe error that should be reported as a bug.

Visualization

-

The cpsagraph program produces a graphical rendering of the output +

The cpsagraph 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.

@@ -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 *, the graphing program sometimes -draws a dashed line between (send (* a b)) and (recv (* b -a)).

+algebra with a commutative operation *, the graphing program sometimes +draws a dashed line between (send (* a b)) and (recv (* b +a)).

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.

-

By the default, cpsagraph generates a view of CPSA S-expressions as +

By the default, cpsagraph generates a view of CPSA S-expressions as a compound document that contains SVG within XHTML. This view integrates graphics with the input text.

-

In compact mode, cpsagraph generates an SVG document. The tree is +

In compact mode, cpsagraph 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.

-

In LaTeX mode, cpsagraph generates LaTeX source. XY-pic is used for +

In LaTeX mode, cpsagraph generates LaTeX source. XY-pic is used for drawings of skeletons. The margin specified in cpsa.mk produces good results.

+href="cpsa.mk">cpsa.mk produces good results.

Usage

@@ -433,7 +431,7 @@

Output Comparisons

-

The cpsadiff program compares CPSA output files +

The cpsadiff program compares CPSA output files S-expression by S-expression, and prints the first skeleton that differs.

@@ -450,7 +448,7 @@

Shape Extraction

-

The cpsashapes program extracts the original problems and the +

The cpsashapes 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.

@@ -467,7 +465,7 @@

Formula Extraction

-

The cpsalogic program extracts a formula in the language +

The cpsalogic 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 @@

Annotations

-

The cpsaannotations program uses protocol annotations to annotate +

The cpsaannotations program uses protocol annotations to annotate shapes and generate protocol soundness obligations.

Usage

@@ -506,8 +504,8 @@

Syntax

-

To be analyzed, each role in a protocol must include an annotations -form. The TERM is a role atom that when instantiated, is the name of a +

To be analyzed, each role in a protocol must include an annotations +form. The TERM 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.

@@ -528,12 +526,12 @@ FTERM ::= TERM | (ID FTERM*) -

Use (and) for truth and (or) for falsehood.

+

Use (and) for truth and (or) for falsehood.

Output

-

On output, each shape contains an annotations form and a -obligations form. The annotations form presents every non-trivial +

On output, each shape contains an annotations form and a +obligations form. The annotations form presents every non-trivial formula derived from the protocol. The obligations form presents every non-trivial soundness obligation.

@@ -560,7 +558,7 @@

Output

-

On output, each role contains a parameters form with a list of sets +

On output, each role contains a parameters form with a list of sets of atoms.

@@ -577,12 +575,12 @@

In this example, the second parameter set is what is expected for a responder role in this version of the Needham-Schroeder protocol.

-

Macro expansion is not performed by this program. Use the -e option -with cpsa to preprocess input that contains macro definitions.

+

Macro expansion is not performed by this program. Use the -e option +with cpsa to preprocess input that contains macro definitions.

Pretty Printing

-

The cpsapp program program pretty prints its input using the CPSA +

The cpsapp program program pretty prints its input using the CPSA specific algorithm.

Usage

@@ -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 -"-*/<=>!?:$%_&~^". A symbol may not begin with a +"-*/<=>!?:$%_&~^". 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 comment symbol.

+the comment symbol.

diff --git a/doc/index.html b/doc/index.html --- a/doc/index.html +++ b/doc/index.html @@ -1,6 +1,4 @@ - @@ -42,26 +40,25 @@ 
$ echo build | ghci Make.hs
-

In Windows, click on Make.hs and type build at - the GHCi - prompt *Make>. The CPSA User - Guide describes a better way to analyze protocols when GNU Make - is available.

+

In Windows, click on Make.hs and type build at + the GHCi prompt *Make>. + The CPSA User Guide describes a + better way to analyze protocols when GNU Make is available.

After running the analysis, you will note files with the extension -.xhtml. These are XHTML/SVG compound documents that can be viewed by +.xhtml. 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 visualization in the user guide for help interpreting these documents.

New users should study CPSA's analysis of the following protocols - in order, Blanchet (blanchet.xhtml), Needham-Schroeder - (ns.xhtml), Woo-Lam (woolam.xhtml), Yahalom - (yahalom.xhtml), ffgg (ffgg.xhtml), and finally - Otway-Rees (or.xhtml). When studying the full output, + in order, Blanchet (blanchet.xhtml), Needham-Schroeder + (ns.xhtml), Woo-Lam (woolam.xhtml), Yahalom + (yahalom.xhtml), ffgg (ffgg.xhtml), and finally + Otway-Rees (or.xhtml). When studying the full output, simultaneously display the extracted shapes. The shapes file has an - extension of _shapes.xhtml.

+ extension of _shapes.xhtml.

To make effective use of CPSA, new users should scan the user guide 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.

+ favor the source distribution if on a Unix-like platform.

Authentication tests guide the search for new skeletons in CPSA. The authentication test solved at each step of the search is - described by the operation form in CPSA output. When CPSA + described by the operation form in CPSA output. When CPSA generates unexpected output, find the first skeleton in the derivation tree that exhibits the problem and read - the operation form to find out what happened. + the operation form to find out what happened. Authentication tests are introduced in the primer and described in full detail in the The CPSA Specification.

An origination assumption - (non-orig, pen-non-orig, and unig-orig), + (non-orig, pen-non-orig, and unig-orig), can be specified in a role or in a skeleton. Be sure to read the advice in the primer on the proper placement of origination assumptions.

Variables of sort message unify with any message. See Otway-Rees - (or.xhtml) for an example of the use of variables of this + (or.xhtml) for an example of the use of variables of this sort.

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.

-

Lisp-like macros in cpsa input can be used to replace +

Lisp-like macros in cpsa input can be used to replace multiple occurrences of a message with one named definition of it. Macros are described in the primer.

-

When the cpsagraph program is given the --zoom +

When the cpsagraph program is given the --zoom option, it produces diagrams that scale. This is useful when viewing large diagrams.

-

When the cpsapp program is given the --json +

When the cpsapp program is given the --json option, it translates S-expressions into JavaScript Object Notation.

diff --git a/doc/macros.tex b/doc/macros.tex --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}} -\newcommand{\version}{2.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 diff --git a/doc/readme.html b/doc/readme.html --- a/doc/readme.html +++ b/doc/readme.html @@ -1,6 +1,4 @@ - diff --git a/setup.bat b/setup.bat --- a/setup.bat +++ b/setup.bat @@ -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 diff --git a/src/CPSA/DiffieHellman/Algebra.hs b/src/CPSA/DiffieHellman/Algebra.hs --- a/src/CPSA/DiffieHellman/Algebra.hs +++ b/src/CPSA/DiffieHellman/Algebra.hs @@ -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 diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs --- a/src/CPSA/Lib/Cohort.hs +++ b/src/CPSA/Lib/Cohort.hs @@ -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 diff --git a/src/perm.pl b/src/perm.pl --- a/src/perm.pl +++ b/src/perm.pl @@ -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). diff --git a/tst/Makefile b/tst/Makefile --- a/tst/Makefile +++ b/tst/Makefile @@ -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. diff --git a/tst/yahalom-6.3.6.scm b/tst/yahalom-6.3.6.scm --- a/tst/yahalom-6.3.6.scm +++ b/tst/yahalom-6.3.6.scm @@ -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 diff --git a/tst/yahalom.scm b/tst/yahalom.scm --- a/tst/yahalom.scm +++ b/tst/yahalom.scm @@ -1,4 +1,4 @@ -(herald "Yahalom Protocol Without Forwarding") +(herald "Yahalom Protocol Without Forwarding" (bound 15)) (defprotocol yahalom basic (defrole init