packages feed

cpsa 2.2.9 → 2.2.10

raw patch · 89 files changed

+681/−107 lines, 89 files

Files

ChangeLog view
@@ -1,3 +1,21 @@+2012-06-28  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version):  Tagged as version 2.2.10.++	* src/CPSA/Lib/Entry.hs (tryIO): Made error option in return value+	a string so that error messages are correctly parsed Emacs.++2012-06-06  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Entry.hs (tryIO): The use of System.IO.Error.try+	has been deprecated, so CPSA.LIB.Entry now exports a replacement.++2012-06-06  John D. Ramsdell  <ramsdell@mitre.org>++	* {doc,tst}/Make.hs: Changed imports so that ExitCode and system+	come from System.Exit and System.process, not System, which is+	part of the haskell98 package that is now hidden by default.+ 2012-05-25  John D. Ramsdell  <ramsdell@mitre.org>  	* cpsa.cabal (Version):  Tagged as version 2.2.9.
NEWS view
@@ -1,5 +1,11 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.10++** The Make.hs program now works with latest Haskell Platform+   The imports have been changed so that it no longer uses the+   haskell98 package, which is now hidden by default.+ * Changes in version 2.2.9  ** Penetrator non-origination assumptions added
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.2.9+Version:		2.2.10 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3@@ -103,6 +103,8 @@   tst/wang-key-hash.scm tst/wang-key-hash.tst tst/wang-hash.scm   tst/wang-hash.tst tst/mass.lsp tst/mass.tst tst/mass2.lsp tst/mass2.tst   tst/DH_hack.scm tst/DH_hack.tst tst/timestamping.scm tst/timestamping.tst+  tst/ns-l.scm tst/ns-l.tst tst/pen-non-orig-test.scm+  tst/pen-non-orig-test.tst tst/preprocess.scm tst/preprocess.tst  -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry.
doc/Make.hs view
@@ -63,7 +63,8 @@ import Control.Monad (mapM_) import Data.List (sort) import Data.IORef (IORef, newIORef, readIORef, writeIORef)-import System (ExitCode (..), system)+import System.Exit (ExitCode (..))+import System.Process (system) import System.IO (putStrLn) import System.IO.Unsafe (unsafePerformIO) import System.FilePath (FilePath, splitExtension)
doc/cpsa.bib view
@@ -327,3 +327,13 @@     pages = {325--339},     publisher = {Springer-Verlag} }++@Unpublished{ramsdell12,+  author = 	 {John D. Ramsdell},+  title = 	 {Deducing Security Goals From Shape Analysis Sentences},+  note = 	 {\url{http://arxiv.org/abs/1204.0480}},+  OPTkey = 	 {},+  month = 	 apr,+  year = 	 2012,+  OPTannote = 	 {}+}
doc/cpsadesign.pdf view

binary file changed (203159 → 203156 bytes)

doc/cpsadha.pdf view

binary file changed (129997 → 129993 bytes)

doc/cpsaoverview.pdf view

binary file changed (76120 → 76306 bytes)

doc/cpsaprimer.pdf view

binary file changed (187383 → 187208 bytes)

doc/cpsaspec.pdf view

binary file changed (328419 → 329325 bytes)

doc/cpsaspec.tex view
@@ -2101,15 +2101,16 @@ 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.  The sentence has a special form,+shortened to a shape sentence~\cite{ramsdell12}.  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$ and~$Y_i$ are variable sets.  This fragment of first-order logic is called coherent logic.  Formula~$\Psi$ describes the point-of-view skeleton~$k_0$.  For each homomorphism to a shape, $k_0\homomorphism{\delta_i}k_i$, formula~$\Delta_i$ describes the-structure preserving maps~$\delta_i$, and the shape~$k_i$ is-described by~$\Phi_i$.+structure preserving maps~$\delta_i$, and the shape~$k_i$ is described+by~$\Phi_i$.  An interpretation of a shape sentence is a skeleton.  If {\cpsa} finds all of the shapes and the homomorphisms associated with a
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.2.9}+\newcommand{\version}{2.2.10} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
src/CPSA/Annotations/Main.hs view
@@ -12,7 +12,6 @@ module Main (main) where  import System.IO-import System.IO.Error import CPSA.Lib.CPSA import CPSA.Lib.Entry import CPSA.Annotations.Annotations@@ -72,11 +71,11 @@         SExpr Pos -> IO [Prot t p g s e c] step output name origin margin ps sexpr =     do-      x <- try (annotations name origin ps sexpr)+      x <- tryIO (annotations name origin ps sexpr)       case x of         Right (ps, sexpr) ->             do               writeLnSEexpr output margin sexpr               return ps         Left err ->-            abort (ioeGetErrorString err)+            abort (show err)
src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs view
@@ -16,7 +16,7 @@  {-# LANGUAGE MultiParamTypeClasses, CPP #-} -#define INTERACTIVE_DEBUGGING+-- #define INTERACTIVE_DEBUGGING  module CPSA.DiffieHellmanNoReciprocal.Algebra (name, origin #if defined INTERACTIVE_DEBUGGING@@ -26,7 +26,7 @@  #if defined INTERACTIVE_DEBUGGING import System.IO(stdin)-import System.IO.Error(try)+import Control.Exception(try) #endif  import Control.Monad (foldM)@@ -74,6 +74,9 @@ -- Both functions request a declaration and then two terms. -- Example: ((x y z expn)) (mul x x y) z #if defined INTERACTIVE_DEBUGGING+tryIO :: IO a -> IO (Either IOError a)+tryIO x = try x+ iUnify :: IO [Subst] iUnify =     iRun f emptySubst@@ -83,7 +86,7 @@ iMatch :: IO [Env] iMatch =     do-      ans <- try (iRun aMatch emptyEnv)+      ans <- tryIO (iRun aMatch emptyEnv)       case ans of         Right ans -> return ans         Left err -> fail (show err)@@ -115,7 +118,7 @@ load =     do       h <- C.posHandle "" stdin-      content <- try (C.load h)+      content <- tryIO (C.load h)       case content of         Left msg ->             do
src/CPSA/Graph/Main.hs view
@@ -10,7 +10,6 @@  import Numeric import System.IO-import System.IO.Error import System.Console.GetOpt import CPSA.Lib.CPSA (PosHandle, SExpr, Pos) import CPSA.Lib.Entry@@ -46,9 +45,9 @@ loadAll :: PosHandle -> Params -> IO () loadAll p params =     do-      preskels <- try (loadDefs p)+      preskels <- tryIO (loadDefs p)       case preskels of-        Left err -> abort (ioeGetErrorString err)+        Left err -> abort (show err)         Right (cmts, preskels) ->             do               h <- outputHandle (file params)@@ -85,28 +84,28 @@ treeless :: PosHandle -> Params -> IO () treeless p params =     do-      preskel <- try (loadFirst p)+      preskel <- tryIO (loadFirst p)       case preskel of-        Left err -> abort (ioeGetErrorString err)+        Left err -> abort (show err)         Right (cmts, preskel, state) ->             do               h <- outputHandle (file params)               hPutStrLn h "<?xml version=\"1.0\"?>"               hPutStrLn h ("<!-- " ++ cpsaVersion ++ " -->")               let conf = config (prefix params) (scripted params) False-              ans <- try (treelessView h conf (margin params)-                                       cmts preskel state)+              ans <- tryIO (treelessView h conf (margin params)+                                         cmts preskel state)               case ans of-                Left err -> abort (ioeGetErrorString err)+                Left err -> abort (show err)                 Right () -> return ()  -- LaTeX graphing. latex :: PosHandle -> Params -> IO () latex p params =     do-      preskel <- try (loadFirst p)+      preskel <- tryIO (loadFirst p)       case preskel of-        Left err -> abort (ioeGetErrorString err)+        Left err -> abort (show err)         Right (cmts, preskel, state) ->             do               h <- outputHandle (file params)@@ -114,9 +113,9 @@               hPutStrLn h ("% " ++ cpsaVersion)               let conf = config (prefix params) (scripted params) False               let pp = printer conf-              ans <- try (latexView h (margin params) pp cmts preskel state)+              ans <- tryIO (latexView h (margin params) pp cmts preskel state)               case ans of-                Left err -> abort (ioeGetErrorString err)+                Left err -> abort (show err)                 Right () -> return ()  -- Command line option flags
src/CPSA/Lib/Entry.hs view
@@ -11,11 +11,12 @@                        filterOptions, filterInterp, readSExpr,                        gentlyReadSExpr, outputHandle, writeSExpr,                        writeLnSEexpr, cpsaVersion, comment,-                       writeComment) where+                       writeComment, tryIO) where  import Numeric+import Control.Exception (try) import System.IO-import System.IO.Error+import System.IO.Error (ioeGetErrorString) import System.Environment import System.Console.GetOpt import System.Exit@@ -243,23 +244,34 @@ readSExpr :: PosHandle -> IO (Maybe (SExpr Pos)) readSExpr p =     do-      x <- try (load p)+      x <- tryIO (load p)       case x of         Right x ->             return x         Left err ->-            abort (ioeGetErrorString err)+            abort err  -- Read an S-expression, and gently fail on error by printing the -- error message to standard error and returning EOF. gentlyReadSExpr :: PosHandle -> IO (Maybe (SExpr Pos)) gentlyReadSExpr p =     do-      x <- try (load p)+      x <- tryIO (load p)       case x of         Right x ->             return x         Left err ->             do-              hPutStrLn stderr (ioeGetErrorString err)+              hPutStrLn stderr (show err)               return Nothing++-- Exception handling for IO errors+tryIO :: IO a -> IO (Either String a)+tryIO x = +    do +      y <- try x+      case y of+        Right x ->+            return (Right x)+        Left err ->+            return (Left (ioeGetErrorString err))
src/CPSA/Lib/Main.hs view
@@ -11,7 +11,6 @@ import Numeric import Control.Monad (forM_) import System.IO-import System.IO.Error import System.Environment import System.Console.GetOpt import CPSA.Lib.SExpr@@ -55,9 +54,9 @@       forM_ heraldFlags checkHeraldFlag       opts <- interp algs defaultOptions heraldFlags       opts <- interp algs opts flags-      sexprs <- try (expand sexprs) -- Expand macros+      sexprs <- tryIO (expand sexprs) -- Expand macros       case sexprs of-        Left err -> abort (ioeGetErrorString err)+        Left err -> abort err         Right sexprs ->             if optAnalyze opts then                 select herald opts sexprs@@ -130,9 +129,9 @@       Options -> [SExpr Pos] -> IO () go name origin herald opts sexprs =     do-      preskels <- try (loadSExprs name origin sexprs)+      preskels <- tryIO (loadSExprs name origin sexprs)       case preskels of          -- Load protocols and preskeletons-        Left err -> abort (ioeGetErrorString err)+        Left err -> abort err         Right preskels ->             do               h <- outputHandle (optFile opts)
src/CPSA/Logic/Main.hs view
@@ -9,7 +9,6 @@ module Main (main) where  import System.IO-import System.IO.Error import CPSA.Lib.CPSA import CPSA.Lib.Entry import CPSA.Logic.Logic@@ -78,7 +77,7 @@            return state step output name origin margin state sexpr =     do-      x <- try (logic name origin state sexpr)+      x <- tryIO (logic name origin state sexpr)       case x of         Right (acc, Nothing) ->             after output margin acc sexpr@@ -87,7 +86,7 @@               writeLnSEexpr output margin x               after output margin acc sexpr         Left err ->-            abort (ioeGetErrorString err)+            abort (show err)  after :: Algebra t p g s e c => Handle -> Int -> State t p g s e c ->          Maybe (SExpr Pos) -> IO (State t p g s e c)
src/CPSA/Parameters/Main.hs view
@@ -12,7 +12,6 @@ module Main (main) where  import System.IO-import System.IO.Error import CPSA.Lib.CPSA import CPSA.Lib.Entry import CPSA.Parameters.Flow@@ -69,9 +68,9 @@         String -> g -> Int -> SExpr Pos -> IO () step output name origin margin sexpr =     do-      sexpr <- try (dataFlow name origin sexpr)+      sexpr <- tryIO (dataFlow name origin sexpr)       case sexpr of         Right sexpr ->             writeLnSEexpr output margin sexpr         Left err ->-            abort (ioeGetErrorString err)+            abort (show err)
src/CPSA/Shapes/Main.hs view
@@ -12,7 +12,6 @@ module Main (main) where  import System.IO-import System.IO.Error import CPSA.Lib.CPSA (PosHandle, SExpr, Pos) import CPSA.Lib.Entry import CPSA.Shapes.Shapes@@ -45,7 +44,7 @@ step :: Handle -> Int -> Map -> SExpr Pos -> IO Map step output margin acc sexpr =     do-      x <- try (shape acc sexpr)+      x <- tryIO (shape acc sexpr)       case x of         Right (acc, sexpr) ->             case sexpr of@@ -56,4 +55,4 @@                     writeLnSEexpr output margin sexpr                     return acc         Left err ->-            abort (ioeGetErrorString err)+            abort (show err)
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read") (comment "Strand count bounded at 15")
tst/Make.hs view
@@ -63,7 +63,8 @@ import Control.Monad (mapM_) import Data.List (sort) import Data.IORef (IORef, newIORef, readIORef, writeIORef)-import System (ExitCode (..), system)+import System.Exit (ExitCode (..))+import System.Process (system) import System.IO (putStrLn) import System.IO.Unsafe (unsafePerformIO) import System.FilePath (FilePath, splitExtension)
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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol crushing basic
tst/dass_simple.tst view
@@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol dass-simple basic
tst/denning-sacco.tst view
@@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol deorig-contract basic
tst/deorig_mesg.tst view
@@ -1,6 +1,6 @@ (herald deorig-mesg) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol deorig-mesg basic
tst/deorig_simple.tst view
@@ -1,6 +1,6 @@ (herald deorig-simple) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol deorig-simple basic
tst/dh_cert.tst view
@@ -1,6 +1,6 @@ (herald "Diffie-Hellman with Certificate" (algebra diffie-hellman)) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol dh-cert diffie-hellman
tst/dhke.tst view
@@ -1,6 +1,6 @@ (herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman)) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol dhke diffie-hellman
tst/dy.tst view
@@ -1,6 +1,6 @@ (herald "Example 1.3 from 1983 Dolev-Yao Paper") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol epmo_acctnum basic
tst/epmo_acctnum.tst view

