diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2015-07-27 John D. Ramsdell + + * 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 + + * 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 * cpsa.cabal (Version): Tagged as version 2.5.1 diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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 diff --git a/README b/README --- a/README +++ b/README @@ -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 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 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 diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.5.1 +Version: 2.5.2 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ diff --git a/doc/cpsagoals.pdf b/doc/cpsagoals.pdf Binary files a/doc/cpsagoals.pdf and b/doc/cpsagoals.pdf differ diff --git a/doc/cpsaintroslides.pdf b/doc/cpsaintroslides.pdf Binary files a/doc/cpsaintroslides.pdf and b/doc/cpsaintroslides.pdf differ diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -507,16 +507,17 @@ 
$ 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
+ -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

Output Comparisons

diff --git a/doc/macros.tex b/doc/macros.tex --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}} -\newcommand{\version}{2.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 diff --git a/src/CPSA/Graph/Config.hs b/src/CPSA/Graph/Config.hs --- a/src/CPSA/Graph/Config.hs +++ b/src/CPSA/Graph/Config.hs @@ -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) diff --git a/src/CPSA/Graph/ExpandedView.hs b/src/CPSA/Graph/ExpandedView.hs --- a/src/CPSA/Graph/ExpandedView.hs +++ b/src/CPSA/Graph/ExpandedView.hs @@ -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 diff --git a/src/CPSA/Graph/Main.hs b/src/CPSA/Graph/Main.hs --- a/src/CPSA/Graph/Main.hs +++ b/src/CPSA/Graph/Main.hs @@ -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 "" hPutStrLn h ("") - 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 "" hPutStrLn h ("") - 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 diff --git a/tst/DH_hack.tst b/tst/DH_hack.tst --- a/tst/DH_hack.tst +++ b/tst/DH_hack.tst @@ -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") diff --git a/tst/blanchet.tst b/tst/blanchet.tst --- a/tst/blanchet.tst +++ b/tst/blanchet.tst @@ -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 diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst --- a/tst/completeness-test.tst +++ b/tst/completeness-test.tst @@ -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 diff --git a/tst/crushing.tst b/tst/crushing.tst --- a/tst/crushing.tst +++ b/tst/crushing.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from crushing.scm") (defprotocol crushing basic diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst --- a/tst/dass_simple.tst +++ b/tst/dass_simple.tst @@ -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 diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst --- a/tst/denning-sacco.tst +++ b/tst/denning-sacco.tst @@ -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 diff --git a/tst/deorig_contract.tst b/tst/deorig_contract.tst --- a/tst/deorig_contract.tst +++ b/tst/deorig_contract.tst @@ -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 diff --git a/tst/deorig_mesg.tst b/tst/deorig_mesg.tst --- a/tst/deorig_mesg.tst +++ b/tst/deorig_mesg.tst @@ -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 diff --git a/tst/deorig_simple.tst b/tst/deorig_simple.tst --- a/tst/deorig_simple.tst +++ b/tst/deorig_simple.tst @@ -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 diff --git a/tst/dy.tst b/tst/dy.tst --- a/tst/dy.tst +++ b/tst/dy.tst @@ -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 diff --git a/tst/encsig.tst b/tst/encsig.tst --- a/tst/encsig.tst +++ b/tst/encsig.tst @@ -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 diff --git a/tst/epmo-hash.tst b/tst/epmo-hash.tst --- a/tst/epmo-hash.tst +++ b/tst/epmo-hash.tst @@ -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 diff --git a/tst/epmo-key-hash.tst b/tst/epmo-key-hash.tst --- a/tst/epmo-key-hash.tst +++ b/tst/epmo-key-hash.tst @@ -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 diff --git a/tst/epmo.tst b/tst/epmo.tst --- a/tst/epmo.tst +++ b/tst/epmo.tst @@ -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 diff --git a/tst/epmo_acctnum-key-hash.tst b/tst/epmo_acctnum-key-hash.tst --- a/tst/epmo_acctnum-key-hash.tst +++ b/tst/epmo_acctnum-key-hash.tst @@ -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 diff --git a/tst/ffgg.tst b/tst/ffgg.tst --- a/tst/ffgg.tst +++ b/tst/ffgg.tst @@ -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 diff --git a/tst/fragile_pruning.tst b/tst/fragile_pruning.tst --- a/tst/fragile_pruning.tst +++ b/tst/fragile_pruning.tst @@ -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 diff --git a/tst/goals.tst b/tst/goals.tst --- a/tst/goals.tst +++ b/tst/goals.tst @@ -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 diff --git a/tst/hashtest-key-hash.tst b/tst/hashtest-key-hash.tst --- a/tst/hashtest-key-hash.tst +++ b/tst/hashtest-key-hash.tst @@ -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 diff --git a/tst/hashtest.tst b/tst/hashtest.tst --- a/tst/hashtest.tst +++ b/tst/hashtest.tst @@ -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 diff --git a/tst/incompleteness_example.tst b/tst/incompleteness_example.tst --- a/tst/incompleteness_example.tst +++ b/tst/incompleteness_example.tst @@ -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 diff --git a/tst/isoreject.tst b/tst/isoreject.tst --- a/tst/isoreject.tst +++ b/tst/isoreject.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from isoreject.scm") (defprotocol isoreject basic diff --git a/tst/kelly1.tst b/tst/kelly1.tst --- a/tst/kelly1.tst +++ b/tst/kelly1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from kelly1.scm") (defprotocol kelly1 basic diff --git a/tst/kerberos.tst b/tst/kerberos.tst --- a/tst/kerberos.tst +++ b/tst/kerberos.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from kerberos.scm") (defprotocol kerberos basic diff --git a/tst/mass.tst b/tst/mass.tst --- a/tst/mass.tst +++ b/tst/mass.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from mass.lsp") (defprotocol mass basic diff --git a/tst/mass2.tst b/tst/mass2.tst --- a/tst/mass2.tst +++ b/tst/mass2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from mass2.lsp") (defprotocol mass2 basic diff --git a/tst/missing_contraction.tst b/tst/missing_contraction.tst --- a/tst/missing_contraction.tst +++ b/tst/missing_contraction.tst @@ -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 diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst --- a/tst/neuman-stubblebine-reauth.tst +++ b/tst/neuman-stubblebine-reauth.tst @@ -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 diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst --- a/tst/neuman-stubblebine.tst +++ b/tst/neuman-stubblebine.tst @@ -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 diff --git a/tst/no_contraction.tst b/tst/no_contraction.tst --- a/tst/no_contraction.tst +++ b/tst/no_contraction.tst @@ -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 diff --git a/tst/non_transforming.tst b/tst/non_transforming.tst --- a/tst/non_transforming.tst +++ b/tst/non_transforming.tst @@ -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 diff --git a/tst/nonaug-prune.tst b/tst/nonaug-prune.tst --- a/tst/nonaug-prune.tst +++ b/tst/nonaug-prune.tst @@ -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 diff --git a/tst/ns-l.tst b/tst/ns-l.tst --- a/tst/ns-l.tst +++ b/tst/ns-l.tst @@ -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 diff --git a/tst/ns.tst b/tst/ns.tst --- a/tst/ns.tst +++ b/tst/ns.tst @@ -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 diff --git a/tst/nsl3.tst b/tst/nsl3.tst --- a/tst/nsl3.tst +++ b/tst/nsl3.tst @@ -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 diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst # file too large to diff: tst/nsl4cm1.tst diff --git a/tst/nslsk.tst b/tst/nslsk.tst --- a/tst/nslsk.tst +++ b/tst/nslsk.tst @@ -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 diff --git a/tst/or.tst b/tst/or.tst --- a/tst/or.tst +++ b/tst/or.tst @@ -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 diff --git a/tst/pca.tst b/tst/pca.tst --- a/tst/pca.tst +++ b/tst/pca.tst @@ -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") diff --git a/tst/pen-non-orig-test.tst b/tst/pen-non-orig-test.tst --- a/tst/pen-non-orig-test.tst +++ b/tst/pen-non-orig-test.tst @@ -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 diff --git a/tst/pkinit.tst b/tst/pkinit.tst --- a/tst/pkinit.tst +++ b/tst/pkinit.tst @@ -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 diff --git a/tst/preprocess.tst b/tst/preprocess.tst --- a/tst/preprocess.tst +++ b/tst/preprocess.tst @@ -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 diff --git a/tst/print.tst b/tst/print.tst --- a/tst/print.tst +++ b/tst/print.tst @@ -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 diff --git a/tst/pruning1.tst b/tst/pruning1.tst --- a/tst/pruning1.tst +++ b/tst/pruning1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from pruning1.scm") (defprotocol prune basic diff --git a/tst/sigenc.tst b/tst/sigenc.tst --- a/tst/sigenc.tst +++ b/tst/sigenc.tst @@ -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 diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst --- a/tst/sorted_epmo_acctnum.tst +++ b/tst/sorted_epmo_acctnum.tst @@ -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") diff --git a/tst/targetterms2.tst b/tst/targetterms2.tst --- a/tst/targetterms2.tst +++ b/tst/targetterms2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from targetterms2.scm") (defprotocol targetterms2 basic diff --git a/tst/targetterms6.tst b/tst/targetterms6.tst --- a/tst/targetterms6.tst +++ b/tst/targetterms6.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from targetterms6.scm") (defprotocol targetterms6 basic diff --git a/tst/targetterms8.tst b/tst/targetterms8.tst --- a/tst/targetterms8.tst +++ b/tst/targetterms8.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from targetterms8.scm") (defprotocol targetterms8 basic diff --git a/tst/timestamping.tst b/tst/timestamping.tst --- a/tst/timestamping.tst +++ b/tst/timestamping.tst @@ -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 diff --git a/tst/uncarried_keys.tst b/tst/uncarried_keys.tst --- a/tst/uncarried_keys.tst +++ b/tst/uncarried_keys.tst @@ -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 diff --git a/tst/unilateral.tst b/tst/unilateral.tst --- a/tst/unilateral.tst +++ b/tst/unilateral.tst @@ -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 diff --git a/tst/uo.tst b/tst/uo.tst --- a/tst/uo.tst +++ b/tst/uo.tst @@ -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 diff --git a/tst/wang-hash.tst b/tst/wang-hash.tst --- a/tst/wang-hash.tst +++ b/tst/wang-hash.tst @@ -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") diff --git a/tst/wang-key-hash.tst b/tst/wang-key-hash.tst --- a/tst/wang-key-hash.tst +++ b/tst/wang-key-hash.tst @@ -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") diff --git a/tst/weird.tst b/tst/weird.tst --- a/tst/weird.tst +++ b/tst/weird.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from weird.scm") (defprotocol weird basic diff --git a/tst/wide-mouth-frog-scyther.tst b/tst/wide-mouth-frog-scyther.tst --- a/tst/wide-mouth-frog-scyther.tst +++ b/tst/wide-mouth-frog-scyther.tst @@ -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 diff --git a/tst/wide-mouth-frog.tst b/tst/wide-mouth-frog.tst --- a/tst/wide-mouth-frog.tst +++ b/tst/wide-mouth-frog.tst @@ -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 diff --git a/tst/wonthull.tst b/tst/wonthull.tst --- a/tst/wonthull.tst +++ b/tst/wonthull.tst @@ -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") diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst --- a/tst/wonthull2.tst +++ b/tst/wonthull2.tst @@ -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") diff --git a/tst/wonthull3.tst b/tst/wonthull3.tst --- a/tst/wonthull3.tst +++ b/tst/wonthull3.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.5.1") +(comment "CPSA 2.5.2") (comment "All input read from wonthull3.scm") (defprotocol wonthull3 basic diff --git a/tst/woolam.tst b/tst/woolam.tst --- a/tst/woolam.tst +++ b/tst/woolam.tst @@ -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 diff --git a/tst/yahalom-6.3.6.tst b/tst/yahalom-6.3.6.tst --- a/tst/yahalom-6.3.6.tst +++ b/tst/yahalom-6.3.6.tst @@ -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") diff --git a/tst/yahalom.tst b/tst/yahalom.tst --- a/tst/yahalom.tst +++ b/tst/yahalom.tst @@ -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")