diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2022-03-20 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as 3.6.10 + +2022-03-17 John D. Ramsdell + + * src/CPSA/Lib/SExpr.hs: Allow double quote and backslash in + strings so that S-expressions can contain Windows file names. + 2022-01-04 John D. Ramsdell * cpsa.cabal (Version): Tagged as 3.6.9 diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ CPSA NEWS + March 2022: + +* Release 3.6.10 allows double quote and backslash in S-expressions so + that they can contain Windows file names. + January 2022: * Release 3.6.9 expunges skeletons that have a value that is both uniq diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 3.6.9 +Version: 3.6.10 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.10 License: BSD3 diff --git a/doc/cpsamanual.pdf b/doc/cpsamanual.pdf Binary files a/doc/cpsamanual.pdf and b/doc/cpsamanual.pdf differ diff --git a/src/CPSA/Lib/Entry.hs b/src/CPSA/Lib/Entry.hs --- a/src/CPSA/Lib/Entry.hs +++ b/src/CPSA/Lib/Entry.hs @@ -240,7 +240,7 @@ comment :: String -> SExpr () comment msg = - L () [S () "comment", Q () msg] + L () [S () "comment", stringSExpr msg] writeComment :: Handle -> Int -> String -> IO () writeComment h margin msg = diff --git a/src/CPSA/Lib/SExpr.hs b/src/CPSA/Lib/SExpr.hs --- a/src/CPSA/Lib/SExpr.hs +++ b/src/CPSA/Lib/SExpr.hs @@ -1,27 +1,54 @@ --- A data structure for S-expressions, the ones that are called --- proper lists. +{-| +Module: CPSA.Lib.SExpr +Description: S-expressions and a reader +Copyright: (c) 2009 The MITRE Corporation +License: BSD +This module provides a data structure for S-expressions, and a reader. +The reader records the position in the file at which items that make +up the list are located. + +The S-expressions used are restricted so that most dialects of Lisp +can read them, and characters within symbols and strings never need +quoting. Every list is proper. An atom is either a symbol, an integer, +or a string. The characters that make up a symbol are the letters, the +digits, and these special characters. + +@ + +-*/<=>!?:$%_&~^ +@ + +A symbol may not begin with a digit or a sign followed by a digit. The +characters that make up a string are the printing characters omitting +double quote and backslash, except when double quote and backslash are +escaped using the backslash character. Double quotes delimit a +string. A comment begins with a semicolon and continues to the end of +the current line. + +-} + -- Copyright (c) 2009 The MITRE Corporation -- -- This program is free software: you can redistribute it and/or -- modify it under the terms of the BSD License as published by the -- University of California. -module CPSA.Lib.SExpr (SExpr(..), showQuoted, annotation, Pos, - PosHandle, posHandle, load) where +module CPSA.Lib.SExpr (SExpr(..), showQuoted, stringSExpr, annotation, + -- * S-expression Reader + Pos, PosHandle, posHandle, load) where import Data.Char (isSpace, isDigit, isAlphaNum, isPrint) import Data.IORef (IORef, newIORef, readIORef, writeIORef) import System.IO (Handle, hIsEOF, hGetChar, hLookAhead, hClose) --- An S-expression--all of its constructors are strict. +-- | An S-expression--all of its constructors are strict. data SExpr a - = S !a !String -- A symbol - | Q !a !String -- A quoted string - | N !a !Int -- An integer - | L !a ![SExpr a] -- A proper list + = S !a !String -- ^ A symbol + | Q !a !String -- ^ A quoted string + | N !a !Int -- ^ An integer + | L !a ![SExpr a] -- ^ A proper list --- Equality ignores position annotations +-- | Equality ignores position annotations. instance Eq (SExpr a) where S _ s == S _ s' = s == s' Q _ s == Q _ s' = s == s' @@ -29,11 +56,29 @@ L _ xs == L _ xs' = xs == xs' _ == _ = False --- Printing support +-- | Ordering ignores position annotations. +instance Ord (SExpr a) where + compare (S _ s) (S _ s') = compare s s' + compare (S _ _) (Q _ _) = LT + compare (S _ _) (N _ _) = LT + compare (S _ _) (L _ _) = LT + compare (Q _ _) (S _ _) = GT + compare (Q _ s) (Q _ s') = compare s s' + compare (Q _ _) (N _ _) = LT + compare (Q _ _) (L _ _) = LT + compare (N _ _) (S _ _) = GT + compare (N _ _) (Q _ _) = GT + compare (N _ n) (N _ n') = compare n n' + compare (N _ _) (L _ _) = LT + compare (L _ _) (S _ _) = GT + compare (L _ _) (Q _ _) = GT + compare (L _ _) (N _ _) = GT + compare (L _ xs) (L _ xs') = compare xs xs' +-- | This printer produces no line breaks. instance Show (SExpr a) where showsPrec _ (S _ s) = showString s - showsPrec _ (Q _ s) = showChar '"' . showString s . showChar '"' + showsPrec _ (Q _ s) = showQuoted s showsPrec _ (N _ n) = shows n showsPrec _ (L _ []) = showString "()" showsPrec _ (L _ (x:xs)) = @@ -42,10 +87,25 @@ showl [] = id showl (x:xs) = showChar ' ' . shows x . showl xs +-- | Add quotes to a string so it reads as an S-expression string. showQuoted :: String -> ShowS -showQuoted s = showChar '"' . showString s . showChar '"' +showQuoted s = showChar '"' . showEscaped s . showChar '"' --- Extract an S-expression's annotation. +showEscaped :: String -> ShowS +showEscaped ('\\' : s) = showString "\\\\" . showEscaped s +showEscaped ('"' : s) = showString "\\\"" . showEscaped s +showEscaped (ch : s) = showChar ch . showEscaped s +showEscaped [] = id + +-- | Convert a raw string into a quoted S-expression. +stringSExpr :: String -> SExpr () +stringSExpr s = + if all isPrint s then + Q () s + else + error "SExpr.stringSExpr: Bad string" + +-- | Extract an S-expression's annotation. annotation :: SExpr a -> a annotation (S a _) = a annotation (Q a _) = a @@ -54,11 +114,11 @@ -- S-expression Reader --- The reader returns objects of type SExpr Pos so that error messages --- can include a location. +-- | The reader returns objects of type 'SExpr' 'Pos' so that error +-- messages can include a location. data Pos = Pos { file :: !String, line :: !Int, column :: !Int } --- Show a position in a form Emacs can read. +-- | Show a position in a form Emacs can read. instance Show Pos where showsPrec _ pos = showString (file pos) . showString ":" . @@ -67,10 +127,10 @@ shows (column pos) . showString ": " --- Bind a position to a handle +-- | Keep track of position information associated with a given handle. data PosHandle = PosHandle { pHandle :: Handle, pFile :: String, pPosition :: IORef (Int, Int) } - +-- | Create a 'PosHandle'. posHandle :: FilePath -> Handle -> IO PosHandle posHandle file handle = do @@ -88,7 +148,7 @@ | Rparen !Pos | Eof --- Read one S-expression or return Nothing on EOF +-- | Read one S-expression or return 'Nothing' on EOF load :: PosHandle -> IO (Maybe (SExpr Pos)) load p = do @@ -215,11 +275,28 @@ abort p (shows pos "End of input in string") Just '"' -> return (l, c + 1, Atom (Q pos (seqrev s))) - Just ch | isStr ch -> + Just '\\' -> + escaped p l (c + 1) pos s + Just ch | isPrint ch -> string p l (c + 1) pos (ch : s) Just _ -> - abort p (shows pos "Bad char for string") + abort p (shows pos "Bad char in string") +-- Scan an escaped character in a quoted string of characters +escaped :: PosHandle -> Int -> Int -> Pos -> String -> IO (Int, Int, Token) +escaped p l c pos s = + do + ch <- get p + case ch of + Nothing -> + abort p (shows pos "End of input in escaped char in string") + Just '"' -> + string p l (c + 1) pos ('"' : s) + Just '\\' -> + string p l (c + 1) pos ('\\' : s) + Just _ -> + abort p (shows pos "Bad escaped char in string") + -- Scan a sequence of digits number :: PosHandle -> Int -> Int -> Pos -> String -> IO (Int, Int, Token) number p l c pos s = @@ -296,12 +373,6 @@ isSym '~' = True isSym '^' = True isSym c = isAlphaNum c - --- A string is made from printable characters. -isStr :: Char -> Bool -isStr '"' = False -isStr '\\' = False -isStr c = isPrint c -- Close input handle and then report failure abort :: PosHandle -> String -> IO a diff --git a/tst/aik.tst b/tst/aik.tst --- a/tst/aik.tst +++ b/tst/aik.tst @@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/aik.scm") (defprotocol aikprot basic diff --git a/tst/attest.tst b/tst/attest.tst --- a/tst/attest.tst +++ b/tst/attest.tst @@ -1,6 +1,6 @@ (herald attest-door) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/attest.scm") (defprotocol attest-door basic diff --git a/tst/axiom2.tst b/tst/axiom2.tst --- a/tst/axiom2.tst +++ b/tst/axiom2.tst @@ -1,6 +1,6 @@ (herald "Axiom 2 Protocol" (bound 20)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/axiom2.scm") (comment "Strand count bounded at 20") 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 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/blanchet.scm") (defprotocol blanchet basic diff --git a/tst/bltk_or.tst b/tst/bltk_or.tst --- a/tst/bltk_or.tst +++ b/tst/bltk_or.tst @@ -2,7 +2,7 @@ (comment "Standard version using variables of sort mesg") (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/bltk_or.scm") (defprotocol or diffie-hellman diff --git a/tst/bltk_test.tst b/tst/bltk_test.tst --- a/tst/bltk_test.tst +++ b/tst/bltk_test.tst @@ -1,6 +1,6 @@ (herald "bltk Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/bltk_test.scm") (defprotocol test diffie-hellman diff --git a/tst/comment.tst b/tst/comment.tst --- a/tst/comment.tst +++ b/tst/comment.tst @@ -1,6 +1,6 @@ (herald comment) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/comment.scm") (defprotocol comment basic diff --git a/tst/comp_test.tst b/tst/comp_test.tst --- a/tst/comp_test.tst +++ b/tst/comp_test.tst @@ -1,6 +1,6 @@ (herald "Main Example") -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/comp_test.scm") (defprotocol main-ex-src basic diff --git a/tst/dh-ca.tst b/tst/dh-ca.tst --- a/tst/dh-ca.tst +++ b/tst/dh-ca.tst @@ -1,6 +1,6 @@ (herald dhca (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dh-ca.scm") (defprotocol dhca diffie-hellman diff --git a/tst/dh_group_sig.tst b/tst/dh_group_sig.tst --- a/tst/dh_group_sig.tst +++ b/tst/dh_group_sig.tst @@ -1,6 +1,6 @@ (herald "Signed group DH exchange" (algebra diffie-hellman) (limit 100)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dh_group_sig.scm") (comment "Step count limited to 100") diff --git a/tst/dh_mim.tst b/tst/dh_mim.tst --- a/tst/dh_mim.tst +++ b/tst/dh_mim.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dh_mim.scm") (defprotocol dh_mim diffie-hellman diff --git a/tst/dh_mim2.tst b/tst/dh_mim2.tst --- a/tst/dh_mim2.tst +++ b/tst/dh_mim2.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dh_mim2.scm") (defprotocol dh_mim diffie-hellman diff --git a/tst/dh_mim_nobase.tst b/tst/dh_mim_nobase.tst --- a/tst/dh_mim_nobase.tst +++ b/tst/dh_mim_nobase.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dh_mim_nobase.scm") (defprotocol dh_mim_nobase diffie-hellman diff --git a/tst/dh_sig.tst b/tst/dh_sig.tst --- a/tst/dh_sig.tst +++ b/tst/dh_sig.tst @@ -1,6 +1,6 @@ (herald "Signed DH exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dh_sig.scm") (defprotocol dh_sig diffie-hellman diff --git a/tst/dh_test.tst b/tst/dh_test.tst --- a/tst/dh_test.tst +++ b/tst/dh_test.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dh_test.scm") (comment "Strand count bounded at 20") diff --git a/tst/dhcr_um.tst b/tst/dhcr_um.tst --- a/tst/dhcr_um.tst +++ b/tst/dhcr_um.tst @@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) original" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dhcr_um.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20") diff --git a/tst/dhcr_um3.tst b/tst/dhcr_um3.tst --- a/tst/dhcr_um3.tst +++ b/tst/dhcr_um3.tst @@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) three-part" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dhcr_um3.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20") diff --git a/tst/dhcr_umx.tst b/tst/dhcr_umx.tst --- a/tst/dhcr_umx.tst +++ b/tst/dhcr_umx.tst @@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) criss-cross" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dhcr_umx.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20") diff --git a/tst/dhnsl_basic.tst b/tst/dhnsl_basic.tst --- a/tst/dhnsl_basic.tst +++ b/tst/dhnsl_basic.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dhnsl_basic.scm") (defprotocol dhnsl diffie-hellman diff --git a/tst/dhnsl_use.tst b/tst/dhnsl_use.tst --- a/tst/dhnsl_use.tst +++ b/tst/dhnsl_use.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/dhnsl_use.scm") (defprotocol dhnsl diffie-hellman diff --git a/tst/doorsep.tst b/tst/doorsep.tst --- a/tst/doorsep.tst +++ b/tst/doorsep.tst @@ -1,6 +1,6 @@ (herald doorsep (comment "Door Simple Example Protocol")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/doorsep.scm") (defprotocol doorsep basic diff --git a/tst/doorsep2invk.tst b/tst/doorsep2invk.tst --- a/tst/doorsep2invk.tst +++ b/tst/doorsep2invk.tst @@ -1,6 +1,6 @@ (herald doorsep2invk (comment "Door Simple Example Protocol")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/doorsep2invk.scm") (defprotocol doorsep basic diff --git a/tst/eadh_um.tst b/tst/eadh_um.tst # file too large to diff: tst/eadh_um.tst diff --git a/tst/enrich.tst b/tst/enrich.tst --- a/tst/enrich.tst +++ b/tst/enrich.tst @@ -1,6 +1,6 @@ (herald enrich) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/enrich.scm") (defprotocol enrich basic diff --git a/tst/envelope.tst b/tst/envelope.tst --- a/tst/envelope.tst +++ b/tst/envelope.tst @@ -1,6 +1,6 @@ (herald "Envelope Protocol" (bound 20)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/envelope.scm") (comment "Strand count bounded at 20") diff --git a/tst/envelope_short.tst b/tst/envelope_short.tst --- a/tst/envelope_short.tst +++ b/tst/envelope_short.tst @@ -1,6 +1,6 @@ (herald "Envelope Protocol" (bound 20)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/envelope_short.scm") (comment "Strand count bounded at 20") diff --git a/tst/eq_test.tst b/tst/eq_test.tst --- a/tst/eq_test.tst +++ b/tst/eq_test.tst @@ -2,7 +2,7 @@ (comment "First skeleton should have a shape," "second, and hird should be dead.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/eq_test.scm") (defprotocol eqtest 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 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/ffgg.scm") (defprotocol ffgg basic diff --git a/tst/fluffy_draft03_gske.tst b/tst/fluffy_draft03_gske.tst --- a/tst/fluffy_draft03_gske.tst +++ b/tst/fluffy_draft03_gske.tst @@ -3,7 +3,7 @@ (comment "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/fluffy_draft03_gske.scm") (defprotocol fluffy basic diff --git a/tst/fnof_or.tst b/tst/fnof_or.tst --- a/tst/fnof_or.tst +++ b/tst/fnof_or.tst @@ -2,7 +2,7 @@ (comment "Version using variables of sort mesg, with ltk function emulated.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/fnof_or.scm") (defprotocol or basic diff --git a/tst/fnof_test.tst b/tst/fnof_test.tst --- a/tst/fnof_test.tst +++ b/tst/fnof_test.tst @@ -1,7 +1,7 @@ (herald "Function constraint test protocol" (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/fnof_test.scm") (defprotocol fnoftest basic diff --git a/tst/fnof_woolam.tst b/tst/fnof_woolam.tst --- a/tst/fnof_woolam.tst +++ b/tst/fnof_woolam.tst @@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol, using fnof to emulate ltk function") -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/fnof_woolam.scm") (defprotocol woolam basic diff --git a/tst/fnof_yahalom.tst b/tst/fnof_yahalom.tst --- a/tst/fnof_yahalom.tst +++ b/tst/fnof_yahalom.tst @@ -2,7 +2,7 @@ "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function" (bound 12)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/fnof_yahalom.scm") (defprotocol yahalom 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 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/goals.scm") (defprotocol ns basic diff --git a/tst/iadh_um.tst b/tst/iadh_um.tst # file too large to diff: tst/iadh_um.tst diff --git a/tst/iadh_um_eq.tst b/tst/iadh_um_eq.tst --- a/tst/iadh_um_eq.tst +++ b/tst/iadh_um_eq.tst @@ -1,7 +1,7 @@ (herald "IADH: unified model (UM)" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/iadh_um_eq.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20") diff --git a/tst/iadh_um_joshua.tst b/tst/iadh_um_joshua.tst --- a/tst/iadh_um_joshua.tst +++ b/tst/iadh_um_joshua.tst @@ -1,7 +1,7 @@ (herald "IADH: unified model (UM)" (bound 20) (limit 2000) (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/iadh_um_joshua.scm") (comment "Strand count bounded at 20") diff --git a/tst/iadh_umx.tst b/tst/iadh_umx.tst --- a/tst/iadh_umx.tst +++ b/tst/iadh_umx.tst @@ -1,7 +1,7 @@ (herald "IADH: unified model (UM), criss-cross variant" (bound 20) (limit 2000) (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/iadh_umx.scm") (comment "Strand count bounded at 20") diff --git a/tst/injection.tst b/tst/injection.tst --- a/tst/injection.tst +++ b/tst/injection.tst @@ -2,7 +2,7 @@ (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/injection.scm") (defprotocol ns diffie-hellman diff --git a/tst/kerb.tst b/tst/kerb.tst --- a/tst/kerb.tst +++ b/tst/kerb.tst @@ -1,4 +1,4 @@ -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/kerb.scm") (defprotocol kerb-flawed 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 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/kerberos++.scm") (defprotocol kerberos basic diff --git a/tst/lt_test.tst b/tst/lt_test.tst --- a/tst/lt_test.tst +++ b/tst/lt_test.tst @@ -2,7 +2,7 @@ (comment "First and third skeletons should have a shape," "second and fourth should be dead.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/lt_test.scm") (defprotocol lttest basic diff --git a/tst/neq_test.tst b/tst/neq_test.tst --- a/tst/neq_test.tst +++ b/tst/neq_test.tst @@ -2,7 +2,7 @@ (comment "First skeleton should have a shape," "second, and hird should be dead.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/neq_test.scm") (defprotocol neqtest basic diff --git a/tst/nh-ca-w-dh.tst b/tst/nh-ca-w-dh.tst --- a/tst/nh-ca-w-dh.tst +++ b/tst/nh-ca-w-dh.tst @@ -1,6 +1,6 @@ (herald nhca (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.7") +(comment "CPSA 3.6.10") (comment "All input read from tst/nh-ca-w-dh.scm") (comment "Strand count bounded at 20") diff --git a/tst/nh-ca.tst b/tst/nh-ca.tst --- a/tst/nh-ca.tst +++ b/tst/nh-ca.tst @@ -1,6 +1,6 @@ (herald nhca (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.7") +(comment "CPSA 3.6.10") (comment "All input read from tst/nh-ca.scm") (comment "Strand count bounded at 20") diff --git a/tst/nhcr_um.tst b/tst/nhcr_um.tst --- a/tst/nhcr_um.tst +++ b/tst/nhcr_um.tst @@ -1,7 +1,7 @@ (herald "NHCR: unified model (UM)" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.7") +(comment "CPSA 3.6.10") (comment "All input read from tst/nhcr_um.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20") diff --git a/tst/nhcr_um3.tst b/tst/nhcr_um3.tst --- a/tst/nhcr_um3.tst +++ b/tst/nhcr_um3.tst @@ -1,7 +1,7 @@ (herald "NHCR: unified model (UM3) original" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.7") +(comment "CPSA 3.6.10") (comment "All input read from tst/nhcr_um3.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20") diff --git a/tst/nhcr_umx.tst b/tst/nhcr_umx.tst --- a/tst/nhcr_umx.tst +++ b/tst/nhcr_umx.tst @@ -1,7 +1,7 @@ (herald "NHCR: unified model (UMX) criss-cross" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.7") +(comment "CPSA 3.6.10") (comment "All input read from tst/nhcr_umx.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20") diff --git a/tst/ns.tst b/tst/ns.tst --- a/tst/ns.tst +++ b/tst/ns.tst @@ -2,7 +2,7 @@ (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/ns.scm") (defprotocol ns 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 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/or.scm") (defprotocol or basic diff --git a/tst/ordered.tst b/tst/ordered.tst --- a/tst/ordered.tst +++ b/tst/ordered.tst @@ -1,6 +1,6 @@ (herald ordered) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/ordered.scm") (defprotocol ordered basic diff --git a/tst/owang.tst b/tst/owang.tst --- a/tst/owang.tst +++ b/tst/owang.tst @@ -1,4 +1,4 @@ -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/owang.scm") (defprotocol wang basic diff --git a/tst/owat.tst b/tst/owat.tst --- a/tst/owat.tst +++ b/tst/owat.tst @@ -1,7 +1,7 @@ (herald "One-way Authentication Test with bltk keys" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/owat.scm") (defprotocol owa diffie-hellman diff --git a/tst/pkinit.tst b/tst/pkinit.tst --- a/tst/pkinit.tst +++ b/tst/pkinit.tst @@ -1,6 +1,6 @@ (herald "Kerberos PKINIT") -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/pkinit.scm") (defprotocol pkinit-flawed basic diff --git a/tst/plaindh.tst b/tst/plaindh.tst --- a/tst/plaindh.tst +++ b/tst/plaindh.tst @@ -1,7 +1,7 @@ (herald "Plain diffie-hellman protocol with challenge-response" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/plaindh.scm") (defprotocol plaindh diffie-hellman diff --git a/tst/precursor.tst b/tst/precursor.tst --- a/tst/precursor.tst +++ b/tst/precursor.tst @@ -1,6 +1,6 @@ (herald precursor (algebra diffie-hellman) (bound 6)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/precursor.scm") (comment "Strand count bounded at 6") diff --git a/tst/priority_test.tst b/tst/priority_test.tst --- a/tst/priority_test.tst +++ b/tst/priority_test.tst @@ -1,6 +1,6 @@ (herald "Receive priority test protocol") -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/priority_test.scm") (defprotocol priority_test basic diff --git a/tst/prottrans.tst b/tst/prottrans.tst --- a/tst/prottrans.tst +++ b/tst/prottrans.tst @@ -1,6 +1,6 @@ (herald "Protocol Transformations With Rules") -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/prottrans.scm") (defprotocol ns basic diff --git a/tst/reflect.tst b/tst/reflect.tst --- a/tst/reflect.tst +++ b/tst/reflect.tst @@ -1,6 +1,6 @@ (herald reflect) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/reflect.scm") (defprotocol reflect basic diff --git a/tst/reflect_dh.tst b/tst/reflect_dh.tst --- a/tst/reflect_dh.tst +++ b/tst/reflect_dh.tst @@ -1,6 +1,6 @@ (herald reflect (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/reflect_dh.scm") (defprotocol reflect diffie-hellman diff --git a/tst/role_uniq.tst b/tst/role_uniq.tst --- a/tst/role_uniq.tst +++ b/tst/role_uniq.tst @@ -1,6 +1,6 @@ (herald "Role Unique Origination") -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/role_uniq.scm") (defprotocol blanchet basic diff --git a/tst/rule-order.tst b/tst/rule-order.tst --- a/tst/rule-order.tst +++ b/tst/rule-order.tst @@ -1,6 +1,6 @@ (herald rule-order) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/rule-order.scm") (defprotocol rule-order basic diff --git a/tst/staticdh.tst b/tst/staticdh.tst --- a/tst/staticdh.tst +++ b/tst/staticdh.tst @@ -1,6 +1,6 @@ (herald "Static DH key exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/staticdh.scm") (defprotocol staticdh1 diffie-hellman diff --git a/tst/station.tst b/tst/station.tst --- a/tst/station.tst +++ b/tst/station.tst @@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/station.scm") (defprotocol station-to-station diffie-hellman diff --git a/tst/station2.tst b/tst/station2.tst --- a/tst/station2.tst +++ b/tst/station2.tst @@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/station2.scm") (defprotocol station-to-station diffie-hellman diff --git a/tst/station_newhope.tst b/tst/station_newhope.tst --- a/tst/station_newhope.tst +++ b/tst/station_newhope.tst @@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.7") +(comment "CPSA 3.6.10") (comment "All input read from tst/station_newhope.scm") (defprotocol station-to-station diffie-hellman diff --git a/tst/station_nobase.tst b/tst/station_nobase.tst --- a/tst/station_nobase.tst +++ b/tst/station_nobase.tst @@ -1,7 +1,7 @@ (herald "Station-to-station protocol no base vars" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/station_nobase.scm") (defprotocol station-to-station diffie-hellman diff --git a/tst/stationbase.tst b/tst/stationbase.tst --- a/tst/stationbase.tst +++ b/tst/stationbase.tst @@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/stationbase.scm") (defprotocol station-to-station diffie-hellman diff --git a/tst/subsort_test.tst b/tst/subsort_test.tst --- a/tst/subsort_test.tst +++ b/tst/subsort_test.tst @@ -2,7 +2,7 @@ (comment "First, third, and fourth skeletons should have a shape," "second should be dead.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/subsort_test.scm") (defprotocol subsorttest basic diff --git a/tst/tag_test.tst b/tst/tag_test.tst --- a/tst/tag_test.tst +++ b/tst/tag_test.tst @@ -1,6 +1,6 @@ (herald "Tag Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/tag_test.scm") (defprotocol test diffie-hellman diff --git a/tst/target.tst b/tst/target.tst --- a/tst/target.tst +++ b/tst/target.tst @@ -1,4 +1,4 @@ -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/target.scm") (defprotocol target-simple basic diff --git a/tst/test_g.tst b/tst/test_g.tst --- a/tst/test_g.tst +++ b/tst/test_g.tst @@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/test_g.scm") (defprotocol test1 diffie-hellman diff --git a/tst/test_small.tst b/tst/test_small.tst --- a/tst/test_small.tst +++ b/tst/test_small.tst @@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/test_small.scm") (defprotocol test diffie-hellman diff --git a/tst/thinning.tst b/tst/thinning.tst --- a/tst/thinning.tst +++ b/tst/thinning.tst @@ -1,6 +1,6 @@ (herald thinning (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/thinning.scm") (defprotocol provision diffie-hellman diff --git a/tst/trust-anchor.tst b/tst/trust-anchor.tst --- a/tst/trust-anchor.tst +++ b/tst/trust-anchor.tst @@ -1,7 +1,7 @@ (herald trust-anchor (comment "Tests rule application on initial skeleton")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/trust-anchor.scm") (defprotocol trust-anchor basic diff --git a/tst/ugen_test.tst b/tst/ugen_test.tst --- a/tst/ugen_test.tst +++ b/tst/ugen_test.tst @@ -3,7 +3,7 @@ origination are not always preserved for skeleton uniq-orig assumptions) (algebra diffie-hellman)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/ugen_test.scm") (defprotocol uof diffie-hellman 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 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/unilateral.scm") (defprotocol unilateral basic diff --git a/tst/uniq-gen-test.tst b/tst/uniq-gen-test.tst --- a/tst/uniq-gen-test.tst +++ b/tst/uniq-gen-test.tst @@ -1,7 +1,7 @@ (herald "Unique generation test protocols." (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/uniq-gen-test.scm") (defprotocol uniqgentest basic diff --git a/tst/uniq_orig_doesnt_fail.tst b/tst/uniq_orig_doesnt_fail.tst --- a/tst/uniq_orig_doesnt_fail.tst +++ b/tst/uniq_orig_doesnt_fail.tst @@ -3,7 +3,7 @@ origination are not always preserved for skeleton uniq-orig assumptions)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/uniq_orig_doesnt_fail.scm") (defprotocol uof basic diff --git a/tst/wd-goalssat.tst b/tst/wd-goalssat.tst --- a/tst/wd-goalssat.tst +++ b/tst/wd-goalssat.tst @@ -1,6 +1,6 @@ (herald "Wrap-Decrypt example" (bound 24) (limit 2000) (goals-sat)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/wd-goalssat.scm") (comment "Strand count bounded at 24") (comment "Stop when goals satisfied") diff --git a/tst/wd-gs-simple.tst b/tst/wd-gs-simple.tst --- a/tst/wd-gs-simple.tst +++ b/tst/wd-gs-simple.tst @@ -1,7 +1,7 @@ (herald "Wrap-Decrypt example, simplified" (bound 24) (limit 500) (goals-sat)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/wd-gs-simple.scm") (comment "Step count limited to 500") (comment "Strand count bounded at 24") 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 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/woolam.scm") (defprotocol woolam basic diff --git a/tst/wrap_decrypt.tst b/tst/wrap_decrypt.tst --- a/tst/wrap_decrypt.tst +++ b/tst/wrap_decrypt.tst @@ -1,6 +1,6 @@ (herald wrap-decrypt (bound 10)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/wrap_decrypt.lsp") (comment "Strand count bounded at 10") diff --git a/tst/yahalom.tst b/tst/yahalom.tst --- a/tst/yahalom.tst +++ b/tst/yahalom.tst @@ -1,7 +1,7 @@ (herald "Yahalom Protocol with Forwarding Removed" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/yahalom.scm") (defprotocol yahalom diffie-hellman diff --git a/tst/yolo.tst b/tst/yolo.tst --- a/tst/yolo.tst +++ b/tst/yolo.tst @@ -1,6 +1,6 @@ (herald yolo) -(comment "CPSA 3.6.8") +(comment "CPSA 3.6.10") (comment "All input read from tst/yolo.scm") (defprotocol yolo basic