diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,34 @@ +2014-09-05 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.3.5 + + +2014-09-02 John D. Ramsdell + + * src/unsorted.pl (decl_as_pairs): Fixed bug in the case of + variables of sort mesg. + +2014-08-25 John D. Ramsdell + + * src/split.py: Added the skeleton split program that copies the + skeletons in a CPSA source file into separate files. + +2014-08-23 John D. Ramsdell + + * src/cpsajson.py (load): Added a reader in Python for JSON + produced by CPSA's pretty printer program cpsa3pp -j. + +2014-08-21 John D. Ramsdell + + * src/CPSA/JSON/Main.hs: Added the program cpsajson that + translates JSON encoded CPSA into CPSA S-Expressions. It expects + the JSON input to follow the conventions of the JSON produced by + the cpsapp program when given the -j option. + + * src/CPSA/Lib/SExpr.hs (numOrSym): Enabled parsing a number with + a plus sign by removing the sign before translating the string of + digits into a number. + 2014-06-06 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 2.3.4 diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,18 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.3.5 + +** Added a translator from JSON to CPSA S-Expressions + + When given the -j option, the program cpsapp translates + S-Expressions into JavaScript Object Notation (JSON) to ease + processing in other languages. The new program cpsajson translates + JSON encoded CPSA into CPSA S-Expressions. + + An example of using JSON for input and output in Python is in + src/split.pl. This program copies the skeletons in a CPSA source + file into separate files. + * Changes in version 2.3.4 ** Splicing added to macros diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.3.4 +Version: 2.3.5 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -57,12 +57,13 @@ doc/cpsadiagrams.mp doc/strands.mp doc/cmstrands.mp doc/carriers.mp doc/termtree.mp doc/blanchet.mp doc/mitrelogo.mp doc/cpsa.bib doc/SDAG.lhs - src/index.html src/cpsacgi src/cpsacgi.py src/cpsa2svg src/cpsa.el - src/httpd_allow_execmem.te src/cpsaperm.scm src/cpsaops.scm - src/preskel src/cpsa.pl src/unsorted.pl src/pp.pl src/sexpr.pl src/perm.pl - src/prover9.pl src/zoom.js src/js2hs src/ghcmemlimit build.xml - src/cpsaextras/Main.scala src/cpsaextras/Pretty.scala - src/cpsaextras/Printer.scala src/cpsaextras/SExpr.scala + src/index.html src/cpsacgi src/cpsacgi.py src/cpsajson.py src/split.py + src/cpsa2svg src/cpsa.el src/httpd_allow_execmem.te src/cpsaperm.scm + src/cpsaops.scm src/preskel src/cpsa.pl src/unsorted.pl src/pp.pl + src/sexpr.pl src/perm.pl src/prover9.pl src/zoom.js src/js2hs + src/ghcmemlimit build.xml src/cpsaextras/Main.scala + src/cpsaextras/Pretty.scala src/cpsaextras/Printer.scala + src/cpsaextras/SExpr.scala tst/README tst/Makefile tst/Make.hs tst/checktst tst/cpsagraphall tst/cpsashapesall tst/blanchet.scm tst/blanchet.tst tst/completeness-test.scm @@ -186,6 +187,18 @@ Executable cpsapp Main-Is: CPSA/Pretty/Main.hs + Build-Depends: base >= 3 && < 5, containers + GHC-Options: + -Wall -fno-warn-name-shadowing -fwarn-unused-imports + Hs-Source-Dirs: src + Other-Modules: + Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr + CPSA.Lib.Printer CPSA.Lib.Notation CPSA.Lib.Entry CPSA.Lib.Algebra + CPSA.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader + CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.CPSA + +Executable cpsajson + Main-Is: CPSA/JSON/Main.hs Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports 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/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/cpsaspec.tex b/doc/cpsaspec.tex --- a/doc/cpsaspec.tex +++ b/doc/cpsaspec.tex @@ -2074,12 +2074,12 @@ are carried, which are protected, and which sorts are atoms can be defined in terms of the inferences available. -\chapter{Shape Analysis and First-Order Logic}\label{chp:logic} +\chapter{Shape Analysis Sentences}\label{chp:logic} For each point-of-view skeleton and its shapes found by {\cpsa}, there is a formula in the language of order-sorted first-order logic called a \index{shape analysis sentence}\emph{shape analysis sentence,} often -shortened to a shape sentence~\cite{ramsdell12}. The sentence has a +shortened to a shape sentence. The sentence has a special form, $\all{X}(\Psi\supset\bigvee_i\some{Y_i}(\Delta_i\wedge\Phi_i))$, where~$\Psi$ and~$\Phi_i$ are conjunctions of atomic formulas and~$X$ @@ -2094,7 +2094,9 @@ all of the shapes and the homomorphisms associated with a point-of-view skeleton, the analysis' shape sentence is satisfied in all realized skeletons. Shape sentences are closely related to -security goals~\cite{guttman09}, and motivated by that work. +security goals~\cite{guttman09}, and were motivated by that work. +This material was extracted from~\cite{ramsdell12}, the paper that +introduced shape analysis sentences. \section{Shape Formulas} diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -51,8 +51,13 @@ annotations to annotate shapes and generate protocol soundness obligations. The cpsaparameters program detects some specification errors by performing a data flow analysis on protocol roles. The -cpsapp program pretty prints its input using a -CPSA specific algorithm.

