cpsa 3.6.9 → 3.6.10

raw patch · 91 files changed

+198/−113 lines, 91 files

Files

• ChangeLog +9/−0
• NEWS +5/−0
• cpsa.cabal +1/−1
• doc/cpsamanual.pdf binary
• src/CPSA/Lib/Entry.hs +1/−1
• src/CPSA/Lib/SExpr.hs +99/−28
• tst/aik.tst +1/−1
• tst/attest.tst +1/−1
• tst/axiom2.tst +1/−1
• tst/blanchet.tst +1/−1
• tst/bltk_or.tst +1/−1
• tst/bltk_test.tst +1/−1
• tst/comment.tst +1/−1
• tst/comp_test.tst +1/−1
• tst/dh-ca.tst +1/−1
• tst/dh_group_sig.tst +1/−1
• tst/dh_mim.tst +1/−1
• tst/dh_mim2.tst +1/−1
• tst/dh_mim_nobase.tst +1/−1
• tst/dh_sig.tst +1/−1
• tst/dh_test.tst +1/−1
• tst/dhcr_um.tst +1/−1
• tst/dhcr_um3.tst +1/−1
• tst/dhcr_umx.tst +1/−1
• tst/dhnsl_basic.tst +1/−1
• tst/dhnsl_use.tst +1/−1
• tst/doorsep.tst +1/−1
• tst/doorsep2invk.tst +1/−1
• tst/eadh_um.tst too large to diff
• tst/enrich.tst +1/−1
• tst/envelope.tst +1/−1
• tst/envelope_short.tst +1/−1
• tst/eq_test.tst +1/−1
• tst/ffgg.tst +1/−1
• tst/fluffy_draft03_gske.tst +1/−1
• tst/fnof_or.tst +1/−1
• tst/fnof_test.tst +1/−1
• tst/fnof_woolam.tst +1/−1
• tst/fnof_yahalom.tst +1/−1
• tst/goals.tst +1/−1
• tst/iadh_um.tst too large to diff
• tst/iadh_um_eq.tst +1/−1
• tst/iadh_um_joshua.tst +1/−1
• tst/iadh_umx.tst +1/−1
• tst/injection.tst +1/−1
• tst/kerb.tst +1/−1
• tst/kerberos++.tst +1/−1
• tst/lt_test.tst +1/−1
• tst/neq_test.tst +1/−1
• tst/nh-ca-w-dh.tst +1/−1
• tst/nh-ca.tst +1/−1
• tst/nhcr_um.tst +1/−1
• tst/nhcr_um3.tst +1/−1
• tst/nhcr_umx.tst +1/−1
• tst/ns.tst +1/−1
• tst/or.tst +1/−1
• tst/ordered.tst +1/−1
• tst/owang.tst +1/−1
• tst/owat.tst +1/−1
• tst/pkinit.tst +1/−1
• tst/plaindh.tst +1/−1
• tst/precursor.tst +1/−1
• tst/priority_test.tst +1/−1
• tst/prottrans.tst +1/−1
• tst/reflect.tst +1/−1
• tst/reflect_dh.tst +1/−1
• tst/role_uniq.tst +1/−1
• tst/rule-order.tst +1/−1
• tst/staticdh.tst +1/−1
• tst/station.tst +1/−1
• tst/station2.tst +1/−1
• tst/station_newhope.tst +1/−1
• tst/station_nobase.tst +1/−1
• tst/stationbase.tst +1/−1
• tst/subsort_test.tst +1/−1
• tst/tag_test.tst +1/−1
• tst/target.tst +1/−1
• tst/test_g.tst +1/−1
• tst/test_small.tst +1/−1
• tst/thinning.tst +1/−1
• tst/trust-anchor.tst +1/−1
• tst/ugen_test.tst +1/−1
• tst/unilateral.tst +1/−1
• tst/uniq-gen-test.tst +1/−1
• tst/uniq_orig_doesnt_fail.tst +1/−1
• tst/wd-goalssat.tst +1/−1
• tst/wd-gs-simple.tst +1/−1
• tst/woolam.tst +1/−1
• tst/wrap_decrypt.tst +1/−1
• tst/yahalom.tst +1/−1
• tst/yolo.tst +1/−1

@@ -1,3 +1,12 @@+2022-03-20  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version): Tagged as 3.6.10++2022-03-17  John D. Ramsdell  <ramsdell@mitre.org>++	* 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  <ramsdell@mitre.org>  	* cpsa.cabal (Version): Tagged as 3.6.9

@@ -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

@@ -1,5 +1,5 @@ Name:                   cpsa-Version:                3.6.9+Version:                3.6.10 Maintainer:             mliskov@mitre.org Cabal-Version:          >= 1.10 License:                BSD3

binary file changed (1032704 → 1042991 bytes)

@@ -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 =

@@ -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

@@ -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

@@ -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

@@ -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") 

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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") 

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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") 

@@ -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")

@@ -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")

@@ -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")

@@ -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

@@ -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

@@ -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

@@ -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

file too large to diff

@@ -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

@@ -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") 

@@ -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") 

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

file too large to diff

@@ -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")

@@ -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") 

@@ -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") 

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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") 

@@ -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") 

@@ -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")

@@ -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")

@@ -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")

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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") 

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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")

@@ -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")

@@ -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

@@ -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") 

@@ -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

@@ -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