packages feed

cpsa 2.3.4 → 2.3.5

raw patch · 80 files changed

+573/−93 lines, 80 filesnew-component:exe:cpsajson

Files

ChangeLog view
@@ -1,3 +1,34 @@+2014-09-05  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version): Tagged as version 2.3.5+++2014-09-02  John D. Ramsdell  <ramsdell@mitre.org>++	* src/unsorted.pl (decl_as_pairs):  Fixed bug in the case of+	variables of sort mesg.++2014-08-25  John D.  Ramsdell  <ramsdell@mitre.org>++	* 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  <ramsdell@mitre.org>++	* 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  <ramsdell@mitre.org>++	* 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  <ramsdell@mitre.org>  	* cpsa.cabal (Version): Tagged as version 2.3.4
NEWS view
@@ -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
cpsa.cabal view
@@ -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
doc/cpsadesign.pdf view

binary file changed (273513 → 273516 bytes)

doc/cpsaintroslides.pdf view

binary file changed (93144 → 93144 bytes)

doc/cpsaoverview.pdf view

binary file changed (128994 → 129002 bytes)

doc/cpsaprimer.pdf view

binary file changed (273718 → 273733 bytes)

doc/cpsaspec.pdf view

binary file changed (388829 → 388817 bytes)

doc/cpsaspec.tex view
@@ -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}
doc/cpsauser.html view
@@ -51,8 +51,13 @@ annotations to annotate shapes and generate protocol soundness obligations. The <a href="#cpsaparameters"><code>cpsaparameters</code></a> program detects some specification errors by performing a data flow analysis on protocol roles. The-<a href="#cpsapp"><code>cpsapp</code></a> program pretty prints its input using a-CPSA specific algorithm.</p>+<a href="#cpsapp"><code>cpsapp</code></a> program pretty prints its+input using a CPSA specific algorithm.  It also translates+S-Expressions into JavaScript Object Notation+(<a href="http://json.org">JSON</a>) to ease processing in other+languages.  The+<a href="#cpsajson"><code>cpsajson</code></a> program translates JSON+encoded CPSA into CPSA S-Expressions.</p>  <p>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 @@  <p>The axioms for Diffie-Hellman values are the usual ones for an   Abelian group for terms of sort <code>expr</code>.  For terms of-  sort <code>base</code>, <code>(exp h (one)) = h</code> and +  sort <code>base</code>, <code>(exp h (one)) = h</code> and <code>(exp (exp h x) y) = (exp h (mul x y)</code>.</p>  -->@@ -613,8 +618,10 @@  <h2 id="cpsapp">Pretty Printing</h2> -<p>The <code>cpsapp</code> program program pretty prints its input using the CPSA-specific algorithm.</p>+<p>The <code>cpsapp</code> program program pretty prints its input+using the CPSA specific algorithm.  It also translates S-Expressions+into JavaScript Object Notation (<a href="http://json.org">JSON</a>)+to ease processing in other languages.</p>  <h3>Usage</h3> @@ -629,6 +636,23 @@   -v       --version      show version number</pre> </blockquote> +<h2 id="cpsajson">JSON to S-Expression Translation</h2>++<p>The <code>cpsajson</code> program translates JSON encoded CPSA into+CPSA S-Expressions.</p>++<h3>Usage</h3>++<blockquote>+  <pre>$ 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</pre>+</blockquote>+ <h2>S-expressions</h2>  <p>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-"<code>-*/&lt;=&gt;!?:$%_&amp;~^</code>". A symbol may not begin with a+"<code>+-*/&lt;=&gt;!?:$%_&amp;~^</code>". 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
doc/macros.tex view
@@ -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
+ src/CPSA/JSON/Main.hs view
@@ -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"
src/CPSA/Lib/Cohort.hs view
@@ -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
src/CPSA/Lib/SExpr.hs view
@@ -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
src/CPSA/Lib/Strand.hs view
@@ -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
+ src/cpsajson.py view
@@ -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
+ src/split.py view
@@ -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()
src/unsorted.pl view
@@ -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).
tst/DH_hack.tst view
@@ -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")
tst/blanchet.tst view
@@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol"   (comment "There is a flaw in this protocol by design")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from blanchet.scm")  (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -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
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from crushing.scm")  (defprotocol crushing basic
tst/dass_simple.tst view
@@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from dass_simple.scm")  (defprotocol dass-simple basic
tst/denning-sacco.tst view
@@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from denning-sacco.scm")  (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -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
tst/deorig_mesg.tst view
@@ -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
tst/deorig_simple.tst view
@@ -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
tst/dy.tst view
@@ -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
tst/encsig.tst view
@@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example"   (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from encsig.scm")  (defprotocol mult-keys-enc-sig basic
tst/epmo-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from epmo-hash.scm")  (defprotocol epmo basic
tst/epmo-key-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from epmo-key-hash.scm")  (defprotocol epmo basic
tst/epmo.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from epmo.scm")  (defprotocol epmo basic
tst/epmo_acctnum-key-hash.tst view
@@ -2,7 +2,7 @@   "Electronic Purchase with Money Order Protocol Variant with Key Hashing"   (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from epmo_acctnum-key-hash.scm")  (defprotocol epmo_acctnum basic
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol"   (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from ffgg.scm")  (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -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
tst/hashtest-key-hash.tst view
@@ -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
tst/hashtest.tst view
@@ -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
tst/incompleteness_example.tst view
@@ -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
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from isoreject.scm")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from kelly1.scm")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from kerberos.scm")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from mass.lsp")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from mass2.lsp")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -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
tst/neuman-stubblebine-reauth.tst view
@@ -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
tst/neuman-stubblebine.tst view
@@ -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
tst/no_contraction.tst view
@@ -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
tst/non_transforming.tst view
@@ -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
tst/nonaug-prune.tst view
@@ -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
tst/ns-l.tst view
@@ -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
tst/ns.tst view
@@ -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
tst/nsl3.tst view
@@ -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
tst/nsl4cm1.tst view

