packages feed

cpsa 2.5.1 → 2.5.2

raw patch · 79 files changed

+141/−129 lines, 79 files

Files

ChangeLog view
@@ -1,3 +1,16 @@+2015-07-27  John D. Ramsdell  <ramsdell@mitre.org>++	* README: Updated to reflect that Haskell Platform should always+	be used.++	* cpsa.cabal (Version): Tagged as version 2.5.2++2015-07-09  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Graph/ExpandedView.hs (purgeTraces): Added -p flag to+	the graph program.  When present, the graph program purges traces+	in skeletons it prints.+ 2015-07-08  John D. Ramsdell  <ramsdell@mitre.org>  	* cpsa.cabal (Version): Tagged as version 2.5.1
NEWS view
@@ -1,5 +1,15 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.5.2++** Added an option to purge traces in skeletons while graphing+   In cpsagraph, supplying the --purge-traces option causes skeletons+   to be printed without their traces.  This saves on clutter when+   traces are large and unused.++** Updated README to reflect that Haskell Platform should always be used.+   It's available everywhere now.+ * Changes in version 2.5.1  ** CPSA Goals document updated
README view
@@ -1,29 +1,16 @@ CPSA: A Crptographic Protocol Shapes Analyzer -This program has been built and tested using the Glasgow Haskell-Compiler (GHC), which is available for Linux, Macs, and Windows.  If-possible, install Haskell Platform from <http://haskell.org> or from-an operating system specific source.  If the Internet is available,-install CPSA with:+This program has been built and tested using Haskell Platform.+It is available from <http://haskell.org> or from+an operating system specific source. +$ cabal update $ cabal install cpsa--Find the documentation directory by typing "cpsa -h" in a command-shell, and view index.html in a browser.--Cabal installation options are listed with:--$ cabal help install+: Documentation and samples are in the directory given by+$ cpsa -h  INSTALLING FROM A TARBALL -If Haskell Platform is not available, install GHC and its parallel-library, and then follow one of these operating system specific-instructions.  For example, to install on older Debian-based systems,-ones that have only GHC 6, try:--$ sudo apt-get install ghc6 libghc6-parallel-dev- QUICK START (Linux)  : To build and install CPSA type:@@ -62,10 +49,10 @@  QUICK START (Windows) -Unless you are using Cygwin or MinGW, the cabal install above is your-best bet.  The software has been tested on a Windows system on which-neither MinGW or Cygwin has been installed.  Install GHC and then run-the "setup.bat" batch file with administrator privileges.+With Cygwin or MinGW, the installation is similar to the Linux+install.  The software has been tested on a Windows system on which+neither MinGW or Cygwin has been installed.  Install Haskell Platform+and then run the "setup.bat" batch file with administrator privileges.  If you do not have administrator privileges, run: @@ -149,29 +136,6 @@ results.  The script in src/ghcmemlimit sets an environment variable that limits memory to the amount of free and reclaimable memory on your machine.--WEB CPSA--To make CPSA service available:--(1) Install the four programs into the CGI bin directory.--(2) Change directory to the src directory, and copy cpsacgi and-cpsacgi.py into the CGI bin directory.--(3) Copy index.html, ../doc/cpsauser.html, and ../doc/cpsaprimer.pdf-into your choice of the web document directory.--(4) Make an examples directory in the web document directory.--(5) Copy ../tst/*.scm into the examples directory.--SELINUX--You must modify the default policy to allow unconfined executables to-make their heap memory executable, has CPSA is written in Haskell, and-its runtime puts executable code in its heap.  The policy module is in-src/httpd_allow_execmem.te.  KNOWN BUGS
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.5.1+Version:		2.5.2 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3
doc/cpsadesign.pdf view

binary file changed (275303 → 275415 bytes)

doc/cpsagoals.pdf view

binary file changed (194667 → 194752 bytes)

doc/cpsaintroslides.pdf view

binary file changed (93123 → 93179 bytes)

doc/cpsaoverview.pdf view

