packages feed

cpsa 2.5.2 → 2.5.3

raw patch · 86 files changed

+184/−138 lines, 86 files

Files

ChangeLog view
@@ -1,3 +1,24 @@+2015-08-21  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/*/*.h:  Removed leading tabs.++	* src/CPSA/Annotations/Formulas.hs (EitherS): Made EitherS an+	instance of Applicative.++2015-08-07  John D. Ramsdell  <ramsdell@mitre.org>++	* doc/cpsagoals.tex: Corrected the definition of satisfaction.++2015-08-06  John D. Ramsdell  <ramsdell@mitre.org>++	* doc/cpsagoals.tex: Made minor fixes due to another review.  Also+	fixed the definition of a characteristic skeleton.++2015-08-04  John D. Ramsdell  <ramsdell@mitre.org>++	* doc/cpsaprimer.tex (section{Macros}\label{sec:macros}):  Added+	text describing splicing.+ 2015-07-27  John D. Ramsdell  <ramsdell@mitre.org>  	* README: Updated to reflect that Haskell Platform should always
NEWS view
@@ -1,5 +1,12 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.5.3++** Corrected errors in the documentation on security goals.++** Enabled compilation using GHC 7.10 by making some monads+   applicative.+ * Changes in version 2.5.2  ** Added an option to purge traces in skeletons while graphing
README view
@@ -1,8 +1,9 @@ CPSA: A Crptographic Protocol Shapes Analyzer  This program has been built and tested using Haskell Platform.-It is available from <http://haskell.org> or from-an operating system specific source.+It is available from <http://haskell.org> or from an operating+system specific source.  The name of the Linux package is usually+haskell-platform.  $ cabal update $ cabal install cpsa
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.5.2+Version:		2.5.3 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3@@ -92,7 +92,7 @@   tst/neuman-stubblebine.tst tst/no_contraction.scm   tst/no_contraction.tst tst/nonaug-prune.scm tst/nonaug-prune.tst   tst/non_transforming.scm tst/non_transforming.tst tst/nsl3.scm-  tst/nsl3.tst tst/nsl4cm1.lsp tst/nsl4cm1.tst tst/nsl4.lisp+  tst/nsl3.tst tst/nsl4cm1.lisp tst/nsl4.lisp   tst/nsl4resp2.lisp tst/nsl5i.lisp tst/nsl5.lisp tst/ns-l.scm   tst/nslsk.scm tst/nslsk.tst tst/ns-l.tst tst/ns.scm tst/ns.tst   tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst
doc/cpsadesign.pdf view

binary file changed (275415 → 275413 bytes)

doc/cpsagoals.pdf view

binary file changed (194752 → 194913 bytes)

doc/cpsagoals.tex view
@@ -174,7 +174,7 @@ existentially quantified conjunction of atomic formulas, but in general, the conclusion is a disjunction of existentially quantified conjunctions of atomic formulas.  In what follows, \sym{(false)} is a-synonym for \sym{(or)}.+synonym for the empty disjunction, \sym{(or)}.  \begin{center}\scshape   \begin{tabular}{rcl}@@ -215,18 +215,19 @@ contains three tokens, \texttt{p}, a string that names a role, and a string that names a role variable.  For role~$r$, there is role parameter predicate for each variable declared by~$r$.  Thus-\verb|(p "init" 2 "n1" z0 n1)| is an atomic formula using the role+\verb|(p "init" "n1" z0 n1)| is an atomic formula using the role parameter predicate for parameter \text{n1} in the \texttt{init} role of the protocol.  The empty string names the listener role of a protocol.  The role has the variable \texttt{x} of sort \texttt{mesg} as its only role-variable.  There are two positions in the listener role.+variable.  There are two positions in the listener role.  Its trace is+\texttt{(trace (recv x) (send x))}.  When a variable of sort \sym{node} occurs in a formula, its position must be specified using a role position formula.  When an algebra-variable occurs in formula, its association with the parameter of some-role must be specified using a role parameter formula.+variable occurs in a formula, its association with the parameter of+some role must be specified using a role parameter formula.  \begin{table} \begin{center}@@ -283,8 +284,8 @@ Our aim now is to specify how to decide if a security goal is true in all possible executions of a protocol.  A skeleton defines a set of executions that contain the skeleton's structure.  We say a skeleton-\emph{satisfies} a formula if the formula is true in all executions-that contain the skeleton's structure.  To decide if a skeleton+\emph{satisfies} a formula if the skeleton contains all of the+structure specified by the formula.  To decide if a skeleton satisfies a formula, we decide if it satisfies each of its atomic formulas, and combine the results using the rules of first-order logic.@@ -373,12 +374,13 @@  When {\cpsa} performs a shape analysis, every shape it generates refines the input skeleton.  Skeleton refinement is defined-in~\cite[Section~6]{cpsaprimer09}, but roughly speaking, skeleton~$A$-refines skeleton~$B$ if~$A$ contains the structure of skeleton~$B$.+in~\cite[Section~6]{cpsaprimer09}.  The definition makes precise the+notion of structure containment, as skeleton~$A$ refines skeleton~$B$+if and only if~$A$ contains the structure of skeleton~$B$.  The skeleton~$k_0$ extracted from the antecedent of a security goal-has the property that every skeleton than refines~$k_0$ satisfies the-antecedent.  A skeleton with this property is called the+has the property that a skeleton refines~$k_0$ if and only if it+satisfies the antecedent.  A skeleton with this property is called the \emph{characteristic skeleton} of the antecedent.  Given a goal~\(\Phi\), consider a shape analysis starting from the@@ -388,8 +390,9 @@ in~$k_0$.  {\cpsa} tells us that each execution is in the executions that contain the structure of some~$k_i$.  Furthermore, because~$k_0$ is a characteristic skeleton, each~$k_i$ satisfies the antecedent-of~$\Phi$.  Therefore,~$\Phi$ is true in all executions of the-protocol and maximally informative.+of~$\Phi$.  Executions that do not contain the structure in~$k_0$ do+not satisfy the antecedent.  Therefore,~$\Phi$ is true in all+executions of the protocol and maximally informative.  \section{Examples}\label{sec:examples}
doc/cpsaintroslides.pdf view

binary file changed (93179 → 93179 bytes)

doc/cpsaoverview.pdf view

binary file changed (129006 → 129008 bytes)

doc/cpsaprimer.pdf view

binary file changed (276712 → 277023 bytes)

doc/cpsaprimer.tex view
@@ -1132,6 +1132,10 @@ takes precedence. The {\cpsa} program omits macro definitions from its output. +After expanding a list, elements of the list of the form+\verb|(^ |$\cdots$\verb| )| are spliced into the output.  Thus+\verb|(a ^(b c) d)| becomes \verb|(a b c d)| after macro expansion.+ \section{Includes}\label{sec:include}  While performing macro expansion, {\cpsa} includes other source files
doc/cpsaspec.pdf view

binary file changed (388029 → 388032 bytes)

doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.5.2}+\newcommand{\version}{2.5.3} \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
@@ -85,7 +85,7 @@             SExpr Pos -> m (g, Role t) loadRole gen (L pos (S _ "defrole" :                      S _ name :-	             L _ (S _ "vars" : vars) :+                     L _ (S _ "vars" : vars) :                      L _ (S _ "trace" : _ : c) :                      rest)) =     do
src/CPSA/Annotations/Formulas.hs view
@@ -11,6 +11,7 @@     displayFormula) where  import Control.Monad+import Control.Applicative import qualified Data.Set as S import CPSA.Lib.CPSA @@ -177,6 +178,15 @@ data EitherS a     = RightS a     | LeftS String++instance Functor (EitherS) where+    fmap _ (LeftS x) = LeftS x+    fmap f (RightS y) = RightS (f y)++instance Applicative (EitherS) where+    pure          = RightS+    LeftS e <*> _ = LeftS e+    RightS f <*> r = fmap f r  instance Monad EitherS where     return = RightS
src/CPSA/Graph/Loader.hs view
@@ -200,7 +200,7 @@  loadRole :: Monad m => Pos -> [SExpr Pos] -> m (String, Trace) loadRole _ (S _ name :-	    L _ (S _ "vars" : _) :+            L _ (S _ "vars" : _) :             L _ (S _ "trace" : trace) : _) = return (name, trace) loadRole pos _ = fail (shows pos "Malformed role")
src/CPSA/Lib/Displayer.hs view
@@ -141,11 +141,11 @@           displayCause (L () (S () "contracted" : substitution)) cause       Displaced s s' role height cause ->           displayCause-	  (L () [S () "displaced", N () s, N () s', S () role, N () height])+          (L () [S () "displaced", N () s, N () s', S () role, N () height])           cause       AddedStrand role height cause ->           displayCause-	  (L () [S () "added-strand", S () role, N () height]) cause+          (L () [S () "added-strand", S () role, N () height]) cause       AddedListener t cause ->           displayCause (L () [S () "added-listener", displayOpTerm ctx t]) cause       Generalized method ->
src/CPSA/Lib/Loader.hs view
@@ -97,7 +97,7 @@ loadRole :: (Algebra t p g s e c, Monad m) => g -> Pos ->             [SExpr Pos] -> m (g, Role t) loadRole gen pos (S _ name :-	          L _ (S _ "vars" : vars) :+                  L _ (S _ "vars" : vars) :                   L _ (S _ "trace" : evt : c) :                   rest) =     do
src/CPSA/Parameters/Flow.hs view
@@ -38,7 +38,7 @@            SExpr Pos -> m (SExpr ()) mapRole gen (L _ (S _ "defrole" :                   S _ name :-	          L _ (S _ "vars" : vars) :+                  L _ (S _ "vars" : vars) :                   L _ (S _ "trace" : trace) :                   rest)) =     do@@ -48,7 +48,7 @@       trace <- mapM stripEvt trace       return (L () (S () "defrole" :                     S () name :-	            L () (S () "vars" : map strip vars) :+                    L () (S () "vars" : map strip vars) :                     L () (S () "trace" : trace) :                     rest')) mapRole _ x = return (strip x)
src/CPSA/SAS/SAS.hs view
@@ -134,7 +134,7 @@             SExpr Pos -> m (g, Role t c) loadRole gen (L _ (S _ "defrole" :                      S _ name :-	             L _ (S _ "vars" : vars) :+                     L _ (S _ "vars" : vars) :                      L _ (S _ "trace" : _ : _) :                      _)) =     do
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from blanchet.scm")  (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from completeness-test.scm")  (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from denning-sacco.scm")  (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from deorig_simple.scm")  (defprotocol deorig-simple basic
tst/dy.tst view
@@ -1,6 +1,6 @@ (herald "Example 1.3 from 1983 Dolev-Yao Paper") -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from epmo_acctnum-key-hash.scm")  (defprotocol epmo_acctnum basic
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol"   (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from ffgg.scm")  (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from fragile_pruning.scm")  (defprotocol fragile_pruning basic
tst/goals.tst view
@@ -1,6 +1,6 @@ (herald goals) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from goals.scm")  (defprotocol ns basic
tst/hashtest-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from hashtest.scm")  (defprotocol hashtest basic
tst/incompleteness_example.tst view
@@ -1,7 +1,7 @@ (herald incompleteness-example   (comment "Shows a shape not found by CPSA")) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from incompleteness_example.scm")  (defprotocol incompleteness-example basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from isoreject.scm")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from kelly1.scm")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from kerberos.scm")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from mass.lsp")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from mass2.lsp")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from neuman-stubblebine.scm")  (defprotocol neuman-stubblebine basic
tst/no_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from no_contraction.scm")  (defprotocol no-contraction basic
tst/non_transforming.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from non_transforming.scm")  (defprotocol non_transforming basic
tst/nonaug-prune.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from nsl3.scm")  (defprotocol nsl3 basic
+ tst/nsl4cm1.lisp view
@@ -0,0 +1,49 @@+(herald "Four Party Needham-Schroeder-Lowe Protocol")++(defprotocol nsl4cm basic+   (defrole init+      (vars (a b c d name) (na nb nc nd text))+      (trace+         (send (enc a c d na (pubk b)))+	 (recv (enc b c d na nb nc nd (pubk a)))+	 (send (enc nb nc nd (pubk b)))))+   (defrole resp1+      (vars (a b c d name) (na nb nc nd text))+      (trace+         (recv (enc a c d na (pubk b)))+	 (send (enc a b d na nb (pubk c)))+	 (recv (enc nb nc nd (pubk b)))+	 (send (enc nc nd (pubk c)))))+   (defrole resp2+      (vars (a b c d name) (na nb nc nd text))+      (trace+         (recv (enc a b d na nb (pubk c)))+	 (send (enc a b c na nb nc (pubk d)))+	 (recv (enc nc nd (pubk c)))+	 (send (enc nd (pubk d)))))+   (defrole resp3+      (vars (a b c d name) (na nb nc nd text))+      (trace+         (recv (enc a b c na nb nc (pubk d)))+	 (send (enc b c d na nb nc nd (pubk a)))+	 (recv (enc nd (pubk d))))))++(defskeleton nsl4cm (vars (a b c d name) (na text))+  (defstrand init 3 (a a) (b b) (c c) (d d) (na na))+   (non-orig (privk a) (privk b) (privk c) (privk d))+   (uniq-orig na))++(comment (defskeleton nsl4cm (vars (a b c d name) (nb text))+   (defstrand resp1 4 (a a) (b b) (c c) (d d) (nb nb))+   (non-orig (privk a) (privk b) (privk c) (privk d))+   (uniq-orig nb))++(defskeleton nsl4cm (vars (a b c d name) (nc text))+   (defstrand resp2 4 (a a) (b b) (c c) (d d) (nc nc))+   (non-orig (privk a) (privk b) (privk c) (privk d))+   (uniq-orig nc))++(defskeleton nsl4cm (vars (a b c d name) (nd text))+   (defstrand resp3 3 (a a) (b b) (c c) (d d) (nd nd))+   (non-orig (privk a) (privk b) (privk c) (privk d))+   (uniq-orig nd)))
− tst/nsl4cm1.lsp 
@@ -1,49 +0,0 @@-(herald "Four Party Needham-Schroeder-Lowe Protocol")--(defprotocol nsl4cm basic-   (defrole init-      (vars (a b c d name) (na nb nc nd text))-      (trace-         (send (enc a c d na (pubk b)))-	 (recv (enc b c d na nb nc nd (pubk a)))-	 (send (enc nb nc nd (pubk b)))))-   (defrole resp1-      (vars (a b c d name) (na nb nc nd text))-      (trace-         (recv (enc a c d na (pubk b)))-	 (send (enc a b d na nb (pubk c)))-	 (recv (enc nb nc nd (pubk b)))-	 (send (enc nc nd (pubk c)))))-   (defrole resp2-      (vars (a b c d name) (na nb nc nd text))-      (trace-         (recv (enc a b d na nb (pubk c)))-	 (send (enc a b c na nb nc (pubk d)))-	 (recv (enc nc nd (pubk c)))-	 (send (enc nd (pubk d)))))-   (defrole resp3-      (vars (a b c d name) (na nb nc nd text))-      (trace-         (recv (enc a b c na nb nc (pubk d)))-	 (send (enc b c d na nb nc nd (pubk a)))-	 (recv (enc nd (pubk d))))))--(defskeleton nsl4cm (vars (a b c d name) (na text))-  (defstrand init 3 (a a) (b b) (c c) (d d) (na na))-   (non-orig (privk a) (privk b) (privk c) (privk d))-   (uniq-orig na))--(comment (defskeleton nsl4cm (vars (a b c d name) (nb text))-   (defstrand resp1 4 (a a) (b b) (c c) (d d) (nb nb))-   (non-orig (privk a) (privk b) (privk c) (privk d))-   (uniq-orig nb))--(defskeleton nsl4cm (vars (a b c d name) (nc text))-   (defstrand resp2 4 (a a) (b b) (c c) (d d) (nc nc))-   (non-orig (privk a) (privk b) (privk c) (privk d))-   (uniq-orig nc))--(defskeleton nsl4cm (vars (a b c d name) (nd text))-   (defstrand resp3 3 (a a) (b b) (c c) (d d) (nd nd))-   (non-orig (privk a) (privk b) (privk c) (privk d))-   (uniq-orig nd)))
− tst/nsl4cm1.tst

file too large to diff

tst/nslsk.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from print.scm")  (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from targetterms2.scm")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from targetterms6.scm")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from targetterms8.scm")  (defprotocol targetterms8 basic
tst/timestamping.tst view
@@ -1,6 +1,6 @@ (herald timestamping-service) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from timestamping.scm")  (defprotocol timestamping-service basic
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from uncarried_keys.scm")  (defprotocol uncarried-keys basic
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from unilateral.scm")  (defprotocol unilateral basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from wide-mouth-frog.lsp")  (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,6 +1,6 @@ (herald wonthull (bound 9)) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from wonthull.scm") (comment "Strand count bounded at 9")
tst/wonthull2.tst view
@@ -1,6 +1,6 @@ (herald wonthull2 (bound 9)) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from wonthull2.scm") (comment "Strand count bounded at 9")
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (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.5.2")+(comment "CPSA 2.5.3") (comment "All input read from woolam.scm")  (defprotocol woolam basic
tst/yahalom-6.3.6.tst view
@@ -5,7 +5,7 @@   (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")   (bound 15)) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from yahalom-6.3.6.scm") (comment "Strand count bounded at 15")
tst/yahalom.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding" (bound 15)) -(comment "CPSA 2.5.2")+(comment "CPSA 2.5.3") (comment "All input read from yahalom.scm") (comment "Strand count bounded at 15")