file too large to diff

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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol fragile_pruning basic
tst/hashtest-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol hashtest basic
tst/hashtest.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol hashtest basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol missing-contraction basic
tst/neuman-stubblebine-reauth.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol neuman-stubblebine-reauth basic
tst/neuman-stubblebine.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol neuman-stubblebine basic
tst/no_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol no-contraction basic
tst/non_transforming.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol non_transforming basic
tst/nonaug-prune.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol nonaug-prune basic
+ tst/ns-l.scm view
@@ -0,0 +1,38 @@+(herald "Needham-Schroeder-Low Public-Key Protocol"+	(comment "With deflistener's"))++;;; Used to generate output for inclusion in the primer.+;;; Use margin = 60 (-m 60) to generate the output.++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace+     (send (enc n1 a (pubk b)))+     (recv (enc b n1 n2 (pubk a)))+     (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace+     (recv (enc n1 a (pubk b)))+     (send (enc b n1 n2 (pubk a)))+     (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder"))++;;; The initiator point-of-view+(defskeleton ns+  (vars (a b name) (n1 text))+  (defstrand init 3 (a a) (b b) (n1 n1))+  (deflistener n1)+  (non-orig (privk b) (privk a))+  (uniq-orig n1)+  (comment "Initiator point-of-view with a listener"))++;;; The responder point-of-view+(defskeleton ns+  (vars (a name) (n2 text))+  (defstrand resp 3 (a a) (n2 n2))+  (deflistener n2)+  (non-orig (privk a))+  (uniq-orig n2)+  (comment "Responder point-of-view with a listener"))
+ tst/ns-l.tst view
@@ -0,0 +1,220 @@+(herald "Needham-Schroeder-Low Public-Key Protocol"+  (comment "With deflistener's"))++(comment "CPSA 2.2.10")+(comment "All input read")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (deflistener n1)+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (comment "Initiator point-of-view with a listener")+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))) ((recv n1) (send n1)))+  (label 0)+  (unrealized (0 1) (1 0))+  (preskeleton)+  (comment "Not a skeleton"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (deflistener n1)+  (precedes ((0 0) (1 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))) ((recv n1) (send n1)))+  (label 1)+  (parent 0)+  (unrealized (0 1) (1 0))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (deflistener n1)+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (2 0)) ((2 1) (1 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (1 0)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))) ((recv n1) (send n1))+    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2-0 (pubk a)))))+  (label 2)+  (parent 1)+  (unrealized (0 1) (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n2 text) (a b name))+  (defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))+  (deflistener n2)+  (defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))+  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (1 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (displaced 3 0 init 3) n2-0 (1 0)+    (enc n2-0 a (pubk b)) (enc b n2-0 n2-0 (pubk a)))+  (traces+    ((send (enc n2 a (pubk b))) (recv (enc b n2 n2 (pubk a)))+      (send (enc n2 (pubk b)))) ((recv n2) (send n2))+    ((recv (enc n2 a (pubk b))) (send (enc b n2 n2 (pubk a)))))+  (label 3)+  (parent 2)+  (unrealized (0 1) (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))+  (deflistener n2)+  (defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))+  (defstrand resp 2 (n2 n2-0) (n1 n2) (b b) (a a))+  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0))+    ((3 1) (1 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (added-strand resp 2) n2 (1 0) (enc n2 (pubk b))+    (enc n2 a (pubk b)) (enc b n2 n2 (pubk a)))+  (traces+    ((send (enc n2 a (pubk b))) (recv (enc b n2 n2 (pubk a)))+      (send (enc n2 (pubk b)))) ((recv n2) (send n2))+    ((recv (enc n2 a (pubk b))) (send (enc b n2 n2 (pubk a))))+    ((recv (enc n2 a (pubk b))) (send (enc b n2 n2-0 (pubk a)))))+  (label 4)+  (parent 3)+  (unrealized (0 1) (1 0))+  (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (deflistener n2)+  (non-orig (privk a))+  (uniq-orig n2)+  (comment "Responder point-of-view with a listener")+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))+  (label 5)+  (unrealized (0 2) (1 0))+  (preskeleton)+  (comment "Not a skeleton"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (deflistener n2)+  (precedes ((0 1) (1 0)))+  (non-orig (privk a))+  (uniq-orig n2)+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))+  (label 6)+  (parent 5)+  (unrealized (0 2) (1 0))+  (origs (n2 (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (deflistener n2)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (precedes ((0 1) (2 1)) ((2 2) (1 0)))+  (non-orig (privk a))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (1 0)+    (enc b n1 n2 (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))) ((recv n2) (send n2))+    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 7)+  (parent 6)+  (unrealized (0 2))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (deflistener n2)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (precedes ((0 1) (2 1)) ((2 2) (0 2)) ((2 2) (1 0)))+  (non-orig (privk a))+  (uniq-orig n2)+  (operation nonce-test (displaced 3 2 init 3) n2 (0 2)+    (enc b n1 n2 (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))) ((recv n2) (send n2))+    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 8)+  (parent 7)+  (unrealized)+  (shape)+  (maps ((0 1) ((a a) (n2 n2) (b b) (n1 n1))))+  (origs (n2 (0 1))))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (deflistener n2)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (precedes ((0 1) (2 1)) ((0 1) (3 1)) ((2 2) (1 0)) ((3 2) (0 2)))+  (non-orig (privk a))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (0 2)+    (enc b n1 n2 (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))) ((recv n2) (send n2))+    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 9)+  (parent 7)+  (unrealized)+  (shape)+  (maps ((0 1) ((a a) (n2 n2) (b b) (n1 n1))))+  (origs (n2 (0 1))))++(comment "Nothing left to do")
tst/ns.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol ns basic
tst/nsl3.tst view
@@ -1,6 +1,6 @@ (herald "Three Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol nsl3 basic
tst/nsl4cm1.tst view
@@ -1,6 +1,6 @@ (herald "Four Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol nsl4cm basic
tst/nslsk.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read") (comment "Strand count bounded at 15")
+ tst/pen-non-orig-test.scm view
@@ -0,0 +1,29 @@+;; This is to test the pen-non-orig declaration.+;; The password, pwd, should not be known to the+;; penetrator at the outset.  Thus, even over an+;; unencrypted channel, the server should infer+;; a good client.  However, the password is+;; learned in the process, hence the skeleton+;; with a listener will also be realized.++(herald "pen-non-orig test")++(defprotocol pennonorigtest basic+  (defrole client+    (vars (userid name) (pwd text))+    (trace+     (send (cat userid pwd))))+  (defrole server+    (vars (userid name) (pwd text))+    (trace+     (recv (cat userid pwd)))+    (pen-non-orig pwd)))++(defskeleton pennonorigtest+  (vars (pwd text))+  (defstrand server 1 (pwd pwd)))++(defskeleton pennonorigtest+  (vars (pwd text))+  (defstrand server 1 (pwd pwd))+  (deflistener pwd))
+ tst/pen-non-orig-test.tst view
@@ -0,0 +1,112 @@+(herald "pen-non-orig test")++(comment "CPSA 2.2.10")+(comment "All input read")++(defprotocol pennonorigtest basic+  (defrole client+    (vars (userid name) (pwd text))+    (trace (send (cat userid pwd))))+  (defrole server+    (vars (userid name) (pwd text))+    (trace (recv (cat userid pwd)))+    (pen-non-orig pwd)))++(defskeleton pennonorigtest+  (vars (pwd text) (userid name))+  (defstrand server 1 (pwd pwd) (userid userid))+  (pen-non-orig pwd)+  (traces ((recv (cat userid pwd))))+  (label 0)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton pennonorigtest+  (vars (pwd text) (userid userid-0 name))+  (defstrand server 1 (pwd pwd) (userid userid))+  (defstrand client 1 (pwd pwd) (userid userid-0))+  (precedes ((1 0) (0 0)))+  (pen-non-orig pwd)+  (operation nonce-test (added-strand client 1) pwd (0 0))+  (traces ((recv (cat userid pwd))) ((send (cat userid-0 pwd))))+  (label 1)+  (parent 0)+  (unrealized)+  (shape)+  (maps ((0) ((pwd pwd) (userid userid))))+  (origs))++(comment "Nothing left to do")++(defprotocol pennonorigtest basic+  (defrole client+    (vars (userid name) (pwd text))+    (trace (send (cat userid pwd))))+  (defrole server+    (vars (userid name) (pwd text))+    (trace (recv (cat userid pwd)))+    (pen-non-orig pwd)))++(defskeleton pennonorigtest+  (vars (pwd text) (userid name))+  (defstrand server 1 (pwd pwd) (userid userid))+  (deflistener pwd)+  (pen-non-orig pwd)+  (traces ((recv (cat userid pwd))) ((recv pwd) (send pwd)))+  (label 2)+  (unrealized (0 0) (1 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton pennonorigtest+  (vars (pwd text) (userid userid-0 name))+  (defstrand server 1 (pwd pwd) (userid userid))+  (deflistener pwd)+  (defstrand client 1 (pwd pwd) (userid userid-0))+  (precedes ((2 0) (1 0)))+  (pen-non-orig pwd)+  (operation nonce-test (added-strand client 1) pwd (1 0))+  (traces ((recv (cat userid pwd))) ((recv pwd) (send pwd))+    ((send (cat userid-0 pwd))))+  (label 3)+  (parent 2)+  (unrealized (0 0))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton pennonorigtest+  (vars (pwd text) (userid userid-0 name))+  (defstrand server 1 (pwd pwd) (userid userid))+  (deflistener pwd)+  (defstrand client 1 (pwd pwd) (userid userid-0))+  (precedes ((2 0) (0 0)) ((2 0) (1 0)))+  (pen-non-orig pwd)+  (operation nonce-test (displaced 3 2 client 1) pwd (0 0))+  (traces ((recv (cat userid pwd))) ((recv pwd) (send pwd))+    ((send (cat userid-0 pwd))))+  (label 4)+  (parent 3)+  (unrealized)+  (shape)+  (maps ((0 1) ((pwd pwd) (userid userid))))+  (origs))++(defskeleton pennonorigtest+  (vars (pwd text) (userid userid-0 userid-1 name))+  (defstrand server 1 (pwd pwd) (userid userid))+  (deflistener pwd)+  (defstrand client 1 (pwd pwd) (userid userid-0))+  (defstrand client 1 (pwd pwd) (userid userid-1))+  (precedes ((2 0) (1 0)) ((3 0) (0 0)))+  (pen-non-orig pwd)+  (operation nonce-test (added-strand client 1) pwd (0 0))+  (traces ((recv (cat userid pwd))) ((recv pwd) (send pwd))+    ((send (cat userid-0 pwd))) ((send (cat userid-1 pwd))))+  (label 5)+  (parent 3)+  (unrealized)+  (shape)+  (maps ((0 1) ((pwd pwd) (userid userid))))+  (origs))++(comment "Nothing left to do")
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol pkinit basic
+ tst/preprocess.scm view
@@ -0,0 +1,27 @@+(herald "Pre-processing test example: modified NS with two responders")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 n3 text))+    (trace+     (send (enc n1 a (pubk b)))+     (recv (enc n1 n2 n3 (pubk a)))+     (send (enc n2 n3 (pubk b))))+	(uniq-orig n1))+  (defrole resp+    (vars (a b name) (n1 n2 n3 text))+    (trace+     (recv (enc n1 a (pubk b)))+     (send (enc n1 n2 n3 (pubk a)))+     (recv (enc n2 n3 (pubk b))))+	(uniq-orig n2 n3))+  (comment "modified Needham-Schroeder with role origination assumptions"))++;;; The initiator and two entangled responders POV+(defskeleton ns+  (vars (a b name) (n1 n2 n3 n2p n3p text))+  (defstrand init 3 (a a) (b b) (n1 n1) (n2 n2) (n3 n3))+  (defstrand resp 3 (a a) (b b) (n1 n1) (n2 n2) (n3 n3p))+  (defstrand resp 3 (a a) (b b) (n1 n1) (n2 n2p) (n3 n3))+  (non-orig (privk b) (privk a))+)
+ tst/preprocess.tst view
@@ -0,0 +1,100 @@+(herald "Pre-processing test example: modified NS with two responders")++(comment "CPSA 2.2.10")+(comment "All input read")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 n3 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 n3 (pubk a)))+      (send (enc n2 n3 (pubk b))))+    (uniq-orig n1))+  (defrole resp+    (vars (a b name) (n1 n2 n3 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 n3 (pubk a)))+      (recv (enc n2 n3 (pubk b))))+    (uniq-orig n2 n3))+  (comment+    "modified Needham-Schroeder with role origination assumptions"))++(defskeleton ns+  (vars (n1 n2 n3 n2p n3p text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))+  (defstrand resp 3 (n1 n1) (n2 n2) (n3 n3p) (a a) (b b))+  (defstrand resp 3 (n1 n1) (n2 n2p) (n3 n3) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n2 n3 n2p n3p)+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 n3 (pubk a)))+      (send (enc n2 n3 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 n3p (pubk a)))+      (recv (enc n2 n3p (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2p n3 (pubk a)))+      (recv (enc n2p n3 (pubk b)))))+  (label 0)+  (unrealized (0 1) (1 0) (1 2) (2 0) (2 2))+  (preskeleton)+  (comment "Not a skeleton"))++(defskeleton ns+  (vars (n1 n2 n3 n2p n3p text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))+  (defstrand resp 3 (n1 n1) (n2 n2) (n3 n3p) (a a) (b b))+  (defstrand resp 3 (n1 n1) (n2 n2p) (n3 n3) (a a) (b b))+  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n2 n3 n2p n3p)+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 n3 (pubk a)))+      (send (enc n2 n3 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 n3p (pubk a)))+      (recv (enc n2 n3p (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2p n3 (pubk a)))+      (recv (enc n2p n3 (pubk b)))))+  (label 1)+  (parent 0)+  (unrealized (0 1) (1 2) (2 2))+  (origs (n3 (2 1)) (n2p (2 1)) (n3p (1 1)) (n2 (1 1)) (n1 (0 0)))+  (comment "empty cohort"))++(defskeleton ns+  (vars (n1 n2 n3p text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3p) (a a) (b b))+  (defstrand resp 3 (n1 n1) (n2 n2) (n3 n3p) (a a) (b b))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n2 n3p)+  (operation collapsed 2 1)+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 n3p (pubk a)))+      (send (enc n2 n3p (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 n3p (pubk a)))+      (recv (enc n2 n3p (pubk b)))))+  (label 2)+  (parent 1)+  (unrealized (1 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n3p text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3p) (a a) (b b))+  (defstrand resp 3 (n1 n1) (n2 n2) (n3 n3p) (a a) (b b))+  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n2 n3p)+  (operation nonce-test (displaced 2 0 init 3) n2 (1 2)+    (enc n1 n2 n3p (pubk a)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 n3p (pubk a)))+      (send (enc n2 n3p (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 n3p (pubk a)))+      (recv (enc n2 n3p (pubk b)))))+  (label 3)+  (parent 2)+  (unrealized)+  (shape)+  (maps+    ((0 1 1) ((a a) (b b) (n1 n1) (n2 n2) (n3 n3p) (n2p n2) (n3p n3p))))+  (origs (n1 (0 0)) (n3p (1 1)) (n2 (1 1))))++(comment "Nothing left to do")
tst/print.tst view
@@ -1,7 +1,7 @@ (herald "Print Test"   (comment "See if read forms look like printed ones")) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read") (comment "Strand count bounded at 12")
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol targetterms8 basic
tst/timestamping.tst view
@@ -1,6 +1,6 @@ (herald timestamping-service) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol timestamping-service basic
tst/tor.tst view
@@ -1,7 +1,7 @@ (herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman)   (comment "Achieves unilateral authentication")) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol tor diffie-hellman
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol uncarried-keys basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol uniq-orig basic
tst/wang-hash.tst view
@@ -1,6 +1,6 @@ (herald "Wang's Fair Exchange Protocol" (bound 10)) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read") (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read") (comment "Strand count bounded at 10")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (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.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol wonthull basic
tst/wonthull2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol wonthull2 basic
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol woolam basic
tst/yahalom-6.3.6.tst view
@@ -4,7 +4,7 @@     "Yahalom Protocol, Section 6.3.6, Page 49")   (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")) -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol yahalom basic
tst/yahalom.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding") -(comment "CPSA 2.2.9")+(comment "CPSA 2.2.10") (comment "All input read")  (defprotocol yahalom basic