diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2012-02-27 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.2.8. + +2012-02-23 John D. Ramsdell + + * src/CPSA/Lib/Strand.hs (separateVariablesLimit): Added a hard + coded limit to the number of attempts to perform variable + separation during generalization. + +2012-02-22 John D. Ramsdell + + * doc/cpsa.mk,doc/Make.hs: Removed rules for *.sch files. + +2012-02-02 John D. Ramsdell + + * src/CPSA/Lib/Strand.hs (usePrunedStrandNotInPOV): Turned this + flag on. It never was supposed to be off except for when + experimenting. + 2012-02-01 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 2.2.7. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,17 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.8 + +** Performance enhancement + In special circumstances, the generalization method called variable + separation takes too long. A bound has been added that limits the + number of attempts to separate variables. The result is CPSA may + report a skeleton is a shape when another is more general. + +** Pruning bug fixed + Pruning is never supposed to apply to strands in the image of the + point-of-view skeleton, but previous version did so. + * Changes in version 2.2.7 ** A bug in the matcher in each algebra was repaired @@ -18,7 +30,7 @@ ** Diffie-Hellman algebra documentation added The document titled "Simple Diffie-Hellman Algebra" is in cpsasdha.pdf. - + * Changes in version 2.2.6 ** SVG tooltips work once again @@ -287,7 +299,6 @@ Makefiles use the *.sch the extension for problems that use Diffie-Hellman. - * Changes in version 1.5.5 ** Encryption tests solved before nonce tests @@ -367,7 +378,7 @@ ** Outer most encryptions preferred for encryption tests When choosing among encryptions for critical messages, CPSA prefers -outer most encryptions over ones within another encryption. +outer most encryptions over ones within another encryption. * Changes in version 1.4.8 @@ -602,7 +613,7 @@ The name of the first protocol is included in the title of the generated XML document. -** Testing showed enabling multiprocess support gives no speedup. +** Testing showed enabling multiprocess support gives no speedup. * Changes in version 1.2.2 diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.2.7 +Version: 2.2.8 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -90,7 +90,8 @@ tst/targetterms8.scm tst/targetterms8.tst tst/tnsl5.lisp tst/uncarried_keys.scm tst/uncarried_keys.tst tst/uo.scm tst/uo.tst tst/updatetst tst/weird.scm tst/weird.tst tst/wide-mouth-frog.lsp - tst/wide-mouth-frog.tst tst/wonthull2.scm tst/wonthull2.tst + tst/wide-mouth-frog.tst tst/wide-mouth-frog-scyther.lsp + tst/wide-mouth-frog-scyther.tst tst/wonthull2.scm tst/wonthull2.tst tst/wonthull3.scm tst/wonthull3.tst tst/wonthull.scm tst/wonthull.tst tst/woolam.scm tst/woolam.tst tst/yahalom-6.3.6.scm tst/yahalom-6.3.6.tst tst/yahalom.scm tst/yahalom.tst tst/tor.scm diff --git a/doc/Make.hs b/doc/Make.hs --- a/doc/Make.hs +++ b/doc/Make.hs @@ -17,10 +17,6 @@ If successful, the analysis is in the file prob.xhtml, which can be viewed with a standards-compliant browser. -To analyze a problem in prob.sch using the Diffie-Hellman algebra, type: - -*Make> cpsa "prob" - For a shapes only version of the analysis, type: *Make> shapes "prob" @@ -122,18 +118,10 @@ cpsa :: FilePath -> IO () cpsa root = do - cpsaAll root + cpsaBasic root shapes root graph root -cpsaAll :: FilePath -> IO () -cpsaAll root = - do - exists <- doesFileExist (root ++ sourceDhExt) - case exists of - True -> cpsaDh root - False -> cpsaBasic root - -- CPSA using Basic rule cpsaBasic :: FilePath -> IO () @@ -148,26 +136,12 @@ inputExt = sourceBasicExt, outputExt = cpsaExt } --- CPSA using Diffie-Hellman Rule - -cpsaDh :: FilePath -> IO () -cpsaDh root = - do - flags <- get -- get CPSA flags - make (cpsaDhRule flags) root -- make CPSA output using given rule - -cpsaDhRule :: String -> Rule -cpsaDhRule flags = - Rule { prog = "cpsa -a diffie-hellman " ++ flags, - inputExt = sourceDhExt, - outputExt = cpsaExt } - -- Shapes Rule shapes :: FilePath -> IO () shapes root = do - cpsaAll root -- Run CPSA if need be + cpsaBasic root -- Run CPSA if need be make shapesRule root graph $ root ++ shapesRoot @@ -182,7 +156,7 @@ logic :: FilePath -> IO () logic root = do - cpsaAll root -- Run CPSA if need be + cpsaBasic root -- Run CPSA if need be make logicRule root logicRule :: Rule @@ -238,10 +212,6 @@ sourceBasicExt :: String sourceBasicExt = ".scm" --- Diffie-hellman source file -sourceDhExt :: String -sourceDhExt = ".sch" - cpsaExt :: String cpsaExt = ".txt" @@ -336,7 +306,7 @@ build :: IO () build = do - probs <- roots [sourceBasicExt, sourceDhExt] + probs <- roots [sourceBasicExt] mapM_ cpsa probs -- Clean files generated for all the source files in the current directory. @@ -344,5 +314,5 @@ clean :: IO () clean = do - probs <- roots [sourceBasicExt, sourceDhExt] + probs <- roots [sourceBasicExt] mapM_ cleanse probs diff --git a/doc/cpsa.mk b/doc/cpsa.mk --- a/doc/cpsa.mk +++ b/doc/cpsa.mk @@ -11,10 +11,6 @@ %.txt: %.lsp -$(CPSATIME) cpsa $(CPSAFLAGS) -o $@ $< -# Analyze protocols for shapes using Diffie-Hellman algebra -%.txt: %.sch - $(CPSATIME) cpsa -a diffie-hellman $(CPSAFLAGS) -o $@ $< - # Extract shapes %_shapes.txt: %.txt cpsashapes $(SHAPESFLAGS) -o $@ $< 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/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/cpsasdha.pdf b/doc/cpsasdha.pdf Binary files a/doc/cpsasdha.pdf and b/doc/cpsasdha.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/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.7} +\newcommand{\version}{2.2.8} \newcommand{\cpsacopying}{\begingroup \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The MITRE Corporation. Permission to copy without fee all or part of diff --git a/setup.bat b/setup.bat --- a/setup.bat +++ b/setup.bat @@ -1,3 +1,3 @@ -runghc Setup.hs configure -runghc Setup.hs build +runghc Setup.hs configure +runghc Setup.hs build runghc Setup.hs install diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -94,7 +94,7 @@ usePruningWhileSolving = True -- False usePrunedStrandNotInPOV :: Bool -usePrunedStrandNotInPOV = False -- True +usePrunedStrandNotInPOV = True -- False useStrictPrecedesCheck :: Bool useStrictPrecedesCheck = False -- True @@ -105,6 +105,9 @@ useNoOrigPreservation :: Bool useNoOrigPreservation = False -- True +useHullingByCompression :: Bool +useHullingByCompression = True -- False + -- Instances and Strand Identifiers -- An Instance is an instance of a role, in the sense that each @@ -957,7 +960,7 @@ do let perm = updatePerm s s' (strandids k) orderings' <- normalizeOrderings False - (permuteOrderings perm + (permuteOrderings perm (forward s (orderings k))) -- Pruning difference let k' = newPreskel @@ -1006,12 +1009,13 @@ hullByCompressing :: Algebra t p g s e c => Bool -> PRS t p g s e c -> Sid -> Sid -> [PRS t p g s e c] -hullByCompressing prune prs s s' = +hullByCompressing prune prs s s' | useHullingByCompression = do (s'', s''', subst) <- unifyStrands (skel prs) s s' prs <- ksubst False prs subst prs' <- compress True prs s'' s''' hull prune prs' +hullByCompressing _ _ _ _ = [] -- Hulling by compression disabled -- See if two strands unify. They can be of differing heights. The -- second strand returned may be longer. @@ -1692,12 +1696,15 @@ Candidate t p g s e c addIdentity k = (k, strandids k) +separateVariablesLimit :: Int +separateVariablesLimit = 1024 + generalize :: Algebra t p g s e c => Preskel t p g s e c -> [Candidate t p g s e c] generalize k = deleteNodes k ++ weakenOrderings k ++ forgetAssumption k ++ - separateVariables k + take separateVariablesLimit (separateVariables k) -- Node deletion 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.7") +(comment "CPSA 2.2.8") (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 @@ -1,6 +1,6 @@ -- A simple, CPSA specific make system -module Make (cpsa, shapes, annos, cleanse, get, set, +module Make (cpsa, shapes, logic, annos, params, cleanse, get, set, build, clean, roots) where {- Place a copy of this source file in the directory used to store @@ -17,22 +17,27 @@ If successful, the analysis is in the file prob.xhtml, which can be viewed with a standards-compliant browser. -To analyze a problem in prob.sch using the Diffie-Hellman algebra, type: - -*Make> cpsa "prob" - For a shapes only version of the analysis, type: *Make> shapes "prob" If successful, the shapes are in the file prob_shapes.xhtml. +*Make> logic "prob" + +If successful, the shape analysis sentences are in the file +prob_logic.text. + When the protocol is annotated with rely-guarantee formulas, type: *Make> annos "prob" If successful, the annotated shapes are in the file prob_annotations.xhtml. +*Make> params "prob" + +If successful, roles with parameter descriptions are in prob_parameters.txt. + To remove the files generated from source files, type: *Make> cleanse "prob" @@ -113,18 +118,10 @@ cpsa :: FilePath -> IO () cpsa root = do - cpsaAll root + cpsaBasic root shapes root graph root -cpsaAll :: FilePath -> IO () -cpsaAll root = - do - exists <- doesFileExist (root ++ sourceDhExt) - case exists of - True -> cpsaDh root - False -> cpsaBasic root - -- CPSA using Basic rule cpsaBasic :: FilePath -> IO () @@ -139,26 +136,12 @@ inputExt = sourceBasicExt, outputExt = cpsaExt } --- CPSA using Diffie-Hellman Rule - -cpsaDh :: FilePath -> IO () -cpsaDh root = - do - flags <- get -- get CPSA flags - make (cpsaDhRule flags) root -- make CPSA output using given rule - -cpsaDhRule :: String -> Rule -cpsaDhRule flags = - Rule { prog = "cpsa -a diffie-hellman " ++ flags, - inputExt = sourceDhExt, - outputExt = cpsaExt } - -- Shapes Rule shapes :: FilePath -> IO () shapes root = do - cpsaAll root -- Run CPSA if need be + cpsaBasic root -- Run CPSA if need be make shapesRule root graph $ root ++ shapesRoot @@ -168,6 +151,20 @@ inputExt = cpsaExt, outputExt = shapesRoot ++ cpsaExt } +-- Logic Rule + +logic :: FilePath -> IO () +logic root = + do + cpsaBasic root -- Run CPSA if need be + make logicRule root + +logicRule :: Rule +logicRule = + Rule { prog = "cpsalogic", + inputExt = cpsaExt, + outputExt = logicExt } + -- Annotations Rule annos :: FilePath -> IO () @@ -205,6 +202,7 @@ rm $ root ++ graphExt rm $ root ++ shapesRoot ++ cpsaExt rm $ root ++ shapesRoot ++ graphExt + rm $ root ++ logicExt rm $ root ++ annosRoot ++ cpsaExt rm $ root ++ annosRoot ++ graphExt rm $ root ++ paramsRoot ++ cpsaExt @@ -214,16 +212,15 @@ sourceBasicExt :: String sourceBasicExt = ".scm" --- Diffie-hellman source file -sourceDhExt :: String -sourceDhExt = ".sch" - cpsaExt :: String cpsaExt = ".txt" shapesRoot :: String shapesRoot = "_shapes" +logicExt :: String +logicExt = "_logic.text" + annosRoot :: String annosRoot = "_annotations" @@ -309,7 +306,7 @@ build :: IO () build = do - probs <- roots [sourceBasicExt, sourceDhExt] + probs <- roots [sourceBasicExt] mapM_ cpsa probs -- Clean files generated for all the source files in the current directory. @@ -317,5 +314,5 @@ clean :: IO () clean = do - probs <- roots [sourceBasicExt, sourceDhExt] + probs <- roots [sourceBasicExt] mapM_ cleanse probs diff --git a/tst/Makefile b/tst/Makefile --- a/tst/Makefile +++ b/tst/Makefile @@ -1,51 +1,48 @@ # When the binary changes, run the test suite, and look for changes in -# the output. The changes are not fatal errors, but for a *.sc{m,h} input +# the output. The changes are not fatal errors, but for a *.scm input # file, an error produced by the binary is fatal. TSTS := $(patsubst %.scm,%.txt,$(wildcard *.scm)) \ - $(patsubst %.sch,%.txt,$(wildcard *.sch)) \ $(patsubst %.lsp,%.txt,$(wildcard *.lsp)) -PROG = ../dist/build/cpsa/cpsa +CPSA = ../dist/build/cpsa/cpsa DIFF = ../dist/build/cpsadiff/cpsadiff +SHAPES = ../dist/build/cpsashapes/cpsashapes +LOGIC = ../dist/build/cpsalogic/cpsalogic +ANNOTATIONS = ../dist/build/cpsaannotations/cpsaannotations +GRAPH = ../dist/build/cpsagraph/cpsagraph CPSAFLAGS = +RTS -M512m -RTS # The expected answers are in files with the .tst extension. # Analyze protocols for shapes expecting success -%.txt: %.scm $(PROG) - $(PROG) $(CPSAFLAGS) -o $@ $*.scm +%.txt: %.scm $(CPSA) + $(CPSA) $(CPSAFLAGS) -o $@ $*.scm -$(DIFF) $(DIFFFLAGS) $*.tst $*.txt # Analyze protocols for shapes expecting failure -%.txt: %.lsp $(PROG) - -$(PROG) $(CPSAFLAGS) -o $@ $*.lsp - -$(DIFF) $(DIFFFLAGS) $*.tst $*.txt - -# Analyze protocols for shapes expecting success using Diffie-Hellman -%.txt: %.sch $(PROG) - $(PROG) $(CPSAFLAGS) -a diffie-hellman -o $@ $*.sch +%.txt: %.lsp $(CPSA) + -$(CPSA) $(CPSAFLAGS) -o $@ $*.lsp -$(DIFF) $(DIFFFLAGS) $*.tst $*.txt # Extract shapes %_shapes.txt: %.txt - ../dist/build/cpsashapes/cpsashapes $(SHAPESFLAGS) -o $@ $< + $(SHAPES) $(SHAPESFLAGS) -o $@ $< # Extract shape analysis sentences %_logic.text: %.txt - ../dist/build/cpsalogic/cpsalogic $(LOGICFLAGS) -o $@ $< + $(LOGIC) $(LOGICFLAGS) -o $@ $< # Annotate shapes %_annotations.txt: %_shapes.txt - ../dist/build/cpsaannotations/cpsaannotations \ - $(ANNOTATIONSFLAGS) -o $@ $< + $(ANNOTATIONS) $(ANNOTATIONSFLAGS) -o $@ $< # Visualize output %.svg: %.txt - ../dist/build/cpsagraph/cpsagraph -c -o $@ $< + $(GRAPH) -c -o $@ $< # Visualize output using the expanded format %.xhtml: %.txt - ../dist/build/cpsagraph/cpsagraph $(GRAPHFLAGS) -o $@ $< + $(GRAPH) $(GRAPHFLAGS) -o $@ $< .PRECIOUS: %.txt %_shapes.txt %_annotations.txt diff --git a/tst/README b/tst/README --- a/tst/README +++ b/tst/README @@ -2,18 +2,18 @@ extension are expected to succeed, ones with a .lsp extension expected are expected to fail, and ones with a .lisp are not run. The .lisp files may run for a long time and succeed or maybe they fail. The -test suite is usually run by typing "sh cpsatst.sh" in the parent +test suite is usually run by typing "./cpsatst" in the parent directory. After running the test suite, you will note files with the extension -.xml. These are XHTML/SVG compound documents that can be viewed by +.xhtml. These are XHTML/SVG compound documents that can be viewed by standards compliant browsers such as Firefox and Safari. New users should study CPSA's analysis of the following protocols in -order, Needham-Schroeder (ns.xml), Woo-Lam (woolan.xml), Yahalom -(yahalom.xml), ffgg (ffgg.xml), and finally Otway-Rees (or.xml). When -studying the full output, simultaneously display the extracted shapes. -The shapes file has an extension of _shapes.xml. +order, Needham-Schroeder (ns.xhtml), Woo-Lam (woolan.xhtml), Yahalom +(yahalom.xhtml), ffgg (ffgg.xhtml), and finally Otway-Rees (or.xhtml). +When studying the full output, simultaneously display the extracted +shapes. The shapes file has an extension of _shapes.xhtml. On the first pass, just look at the first two problems in the analysis of the Needham-Schroeder Protocol, and return to this test case when 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol deorig-contract basic diff --git a/tst/deorig_mesg.scm b/tst/deorig_mesg.scm --- a/tst/deorig_mesg.scm +++ b/tst/deorig_mesg.scm @@ -17,4 +17,3 @@ (defstrand init 2 (k k) (x z)) (defstrand resp 2 (x (enc z k)) (y z)) (precedes ((0 0) (1 0)) ((1 1) (0 1)))) - 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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol deorig-mesg basic diff --git a/tst/deorig_simple.scm b/tst/deorig_simple.scm --- a/tst/deorig_simple.scm +++ b/tst/deorig_simple.scm @@ -19,8 +19,8 @@ (vars (k akey) (x y text)) (trace (recv (enc x k)) (send y)))) -(defskeleton deorig-simple - (vars) +(defskeleton deorig-simple + (vars) (defstrand init 2)) (defskeleton deorig-simple @@ -28,4 +28,3 @@ (defstrand init 2 (k k) (x z)) (defstrand resp 2 (k k) (x z) (y z)) (precedes ((0 0) (1 0)) ((1 1) (0 1)))) - 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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 @@ -3,7 +3,7 @@ (displacement) (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.2.7") +(comment "CPSA 2.2.8") (comment "All input read") (comment "Displacement disabled") diff --git a/tst/epmo_acctnum.tst b/tst/epmo_acctnum.tst --- a/tst/epmo_acctnum.tst +++ b/tst/epmo_acctnum.tst @@ -2,7 +2,7 @@ (displacement) (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.2.7") +(comment "CPSA 2.2.8") (comment "All input read") (comment "Displacement disabled") 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol nonaug-prune basic @@ -36,21 +36,22 @@ (defskeleton nonaug-prune (vars (n text) (B C name) (k akey)) (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand trans2 2 (n n) (A B) (k k)) (defstrand orig 3 (n n) (A B) (B B) (k k)) (defstrand trans1 3 (n n) (A B) (C C) (k k)) - (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (1 2))) + (precedes ((2 0) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 2) (2 2))) (non-orig (invk k)) (uniq-orig n) (operation nonce-test (added-strand trans1 3) n (2 2) (enc n B k) (enc n B B k)) (traces ((recv (enc n B k)) (send (enc n B B B k))) + ((recv (enc n B k)) (send (enc n B B B k))) ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) (label 1) (parent 0) (seen 4) - (unrealized (0 0) (1 2) (2 1)) - (origs (n (1 0))) + (unrealized (0 0) (1 0) (2 2) (3 1)) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune @@ -76,38 +77,43 @@ (defskeleton nonaug-prune (vars (n text) (B name) (k akey)) (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand trans2 2 (n n) (A B) (k k)) (defstrand orig 3 (n n) (A B) (B B) (k k)) - (precedes ((0 1) (1 2)) ((1 0) (0 0))) + (precedes ((0 1) (2 2)) ((2 0) (0 0)) ((2 0) (1 0))) (non-orig (invk k)) (uniq-orig n) (operation nonce-test (displaced 3 0 trans2 2) n (2 2) (enc n A k) (enc n B B k)) (traces ((recv (enc n B k)) (send (enc n B B B k))) + ((recv (enc n B k)) (send (enc n B B B k))) ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))) (label 3) (parent 0) (seen 6) - (unrealized (0 0)) + (unrealized (0 0) (1 0)) + (origs (n (2 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune (vars (n text) (B C name) (k akey)) (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand trans2 2 (n n) (A B) (k k)) (defstrand orig 3 (n n) (A B) (B B) (k k)) (defstrand trans1 3 (n n) (A B) (C C) (k k)) - (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((1 1) (2 1)) ((2 2) (1 2))) + (precedes ((2 0) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((2 1) (3 1)) + ((3 2) (2 2))) (non-orig (invk k)) (uniq-orig n) - (operation nonce-test (added-strand orig 2) n (2 1) (enc n B B k)) + (operation nonce-test (added-strand orig 2) n (3 1) (enc n B B k)) (traces ((recv (enc n B k)) (send (enc n B B B k))) + ((recv (enc n B k)) (send (enc n B B B k))) ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) (label 4) (parent 1) (seen 7) - (unrealized (0 0) (1 2)) - (origs (n (1 0))) - (comment "2 in cohort - 1 not yet seen")) + (unrealized (0 0) (1 0) (2 2)) + (comment "3 in cohort - 1 not yet seen")) (defskeleton nonaug-prune (vars (n text) (A B name) (k akey)) @@ -131,40 +137,42 @@ (defskeleton nonaug-prune (vars (n text) (B name) (k akey)) (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand trans2 2 (n n) (A B) (k k)) (defstrand orig 3 (n n) (A B) (B B) (k k)) - (precedes ((0 1) (1 2)) ((1 1) (0 0))) + (precedes ((0 1) (2 2)) ((2 0) (0 0)) ((2 1) (1 0))) (non-orig (invk k)) (uniq-orig n) - (operation nonce-test (added-strand orig 2) n (0 0) (enc n B B k)) + (operation nonce-test (added-strand orig 2) n (1 0) (enc n B B k)) (traces ((recv (enc n B k)) (send (enc n B B B k))) + ((recv (enc n B k)) (send (enc n B B B k))) ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))) (label 6) (parent 3) - (unrealized) - (shape) - (maps ((0 0 1) ((n n) (A B) (B B) (k k)))) - (origs (n (1 0)))) + (seen 9) + (unrealized (0 0)) + (origs (n (2 0))) + (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune (vars (n text) (B C name) (k akey)) + (defstrand trans2 2 (n n) (A B) (k k)) (defstrand orig 3 (n n) (A B) (B B) (k k)) (defstrand trans1 3 (n n) (A B) (C C) (k k)) (defstrand trans2 2 (n n) (A B) (k k)) - (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 1) (1 1)) ((1 2) (0 2)) - ((2 1) (0 2))) + (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((1 0) (3 0)) ((1 1) (2 1)) + ((2 2) (1 2)) ((3 1) (1 2))) (non-orig (invk k)) (uniq-orig n) - (operation nonce-test (added-strand trans2 2) n (1 2) (enc n B k) + (operation nonce-test (added-strand trans2 2) n (2 2) (enc n B k) (enc n n C k) (enc n B B k)) - (traces + (traces ((recv (enc n B k)) (send (enc n B B B k))) ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))) ((recv (enc n B k)) (send (enc n B B B k)))) (label 7) (parent 4) - (seen 9) - (unrealized (2 0)) - (origs (n (0 0))) + (seen 10) + (unrealized (0 0) (3 0)) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune @@ -181,31 +189,51 @@ ((recv (enc n A k)) (send (enc n A A A k)))) (label 8) (parent 5) - (seen 6) + (seen 9) (unrealized (0 0)) (origs (n (1 0))) (comment "4 in cohort - 3 not yet seen")) (defskeleton nonaug-prune + (vars (n text) (B name) (k akey)) + (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand orig 3 (n n) (A B) (B B) (k k)) + (precedes ((0 1) (2 2)) ((2 1) (0 0)) ((2 1) (1 0))) + (non-orig (invk k)) + (uniq-orig n) + (operation nonce-test (added-strand orig 2) n (0 0) (enc n B B k)) + (traces ((recv (enc n B k)) (send (enc n B B B k))) + ((recv (enc n B k)) (send (enc n B B B k))) + ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))) + (label 9) + (parent 6) + (unrealized) + (shape) + (maps ((0 1 2) ((n n) (A B) (B B) (k k)))) + (origs (n (2 0))) + (comment "1 in cohort - 1 not yet seen")) + +(defskeleton nonaug-prune (vars (n text) (B C name) (k akey)) + (defstrand trans2 2 (n n) (A B) (k k)) (defstrand orig 3 (n n) (A B) (B B) (k k)) (defstrand trans1 3 (n n) (A B) (C C) (k k)) (defstrand trans2 2 (n n) (A B) (k k)) - (precedes ((0 0) (1 0)) ((0 1) (1 1)) ((0 1) (2 0)) ((1 2) (0 2)) - ((2 1) (0 2))) + (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((1 1) (2 1)) ((1 1) (3 0)) + ((2 2) (1 2)) ((3 1) (1 2))) (non-orig (invk k)) (uniq-orig n) - (operation nonce-test (added-strand orig 2) n (2 0) (enc n B B k)) - (traces + (operation nonce-test (added-strand orig 2) n (3 0) (enc n B B k)) + (traces ((recv (enc n B k)) (send (enc n B B B k))) ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))) ((recv (enc n B k)) (send (enc n B B B k)))) - (label 9) + (label 10) (parent 7) - (seen 6) - (unrealized) - (origs (n (0 0))) - (comment "1 in cohort - 0 not yet seen")) + (seen 15) + (unrealized (0 0)) + (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune (vars (n text) (B C name) (k akey)) @@ -223,9 +251,9 @@ ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) - (label 10) + (label 11) (parent 8) - (seen 13) + (seen 16) (unrealized (3 1)) (comment "2 in cohort - 1 not yet seen")) @@ -245,9 +273,9 @@ ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k)))) - (label 11) + (label 12) (parent 8) - (seen 14) + (seen 17) (unrealized (0 0) (3 0)) (comment "2 in cohort - 1 not yet seen")) @@ -264,17 +292,55 @@ (traces ((recv (enc n B k)) (send (enc n B B B k))) ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k)))) - (label 12) + (label 13) (parent 8) (unrealized (0 0)) (origs (n (1 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton nonaug-prune + (vars (n text) (B name) (k akey)) + (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand orig 3 (n n) (A B) (B B) (k k)) + (precedes ((0 1) (1 2)) ((1 1) (0 0))) + (non-orig (invk k)) + (uniq-orig n) + (operation collapsed 1 0) + (traces ((recv (enc n B k)) (send (enc n B B B k))) + ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k)))) + (label 14) + (parent 9) + (unrealized) + (shape) + (maps ((0 0 1) ((n n) (A B) (B B) (k k)))) + (origs (n (1 0)))) + +(defskeleton nonaug-prune (vars (n text) (B C name) (k akey)) (defstrand trans2 2 (n n) (A B) (k k)) (defstrand orig 3 (n n) (A B) (B B) (k k)) + (defstrand trans1 3 (n n) (A B) (C C) (k k)) (defstrand trans2 2 (n n) (A B) (k k)) + (precedes ((1 0) (2 0)) ((1 1) (0 0)) ((1 1) (2 1)) ((1 1) (3 0)) + ((2 2) (1 2)) ((3 1) (1 2))) + (non-orig (invk k)) + (uniq-orig n) + (operation nonce-test (added-strand orig 2) n (0 0) (enc n B B k)) + (traces ((recv (enc n B k)) (send (enc n B B B k))) + ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) + ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k))) + ((recv (enc n B k)) (send (enc n B B B k)))) + (label 15) + (parent 10) + (seen 9) + (unrealized) + (comment "1 in cohort - 0 not yet seen")) + +(defskeleton nonaug-prune + (vars (n text) (B C name) (k akey)) + (defstrand trans2 2 (n n) (A B) (k k)) + (defstrand orig 3 (n n) (A B) (B B) (k k)) + (defstrand trans2 2 (n n) (A B) (k k)) (defstrand trans1 3 (n n) (A B) (C C) (k k)) (precedes ((1 0) (3 0)) ((1 1) (2 0)) ((1 1) (3 1)) ((2 1) (1 2)) ((3 2) (0 0))) @@ -285,10 +351,11 @@ ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) - (label 13) - (parent 10) + (label 16) + (parent 11) + (seen 9) (unrealized) - (comment "1 in cohort - 1 not yet seen")) + (comment "1 in cohort - 0 not yet seen")) (defskeleton nonaug-prune (vars (n text) (A B name) (k akey)) @@ -304,8 +371,8 @@ ((send (enc n B B k)) (send (enc n A k)) (recv (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k)))) - (label 14) - (parent 11) + (label 17) + (parent 12) (unrealized (0 0)) (comment "2 in cohort - 2 not yet seen")) @@ -322,9 +389,9 @@ (traces ((recv (enc n A k)) (send (enc n A A A k))) ((send (enc n A A k)) (send (enc n A k)) (recv (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k)))) - (label 15) - (parent 12) - (seen 17) + (label 18) + (parent 13) + (seen 9) (unrealized) (origs (n (1 0))) (comment "1 in cohort - 0 not yet seen")) @@ -345,34 +412,13 @@ ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) - (label 16) - (parent 12) - (seen 20) + (label 19) + (parent 13) + (seen 22) (unrealized (3 1)) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune - (vars (n text) (B name) (k akey)) - (defstrand trans2 2 (n n) (A B) (k k)) - (defstrand orig 3 (n n) (A B) (B B) (k k)) - (defstrand trans2 2 (n n) (A B) (k k)) - (precedes ((1 1) (0 0)) ((1 1) (2 0)) ((2 1) (1 2))) - (non-orig (invk k)) - (uniq-orig n) - (operation generalization deleted (3 0)) - (traces ((recv (enc n B k)) (send (enc n B B B k))) - ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) - ((recv (enc n B k)) (send (enc n B B B k)))) - (label 17) - (parent 13) - (seen 6) - (unrealized) - (shape) - (maps ((0 2 1) ((n n) (A B) (B B) (k k)))) - (origs (n (1 0))) - (comment "1 in cohort - 0 not yet seen")) - -(defskeleton nonaug-prune (vars (n text) (A name) (k akey)) (defstrand trans2 2 (n n) (A A) (k k)) (defstrand orig 3 (n n) (A A) (B A) (k k)) @@ -387,9 +433,9 @@ ((send (enc n A A k)) (send (enc n A k)) (recv (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k))) ((recv (enc n A k)) (send (enc n A A A k)))) - (label 18) - (parent 14) - (seen 17) + (label 20) + (parent 17) + (seen 9) (unrealized) (comment "1 in cohort - 0 not yet seen")) @@ -411,9 +457,9 @@ ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) - (label 19) - (parent 14) - (seen 21) + (label 21) + (parent 17) + (seen 23) (unrealized (4 1)) (comment "2 in cohort - 1 not yet seen")) @@ -432,9 +478,9 @@ ((send (enc n B B k)) (send (enc n B k)) (recv (enc n B B B k))) ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) - (label 20) - (parent 16) - (seen 15) + (label 22) + (parent 19) + (seen 18) (unrealized) (comment "1 in cohort - 0 not yet seen")) @@ -455,9 +501,9 @@ ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B k)) (send (enc n B B B k))) ((recv (enc n B B k)) (recv (enc n B k)) (send (enc n n C k)))) - (label 21) - (parent 19) - (seen 13) + (label 23) + (parent 21) + (seen 16) (unrealized) (comment "1 in cohort - 0 not yet seen")) 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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol ns basic @@ -97,44 +97,160 @@ (comment "1 in cohort - 1 not yet seen")) (defskeleton ns - (vars (n1 n2 n2-0 text) (a b name)) + (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name)) (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) - (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a)) - (precedes ((0 0) (1 0)) ((1 1) (0 1))) + (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b)) + (defstrand resp 2 (n2 n2-1) (n1 n1-0) (b b) (a a)) + (precedes ((1 0) (2 0)) ((2 1) (1 1))) (non-orig (privk a) (privk b)) - (uniq-orig n1) - (operation nonce-test (added-strand resp 2) n1 (1 1) - (enc n1 a (pubk b))) + (uniq-orig n1 n1-0) + (operation nonce-test (added-strand resp 2) n1-0 (1 1) + (enc n1-0 a (pubk b))) (traces ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b)))) - ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a))))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-1 (pubk a))))) (label 4) (parent 3) - (unrealized (0 1)) - (origs (n1 (0 0))) + (unrealized (0 1) (1 1)) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns + (vars (n1 n1-0 n2 n2-0 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b)) + (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a)) + (precedes ((1 0) (2 0)) ((2 1) (1 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (operation nonce-test (contracted (n2-1 n2-0)) n1-0 (1 1) + (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a))))) + (label 5) + (parent 4) + (seen 6) + (unrealized (0 1)) + (comment "3 in cohort - 2 not yet seen")) + +(defskeleton ns (vars (n1 n2 text) (a b name)) (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a)) (precedes ((0 0) (1 0)) ((1 1) (0 1))) (non-orig (privk a) (privk b)) (uniq-orig n1) - (operation nonce-test (contracted (n2-0 n2)) n1 (0 1) - (enc n1 n2 (pubk a)) (enc n1 a (pubk b))) + (operation nonce-test (displaced 3 1 init 1) n1-0 (0 1) + (enc n1-0 a (pubk b))) (traces ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))) - (label 5) - (parent 4) + (label 6) + (parent 5) (unrealized) (shape) (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2)))) (origs (n1 (0 0)))) +(defskeleton ns + (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b)) + (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a)) + (defstrand resp 2 (n2 n2-1) (n1 n1) (b b) (a a)) + (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (operation nonce-test (added-strand resp 2) n1 (0 1) + (enc n1 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2-1 (pubk a))))) + (label 7) + (parent 5) + (seen 9) + (unrealized (0 1)) + (comment "3 in cohort - 2 not yet seen")) + +(defskeleton ns + (vars (n1 n1-0 n2 n2-0 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b)) + (defstrand resp 2 (n2 n2) (n1 n1-0) (b b) (a a)) + (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a)) + (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1) + (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2 (pubk a)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a))))) + (label 8) + (parent 7) + (seen 6) + (unrealized) + (shape) + (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2)))) + (origs (n1 (0 0)) (n1-0 (1 0))) + (comment "2 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)) + (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a)) + (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a)) + (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) + (operation nonce-test (displaced 4 1 init 1) n1-0 (0 1) + (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a))))) + (label 9) + (parent 7) + (seen 6) + (unrealized) + (comment "1 in cohort - 0 not yet seen")) + +(defskeleton ns + (vars (n1 n2 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a)) + (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a)) + (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) + (operation collapsed 1 0) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))) + (label 10) + (parent 8) + (seen 6) + (unrealized) + (comment "1 in cohort - 0 not yet seen")) + (comment "Nothing left to do") (defprotocol ns basic @@ -157,7 +273,7 @@ (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b))))) - (label 6) + (label 11) (unrealized (0 2)) (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) @@ -176,8 +292,8 @@ (recv (enc n2 (pubk b)))) ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b-0))))) - (label 7) - (parent 6) + (label 12) + (parent 11) (unrealized) (shape) (maps ((0) ((a a) (n2 n2) (b b) (n1 n1)))) @@ -209,7 +325,7 @@ (traces ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b))))) - (label 8) + (label 13) (unrealized (0 1)) (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) @@ -227,8 +343,8 @@ ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a))))) - (label 9) - (parent 8) + (label 14) + (parent 13) (unrealized (0 1)) (comment "1 in cohort - 1 not yet seen")) @@ -245,8 +361,8 @@ ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))) - (label 10) - (parent 9) + (label 15) + (parent 14) (unrealized) (shape) (maps ((0) ((a a) (b b) (n1 n1) (n2 n2)))) @@ -278,7 +394,7 @@ (traces ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) (recv (enc n2 (pubk b))))) - (label 11) + (label 16) (unrealized (0 2)) (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) @@ -297,8 +413,8 @@ (recv (enc n2 (pubk b)))) ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b-0))))) - (label 12) - (parent 11) + (label 17) + (parent 16) (unrealized (0 0) (0 2)) (comment "2 in cohort - 2 not yet seen")) @@ -316,8 +432,8 @@ (recv (enc n2 (pubk b)))) ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b))))) - (label 13) - (parent 12) + (label 18) + (parent 17) (unrealized) (shape) (maps ((0) ((b b) (a a) (n2 n2) (n1 n1)))) @@ -339,8 +455,8 @@ ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b-0)))) ((recv (enc n1 a (pubk b-0))) (send (enc n1 n2-0 (pubk a))))) - (label 14) - (parent 12) + (label 19) + (parent 17) (unrealized (0 0) (0 2)) (comment "1 in cohort - 1 not yet seen")) @@ -360,9 +476,9 @@ ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a))))) - (label 15) - (parent 14) - (seen 13) + (label 20) + (parent 19) + (seen 18) (unrealized) (comment "1 in cohort - 0 not yet seen")) @@ -388,7 +504,7 @@ (traces ((send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b))))) - (label 16) + (label 21) (unrealized (0 1)) (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) @@ -406,8 +522,8 @@ ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2-0 (pubk a))))) - (label 17) - (parent 16) + (label 22) + (parent 21) (unrealized (0 1)) (comment "1 in cohort - 1 not yet seen")) @@ -424,8 +540,8 @@ ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2 (pubk a))))) - (label 18) - (parent 17) + (label 23) + (parent 22) (unrealized) (shape) (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3)))) @@ -455,7 +571,7 @@ ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) (send (enc n2 (pubk b)))) ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))) - (label 19) + (label 24) (unrealized) (shape) (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b)))) @@ -483,7 +599,7 @@ (comment "Shows typeflaw in typeless NSL") (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))) ((recv n2) (send n2))) - (label 20) + (label 25) (unrealized (1 0)) (preskeleton) (comment "Not a skeleton")) @@ -497,8 +613,8 @@ (uniq-orig n2) (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))) ((recv n2) (send n2))) - (label 21) - (parent 20) + (label 26) + (parent 25) (unrealized (1 0)) (origs (n2 (0 1))) (comment "2 in cohort - 2 not yet seen")) @@ -517,8 +633,8 @@ ((recv n2) (send n2)) ((send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a))) (send (enc n2 (pubk b))))) - (label 22) - (parent 21) + (label 27) + (parent 26) (unrealized (1 0)) (comment "empty cohort")) @@ -536,8 +652,8 @@ ((recv n2) (send n2)) ((recv (enc a-0 n2 b (pubk a))) (send (enc (cat n2 b) n2-0 a (pubk a-0))))) - (label 23) - (parent 21) + (label 28) + (parent 26) (unrealized) (shape) (maps ((0 1) ((a a) (b b) (n2 n2) (n1 a-0)))) 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol nsl4cm basic @@ -2432,9 +2432,10 @@ (send (enc b c d nc nc nc nd (pubk a))))) (label 73) (parent 25) - (seen 171) (unrealized) - (comment "1 in cohort - 0 not yet seen")) + (shape) + (maps ((0) ((a a) (b b) (c c) (d d) (na nc) (nb nc) (nc nc) (nd nd)))) + (origs (nc (0 0)))) (defskeleton nsl4cm (vars (nb nc nd nc-0 nd-0 nc-1 text) (a b c d name)) 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (comment "Strand count bounded at 15") 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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol pkinit basic diff --git a/tst/print.tst b/tst/print.tst --- a/tst/print.tst +++ b/tst/print.tst @@ -1,7 +1,7 @@ (herald "Print Test" (comment "See if read forms look like printed ones")) -(comment "CPSA 2.2.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (comment "Displacement disabled") 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol uniq-orig basic diff --git a/tst/updatetst b/tst/updatetst --- a/tst/updatetst +++ b/tst/updatetst @@ -3,7 +3,7 @@ for f in *.scm do if test -f "$f" - then + then b=`basename $f .scm` mv "$b.txt" "$b.tst" fi @@ -12,17 +12,8 @@ for f in *.lsp do if test -f "$f" - then + then b=`basename $f .lsp` - mv "$b.txt" "$b.tst" - fi -done - -for f in *.sch -do - if test -f "$f" - then - b=`basename $f .sch` mv "$b.txt" "$b.tst" fi done 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol weird basic diff --git a/tst/wide-mouth-frog-scyther.lsp b/tst/wide-mouth-frog-scyther.lsp new file mode 100644 --- /dev/null +++ b/tst/wide-mouth-frog-scyther.lsp @@ -0,0 +1,29 @@ +(herald "Wide-Mouth Frog Protocol from Scyther" + (comment "This protocol has an infinite number of shapes")) + +(defprotocol wide-mouth-frog basic + (defrole init (vars (a b t name) (ta text) (k skey)) + (trace (send (cat a (enc a ta b k (ltk a t)))))) + (defrole resp (vars (a b t name) (k skey) (tb text)) + (trace (recv (enc t tb a k (ltk b t))))) + (defrole ks (vars (a b t name) (k skey) (ta tb text)) + (trace (recv (cat a (enc a ta b k (ltk a t)))) + (send (enc t tb a k (ltk b t)))))) + +(defskeleton wide-mouth-frog + (vars (a t name) (k skey)) + (defstrand init 1 (a a) (t t) (k k)) + (non-orig (ltk a t)) + (uniq-orig k)) + +(defskeleton wide-mouth-frog + (vars (b t name) (k skey)) + (defstrand resp 1 (b b) (t t) (k k)) + (non-orig (ltk b t)) + (uniq-orig k)) + +(defskeleton wide-mouth-frog + (vars (a b t name) (k skey)) + (defstrand ks 2 (a a) (b b) (t t) (k k)) + (non-orig (ltk a t) (ltk b t)) + (uniq-orig k)) diff --git a/tst/wide-mouth-frog-scyther.tst b/tst/wide-mouth-frog-scyther.tst new file mode 100644 --- /dev/null +++ b/tst/wide-mouth-frog-scyther.tst @@ -0,0 +1,524 @@ +(herald "Wide-Mouth Frog Protocol from Scyther" + (comment "This protocol has an infinite number of shapes")) + +(comment "CPSA 2.2.8") +(comment "All input read") + +(defprotocol wide-mouth-frog basic + (defrole init + (vars (a b t name) (ta text) (k skey)) + (trace (send (cat a (enc a ta b k (ltk a t)))))) + (defrole resp + (vars (a b t name) (k skey) (tb text)) + (trace (recv (enc t tb a k (ltk b t))))) + (defrole ks + (vars (a b t name) (k skey) (ta tb text)) + (trace (recv (cat a (enc a ta b k (ltk a t)))) + (send (enc t tb a k (ltk b t)))))) + +(defskeleton wide-mouth-frog + (vars (ta text) (a t b name) (k skey)) + (defstrand init 1 (ta ta) (a a) (b b) (t t) (k k)) + (non-orig (ltk a t)) + (uniq-orig k) + (traces ((send (cat a (enc a ta b k (ltk a t)))))) + (label 0) + (unrealized) + (shape) + (maps ((0) ((a a) (t t) (k k) (b b) (ta ta)))) + (origs (k (0 0)))) + +(comment "Nothing left to do") + +(defprotocol wide-mouth-frog basic + (defrole init + (vars (a b t name) (ta text) (k skey)) + (trace (send (cat a (enc a ta b k (ltk a t)))))) + (defrole resp + (vars (a b t name) (k skey) (tb text)) + (trace (recv (enc t tb a k (ltk b t))))) + (defrole ks + (vars (a b t name) (k skey) (ta tb text)) + (trace (recv (cat a (enc a ta b k (ltk a t)))) + (send (enc t tb a k (ltk b t)))))) + +(defskeleton wide-mouth-frog + (vars (tb text) (b t a name) (k skey)) + (defstrand resp 1 (tb tb) (a a) (b b) (t t) (k k)) + (non-orig (ltk b t)) + (uniq-orig k) + (traces ((recv (enc t tb a k (ltk b t))))) + (label 1) + (unrealized (0 0)) + (origs) + (comment "2 in cohort - 2 not yet seen")) + +(defskeleton wide-mouth-frog + (vars (tb text) (b a name) (k skey)) + (defstrand resp 1 (tb tb) (a a) (b b) (t b) (k k)) + (defstrand init 1 (ta tb) (a b) (b a) (t b) (k k)) + (precedes ((1 0) (0 0))) + (non-orig (ltk b b)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc b tb a k (ltk b b)) (0 0)) + (traces ((recv (enc b tb a k (ltk b b)))) + ((send (cat b (enc b tb a k (ltk b b)))))) + (label 2) + (parent 1) + (unrealized) + (shape) + (maps ((0) ((b b) (t b) (k k) (a a) (tb tb)))) + (origs (k (1 0)))) + +(defskeleton wide-mouth-frog + (vars (tb ta text) (b t a name) (k skey)) + (defstrand resp 1 (tb tb) (a a) (b b) (t t) (k k)) + (defstrand ks 2 (ta ta) (tb tb) (a a) (b b) (t t) (k k)) + (precedes ((1 1) (0 0))) + (non-orig (ltk b t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t tb a k (ltk b t)) (0 0)) + (traces ((recv (enc t tb a k (ltk b t)))) + ((recv (cat a (enc a ta b k (ltk a t)))) + (send (enc t tb a k (ltk b t))))) + (label 3) + (parent 1) + (unrealized) + (shape) + (maps ((0) ((b b) (t t) (k k) (a a) (tb tb)))) + (origs)) + +(comment "Nothing left to do") + +(defprotocol wide-mouth-frog basic + (defrole init + (vars (a b t name) (ta text) (k skey)) + (trace (send (cat a (enc a ta b k (ltk a t)))))) + (defrole resp + (vars (a b t name) (k skey) (tb text)) + (trace (recv (enc t tb a k (ltk b t))))) + (defrole ks + (vars (a b t name) (k skey) (ta tb text)) + (trace (recv (cat a (enc a ta b k (ltk a t)))) + (send (enc t tb a k (ltk b t)))))) + +(defskeleton wide-mouth-frog + (vars (ta tb text) (a b t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a a) (b b) (t t) (k k)) + (non-orig (ltk a t) (ltk b t)) + (uniq-orig k) + (traces + ((recv (cat a (enc a ta b k (ltk a t)))) + (send (enc t tb a k (ltk b t))))) + (label 4) + (unrealized (0 0)) + (origs) + (comment "2 in cohort - 2 not yet seen")) + +(defskeleton wide-mouth-frog + (vars (ta tb text) (a b t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a a) (b b) (t t) (k k)) + (defstrand init 1 (ta ta) (a a) (b b) (t t) (k k)) + (precedes ((1 0) (0 0))) + (non-orig (ltk a t) (ltk b t)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc a ta b k (ltk a t)) (0 0)) + (traces + ((recv (cat a (enc a ta b k (ltk a t)))) + (send (enc t tb a k (ltk b t)))) + ((send (cat a (enc a ta b k (ltk a t)))))) + (label 5) + (parent 4) + (unrealized) + (shape) + (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (1 0)))) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 text) (b t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b b) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a b) (b t) (t t) (k k)) + (precedes ((1 1) (0 0))) + (non-orig (ltk b t) (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t ta b k (ltk t t)) (0 0)) + (traces + ((recv (cat t (enc t ta b k (ltk t t)))) + (send (enc t tb t k (ltk b t)))) + ((recv (cat b (enc b ta-0 t k (ltk b t)))) + (send (enc t ta b k (ltk t t))))) + (label 6) + (parent 4) + (unrealized (1 0)) + (comment "2 in cohort - 2 not yet seen")) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 text) (b t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b b) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a b) (b t) (t t) (k k)) + (defstrand init 1 (ta ta-0) (a b) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 0) (1 0))) + (non-orig (ltk b t) (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc b ta-0 t k (ltk b t)) (1 0)) + (traces + ((recv (cat t (enc t ta b k (ltk t t)))) + (send (enc t tb t k (ltk b t)))) + ((recv (cat b (enc b ta-0 t k (ltk b t)))) + (send (enc t ta b k (ltk t t)))) + ((send (cat b (enc b ta-0 t k (ltk b t)))))) + (label 7) + (parent 6) + (unrealized) + (shape) + (maps ((0) ((a t) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (2 0)))) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t ta-0 t k (ltk t t)) (1 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t))))) + (label 8) + (parent 6) + (unrealized (2 0)) + (comment "2 in cohort - 2 not yet seen")) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand init 1 (ta ta-1) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 0) (2 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc t ta-1 t k (ltk t t)) (2 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((send (cat t (enc t ta-1 t k (ltk t t)))))) + (label 9) + (parent 8) + (unrealized) + (shape) + (maps ((0) ((a t) (b t) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (3 0)))) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t ta-1 t k (ltk t t)) (2 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t))))) + (label 10) + (parent 8) + (unrealized (3 0)) + (comment "2 in cohort - 2 not yet seen")) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand init 1 (ta ta-2) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 0) (3 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc t ta-2 t k (ltk t t)) (3 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((send (cat t (enc t ta-2 t k (ltk t t)))))) + (label 11) + (parent 10) + (unrealized) + (shape) + (maps ((0) ((a t) (b t) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (4 0)))) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 ta-3 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-3) (tb ta-2) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t ta-2 t k (ltk t t)) (3 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((recv (cat t (enc t ta-3 t k (ltk t t)))) + (send (enc t ta-2 t k (ltk t t))))) + (label 12) + (parent 10) + (unrealized (4 0)) + (comment "2 in cohort - 2 not yet seen")) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 ta-3 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-3) (tb ta-2) (a t) (b t) (t t) (k k)) + (defstrand init 1 (ta ta-3) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0)) + ((5 0) (4 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc t ta-3 t k (ltk t t)) (4 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((recv (cat t (enc t ta-3 t k (ltk t t)))) + (send (enc t ta-2 t k (ltk t t)))) + ((send (cat t (enc t ta-3 t k (ltk t t)))))) + (label 13) + (parent 12) + (unrealized) + (shape) + (maps ((0) ((a t) (b t) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (5 0)))) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 ta-3 ta-4 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-3) (tb ta-2) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-4) (tb ta-3) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0)) + ((5 1) (4 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t ta-3 t k (ltk t t)) (4 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((recv (cat t (enc t ta-3 t k (ltk t t)))) + (send (enc t ta-2 t k (ltk t t)))) + ((recv (cat t (enc t ta-4 t k (ltk t t)))) + (send (enc t ta-3 t k (ltk t t))))) + (label 14) + (parent 12) + (unrealized (5 0)) + (comment "2 in cohort - 2 not yet seen")) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 ta-3 ta-4 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-3) (tb ta-2) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-4) (tb ta-3) (a t) (b t) (t t) (k k)) + (defstrand init 1 (ta ta-4) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0)) + ((5 1) (4 0)) ((6 0) (5 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc t ta-4 t k (ltk t t)) (5 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((recv (cat t (enc t ta-3 t k (ltk t t)))) + (send (enc t ta-2 t k (ltk t t)))) + ((recv (cat t (enc t ta-4 t k (ltk t t)))) + (send (enc t ta-3 t k (ltk t t)))) + ((send (cat t (enc t ta-4 t k (ltk t t)))))) + (label 15) + (parent 14) + (unrealized) + (shape) + (maps ((0) ((a t) (b t) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (6 0)))) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 ta-3 ta-4 ta-5 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-3) (tb ta-2) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-4) (tb ta-3) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-5) (tb ta-4) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0)) + ((5 1) (4 0)) ((6 1) (5 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t ta-4 t k (ltk t t)) (5 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((recv (cat t (enc t ta-3 t k (ltk t t)))) + (send (enc t ta-2 t k (ltk t t)))) + ((recv (cat t (enc t ta-4 t k (ltk t t)))) + (send (enc t ta-3 t k (ltk t t)))) + ((recv (cat t (enc t ta-5 t k (ltk t t)))) + (send (enc t ta-4 t k (ltk t t))))) + (label 16) + (parent 14) + (unrealized (6 0)) + (comment "2 in cohort - 2 not yet seen")) + +(comment "Strand bound exceeded--aborting run") + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 ta-3 ta-4 ta-5 text) (t name) (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-3) (tb ta-2) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-4) (tb ta-3) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-5) (tb ta-4) (a t) (b t) (t t) (k k)) + (defstrand init 1 (ta ta-5) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0)) + ((5 1) (4 0)) ((6 1) (5 0)) ((7 0) (6 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand init 1) + (enc t ta-5 t k (ltk t t)) (6 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((recv (cat t (enc t ta-3 t k (ltk t t)))) + (send (enc t ta-2 t k (ltk t t)))) + ((recv (cat t (enc t ta-4 t k (ltk t t)))) + (send (enc t ta-3 t k (ltk t t)))) + ((recv (cat t (enc t ta-5 t k (ltk t t)))) + (send (enc t ta-4 t k (ltk t t)))) + ((send (cat t (enc t ta-5 t k (ltk t t)))))) + (label 17) + (parent 16) + (unrealized) + (comment "aborted")) + +(defskeleton wide-mouth-frog + (vars (ta tb ta-0 ta-1 ta-2 ta-3 ta-4 ta-5 ta-6 text) (t name) + (k skey)) + (defstrand ks 2 (ta ta) (tb tb) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-0) (tb ta) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-1) (tb ta-0) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-2) (tb ta-1) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-3) (tb ta-2) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-4) (tb ta-3) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-5) (tb ta-4) (a t) (b t) (t t) (k k)) + (defstrand ks 2 (ta ta-6) (tb ta-5) (a t) (b t) (t t) (k k)) + (precedes ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0)) + ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0))) + (non-orig (ltk t t)) + (uniq-orig k) + (operation encryption-test (added-strand ks 2) + (enc t ta-5 t k (ltk t t)) (6 0)) + (traces + ((recv (cat t (enc t ta t k (ltk t t)))) + (send (enc t tb t k (ltk t t)))) + ((recv (cat t (enc t ta-0 t k (ltk t t)))) + (send (enc t ta t k (ltk t t)))) + ((recv (cat t (enc t ta-1 t k (ltk t t)))) + (send (enc t ta-0 t k (ltk t t)))) + ((recv (cat t (enc t ta-2 t k (ltk t t)))) + (send (enc t ta-1 t k (ltk t t)))) + ((recv (cat t (enc t ta-3 t k (ltk t t)))) + (send (enc t ta-2 t k (ltk t t)))) + ((recv (cat t (enc t ta-4 t k (ltk t t)))) + (send (enc t ta-3 t k (ltk t t)))) + ((recv (cat t (enc t ta-5 t k (ltk t t)))) + (send (enc t ta-4 t k (ltk t t)))) + ((recv (cat t (enc t ta-6 t k (ltk t t)))) + (send (enc t ta-5 t k (ltk t t))))) + (label 18) + (parent 16) + (unrealized (7 0)) + (comment "aborted")) 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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (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.7") +(comment "CPSA 2.2.8") (comment "All input read") (defprotocol yahalom basic