+cpsapp program pretty prints its +input using a CPSA specific algorithm. It also translates +S-Expressions into JavaScript Object Notation +(JSON) to ease processing in other +languages. The +cpsajson program translates JSON +encoded CPSA into CPSA S-Expressions.

The input syntax is essentially the same as the output syntax. A Lisp aware editor will pretty print input, and the output is pretty printed. We use Emacs' @@ -270,7 +275,7 @@

The axioms for Diffie-Hellman values are the usual ones for an Abelian group for terms of sort expr. For terms of - sort base, (exp h (one)) = h and + sort base, (exp h (one)) = h and (exp (exp h x) y) = (exp h (mul x y).

--> @@ -613,8 +618,10 @@

Pretty Printing

-

The cpsapp program program pretty prints its input using the CPSA -specific algorithm.

+

The cpsapp program program pretty prints its input +using the CPSA specific algorithm. It also translates S-Expressions +into JavaScript Object Notation (JSON) +to ease processing in other languages.

Usage

@@ -629,6 +636,23 @@ -v --version show version number +

JSON to S-Expression Translation

+ +

The cpsajson program translates JSON encoded CPSA into +CPSA S-Expressions.

+ +

Usage

+ +
+ 
$ cpsajson -h
+Usage: cpsajson [OPTIONS] [FILE]
+  -o FILE  --output=FILE  output FILE
+  -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
+
+

S-expressions

The S-expressions used are restricted so that most dialects of Lisp @@ -636,7 +660,7 @@ 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 the special characters in -"-*/<=>!?:$%_&~^". A symbol may not begin with a +"+-*/<=>!?:$%_&~^". 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. Double quotes delimit a string. A comment begins with a 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.3.4} +\newcommand{\version}{2.3.5} \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/JSON/Main.hs b/src/CPSA/JSON/Main.hs new file mode 100644 --- /dev/null +++ b/src/CPSA/JSON/Main.hs @@ -0,0 +1,326 @@ +-- Translate JSON encoded CPSA into CPSA S-Expressions + +-- Copyright (c) 2014 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 Main (main) where + +import Numeric +import Data.Char (isSpace, isDigit, isPrint) +import System.IO +import System.Environment +import System.Console.GetOpt +import CPSA.Lib.CPSA +import CPSA.Lib.Entry + +-- Runtime parameters + +data Params = Params + { file :: Maybe FilePath, -- Nothing specifies standard output + prefix :: Bool, -- Use prefix notation? + margin :: Int } -- Output line length + deriving Show + +indent :: Int +indent = optIndent defaultOptions + +main :: IO () +main = + do + (p, params) <- jStart options interp + h <- outputHandle $ file params + let printer = if prefix params then pp else printItem + go (writeCpsaLn (printer (margin params) indent) h) p + hClose h + +writeCpsaLn :: (SExpr a -> String) -> Handle -> SExpr a -> IO () +writeCpsaLn printer h sexpr = + do + hPutStrLn h $ printer sexpr + hPutStrLn h "" + +go :: (SExpr () -> IO ()) -> Handle -> IO () +go f p = + loop + where + loop = + do + x <- jRead p + case x of + Nothing -> + return () + Just sexpr -> + do + f sexpr + loop + +-- Command line option flags +data Flag + = Help -- Help + | Info -- Version information + | Margin String -- Output line length + | Infix -- Select output notation + | Output String -- Output file name + deriving Show + +defaultMargin :: Int +defaultMargin = optMargin defaultOptions + +options :: [OptDescr Flag] +options = + [ Option ['o'] ["output"] (ReqArg Output "FILE") "output FILE", + Option ['m'] ["margin"] (ReqArg Margin "INT") + ("set output margin (default " ++ show defaultMargin ++ ")"), + Option ['i'] ["infix"] (NoArg Infix) "output uses infix notation", + Option ['h'] ["help"] (NoArg Help) "show help message", + Option ['v'] ["version"] (NoArg Info) "show version number" ] + +-- Interpret option flags +interp :: [Flag] -> IO Params +interp flags = + loop flags (Params { file = Nothing, -- By default, no output file + prefix = True, + margin = defaultMargin }) + where + loop [] params = return params + loop (Output name : flags) params + | file params == Nothing = + loop flags $ params { file = Just name } + loop (Infix : flags) params = + loop flags $ params { prefix = False } + loop (Margin value : flags) params = + case readDec value of + [(margin, "")] -> + loop flags $ params { margin = margin } + _ -> + do + msg <- usage options ["Bad value for margin\n"] + abort msg + loop (Info : _) _ = + success cpsaVersion + loop (Help : _) _ = + do -- Show help then exit with success + msg <- usage options [] + success msg + loop _ _ = + do -- Show help then exit with failure + msg <- usage options ["Bad option combination\n"] + abort msg + +-- Returns the input S-expression and an interpretation of the command +-- line options. +jStart :: [OptDescr a] -> ([a] -> IO b) -> IO (Handle, b) +jStart options interp = + do + argv <- getArgs + (flags, files) <- opts options argv + opts <- interp flags + p <- openInput options files + return (p, opts) + +opts :: [OptDescr a] -> [String] -> IO ([a], [String]) +opts options argv = + case getOpt RequireOrder options argv of + (o, n, []) -> return (o, n) + (_, _, errs) -> + do + msg <- usage options errs + abort msg + +openInput :: [OptDescr a] -> [String] -> IO Handle +openInput _ [file] = + openFile file ReadMode -- Input from named file +openInput _ [] = + return stdin -- Input from the standard input +openInput options _ = + do + msg <- usage options ["too many input files\n"] + abort msg + +-- Read a JSON expression, and fail on error +jRead :: Handle -> IO (Maybe (SExpr ())) +jRead p = + do + x <- tryIO (jLoad p) + case x of + Right x -> + return x + Left err -> + abort err + +-- The result of scanning is a token. +data Token + = Atom (SExpr ()) + | Lparen + | Rparen + | Eof + +-- Top level parser +jLoad :: Handle -> IO (Maybe (SExpr ())) +jLoad h = + do + t <- scan h + case t of + Atom x -> + return $ Just x + Lparen -> + do + x <- list h [] + return $ Just x + Rparen -> + abort "Close of unopened list" + Eof -> + do + hClose h + return Nothing + +-- A recursive decent parser +list :: Handle -> [SExpr ()] -> IO (SExpr ()) +list h xs = + do + t <- scan h + case t of + Rparen -> + return (L () (seqrev xs)) + Atom x -> + list h (x : xs) + Lparen -> + do + x <- list h [] + list h (x : xs) + Eof -> + abort "Unexpected end of input in list" + +-- Read the next character returning Nothing on EOF +get :: Handle -> IO (Maybe Char) +get h = + do + eof <- hIsEOF h + case eof of + True -> + return Nothing + False -> + do + ch <- hGetChar h + return $ Just ch + +-- Peek at the next character returning Nothing on EOF +peek :: Handle -> IO (Maybe Char) +peek h = + do + eof <- hIsEOF h + case eof of + True -> + return Nothing + False -> + do + ch <- hLookAhead h + return $ Just ch + +-- Return the next token +scan :: Handle -> IO (Token) +scan h = + do + ch <- get h + case ch of + Nothing -> + return Eof + Just ch -> + skip h ch + +-- Skip whitespace and then handle first character of a token +skip :: Handle -> Char -> IO (Token) +skip h ',' = scan h -- Treat comma as white space +skip h ch | isSpace ch = scan h +skip _ '[' = + return Lparen +skip _ ']' = + return Rparen +skip h ch = + atom h ch + +-- Scan a string, number, or a symbol +atom :: Handle -> Char -> IO (Token) +atom h '"' = string h [] +atom h '+' = sign h True +atom h '-' = sign h False +atom h ch | isDigit ch = number h [ch] +atom _ _ = abort "Bad char in atom" + +-- Scan a quoted string of characters +string :: Handle -> String -> IO (Token) +string h s = + do + ch <- get h + case ch of + Nothing -> + abort "End of input in string" + Just '"' -> + symOrStr s + Just '\\' -> + quote h s + Just ch | isPrint ch -> + string h (ch : s) + Just _ -> + abort "Bad char for string" + +-- Handle backslash in string +quote :: Handle -> String -> IO (Token) +quote h s = + do + ch <- get h + case ch of + Nothing -> + abort "End of input in string" + Just ch | isPrint ch -> + string h (ch : s) + Just _ -> + abort "Bad char for string" + +-- Is string a symbol or a quoted string? +symOrStr :: String -> IO (Token) +symOrStr ('"' : s) = + case seqrev s of + '"' : str -> + return $ Atom (Q () str) + _ -> + abort "Quote in symbol" +symOrStr s = + return $ Atom (S () $ seqrev s) + +-- A reverse that evaluates the list elements. +seqrev :: [a] -> [a] +seqrev l = + foldl (\xs x -> x `seq` xs `seq` (x:xs)) [] l + +-- Scan a sequence of digits +number :: Handle -> String -> IO (Token) +number h s = + do + ch <- peek h + case ch of + Nothing -> + return (Atom (N () (read (seqrev s)))) + Just ch | isDigit ch -> + do + _ <- hGetChar h + number h (ch : s) + Just _ -> + return (Atom (N () (read (seqrev s)))) + +-- Scan a number that starts with a sign +sign :: Handle -> Bool -> IO (Token) +sign h plus = + do + ch <- get h + case ch of + Nothing -> + abort "Sign followed by EOF" + Just ch | isDigit ch -> + let s = if plus then [ch] else [ch, '-'] in + number h s + Just _ -> + abort "Sign not followed by a digit" diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs --- a/src/CPSA/Lib/Cohort.hs +++ b/src/CPSA/Lib/Cohort.hs @@ -94,7 +94,7 @@ Nothing -> (acc, ns) Just t -> let ns' = addSendingBefore ns n - ts = S.map (evtTerm . event) ns' in + ts = termsInNodes ns' in case derivable a ts t of True -> (acc, ns') False -> (graphNode n : acc, ns') @@ -112,6 +112,10 @@ Nothing -> s Just _ -> S.insert n s +termsInNodes :: Algebra t p g s e c => Set (Vertex t e) -> Set t +termsInNodes ns = + S.map (evtTerm . event) ns + -- Returns that atoms that cannot be guess when determining if a -- term is derivable from some other terms, and the atoms that -- uniquely originate in this skeleton. @@ -170,7 +174,7 @@ mappedTargetTerms = S.map (substitute subst) (targetTerms ct escape) targetTermsDiff = S.difference (targetTerms ct' escape') mappedTargetTerms vs = addSendingBefore S.empty v - ts = S.map (evtTerm . event) vs -- Outbound predecessors + ts = termsInNodes vs -- Outbound predecessors (a, _) = avoid k maybeSolved :: Algebra t p g s e c => t -> p -> [t] -> Set t -> @@ -244,7 +248,7 @@ Nothing -> loop nodes Just t -> let ns = addSendingBefore S.empty n - ts = S.map (evtTerm . event) ns -- Public messages + ts = termsInNodes ns -- Public messages der = derivable a ts in -- Derivable before node if der t then loop nodes 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 @@ -246,7 +246,10 @@ Nothing -> symbol p l c pos s Just ch | isDigit ch -> - number p l c pos s + if s == "+" then + number p l c pos [] + else + number p l c pos s Just _ -> symbol p l c pos s diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -188,8 +188,7 @@ loop c c' env loop _ _ _ = [] -makeInstance :: Algebra t p g s e c => Role t -> e -> - Trace t -> Instance t e +makeInstance :: Role t -> e -> Trace t -> Instance t e makeInstance role env trace = Instance { role = role, env = env, @@ -225,7 +224,7 @@ listenerTerm :: Algebra t p g s e c => Instance t e -> Maybe t listenerTerm inst = case rname (role inst) of - "" -> Just $ evtTerm (trace inst !! 0) -- Get first term in trace + "" -> inbnd (trace inst !! 0) -- Get first term in trace _ -> Nothing -- Not a listener strand -- Nodes, Pairs, and Graphs @@ -602,16 +601,13 @@ -- The terms used in the strands in this preskeleton. -- Should this return a set, or a multiset? -kterms :: Algebra t p g s e c => Preskel t g s e -> [t] +kterms :: Eq t => Preskel t g s e -> [t] kterms k = iterms (insts k) -- The terms used in a list of instances. -iterms :: Algebra t p g s e c => [Instance t e] -> [t] +iterms :: Eq t => [Instance t e] -> [t] iterms insts = - foldl addSTerms [] insts - where - addSTerms ts s = - foldl (flip $ adjoin . evtTerm) ts (trace s) + L.nub [evtTerm evt | i <- insts, evt <- trace i] -- The node orderings form an acyclic order if there are no cycles. -- Use depth first search to detect cycles. A graph with no node with diff --git a/src/cpsajson.py b/src/cpsajson.py new file mode 100644 --- /dev/null +++ b/src/cpsajson.py @@ -0,0 +1,22 @@ +# Reader for JSON produced by CPSA's pretty printer program. +# John D. Ramsdell -- August 2014 + +import json + +# Read a file containing a sequence of json objects produced by cpsa's +# pretty printer. Assumes each object is terminated by a blank line. +def load(f): + xs = [] # List of objects read + buf = "" + while True: + l = f.readline() + if l == "": # End of file + if len(buf) > 0: # Extract JSON object from buf + xs.append(json.loads(buf)) + return xs + elif l == "\n": # Blank line + if len(buf) > 0: # Extract JSON object from buf + xs.append(json.loads(buf)) + buf = "" + else: + buf += l # Append line to buf diff --git a/src/split.py b/src/split.py new file mode 100644 --- /dev/null +++ b/src/split.py @@ -0,0 +1,46 @@ +#!/usr/bin/env python3 + +# Skeleton split +# John D. Ramsdell -- August 2014 + +# Copies the skeletons in a CPSA source file into separate files. +# +# If the source filename is root.json, it creates file root_N.json, +# where root_N.json contains the nth skeleton in the source file. +# +# Use cpsapp -j to translate the source file into JSON. Use cpsajson +# to translate the output files into CPSA S-Expressions. + +import sys +import os.path +import json +import cpsajson + +def main(): + if len(sys.argv) != 2: # Ensure one file name supplied + print("Usage: " + sys.argv[0] + " file") + fname = sys.argv[1] + (root, ext) = os.path.splitext(fname) + f = open(fname, 'r') + xs = cpsajson.load(f) + f.close() + i = 0 # Skeleton number + pd = {} # Protocol dictionary + h = [] # Herald form + for x in xs: + if x[0] == "herald": + h = x # Store herald + elif x[0] == "defprotocol": + pd[x[1]] = x # Store protocol + elif x[0] == "defskeleton": + p = pd[x[1]] # Look up protocol + f = open(root + "_" + str(i) + ext, 'w') + i += 1 + if h: # Dump herald (maybe) + json.dump(h, f) + json.dump(p, f) # Dump protocol + json.dump(x, f) # Dump skeleton + f.close() + +if __name__ == "__main__": + main() diff --git a/src/unsorted.pl b/src/unsorted.pl --- a/src/unsorted.pl +++ b/src/unsorted.pl @@ -66,9 +66,9 @@ decl_as_pairs([], _, Decls, VarMap) :- decls_as_pairs(Decls, VarMap). -decl_as_pairs(_, mesg, Decls, VarMap) :- +decl_as_pairs([Var|Vars], mesg, Decls, [(Var, Var)|VarMap]) :- !, - decls_as_pairs(Decls, VarMap). + decl_as_pairs(Vars, mesg, Decls, VarMap). decl_as_pairs([Var|Vars], Sort, Decls, [(Var, Term)|VarMap]) :- Term =.. [Sort, Var], decl_as_pairs(Vars, Sort, Decls, VarMap). 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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (comment "All input read from fragile_pruning.scm") (defprotocol fragile_pruning 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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (comment "All input read from uncarried_keys.scm") (defprotocol uncarried-keys 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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (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.3.4") +(comment "CPSA 2.3.5") (comment "All input read from yahalom.scm") (comment "Strand count bounded at 15")