binary file changed (128941 → 129006 bytes)

doc/cpsaprimer.pdf view

binary file changed (276623 → 276712 bytes)

doc/cpsaspec.pdf view

binary file changed (387769 → 388029 bytes)

doc/cpsauser.html view
@@ -507,16 +507,17 @@ <blockquote>   <pre>$ cpsagraph -h Usage: cpsagraph [OPTIONS] [FILE]-  -o FILE  --output=FILE  output FILE-  -x       --expanded     use expanded format (default)-  -z       --zoom         enable diagram scaling-  -t       --treeless     use treeless expanded format-  -c       --compact      use compact format-  -l       --latex        use LaTeX format-  -m INT   --margin=INT   set output margin (default 72)-  -i       --infix        output uses infix notation-  -h       --help         show help message-  -v       --version      show version number</pre>+  -o FILE  --output=FILE   output FILE+  -x       --expanded      use expanded format (default)+  -z       --zoom          enable diagram scaling+  -t       --treeless      use treeless expanded format+  -c       --compact       use compact format+  -l       --latex         use LaTeX format+  -m INT   --margin=INT    set output margin (default 72)+  -i       --infix         output uses infix notation+  -p       --purge-traces  purge traces+  -h       --help          show help message+  -v       --version       show version number</pre> </blockquote>  <h2 id="cpsadiff">Output Comparisons</h2>
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.5.1}+\newcommand{\version}{2.5.2} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
src/CPSA/Graph/Config.hs view
@@ -27,6 +27,7 @@       br :: Float,              -- Bullet radius       compact :: Bool,          -- Generate compact format       notation :: Notation,     -- Select notation+      purge :: Bool,            -- Enable purging of traces       scripts :: Bool }         -- Enable scripting     deriving (Show, Read)
src/CPSA/Graph/ExpandedView.hs view
@@ -170,7 +170,7 @@       hPutStrLn h ""       let (width, height, es) = skel conf k       hPutStrLn h $ show $ docRoot conf width height (defs conf : es)-      hPutSExpr h margin pp (preskelSrc k)+      hPutSExpr h margin pp (purgeTraces conf $ preskelSrc k)       -- Use a breadth first ordering by appending children to the queue       kdrawer h conf margin pp tid (ts ++ children t) @@ -200,6 +200,19 @@ indent :: Int indent = 2 +purgeTraces :: Config -> SExpr Pos -> SExpr Pos+purgeTraces conf x | purge conf =+  strip "traces" x+purgeTraces _ x = x++strip :: String -> SExpr Pos -> SExpr Pos+strip key (L p xs) =+  L p (filter f xs)+  where+    f (L _ (S _ s : _)) | s == key = False+    f _ = True+strip _ x = x+ -- Encoded from src/zoom.js using src/js2hs javascript :: [String] javascript =@@ -239,7 +252,7 @@       hPutStrLn h ""       let (width, height, es) = skel conf k       hPutStrLn h $ show $ docRoot conf width height (defs conf : es)-      hPutSExpr h margin pp (preskelSrc k)+      hPutSExpr h margin pp (purgeTraces conf $ preskelSrc k)       n <- loadNext s       case n of         Nothing ->              -- EOF
src/CPSA/Graph/Main.hs view
@@ -25,6 +25,7 @@     { file :: Maybe FilePath,   -- Nothing specifies standard output       format :: Format,         -- Output format       prefix :: Bool,           -- Use prefix notation?+      purgeTraces :: Bool,      -- Purge traces?       scripted :: Bool,         -- Use scripting?       margin :: Int }           -- Output line length     deriving Show@@ -53,7 +54,8 @@               h <- outputHandle (file params)               hPutStrLn h "<?xml version=\"1.0\"?>"               hPutStrLn h ("<!-- " ++ cpsaVersion ++ " -->")-              let conf = config (prefix params) (scripted params)+              let conf = config (prefix params) (purgeTraces params)+                         (scripted params)               case format params of                 XHTML -> expandedView h (conf False)                          (margin params) cmts preskels@@ -92,7 +94,8 @@               h <- outputHandle (file params)               hPutStrLn h "<?xml version=\"1.0\"?>"               hPutStrLn h ("<!-- " ++ cpsaVersion ++ " -->")-              let conf = config (prefix params) (scripted params) False+              let conf = config (prefix params) (purgeTraces params)+                         (scripted params) False               ans <- tryIO (treelessView h conf (margin params)                                          cmts preskel state)               case ans of@@ -111,7 +114,8 @@               h <- outputHandle (file params)               hPutStrLn h "\\documentclass[12pt]{article}"               hPutStrLn h ("% " ++ cpsaVersion)-              let conf = config (prefix params) (scripted params) False+              let conf = config (prefix params) (purgeTraces params)+                         (scripted params) False               let pp = printer conf               ans <- tryIO (latexView h (margin params) pp cmts preskel state)               case ans of@@ -124,11 +128,12 @@     | Info                      -- Version information     | Expanded                  -- Select expanded format in XHTML     | Treeless                  -- Select treeless expanded format in XHTML-    | Scripted                  -- Ensable scripting+    | Scripted                  -- Enable scripting     | Compact                   -- Select compact format in SVG     | Text                      -- Select text format in LaTeX     | Margin String             -- Output line length     | InfixFlag                 -- Select output notation+    | PurgeFlag                 -- Enable purging of traces     | Output String             -- Output file name       deriving Show @@ -149,6 +154,7 @@       Option ['m'] ["margin"]   (ReqArg Margin "INT")       ("set output margin (default " ++ show defaultMargin ++ ")"),       Option ['i'] ["infix"]    (NoArg InfixFlag) "output uses infix notation",+      Option ['p'] ["purge-traces"] (NoArg PurgeFlag)  "purge traces",       Option ['h'] ["help"]     (NoArg Help)           "show help message",       Option ['v'] ["version"]  (NoArg Info)           "show version number" ] @@ -158,6 +164,7 @@     loop flags (Params { file = Nothing, -- By default, no output file                          format = XHTML, -- and use expanded format                          prefix = True,+                         purgeTraces = False,                          scripted = False,                          margin = defaultMargin })     where@@ -177,6 +184,8 @@           loop flags $ params { format = LaTeX }       loop (InfixFlag : flags) params =           loop flags $ params { prefix = False }+      loop (PurgeFlag : flags) params =+          loop flags $ params { purgeTraces = True }       loop (Margin value : flags) params =           case readDec value of             [(margin, "")] ->@@ -199,8 +208,8 @@ -- Default configuration.  The lengths are in points, however the more -- natural choice is a font relative unit of length such as ems, -- however FireFox doesn't support these units yet.-config :: Bool -> Bool -> Bool -> Config-config prefix scripts compact =+config :: Bool -> Bool -> Bool -> Bool -> Config+config prefix purge scripts compact =     Config { units = "pt",              font = font,              stroke = 0.08 * font,@@ -217,6 +226,7 @@              br = 0.50 * font,              compact = compact,              notation = if prefix then Prefix else Infix,+             purge = purge,              scripts = scripts }     where       font = 12
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from blanchet.scm")  (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (comment "All input read from completeness-test.scm")  (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from ffgg.scm")  (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from incompleteness_example.scm")  (defprotocol incompleteness-example basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (comment "All input read from isoreject.scm")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (comment "All input read from kelly1.scm")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (comment "All input read from kerberos.scm")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (comment "All input read from mass.lsp")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (comment "All input read from mass2.lsp")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from print.scm")  (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from targetterms2.scm")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (comment "All input read from targetterms6.scm")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from timestamping.scm")  (defprotocol timestamping-service basic
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from unilateral.scm")  (defprotocol unilateral basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (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.1")+(comment "CPSA 2.5.2") (comment "All input read from yahalom.scm") (comment "Strand count bounded at 15")