diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,21 @@ +2012-06-28 John D. Ramsdell + + * 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 + + * 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 + + * {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 * cpsa.cabal (Version): Tagged as version 2.2.9. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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 diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -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. diff --git a/doc/Make.hs b/doc/Make.hs --- a/doc/Make.hs +++ b/doc/Make.hs @@ -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) diff --git a/doc/cpsa.bib b/doc/cpsa.bib --- a/doc/cpsa.bib +++ b/doc/cpsa.bib @@ -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 = {} +} 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/cpsadha.pdf b/doc/cpsadha.pdf Binary files a/doc/cpsadha.pdf and b/doc/cpsadha.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 @@ -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 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.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 diff --git a/src/CPSA/Annotations/Main.hs b/src/CPSA/Annotations/Main.hs --- a/src/CPSA/Annotations/Main.hs +++ b/src/CPSA/Annotations/Main.hs @@ -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) diff --git a/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs b/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs --- a/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs +++ b/src/CPSA/DiffieHellmanNoReciprocal/Algebra.hs @@ -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 diff --git a/src/CPSA/Graph/Main.hs b/src/CPSA/Graph/Main.hs --- a/src/CPSA/Graph/Main.hs +++ b/src/CPSA/Graph/Main.hs @@ -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 "" hPutStrLn h ("") 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 diff --git a/src/CPSA/Lib/Entry.hs b/src/CPSA/Lib/Entry.hs --- a/src/CPSA/Lib/Entry.hs +++ b/src/CPSA/Lib/Entry.hs @@ -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)) diff --git a/src/CPSA/Lib/Main.hs b/src/CPSA/Lib/Main.hs --- a/src/CPSA/Lib/Main.hs +++ b/src/CPSA/Lib/Main.hs @@ -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) diff --git a/src/CPSA/Logic/Main.hs b/src/CPSA/Logic/Main.hs --- a/src/CPSA/Logic/Main.hs +++ b/src/CPSA/Logic/Main.hs @@ -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) diff --git a/src/CPSA/Parameters/Main.hs b/src/CPSA/Parameters/Main.hs --- a/src/CPSA/Parameters/Main.hs +++ b/src/CPSA/Parameters/Main.hs @@ -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) diff --git a/src/CPSA/Shapes/Main.hs b/src/CPSA/Shapes/Main.hs --- a/src/CPSA/Shapes/Main.hs +++ b/src/CPSA/Shapes/Main.hs @@ -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) 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (comment "Strand count bounded at 15") diff --git a/tst/Make.hs b/tst/Make.hs --- a/tst/Make.hs +++ b/tst/Make.hs @@ -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) 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol deorig-simple basic diff --git a/tst/dh_cert.tst b/tst/dh_cert.tst --- a/tst/dh_cert.tst +++ b/tst/dh_cert.tst @@ -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 diff --git a/tst/dhke.tst b/tst/dhke.tst --- a/tst/dhke.tst +++ b/tst/dhke.tst @@ -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 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol epmo_acctnum basic diff --git a/tst/epmo_acctnum.tst b/tst/epmo_acctnum.tst # file too large to diff: tst/epmo_acctnum.tst 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol hashtest 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol nonaug-prune basic diff --git a/tst/ns-l.scm b/tst/ns-l.scm new file mode 100644 --- /dev/null +++ b/tst/ns-l.scm @@ -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")) diff --git a/tst/ns-l.tst b/tst/ns-l.tst new file mode 100644 --- /dev/null +++ b/tst/ns-l.tst @@ -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") 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol nsl3 basic diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst --- a/tst/nsl4cm1.tst +++ b/tst/nsl4cm1.tst @@ -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 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (comment "Strand count bounded at 15") diff --git a/tst/pen-non-orig-test.scm b/tst/pen-non-orig-test.scm new file mode 100644 --- /dev/null +++ b/tst/pen-non-orig-test.scm @@ -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)) diff --git a/tst/pen-non-orig-test.tst b/tst/pen-non-orig-test.tst new file mode 100644 --- /dev/null +++ b/tst/pen-non-orig-test.tst @@ -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") 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol pkinit basic diff --git a/tst/preprocess.scm b/tst/preprocess.scm new file mode 100644 --- /dev/null +++ b/tst/preprocess.scm @@ -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)) +) diff --git a/tst/preprocess.tst b/tst/preprocess.tst new file mode 100644 --- /dev/null +++ b/tst/preprocess.tst @@ -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") 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol timestamping-service basic diff --git a/tst/tor.tst b/tst/tor.tst --- a/tst/tor.tst +++ b/tst/tor.tst @@ -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 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol wide-mouth-frog basic diff --git a/tst/wonthull.tst b/tst/wonthull.tst --- a/tst/wonthull.tst +++ b/tst/wonthull.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol wonthull basic diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst --- a/tst/wonthull2.tst +++ b/tst/wonthull2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol wonthull2 basic 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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (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 @@ -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 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") -(comment "CPSA 2.2.9") +(comment "CPSA 2.2.10") (comment "All input read") (defprotocol yahalom basic