file too large to diff

tst/nslsk.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from nslsk.scm")  (defprotocol nslsk basic
tst/or.tst view
@@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol"   (comment "Standard version using variables of sort mesg")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from or.scm")  (defprotocol or basic
tst/pca.tst view
@@ -1,7 +1,7 @@ (herald "Privacy Certificate Authority" (bound 15)   (comment "Generation of an Attestation Identity Certificate")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from pca.scm") (comment "Strand count bounded at 15")
tst/pen-non-orig-test.tst view
@@ -1,6 +1,6 @@ (herald "pen-non-orig test") -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from pen-non-orig-test.scm")  (defprotocol pennonorigtest basic
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from pkinit.scm")  (defprotocol pkinit basic
tst/preprocess.tst view
@@ -1,6 +1,6 @@ (herald "Pre-processing test example: modified NS with two responders") -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from preprocess.scm")  (defprotocol ns basic
tst/print.tst view
@@ -1,7 +1,7 @@ (herald "Print Test"   (comment "See if read forms look like printed ones")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from print.scm")  (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from pruning1.scm")  (defprotocol prune basic
tst/sigenc.tst view
@@ -1,7 +1,7 @@ (herald "Signed Encrypted Message Example"   (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from sigenc.scm")  (defprotocol mult-keys-sig-enc basic
tst/sorted_epmo_acctnum.tst view
@@ -4,7 +4,7 @@     "This version uses sorts to avoid confusion"     "between a nonce and other data")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from sorted_epmo_acctnum.scm") (comment "Strand count bounded at 12")
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from targetterms2.scm")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from targetterms6.scm")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from targetterms8.scm")  (defprotocol targetterms8 basic
tst/timestamping.tst view
@@ -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
tst/uncarried_keys.tst view
@@ -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
tst/uo.tst view
@@ -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
tst/wang-hash.tst view
@@ -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")
tst/wang-key-hash.tst view
@@ -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")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from weird.scm")  (defprotocol weird basic
tst/wide-mouth-frog-scyther.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol from Scyther"   (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from wide-mouth-frog-scyther.lsp")  (defprotocol wide-mouth-frog basic
tst/wide-mouth-frog.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol"   (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from wide-mouth-frog.lsp")  (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,6 +1,6 @@ (herald wonthull (bound 9)) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from wonthull.scm") (comment "Strand count bounded at 9")
tst/wonthull2.tst view
@@ -1,6 +1,6 @@ (herald wonthull2 (bound 9)) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from wonthull2.scm") (comment "Strand count bounded at 9")
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from wonthull3.scm")  (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from woolam.scm")  (defprotocol woolam basic
tst/yahalom-6.3.6.tst view
@@ -5,7 +5,7 @@   (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")   (bound 15)) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from yahalom-6.3.6.scm") (comment "Strand count bounded at 15")
tst/yahalom.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding" (bound 15)) -(comment "CPSA 2.3.4")+(comment "CPSA 2.3.5") (comment "All input read from yahalom.scm") (comment "Strand count bounded at 15")