packages feed

cpsa 2.2.13 → 2.3.0

raw patch · 95 files changed

+516/−336 lines, 95 files

Files

ChangeLog view
@@ -1,3 +1,59 @@+2013-07-23  John D. Ramsdell  <ramsdell@mitre.org>++        * cpsa.cabal (Version):  Tagged as version 2.3.0++	* src/CPSA/Lib/*.hs:  Added priorities to help guide the search.++	* src/CPSA/Lib/Protocol.hs (mkRole): Positions are now used to+	specify non-origination introductions rather than heights.++	* doc/cpsaspec.tex: Reverted back to zero-based indexing.++	* doc/cpsauser.tex: Removed Diffie-Hellman documentation as the+	implementation of the algebra continues to have serious issues.++2013-07-22  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Graph/Tree.hs (makeTree): Skeletons without children+	that are not marked "empty cohort" are now counted as live.++2013-06-13  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Algebra.hs: Added isMesgVar for acquires check.++	* src/CPSA/Lib/Strand.hs (thinStrand, thinManyStrands):  Added+	transitive reduction before thinning.++	* src/CPSA/*/Algebra.hs:  Removed support for GHC 6.x.++2013-04-23  John D. Ramsdell  <ramsdell@mitre.org>++	* src/prover9.pl: Removed erroneous quotes that were added to the+	translation of constants.++2013-04-10  John D. Ramsdell  <ramsdell@mitre.org>++	* src/prover9.pl: Changed the formula translation algorithm so+	that predicates for the sort declarations of variables are added+	to generated formulas.  Previously, the sort information was+	ignored.++2013-03-29  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/DiffieHellman/Algebra.hs (mgu): Changed so function+	performs substitutions on all vars on LHS, not just the ones not+	that were originally on the LHS.++2013-03-12  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Annotations/Annotations.hs (obligation): Replaced an+	irrefutable pattern that raised an exception with a maybeToList.++2013-03-06  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/DiffieHellman/Algebra.hs (sLoad):  Added code that+	allows testing of unification and matching in GHCi.+ 2013-02-28  John D. Ramsdell  <ramsdell@mitre.org>  	* doc/*.html:  Convert to HTML 5 mainly by eliminating the DOCTYPE
NEWS view
@@ -1,5 +1,23 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.3.0++** Priorities for influencing search order added+   The priority form in roles and skeletons allows the search to focus+   on specific nodes of interest.++** Role non-origination with position changed+   A non-origination assumption of the form (3 a) now means the+   assumption is add when the height of the strand is greater that 3.+   It used to be added when the height of the strand is at least three.++** Shape Analysis Sentence to Prover9 translator improved+   Changed the formula translation algorithm so that predicates for+   the sort declarations of variables are added to generated formulas.+   Previously, the sort information was ignored.++** Bug fixed in cpsaannotations+ * Changes in version 2.2.13  ** Better support for Cygwin users
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.2.13+Version:		2.3.0 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3@@ -47,8 +47,7 @@ Data-Files:   index.html readme.html cpsauser.html cpsa.mk Make.hs cpsaprimer.pdf   cpsaoverview.pdf cpsaintroslides.pdf cpsaspec.pdf cpsadesign.pdf-  cpsadha.pdf ffgg.scm ns.scm blanchet.scm or.scm woolam.scm-  yahalom.scm dhke.scm+  ffgg.scm ns.scm blanchet.scm or.scm woolam.scm yahalom.scm Data-Dir:	    	doc Extra-Source-Files:   Makefile ChangeLog README NEWS ghci cpsatst setup.bat@@ -120,7 +119,7 @@   Main-Is:		CPSA/Lib/Main.hs   Build-Depends:	base >= 3 && < 5, containers, parallel, array   GHC-Options:-    -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded+    -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded -rtsopts   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Vector CPSA.Lib.Utilities CPSA.Lib.Pretty@@ -131,8 +130,6 @@     CPSA.DiffieHellman.IntLinEq CPSA.SimpleDiffieHellman.Algebra     CPSA.DiffieHellmanNoReciprocal.Algebra     CPSA.DiffieHellmanNoReciprocal.LinDiophEq-  if impl(ghc >= 7.0.0)-    GHC-Options: -rtsopts  Executable cpsagraph   Main-Is:		CPSA/Graph/Main.hs
doc/Makefile view
@@ -14,7 +14,6 @@ SLIDES = cpsaintroslides DESIGN = cpsadesign SPEC = cpsaspec-DHA = cpsadha BIB = cpsa  TEX_SRCS = macros.tex bcasyntax.tex@@ -33,7 +32,7 @@ 	makeindex $*  all:	$(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \-		$(DESIGN).pdf $(SPEC).pdf $(DHA).pdf+		$(DESIGN).pdf $(SPEC).pdf  $(PRIMER).pdf:	$(MP_SRCS:.mp=-0.mps) $(TEX_SRCS) \ 		 $(PRIMER).tex $(PRIMER).bbl@@ -60,12 +59,8 @@ 	if test -f $(SPEC).idx; then $(MAKE) $(SPEC).ind; fi 	pdflatex $(SPEC).tex -$(DHA).pdf: $(DHA).tex $(DHA).bbl-	if test ! -f $(DHA).aux; then pdflatex $(DHA).tex; fi-	pdflatex $(DHA).tex- CLEAN_FILES := $(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \-		$(DESIGN).pdf $(SPEC).pdf $(DHA).pdf \+		$(DESIGN).pdf $(SPEC).pdf \ 	$(wildcard *.log *.aux *.toc *.mps *.mpx) \ 	$(wildcard *.bbl *.blg *.ind *.idx *.ilg *.out)
doc/cpsadesign.pdf view

binary file changed (275306 → 275297 bytes)

− doc/cpsadha.pdf

binary file changed (222454 → absent bytes)

doc/cpsaintroslides.pdf view

binary file changed (93151 → 93151 bytes)

doc/cpsaoverview.pdf view

binary file changed (129012 → 129004 bytes)

doc/cpsaprimer.pdf view

binary file changed (273723 → 273712 bytes)

doc/cpsaspec.pdf view

binary file changed (410823 → 410817 bytes)

doc/cpsaspec.tex view
@@ -156,10 +156,10 @@ \section{Notation}\label{sec:notation}  A finite sequence\index{sequence} is a function from an initial-segment of the whole numbers.  The length of a sequence~$X$ is~$|X|$,-and sequence~$X=\seq{X(1),\ldots,X(n)}$ for $n=|X|$.  Alternatively,-$\seq{x_1,x_2,\ldots,x_n} =x_1\cons x_2\cons\ldots\cons-x_n\cons\seq{}$.  If~$S$ is a set, then~$S^\ast$ is the set of finite+segment of the natural numbers.  The length of a sequence~$X$ is~$|X|$,+and sequence~$X=\seq{X(0),\ldots,X(n-1)}$ for $n=|X|$.  Alternatively,+$\seq{x_0,x_1,\ldots,x_{n-1}} =x_0\cons x_1\cons\ldots\cons+x_{n-1}\cons\seq{}$.  If~$S$ is a set, then~$S^\ast$ is the set of finite sequences of~$S$, and~$S^+$ is the non-empty finite sequences of~$S$. The concatenation of sequences~$X_0$ and~$X_1$ is~$X_0\append X_1$. The prefix of sequence~$X$ of length~$n$ is~$\prefix{X}{n}$.@@ -317,15 +317,15 @@ \alga_X\rightarrow\alga_Y$ induced by~$\sigma$ is also denoted~$\sigma$. -A \index{position}\emph{position}~$p$ is a finite sequence of whole+A \index{position}\emph{position}~$p$ is a finite sequence of natural numbers.  The term in~$t$ that \emph{occurs at}~$p$, written~$t\termat p$, is: $$\begin{array}{l} t\termat\seq{}=t;\\-(t_1,t_2)\termat i\cons p=t_i\termat p\mbox{ for $i\in\{1,2\}$};\\-\enc{t_1}{t_2}\termat i\cons p=t_i\termat p\mbox{ for-  $i\in\{1,2\}$};\\-t^{-1}\termat 1\cons p=t\termat p.+(t_0,t_1)\termat i\cons p=t_i\termat p\mbox{ for $i\in\{0,1\}$};\\+\enc{t_0}{t_1}\termat i\cons p=t_i\termat p\mbox{ for+  $i\in\{0,1\}$};\\+t^{-1}\termat 0\cons p=t\termat p. \end{array}$$ A term~$t$ \index{occurs in}\emph{occurs in} term~$t'$ if $t=t'\termat p$ for some~$p$.  A message~$T$ \emph{occurs in} message~$T'$ if the@@ -340,12 +340,12 @@ $$\carpos(t,t')=\left\{ \begin{array}{ll} \{\seq{}\}&\mbox{if $t'\equiv t$, else}\\-\multicolumn{2}{l}{\{1\cons p \mid+\multicolumn{2}{l}{\{0\cons p \mid p\in\carpos(t,t_1)\}}\\-& \mbox{if $t'=\enc{t_1}{t_2}$, else}\\+& \mbox{if $t'=\enc{t_0}{t_1}$, else}\\ \multicolumn{2}{l}{\{i\cons p \mid-i\in\{1,2\}, p\in\carpos(t,t_i)\}} \\-& \mbox{if $t'=(t_1,t_2)$ else}\\+i\in\{0,1\}, p\in\carpos(t,t_i)\}} \\+& \mbox{if $t'=(t_0,t_1)$ else}\\ \emptyset&\mbox{otherwise.} \end{array}\right.$$ @@ -400,13 +400,13 @@ Message events occur at nodes in a strand space.  For each strand~$s$, there is a node for every event in~$\Theta(s)$.  The \index{nodes}\emph{nodes} of strand space $\Theta$ are $\{(s,i)\mid-s\in\sdom(\Theta), 1\leq i\leq |\Theta(s)|\}$, the event at a node is+s\in\sdom(\Theta), 0\leq i< |\Theta(s)|\}$, the event at a node is \index{evt@\evt}$\evt_\Theta(s,i)=\Theta(s)(i)$, and the message at a node is \index{msg@\msg}$\msg_\Theta(s,i) = m$ such that $\evt_\Theta(s,i) = \pm m$.  Just as a position names a subterm within another term, a strand names a trace within a strand space, and a node names an event in a strand space.  The relation~$\Rightarrow$ defined-by $\{(s,i)\Rightarrow(s,i+1)\mid s\in\sdom(\Theta), 1\leq+by $\{(s,i-1)\Rightarrow(s,i)\mid s\in\sdom(\Theta), 1\leq i<|\Theta(s)|\}$ is called the \index{strand succession}\emph{strand   succession relation}. @@ -460,7 +460,7 @@ set of variables that occur in~$\prefix{C}{h}$, (4) if the variables in $t\in N$ occur in $\sdom(\sigma)$, then $\sigma(t)$ is non-originating in $\Upsilon(\Theta_X,\to)$, and (5) if $t\in U$-originates at index~$i$ in~$C$, and $i\leq h$, then $\sigma(t)$+originates at index~$i$ in~$C$, and $i<h$, then $\sigma(t)$ uniquely originates in $\Upsilon(\Theta_X,\to)$ at node $(s,i)$. Origination assumptions in bundles specified by roles are called \index{inherited origination assumptions}\emph{inherited origination@@ -687,7 +687,7 @@ \seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}}\rangle, \end{array} &\mbox{Traces}\\-&\{(1,1)\prec(2,1),(2,2)\prec(1,2)\},+&\{(0,0)\prec(1,0),(1,1)\prec(0,1)\}, &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, &\mbox{Non-origination}\\@@ -752,7 +752,7 @@ \mbox{Traces}\\ \mbox{\emph{Note key is $b'$ not $b$!}} \end{array}\\-&\{(2,1)\prec(1,1)\},+&\{(1,0)\prec(0,0)\}, &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, &\mbox{Non-origination}\\@@ -775,7 +775,7 @@ \seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}}, \seq{\inbnd d,\outbnd d}}, &\mbox{Traces}\\-&\{(1,2)\prec(2,1),+&\{(0,1)\prec(1,0), &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, &\mbox{Non-origination}\\@@ -1143,7 +1143,7 @@ Skeleton~$k_0$ reduces to skeleton~$k_1$ by pruning, written $k_0\reduction{\ops{P}_s}k_1$, iff there is a most general unifier~$\sigma$ such that $\sigma(\Theta_{k_0}(s)(j))\equiv-\Theta_{k_0}(s')(j)$ for all $1\leq j\leq|\Theta_{k_0}(s)|$, no+\Theta_{k_0}(s')(j)$ for all $0\leq j<|\Theta_{k_0}(s)|$, no variable in $\sdom(\sigma)$ occurs in the trace of any strand other than~$s$, $\sigma$ is a renaming, $t\in U_{k_0}$ implies $\sigma(t)\in U_{k_0}$, $t\in N_{k_0}$ implies $\sigma(t)\in N_{k_0}$, there is@@ -1645,7 +1645,7 @@ Suppose there are strands~$s$ and~$s'$, where one of them is the newly created strand, and a most general unifier~$\sigma'$ such that $\sigma'(\Theta_{k_1}(s)(j))\equiv \sigma'(\Theta_{k_1}(s')(j))$ for-$1\leq j\leq|\Theta_{k_1}(s)|$.  Skeleton~$k_4$ is a+$0\leq j<|\Theta_{k_1}(s)|$.  Skeleton~$k_4$ is a \index{displacement}\emph{displacement} if $k_1\reduction{\ops{S}_{\sigma'}}k_2\reduction{\ops{C}_{s,s'}}k_3 \reduction{\fn{pskel}}k_4$.@@ -1718,7 +1718,7 @@   $\sigma'=\sigma_0\circ\sigma_r$ for some $\sigma_0$.)  \item[Ensure previous events do not transform:] For each $\sigma'$,-  find most general unifiers~$\sigma$ such that for $1\leq i<h$,+  find most general unifiers~$\sigma$ such that for $0\leq i<h$,   $\sigma(t_c)$ is carried only within $\sigma(T_e)$ at $\sigma(C(i))$   and $\sigma'\unlhd\sigma$.  The function \fn{cowt}, presented in   Figure~\ref{fig:cowt}, performs the explorations, producing the@@ -1771,7 +1771,7 @@ Let $k_0$ and $k_1$ be two skeletons such that there are two strands,~$s$ and~$s'$, and a most general unifier~$\sigma$ such that $\sigma(\Theta_{k_0}(s)(j))\equiv \sigma(\Theta_{k_0}(s')(j))$ for all-$1\leq j\leq|\Theta_{k_0}(s)|$.  Then~$k_0$ \emph{collapses} to~$k_1$,+$0\leq j<|\Theta_{k_0}(s)|$.  Then~$k_0$ \emph{collapses} to~$k_1$, written $k_0\reduction{\fn{clp}}k_1$, if $k_0\reduction{\ops{S}_\sigma}k\reduction{\ops{C}_{s,s'}}k' \reduction{\fn{skel}}k_1$.@@ -2140,7 +2140,7 @@ 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 $1\leq h\leq|C|$+$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
doc/cpsauser.html view
@@ -3,7 +3,7 @@ <head>   <meta http-equiv="content-type"   content="application/xhtml+xml; charset=UTF-8" />-  <title>CPSA 2.2 User Guide</title>+  <title>CPSA 2.3 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.2 User Guide</h1>+<h1>CPSA 2.3 User Guide</h1>  <p>The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to enumerate all essentially different executions possible for a cryptographic protocol. We call@@ -138,18 +138,18 @@ DECL       ::= (ID+ SORT) TRACE      ::= (trace EVENT+) EVENT      ::= (send TERM) | (recv TERM)-ROLE-ALIST ::= (non-orig HT-TERM*) ROLE-ALIST-            |  (pen-non-orig HT-TERM*) ROLE-ALIST+ROLE-ALIST ::= (non-orig POS-TERM*) ROLE-ALIST+            |  (pen-non-orig POS-TERM*) ROLE-ALIST             |  (uniq-orig TERM*) ROLE-ALIST | ...-HT-TERM    ::= TERM | (INT TERM)+            |  (priority NODE-INT*) SKEL-ALIST+POS-TERM    ::= TERM | (INT TERM) PROT-ALIST ::= ...</pre> </blockquote>  <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 <code>basic</code>. For the Diffie-Hellman Algebra, the symbol is-<code>diffie-hellman</code>. The <code>var</code> form contains symbols that+symbol is <code>basic</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@@ -158,7 +158,7 @@ in the role's trace, but each of its variables must occur in some 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>+unless its height is greater than 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 <code>uniq-orig</code> term must originate in the role's trace. Every@@ -188,7 +188,8 @@ SKEL-ALIST ::= (non-orig TERM*) SKEL-ALIST             |  (pen-non-orig TERM*) SKEL-ALIST             |  (uniq-orig TERM*) SKEL-ALIST-            |  (precedes NODE-PAIR*) SKEL-ALIST | ...+            |  (precedes NODE-PAIR*) SKEL-ALIST+            |  (priority NODE-INT*) SKEL-ALIST | ... NODE-PAIR  ::= (NODE NODE) NODE       ::= (INT INT)</pre> </blockquote>@@ -241,33 +242,6 @@ <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-have flaws. The additional sorts and terms in the Diffie-Hellman-Algebra follow.</p>--<blockquote>-  <pre>SORT ::= ... | base | expn-TERM ::= ... | (gen) | (exp TERM TERM)</pre>-</blockquote>--<p>Given exponent <code>x</code>, <code>(gen)</code> is the group-generator constant, and-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-  following equation.</p>--<blockquote>-  <pre>(exp (exp (gen) x) y) = (exp (exp (gen) y) x)</pre>-</blockquote>--<p>To avoid known Diffie-Hellman flaws, avoid variables of sort base.</p>- <h3>Macros and Includes</h3>  <p>After reading the input, <code>cpsa</code> expands macros before in analyzing@@ -368,6 +342,26 @@  <p>An error message that begins with "No test for unrealized node" identifies a severe error that should be reported as a bug.</p>++<h3 id="priority">Search order</h3>++<p>In its analysis, CPSA will attempt to solve unrealized nodes until the +skeleton is realized, and then generalize until a shape is obtained.  When +there are multiple unrealized nodes, by default, CPSA will chose the topmost,+rightmost unrealized node among those unrealized nodes with maximum priority.+The default priority of a node is 5, and higher numbers represent a higher +priority.  When a node has non-positive priority, it is left unsolved.</p>++<p>In a role, in order to specify a priority for an event other than+the default, add a comment of the+form <code>(priority (<var>i</var> <var>p</var>))</code>,+where <var>i</var> is the index of the event in the trace,+and <var>p</var> is the priority.+Priorities are inherited+from roles, but may be overridden in a skeleton with a +<code>priority</code> comment of the form+<code>(priority (<var>n</var> <var>p</var>))</code>,+where <var>n</var> is a node.  <h2 id="cpsagraph">Visualization</h2>
− doc/dhke.scm 
@@ -1,29 +0,0 @@-(herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman))--;; The Diffie-Hellman problem is given (exp (gen) x), and (exp (gen)-;; y), compute the value of (exp (exp (gen) x) y) which is also (exp-;; (exp (gen) y) x).--(defprotocol dhke diffie-hellman-  (defrole init (vars (a b akey) (x y expn))-    (trace-     (send (enc "i" (exp (gen) x) (invk a)))-     (recv (cat (enc (exp (gen) y) (invk b))-		(enc a b (exp (exp (gen) y) x))))-     (send (enc "i" a b (exp (exp (gen) y) x))))-    (uniq-orig  x))-  (defrole resp (vars (a b akey) (x y expn))-    (trace-     (recv (enc "i" (exp (gen) x) (invk a)))-     (send (cat (enc (exp (gen) y) (invk b))-		(enc a b (exp (exp (gen) x) y))))-     (recv (enc "i" a b (exp (exp (gen) x) y))))-    (uniq-orig y)))--(defskeleton dhke (vars (a b akey))-  (defstrand resp 3 (a a) (b b))-  (non-orig (invk a) (invk b)))-- (defskeleton dhke (vars (a b akey))-   (defstrand init 2 (a a) (b b))-   (non-orig (invk a) (invk b)))
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.2.13}+\newcommand{\version}{2.3.0} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
src/CPSA/Annotations/Annotations.hs view
@@ -11,6 +11,7 @@ import Control.Monad import qualified Data.List as L import qualified Data.Set as S+import qualified Data.Maybe as M import CPSA.Lib.CPSA import CPSA.Annotations.Formulas @@ -457,7 +458,7 @@       (t, fs) <- annos !! s                      -- t relies on (fs !! p)       let guar = [ if t == t' then f else says t' f | -- Believe t                    (s, p) <- ns,                 -- For each predecessor-                   let Just (t', fs) = annos !! s, -- t' is the speaker+                   (t', fs) <- M.maybeToList (annos !! s), -- t' is the speaker                    let f = fs !! p ]               -- f is the guarantee       return (n, t, implies guar (fs !! p))
src/CPSA/Basic/Algebra.hs view
@@ -10,7 +10,7 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE MultiParamTypeClasses, CPP #-}+{-# LANGUAGE MultiParamTypeClasses #-}  module CPSA.Basic.Algebra (name, origin) where @@ -24,14 +24,6 @@ import qualified CPSA.Lib.CPSA as C import CPSA.Lib.CPSA (SExpr(..), Pos, annotation) --- Preserve the ability to use GHC 6.x-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700-foldrWithKey = M.foldWithKey-#else-foldrWithKey = M.foldrWithKey-#endif- name :: String name = "basic" @@ -154,6 +146,10 @@ varId (F Akey [I x]) = x varId _ = error "Algebra.varId: term not a variable with its sort" +isMesgVar :: Term -> Bool+isMesgVar (I _) = True+isMesgVar _ = False+ -- A list of terms are well-formed if each one has the correct -- structure and every occurrence of an identifier in a term has the -- same sort.  Variable environments are used to check the sort@@ -435,6 +431,7 @@  instance C.Term Term where     isVar = isVar+    isMesgVar = isMesgVar     isAtom = isAtom     termsWellFormed = termsWellFormed     occursIn = occursIn@@ -753,7 +750,7 @@ identityEnvFor (Env r) ts =     all (allId $ flip S.notMember dom) ts     where-      dom = foldrWithKey f S.empty r -- The domain of r+      dom = M.foldrWithKey f S.empty r -- The domain of r       f x (I y) dom           | x == y = dom        -- Ignore trivial bindings           | otherwise = S.insert x dom
src/CPSA/DiffieHellman/Algebra.hs view
@@ -14,7 +14,7 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE MultiParamTypeClasses, CPP #-}+{-# LANGUAGE MultiParamTypeClasses #-}  module CPSA.DiffieHellman.Algebra (name, origin) where @@ -29,14 +29,6 @@ import CPSA.Lib.CPSA (SExpr(..), Pos, annotation) import qualified CPSA.DiffieHellman.IntLinEq as I --- Preserve the ability to use GHC 6.x-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700-foldrWithKey = M.foldWithKey-#else-foldrWithKey = M.foldrWithKey-#endif- {-- Debugging support import System.IO.Unsafe @@ -59,11 +51,59 @@ zt _ y = y --} -{-- Export iUnify and iMatch for GHCi for debugging+{- Export iUnify and iMatch for GHCi for debugging++For this to work, you must install the package bytestring-handle from+Hackage and tell GHCi that it is not hidden on the command line or+within GHCi with:++:set -package bytestring-handle++-}++{--+import System.IO (Handle)+import Data.ByteString.Lazy.Char8 (pack)+import Data.ByteString.Handle+import Control.Exception (try)+import System.IO.Unsafe++stringHandle :: String -> IO Handle+stringHandle s = readHandle False (pack s)++stringPosHandle :: String -> IO C.PosHandle+stringPosHandle s =+    do+      h <- stringHandle s+      C.posHandle "" h++stringLoad :: String -> IO [SExpr Pos]+stringLoad s =+    do+      h <- stringPosHandle s+      loop h []+    where+      loop h xs =+          do+            x <- C.load h+            case x of+              Nothing ->+                return $ reverse xs+              Just x ->+                loop h (x : xs)++sLoad :: String -> Maybe [SExpr Pos]+sLoad s =+    unsafePerformIO (stringLoad s >>= return . Just)++-- Test unification+ iUnify :: String -> String -> String -> Maybe Subst iUnify vars t t' =     iRun unify emptySubst vars t t' +-- Test matching+ iMatch :: String -> String -> String -> Maybe Env iMatch vars t t' =     iRun match emptyEnv vars t t'@@ -72,9 +112,9 @@         String -> String -> String -> Maybe a iRun f mt vars t t' =     do-      vars <- C.load "" vars-      [t] <- C.load "" t-      [t'] <- C.load "" t'+      vars <- sLoad vars+      [t] <- sLoad t+      [t'] <- sLoad t'       (gen, vars) <- loadVars origin vars       t <- loadTerm vars t       t' <- loadTerm vars t'@@ -152,7 +192,7 @@  mul :: Group -> Group -> Group mul t t' =-    foldrWithKey f t' t         -- Fold over the mappings in t+    M.foldrWithKey f t' t       -- Fold over the mappings in t     where       f x c t =                 -- Alter the mapping of           M.alter (g c) x t     -- variable x in t@@ -289,6 +329,10 @@ varId (G t) | isGroupVar t = head $ M.keys t varId _ = error "Algebra.varId: term not a variable with its sort" +isMesgVar :: Term -> Bool+isMesgVar (I _) = True+isMesgVar _ = False+ -- A list of terms are well-formed if each one has the correct -- structure and every occurrence of an identifier in a term has the -- same sort.  Variable environments are used to check the sort@@ -475,7 +519,6 @@     ba term     where       ba (I _) = True           -- A mesg sorted variable is always buildable-      ba (F Base [I _]) = True  -- as is a base sorted variable       ba (C _) = True           -- So is a tag       ba (F Cat [t0, t1]) =           ba t0 && ba t1@@ -658,6 +701,7 @@  instance C.Term Term where     isVar = isVar+    isMesgVar = isMesgVar     isAtom = isAtom     termsWellFormed = termsWellFormed     occursIn = occursIn@@ -847,7 +891,7 @@  groupSubst :: IdMap -> Group -> Group groupSubst subst t =-    foldrWithKey f M.empty t+    M.foldrWithKey f M.empty t     where       f x n t =           mul (expg (groupLookup subst x) n) t@@ -1172,28 +1216,28 @@ matchGroup ::  Group -> Group -> Set Id -> Gen -> Maybe (Set Id, Gen, IdMap) matchGroup t0 t1 v g =     case partition t0 t1 v of-      (_, [], []) -> return (v, g, emptyIdMap)-      (_, [], _) -> Nothing-      (n, t0, t1) ->+      ([], []) -> return (v, g, emptyIdMap)+      ([], _) -> Nothing+      (t0, t1) ->           do             subst <- I.intLinEq (map snd t0, map snd t1)-            return $ mgu v n (map fst t0) (map fst t1) subst g+            return $ mgu v (map fst t0) (map fst t1) subst g  type Coeff = [(Id, Int)]  -- Move variables on the RHS of the equation to the LHS-partition ::  Group -> Group -> Set Id -> (Int, Coeff, Coeff)+partition ::  Group -> Group -> Set Id -> (Coeff, Coeff) partition t0 t1 v =-    (length v0, v0 ++ map (\(x,n) -> (x, negate n)) v1, c1)+    (v0 ++ map (\(x,n) -> (x, negate n)) v1, c1)     where       v0 = M.assocs t0       (v1, c1) = L.partition f (M.assocs t1)       f (x, _) = S.member x v -mgu :: Set Id -> Int -> [Id] -> [Id] -> I.Subst -> Gen -> (Set Id, Gen, IdMap)-mgu v _ _ _ [] gen = (v, gen, emptyIdMap)-mgu v n vars syms subst gen =-    (v', gen', foldl f emptyIdMap (zip vars [0..(n - 1)]))+mgu :: Set Id -> [Id] -> [Id] -> I.Subst -> Gen -> (Set Id, Gen, IdMap)+mgu v _ _ [] gen = (v, gen, emptyIdMap)+mgu v vars syms subst gen =+    (v', gen', foldl f emptyIdMap (zip vars [0..]))     where       (gen', genSyms) = genVars vars (length (fst (snd (head subst)))) gen       v' = foldl (flip S.insert) v genSyms@@ -1260,7 +1304,7 @@ groupEnv g v env grp ((x, t):map)     | M.lookup x t /= Just 1 = groupEnv g v env grp map     | otherwise =-        let (_, t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in+        let (t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in         case matchGroup (group t0) (group t1) S.empty g of           Nothing -> groupEnv g v env grp map           Just (v', g', subst) ->@@ -1271,7 +1315,7 @@ -- Specialize an environment by mapping the generated variables to one. specialize :: Env -> Env specialize (Env (v, r)) =-    Env (S.empty, foldrWithKey f M.empty r)+    Env (S.empty, M.foldrWithKey f M.empty r)     where       f x t r = M.insert x (instantiate special t) r       -- Environment mapping generated variables to one@@ -1317,7 +1361,7 @@ matchRenaming :: GenEnv -> Bool matchRenaming (gen, Env (v, e)) =     nonGrp S.empty (M.elems e) &&-    groupMatchRenaming v gen (foldrWithKey grp M.empty e)+    groupMatchRenaming v gen (M.foldrWithKey grp M.empty e)     where       nonGrp _ [] = True       nonGrp s (I x:e) =@@ -1341,7 +1385,7 @@  groupMatchElim :: Set Id -> Gen -> Map Id Group -> Group -> (Id, Int) -> Bool groupMatchElim v gen ge t (x, 1) =-    let (_, t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in+    let (t0, t1) = partition M.empty (mul t (M.singleton x (-1))) v in     case matchGroup (group t0) (group t1) S.empty gen of       Nothing -> False       Just (v', gen', subst) ->
src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs view
@@ -62,14 +62,6 @@ zt _ y = y --} --- Preserve the ability to use GHC 6.x-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700-foldrWithKey = M.foldWithKey-#else-foldrWithKey = M.foldrWithKey-#endif- -- Export iUnify and iMatch for debugging in GHCi. -- Both functions request a declaration and then two terms. -- Example: ((x y z expn)) (mul x x y) z@@ -196,7 +188,7 @@  mul :: Group -> Group -> Group mul t t' =-    foldrWithKey f t' t         -- Fold over the mappings in t+    M.foldrWithKey f t' t       -- Fold over the mappings in t     where       f x c t =                 -- Alter the mapping of           M.alter (g c) x t     -- variable x in t@@ -265,6 +257,10 @@ varId (G t) | isGroupVar t = head $ M.keys t varId _ = error "Algebra.varId: term not a variable with its sort" +isMesgVar :: Term -> Bool+isMesgVar (I _) = True+isMesgVar _ = False+ -- A list of terms are well-formed if each one has the correct -- structure and every occurrence of an identifier in a term has the -- same sort.  Variable environments are used to check the sort@@ -441,7 +437,7 @@  expnHeldBy :: Term -> Term -> Bool expnHeldBy (G t) (G t')-    | t == t' = +    | t == t' =         True expnHeldBy (G t) (G t')     | isGroupVar t =@@ -473,7 +469,7 @@           S.member (F Base [t]) knowns || ba t0 && be t1       bb _ = False       -- Buildable exponent-      be t = buildableExponent t +      be t = buildableExponent t              [ g | t <- S.elems unguessable, g <- getGroup t ]  getGroup :: Term -> [Group]@@ -495,7 +491,7 @@                   usefulKnowns ++ [ mul k k' |                                     k <- usefulKnowns,                                     k' <- filteredLevel (n - 1) ]-      usefulKnowns = L.filter (flip notElem unguessables) +      usefulKnowns = L.filter (flip notElem unguessables)                      (map (flip M.singleton 1) (M.keys t))  -- Compute the decomposition given some known terms and some unguessable@@ -616,6 +612,7 @@  instance C.Term Term where     isVar = isVar+    isMesgVar = isMesgVar     isAtom = isAtom     termsWellFormed = termsWellFormed     occursIn = occursIn@@ -803,7 +800,7 @@  groupSubst :: IdMap -> Group -> Group groupSubst subst t =-    foldrWithKey f M.empty t+    M.foldrWithKey f M.empty t     where       f x n t =           mul (expg (groupLookup subst x) n) t@@ -963,7 +960,7 @@           mkmgus (map fst t) bases (g, Subst s)  mkmgus :: [Id] -> [[Int]] -> GenSubst -> GenSubst-mkmgus vars [] (g, Subst s) = +mkmgus vars [] (g, Subst s) =     (g, Subst $ foldl f s vars)     where       f s v = M.insert v (G M.empty) s@@ -1022,9 +1019,9 @@           | otherwise -> F Exp [t0, G t1']  groupChase :: Subst -> Group -> Group-groupChase (Subst subst) t = +groupChase (Subst subst) t =     loop t-    where +    where       loop t =           case groupSubst subst t of             t' | t == t' -> t'
src/CPSA/Graph/Loader.hs view
@@ -14,7 +14,7 @@ module CPSA.Graph.Loader (Preskel, Vertex, protocol, role, env, inst,                           part, lastVertex, vertices, Node, vnode,                           strands, label, parent, seen, unrealized, shape,-                          protSrc, preskelSrc, initial, strand, pos,+                          empty, protSrc, preskelSrc, initial, strand, pos,                           prev, next, msg, out, succs, preds,                           State, loadFirst, loadNext)                           where@@ -35,7 +35,8 @@       strands :: Int,           -- Number of strands       initial :: [Vertex],      -- The initial node in each strand       unrealized :: Maybe [Vertex], -- Nodes not realized if available-      shape :: Bool,            -- Is preskel ashape?+      shape :: Bool,            -- Is preskel a shape?+      empty :: Bool,            -- Does preskel have an empty cohort?       protSrc :: SExpr Pos,     -- Source for the protocol       preskelSrc :: SExpr Pos } -- Source for this preskeleton     deriving Show@@ -252,6 +253,7 @@       let heights = map (length . trace) insts       unrealized <- loadNodes heights (assoc "unrealized" xs)       let shape = maybe False (const True) (assoc "shape" xs)+      let empty = elem "empty cohort" (qassoc "comment" xs)       let orderings = maybe [] id (assoc "precedes" xs)       pairs <- loadOrderings heights orderings       let graph = adj heights pairs@@ -270,6 +272,7 @@                              initial = initial,                              unrealized = unrealized',                              shape = shape,+                             empty = empty,                              protSrc = src p,                              preskelSrc = s }             where@@ -397,6 +400,16 @@  -- assoc key alist = --    concat [ rest | L _ (S _ head : rest) <- alist, key == head ]++qassoc :: String -> [SExpr Pos] -> [String]+qassoc key xs =+  case assoc key xs of+    Nothing -> []+    Just vals ->+      concatMap f vals+      where+        f (Q _ s) = [s]+        f _ = []  nassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe Int) nassoc key xs =
src/CPSA/Graph/Tree.hs view
@@ -53,6 +53,7 @@     where       live kids dups =           maybe True null (unrealized k) ||+          null kids && null dups && not (empty k) ||           any alive kids || any alive dups       x [] [] = 1       -- The width of a duplicate is one
src/CPSA/Lib/Algebra.hs view
@@ -27,6 +27,7 @@  class (Ord t, Show t) => Term t where     isVar :: t -> Bool          -- Is term a variable in the algebra?+    isMesgVar :: t -> Bool      -- Is term a variable of sort mesg?     isAtom :: t -> Bool       -- Is the sort of this term a base sort?      -- Does a term occur in another term?
src/CPSA/Lib/Cohort.hs view
@@ -76,6 +76,10 @@ usePruningDuringGeneralization :: Bool usePruningDuringGeneralization = False -- True +-- Minimum priority to solve+minPriority :: Int+minPriority = 1+ -- Penetrator derivable predicate and checking for unrealized skeletons.  derivable :: Algebra t p g s e c => Set t -> Set t -> t -> Bool@@ -193,14 +197,32 @@ reduce :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->           [Preskel t p g s e c] reduce mode k =-    firstJust (map (testStrand mode k u a) ss)-                  (whenRealized k) -- Skeleton is realized+    maybe (whenRealized k) id (findTest mode k u a)     where-      ss = strandVisitOrder mode (strands  k)       (a, u) = avoid k       whenRealized k =           if noGeneralization mode then [] else maximize k +prioritizeVertices :: Algebra t p g s e c => Preskel t p g s e c ->+                      [Vertex t p g s e c] -> [Vertex t p g s e c]+prioritizeVertices k vs =+     map fst $ filter keep $ L.sortBy prios $ map addPrio vs+     where+       addPrio v = (v, priority k (sid $ strand v, pos v))+       prios (_, p) (_, p') = compare p p'+       keep (_, p) = p >= minPriority++priority :: Algebra t p g s e c => Preskel t p g s e c -> Node -> Int+priority k (s, i) =+  case lookup (s, i) (kpriority k) of+    Just p -> p+    Nothing -> rpriority (role $ insts k !! s) !! i++nodeOrder :: Algebra t p g s e c => Mode ->+             Preskel t p g s e c -> [Vertex t p g s e c]+nodeOrder mode k =+    concatMap (nodeVisitOrder mode) (strandVisitOrder mode (strands  k))+ strandVisitOrder :: Mode -> [a] -> [a] strandVisitOrder mode ss =     if visitOldStrandsFirst mode then@@ -208,19 +230,19 @@     else         reverse ss     -- Visit recently added strands first (default) --- Returns the first Just value in a list or the default when there is--- none.-firstJust :: [Maybe a] -> a -> a-firstJust [] x = x-firstJust (Just x : _) _ = x-firstJust (Nothing : xs) x = firstJust xs x+nodeVisitOrder :: Algebra t p g s e c => Mode ->+                  Strand t p g s e c -> [Vertex t p g s e c]+nodeVisitOrder mode s =+    if reverseNodeOrder mode == rsearch (role $ inst s) then+        nodes s                -- Visit earliest nodes first (default)+    else+        reverse $ nodes s       -- Visit latest nodes first  -- Look for a test node in a strand-testStrand :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->-              [t] -> Set t -> Strand t p g s e c ->-              Maybe [Preskel t p g s e c]-testStrand mode k u a s =-    loop (nodeVisitOrder mode s)+findTest :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->+              [t] -> Set t -> Maybe [Preskel t p g s e c]+findTest mode k u a =+    loop (prioritizeVertices k $ nodeOrder mode k)     where       loop [] = Nothing       loop (n : nodes) =@@ -234,14 +256,6 @@                     loop nodes                 else                     Just $ testNode mode k u ts der (graphNode n) t--nodeVisitOrder :: Algebra t p g s e c => Mode ->-                  Strand t p g s e c -> [Vertex t p g s e c]-nodeVisitOrder mode s =-    if reverseNodeOrder mode == rsearch (role $ inst s) then-        nodes s                -- Visit earliest nodes first (default)-    else-        reverse $ nodes s       -- Visit latest nodes first  -- Look for a critical term that makes this node a test node. testNode :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->
src/CPSA/Lib/Displayer.hs view
@@ -87,11 +87,17 @@      (displayOptional "non-orig" (displayTerms ctx (knon k))       (displayOptional "pen-non-orig" (displayTerms ctx (kpnon k))        (displayOptional "uniq-orig" (displayTerms ctx (kunique k))-        (kcomment k ++-         (displayOperation k ctx-          (displayOptional "traces" traces rest))))))+        (displayOptional "priority" priorities+         (kcomment k +++          (displayOperation k ctx+           (displayOptional "traces" traces rest)))))))     where+      priorities = map displayPriority (kpriority k)       traces = map (L () . displayTrace ctx . trace) (insts k)++displayPriority :: (Node, Int) -> SExpr ()+displayPriority (n, p) =+    L () [displayNode n, N () p]  displayInst :: Algebra t p g s e c => c ->                Instance t p g s e c -> SExpr ()
src/CPSA/Lib/Loader.hs view
@@ -112,7 +112,8 @@       let as = L.filter (varsSeen vs . snd) a       -- Drop runiques that refer to unused variable declarations       let us = L.filter (varsSeen vs) u-      let r = mkRole name vs c ns as us comment reverseSearch+      prios <- mapM (loadRolePriority (length c)) (assoc "priority" rest)+      let r = mkRole name vs c ns as us comment prios reverseSearch       case roleWellFormed r of         Return () -> return (gen, r)         Fail msg -> fail (shows pos $ showString "Role not well formed: " msg)@@ -128,6 +129,11 @@     Return r >>= k = k r     fail s = Fail s +loadRolePriority :: Monad m => Int -> SExpr Pos -> m (Int, Int)+loadRolePriority n (L _ [N _ i, N _ p])+    | 0 <= i && i < n = return (i, p)+loadRolePriority _ x = fail (shows (annotation x) "Malformed priority")+ -- Are the vars in t a subset of ones in t. varsSeen :: Algebra t p g s e c => [t] -> t -> Bool varsSeen vs t =@@ -158,11 +164,13 @@           failwith (showString "non-orig " $ showst t " carried")                        $ all (not . carriedBy t) terms       lenCheck (Nothing, _) = return ()-      lenCheck (Just len, t) =+      lenCheck (Just len, _) | len >= length (rtrace role) =+          fail $ showString "invalid position " $ show len+      lenCheck (Just len, t) | otherwise =           case usedPos t (rtrace role) of-            Just p | p < len -> return ()+            Just p | p <= len -> return ()             Just _ -> fail $ showst t-                      $ showString " appears after length " $ show len+                      $ showString " appears after position " $ show len             Nothing -> fail msg           where             msg = "no used position for non-originating atom " ++ showst t ""@@ -171,7 +179,8 @@                        $ originates t (rtrace role)       origVarCheck v =           failwith (showString "variable " $ showst v " not acquired")-                       $ isAtom v || isJust (acquiredPos v (rtrace role))+                       $ not (isMesgVar v) ||+                         isJust (acquiredPos v (rtrace role))  failwith :: Monad m => String -> Bool -> m () failwith msg test =@@ -270,9 +279,9 @@ loadPosBaseTerm :: (Algebra t p g s e c, Monad m) => [t] ->                    SExpr Pos -> m (Maybe Int, t) loadPosBaseTerm vars x'@(L _ [N _ opos, x])-    | opos <= 0 =+    | opos < 0 =         fail (shows (annotation x')-              "Expecting a positive non-origination trace length")+              "Expecting a non-negative non-origination position")     | otherwise =         do           t <- loadBaseTerm vars x@@ -326,12 +335,13 @@ loadInsts top p kvars gen insts xs =     do       _ <- alist [] xs          -- Check syntax of xs-      loadRest top kvars p gen (reverse insts) order nr ar ur kcomment+      loadRest top kvars p gen (reverse insts) order nr ar ur pl kcomment     where       order = assoc "precedes" xs       nr = assoc "non-orig" xs       ar = assoc "pen-non-orig" xs       ur = assoc "uniq-orig" xs+      pl = assoc "priority" xs       comment = assoc "comment" xs       kcomment =           if null comment then@@ -382,8 +392,8 @@ loadRest :: (Algebra t p g s e c, Monad m) => Pos -> [t] ->             Prot t p g s e c -> g -> [Instance t p g s e c] ->             [SExpr Pos] -> [SExpr Pos] -> [SExpr Pos] -> [SExpr Pos] ->-            [SExpr ()] -> m (Preskel t p g s e c)-loadRest pos vars p gen insts orderings nr ar ur comment =+            [SExpr Pos] -> [SExpr ()] -> m (Preskel t p g s e c)+loadRest pos vars p gen insts orderings nr ar ur pl comment =     do       case null insts of         True -> fail (shows pos "No strands")@@ -394,7 +404,8 @@       ar <- loadBaseTerms vars ar       ur <- loadBaseTerms vars ur       let (nr', ar', ur') = foldl addInstOrigs (nr, ar, ur) insts-      let k = mkPreskel gen p insts o nr' ar' ur' comment+      prios <- mapM (loadPriorities heights) pl+      let k = mkPreskel gen p insts o nr' ar' ur' prios comment       case termsWellFormed $ nr' ++ ar' ++ ur' ++ kterms k of         False -> fail (shows pos "Terms in skeleton not well formed")         True -> return ()@@ -439,6 +450,14 @@           | s == 0 = Just x           | otherwise = height xs (s - 1) loadNode _ x = fail (shows (annotation x) "Malformed node")++loadPriorities :: Monad m => [Int] -> SExpr Pos -> m (Node, Int)+loadPriorities heights (L _ [x, N _ p]) =+    do+      n <- loadNode heights x+      return (n, p)+loadPriorities _ x =+    fail (shows (annotation x) "Malformed priority")  addInstOrigs :: Algebra t p g s e c => ([t], [t], [t]) ->                 Instance t p g s e c -> ([t], [t], [t])
src/CPSA/Lib/Protocol.hs view
@@ -8,10 +8,10 @@  module CPSA.Lib.Protocol (Event (..), evtTerm, evtMap, Trace, evt,     tterms, originates, originationPos, acquiredPos, usedPos, Role,-    rname, rvars, rtrace, rnon, rpnon, runique, rcomment, rsearch,-    rnorig, rpnorig, ruorig, mkRole, varSubset, varsInTerms, addVars,-    Prot, mkProt, pname, alg, pgen, roles, varsAllAtoms, pcomment,-    flow) where+    rname, rvars, rtrace, rnon, rpnon, runique, rcomment,+    rsearch, rnorig, rpnorig, ruorig, rpriority, mkRole, varSubset,+    varsInTerms, addVars, Prot, mkProt, pname, alg, pgen, roles,+    varsAllAtoms, pcomment, flow) where  import qualified Data.List as L import qualified Data.Set as S@@ -163,9 +163,13 @@       rsearch :: Bool, -- True when suggesting reverse test node search       rnorig :: [(t, Int)],     -- Nons plus origination position       rpnorig :: [(t, Int)], -- Penetrator nons plus origination position-      ruorig :: [(t, Int)] }    -- Uniques plus origination position+      ruorig :: [(t, Int)],     -- Uniques plus origination position+      rpriority :: [Int] }      -- List of all priorities     deriving Show +defaultPriority :: Int+defaultPriority = 5+ -- The empty role name is used with listener strands.  All roles in a -- protocol must have a name with more than one character. @@ -175,11 +179,11 @@ -- Create a role mkRole :: Algebra t p g s e c => String -> [t] -> Trace t p g s e c ->           [(Maybe Int, t)] -> [(Maybe Int, t)] -> [t] ->-          [SExpr ()] -> Bool -> Role t p g s e c-mkRole name vars trace non pnon unique comment rev =+          [SExpr ()] -> [(Int, Int)] -> Bool -> Role t p g s e c+mkRole name vars trace non pnon unique comment priority rev =     Role { rname = name,            rvars = L.nub vars,  -- Every variable here must-           rtrace = trace,      --  occur in the trace.+           rtrace = trace,      -- occur in the trace.            rnon = non,            rpnon = pnon,            runique = L.nub unique,@@ -187,6 +191,7 @@            rnorig = map addNonOrig $ nonNub non,            rpnorig = map addNonOrig $ nonNub pnon,            ruorig = map addUniqueOrig $ L.nub unique,+           rpriority = addDefaultPrio priority,            rsearch = rev          }     where@@ -200,10 +205,10 @@             Just p ->                 case len of                   Nothing -> (t, p)-                  Just len | len > p -> (t, len - 1)+                  Just len | len >= p -> (t, len)                            | otherwise -> error msg           where-            msg = "Protocol.mkRole: Length for atom too early in trace"+            msg = "Protocol.mkRole: Position for atom too early in trace"       -- Drop non-origination assumptions for the same atom.       nonNub nons =           reverse $ foldl f [] nons@@ -211,6 +216,13 @@             f acc non@(_, t)                 | any (\(_, t') -> t == t') acc = acc                 | otherwise = non : acc+      addDefaultPrio priority =+          map f (nats $ length trace)+          where+            f n =+              case lookup n priority of+                Nothing -> defaultPriority+                Just p -> p  -- Protocols
src/CPSA/Lib/Strand.hs view
@@ -9,9 +9,9 @@ module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener,     role, env, trace, height, listenerTerm, Sid, Node, mkPreskel,     firstSkeleton, Pair, Preskel, gen, protocol, insts, orderings,-    pov, knon, kpnon, kunique, korig, kcomment, nstrands, kvars,+    pov, knon, kpnon, kunique, korig, kpriority, kcomment, nstrands, kvars,     kterms, uniqOrig, preskelWellFormed, verbosePreskelWellFormed,-    Strand, inst, nodes, Vertex, preds, event,+    Strand, inst, sid, nodes, Vertex, strand, pos, preds, event,     graphNode, strands, vertex, Gist, gist, contract, augment,     inheritRnon, inheritRpnon, inheritRunique, addListener, Cause     (..), Direction (..), Method (..), Operation (..), operation,@@ -199,7 +199,7 @@               (g, Instance t p g s e c) mkListener gen term =     (gen'', Instance { role = mkRole "" vars [In rterm, Out rterm]-                              [] [] [] [] False,+                              [] [] [] [] [] False,                        env = env,                        trace = [In term, Out term],                        height = 2 })@@ -371,6 +371,7 @@       knon :: ![t],             -- A list of atoms       kpnon :: ![t],            -- A list of atoms       kunique :: ![t],          -- A list of atoms+      kpriority :: [(Node, Int)], -- Override node priority       kcomment :: [SExpr ()],   -- Comments from the input       korig :: ![(t, [Node])],  -- This is an association list with a                                 -- pair for each element of kunique.@@ -433,12 +434,12 @@ -- must be consumed by firstSkeleton. mkPreskel :: Algebra t p g s e c => g -> Prot t p g s e c ->              [Instance t p g s e c] -> [Pair] -> [t] -> [t] -> [t] ->-             [SExpr ()] -> Preskel t p g s e c-mkPreskel gen protocol insts orderings non pnon unique comment =+             [(Node, Int)] -> [SExpr ()] -> Preskel t p g s e c+mkPreskel gen protocol insts orderings non pnon unique prio comment =     k { kcomment = comment }     where       k = newPreskel gen protocol insts orderings non pnon-          unique New prob Nothing+          unique prio New prob Nothing       prob = strandids k        -- Fixed point on k is okay.  -- Strand functions@@ -466,9 +467,9 @@ -- within this module. newPreskel :: Algebra t p g s e c => g -> Prot t p g s e c ->              [Instance t p g s e c] -> [Pair] -> [t] -> [t] -> [t] ->-             Operation t p g s e c -> [Sid] ->+             [(Node, Int)] -> Operation t p g s e c -> [Sid] ->              Maybe (Preskel t p g s e c) -> Preskel t p g s e c-newPreskel gen protocol insts orderings non pnon unique oper prob pov =+newPreskel gen protocol insts orderings non pnon unique prio oper prob pov =     let orderings' = L.nub orderings         unique' = L.nub unique         g = graph trace height insts orderings'@@ -485,6 +486,7 @@                       knon = L.nub non,                       kpnon = L.nub pnon,                       kunique = unique',+                      kpriority = prio,                       kcomment = [],                       korig = orig,                       tc = map graphPair tc,@@ -869,7 +871,8 @@       let unique' = map (substitute subst) (kunique k)       let operation' = substOper subst (operation k)       let k' = newPreskel gen' (protocol k) insts'-               (orderings k) non' pnon' unique' operation' (prob k) (pov k)+               (orderings k) non' pnon' unique' (kpriority k)+               operation' (prob k) (pov k)       k' <- wellFormedPreskel k'       case not validate || validateMappingSubst k0 phi subst k' of         True -> return (k0, k', n, phi, compose subst hsubst)@@ -926,6 +929,7 @@               (knon k)               (kpnon k)               (kunique k)+              (updatePriority perm (kpriority k))               (operation k)               (updateProb perm (prob k))               (pov k)@@ -963,6 +967,10 @@ updateProb mapping prob =     map (mapping !!) prob +updatePriority :: [Sid] -> [(Node, Int)] -> [(Node, Int)]+updatePriority mapping kpriority =+    map (\(n, i) -> (permuteNode mapping n, i)) kpriority+ -- Purge a strand.  Used by thinning.  The same as pruning except -- edges to the purged strand are forwarded as a first step. purge :: Algebra t p g s e c => PRS t p g s e c ->@@ -982,6 +990,7 @@               (knon k)               (kpnon k)               (kunique k)+              (updatePriority perm (kpriority k))               (operation k)               (updateProb perm (prob k))               (pov k)@@ -1072,6 +1081,7 @@                   (knon k)                   (kpnon k)                   (kunique k)+                  (kpriority k)                   (operation k)                   (prob k)                   (pov k)@@ -1306,6 +1316,7 @@             e <- ges             (gen, env) <- thinStrandCheck k s e             [ prs' | prs <- ksubst False prs (gen, substitution env),+                     prs <- reduce prs,                      prs' <- purge prs s s',                      prs'' <- purge prs s' s,                      gist (skel prs') == gist (skel prs'')]@@ -1380,6 +1391,7 @@       let k = skel prs       (gen, env) <- thinManyMatch k ps       [ prs' | prs <- ksubst False prs (gen, substitution env),+               prs <- reduce prs,                prs' <- compressMany prs ps,                prs'' <- compressMany prs (swap ps),                gist (skel prs') == gist (skel prs'')]@@ -1446,6 +1458,7 @@                   (knon k)                   (kpnon k)                   (kunique k)+                  (kpriority k)                   (operation k)                   (prob k)                   (pov k)@@ -1546,7 +1559,8 @@       let pnon' = inheritRpnon inst ++ (kpnon k)       let unique' = inheritRunique inst ++ (kunique k)       let k' = newPreskel (gen k) (protocol k) insts'-           orderings' non' pnon' unique' (operation k) (prob k) (pov k)+           orderings' non' pnon' unique' (kpriority k)+           (operation k) (prob k) (pov k)       k' <- wellFormedPreskel k'       return (k0, k', n, phi, hsubst) @@ -1637,7 +1651,8 @@       homomorphismFilter prs     where       k' = newPreskel gen' (protocol k) insts' orderings' (knon k)-           (kpnon k) (kunique k) (AddedListener t cause) (prob k) (pov k)+           (kpnon k) (kunique k) (kpriority k)+           (AddedListener t cause) (prob k) (pov k)       (gen', inst) = mkListener (gen k) t       insts' = insts k ++ [inst]       pair = ((length (insts k), 1), n)@@ -1785,7 +1800,7 @@                   [Sid] -> Preskel t p g s e c deleteNodeRest k gen n insts' orderings prob =     newPreskel gen (protocol k) insts' orderings non' pnon' unique'-                   (Generalized (Deleted n)) prob (pov k)+                   prio' (Generalized (Deleted n)) prob (pov k)     where       -- Drop nons that aren't mentioned anywhere       non' = filter mentionedIn (knon k)@@ -1795,6 +1810,10 @@       -- Drop uniques that aren't held anywhere       unique' = filter heldIn (kunique k)       heldIn t = any (heldBy t) terms+      -- Drop unused priorities+      prio' = filter within (kpriority k)+      within ((s, i), _) =+        s < fst n || s == fst n && i < snd n  -- Node ordering weakening @@ -1824,7 +1843,7 @@     addIdentity k'     where       k' = newPreskel (gen k) (protocol k) (insts k)-           orderings (knon k) (kpnon k) (kunique k)+           orderings (knon k) (kpnon k) (kunique k) (kpriority k)            (Generalized (Weakened p)) (prob k) (pov k)  -- Origination assumption forgetting@@ -1982,10 +2001,10 @@ changeLocations k env gen t locs =     [addIdentity k0, addIdentity k1]     where-      k0 = newPreskel gen' (protocol k) insts' (orderings k)-           non pnon unique0 (Generalized (Separated t)) (prob k) (pov k)-      k1 = newPreskel gen' (protocol k) insts' (orderings k)-           non pnon unique1 (Generalized (Separated t)) (prob k) (pov k)+      k0 = newPreskel gen' (protocol k) insts' (orderings k) non pnon unique0+           (kpriority k) (Generalized (Separated t)) (prob k) (pov k)+      k1 = newPreskel gen' (protocol k) insts' (orderings k) non pnon unique1+           (kpriority k) (Generalized (Separated t)) (prob k) (pov k)       (gen', insts') = changeStrands locs t gen (strands k)       non = knon k ++ map (instantiate env) (knon k)       pnon = kpnon k ++ map (instantiate env) (kpnon k)
src/CPSA/Pretty/Main.hs view
@@ -97,14 +97,14 @@             do               msg <- usage options ["Bad option combination\n"]               abort msg-          else             +          else             loop flags $ params { prefix = False }       loop (Json : flags) params =           if not (prefix params) then             do               msg <- usage options ["Bad option combination\n"]               abort msg-          else             +          else             loop flags $ params { json = True }       loop (Margin value : flags) params =           case readDec value of
src/CPSA/SimpleDiffieHellman/Algebra.hs view
@@ -15,7 +15,7 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE MultiParamTypeClasses, CPP #-}+{-# LANGUAGE MultiParamTypeClasses #-}  module CPSA.SimpleDiffieHellman.Algebra (name, origin) where @@ -29,14 +29,6 @@ import qualified CPSA.Lib.CPSA as C import CPSA.Lib.CPSA (SExpr(..), Pos, annotation) --- Preserve the ability to use GHC 6.x-foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b-#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700-foldrWithKey = M.foldWithKey-#else-foldrWithKey = M.foldrWithKey-#endif- name :: String name = "diffie-hellman" @@ -225,6 +217,10 @@ varId (F Expn [I x]) = x varId _ = error "Algebra.varId: term not a variable with its sort" +isMesgVar :: Term -> Bool+isMesgVar (I _) = True+isMesgVar _ = False+ -- A list of terms are well-formed if each one has the correct -- structure and every occurrence of an identifier in a term has the -- same sort.  Variable environments are used to check the sort@@ -578,6 +574,7 @@  instance C.Term Term where     isVar = isVar+    isMesgVar = isMesgVar     isAtom = isAtom     termsWellFormed = termsWellFormed     occursIn = occursIn@@ -945,7 +942,7 @@ identityEnvFor (Env r) ts =     all (allId $ flip S.notMember dom) ts     where-      dom = foldrWithKey f S.empty r -- The domain of r+      dom = M.foldrWithKey f S.empty r -- The domain of r       f x (I y) dom           | x == y = dom        -- Ignore trivial bindings           | otherwise = S.insert x dom
src/prover9.pl view
@@ -111,15 +111,15 @@  %% Quantifiers forall and exists -%% This code simply drops the sort declarations.- quantifier(_, [[], Body], Pretty) :- 	!, 	form_to_pretty(Body, Pretty). quantifier(Kind, [Decls, Body], Pretty) :- 	quantifier_op(Kind, Op),-	decls(Decls, Vars),-	quantifier_rest(Op, Vars, Body, Pretties),+	decls(Decls, SVars),+	quantifier_preds(SVars, Vars, Preds),+	quantifier_body(Kind, Preds, Body, SBody),+	quantifier_rest(Op, Vars, SBody, Pretties), 	pp:blo(2, Pretties, Pretty).  quantifier_op(forall, Pretty) :-@@ -129,19 +129,44 @@  %% Collect vars in declarations. -decls(Decls, Vars) :--	decls(Decls, Vars, []).+decls(Decls, SortedVars) :-+	decls(Decls, SortedVars, []). -decls([], Vars, Vars).-decls([Decl|Decls], Vars, End) :--	decl(Decl, Vars, Middle),+decls([], SVars, SVars).+decls([Decl|Decls], SVars, End) :-+	decl(Decl, _, SVars, Middle), 	decls(Decls, Middle, End). -decl([_], Vars, Vars).-decl([Var|Decl], [Var|Vars], End) :-+decl([Sort], Sort, SVars, SVars) :-+	atom(Sort).+decl([Var|Decl], Sort, [(Var,Sort)|SVars], End) :- 	atom(Var),-	decl(Decl, Vars, End).+	decl(Decl, Sort, SVars, End). +quantifier_preds([], [], []).+quantifier_preds([(Var,mesg)|SVars], [Var|Vars], Preds) :-+        !,+        quantifier_preds(SVars, Vars, Preds).+quantifier_preds([(Var,Sort)|SVars], [Var|Vars], [[Sort, Var]|Preds]) :-+        quantifier_preds(SVars, Vars, Preds).++quantifier_body(_, [], Body, Body) :-+        !.+quantifier_body(exists, Preds, [and|Forms], [and|Conj]) :-+        !,+        append(Preds, Forms, Conj).+quantifier_body(exists, Preds, Body, [and|Conj]) :-+        append(Preds, [Body], Conj).+quantifier_body(forall, Preds, [implies, [and|Forms], Body],+		[implies, [and|Conj], Body]) :-+        !,+        append(Preds, Forms, Conj).+quantifier_body(forall, Preds, [implies, Form, Body],+		[implies, [and|Conj], Body]) :-+        !,+        append(Preds, [Form], Conj).+quantifier_body(forall, Preds, Body, [implies, [and|Preds], Body]).+ quantifier_rest(_, [], Body, [Left, Brk, Pretty, Right]) :- 	pp:atm('(', Left), 	pp:brk(0, Brk),@@ -178,16 +203,11 @@ 	load_term(Term, Internal), 	term_pp(Internal, Pretty). -%% Load a term using CPSA's parsing rules for terms.  Also, convert-%% variables into uppercase atoms, and constants into lowercase atoms.+%% Load a term using CPSA's parsing rules for terms.  load_term(Term, Internal) :- 	atom(Term),-	upcase_symbol(Term, Internal).-load_term(Term, Internal) :--	string(Term),-	string_to_atom(Term, Atom),-	downcase_symbol(Atom, Internal).+	load_atom(Term, Internal). load_term(Term, Term) :- 	integer(Term), 	Term >= 0.@@ -208,28 +228,33 @@ 	atom(Term), 	load_terms(Terms, Internals). -upcase_symbol(Atom, Symbol) :--	atom_chars(Atom, Chars),-	upcase_parts(Chars, Parts),-	atom_chars(Symbol, Parts).--upcase_parts([First|Rest], [Lead|Tail]) :--	upcase_atom(First, Lead),-	symbol_parts(Rest, Tail).+%% Convert variables into uppercase atoms, and constants into+%% lowercase atoms. -downcase_symbol(Atom, Symbol) :--	atom_chars(Atom, Chars),-	downcase_parts(Chars, Parts),+load_atom('""', []) :- % The name for a listener is the null constant.+        !.+load_atom(Atom, Symbol) :-+        atom_chars(Atom, Chars),+	parts(Chars, Parts), 	atom_chars(Symbol, Parts). -%% The null constant is used for the name of the listener role.+parts(['"'|Chars], Parts) :-+        !,+        downcase_parts(Chars, Parts).+parts(Chars, Parts) :-+        upcase_parts(Chars, Parts). -downcase_parts([], ['"', '"']). downcase_parts([First|Rest], [Lead|Tail]) :- 	downcase_atom(First, Lead), 	symbol_parts(Rest, Tail). +upcase_parts([First|Rest], [Lead|Tail]) :-+	upcase_atom(First, Lead),+	symbol_parts(Rest, Tail).+ symbol_parts([], []).+symbol_parts(['"'], []) :-+        !. symbol_parts(['-'|Rest], ['_'|Tail]) :- 	!, 	symbol_parts(Rest, Tail).
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from DH_hack.scm") (comment "Strand count bounded at 15")
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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from blanchet.scm")  (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from completeness-test.scm")  (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from deorig_simple.scm")  (defprotocol deorig-simple basic
tst/dh_cert.tst view
@@ -1,6 +1,6 @@ (herald "Diffie-Hellman with Certificate" (algebra diffie-hellman)) -(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from dh_cert.scm")  (defprotocol dh-cert diffie-hellman
tst/dhke.tst view
@@ -1,6 +1,6 @@ (herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman)) -(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from dhke.scm")  (defprotocol dhke diffie-hellman
tst/dy.tst view
@@ -1,6 +1,6 @@ (herald "Example 1.3 from 1983 Dolev-Yao Paper") -(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from epmo_acctnum-key-hash.scm")  (defprotocol epmo_acctnum basic
tst/epmo_acctnum.tst view

file too large to diff

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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from ffgg.scm")  (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from hashtest.scm")  (defprotocol hashtest basic
tst/incompleteness_example.tst view
@@ -1,8 +1,8 @@ (herald incompleteness-example   (comment "Shows a shape not found by CPSA")) -(comment "CPSA 2.2.11")-(comment "All input read from incompleteness-example.scm")+(comment "CPSA 2.3.0")+(comment "All input read from incompleteness_example.scm")  (defprotocol incompleteness-example basic   (defrole init
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from isoreject.scm")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from kelly1.scm")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from kerberos.scm")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from mass.lsp")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from mass2.lsp")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from print.scm")  (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from targetterms2.scm")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from targetterms6.scm")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from timestamping.scm")  (defprotocol timestamping-service basic
tst/tor.tst view
@@ -1,7 +1,7 @@ (herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman)   (comment "Achieves unilateral authentication")) -(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from tor.scm")  (defprotocol tor diffie-hellman
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from uncarried_keys.scm")  (defprotocol uncarried-keys basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from wide-mouth-frog.lsp")  (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from wonthull.scm")  (defprotocol wonthull basic
tst/wonthull2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from wonthull2.scm")  (defprotocol wonthull2 basic
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.11")+(comment "CPSA 2.3.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.2.11")+(comment "CPSA 2.3.0") (comment "All input read from woolam.scm")  (defprotocol woolam basic
tst/yahalom-6.3.6.tst view
@@ -2,10 +2,12 @@   (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)) -(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from yahalom-6.3.6.scm")+(comment "Strand count bounded at 15")  (defprotocol yahalom basic   (defrole init
tst/yahalom.tst view
@@ -1,7 +1,8 @@-(herald "Yahalom Protocol Without Forwarding")+(herald "Yahalom Protocol Without Forwarding" (bound 15)) -(comment "CPSA 2.2.11")+(comment "CPSA 2.3.0") (comment "All input read from yahalom.scm")+(comment "Strand count bounded at 15")  (defprotocol yahalom basic   (defrole init