cpsa 2.2.7 → 2.2.8
raw patch · 82 files changed
+1019/−315 lines, 82 files
Files
- ChangeLog +20/−0
- NEWS +15/−4
- cpsa.cabal +3/−2
- doc/Make.hs +5/−35
- doc/cpsa.mk +0/−4
- doc/cpsadesign.pdf binary
- doc/cpsaoverview.pdf binary
- doc/cpsaprimer.pdf binary
- doc/cpsasdha.pdf binary
- doc/cpsaspec.pdf binary
- doc/macros.tex +1/−1
- setup.bat +2/−2
- src/CPSA/Lib/Strand.hs +11/−4
- tst/DH_hack.tst +1/−1
- tst/Make.hs +32/−35
- tst/Makefile +15/−18
- tst/README +6/−6
- tst/blanchet.tst +1/−1
- tst/completeness-test.tst +1/−1
- tst/crushing.tst +1/−1
- tst/dass_simple.tst +1/−1
- tst/denning-sacco.tst +1/−1
- tst/deorig_contract.tst +1/−1
- tst/deorig_mesg.scm +0/−1
- tst/deorig_mesg.tst +1/−1
- tst/deorig_simple.scm +2/−3
- tst/deorig_simple.tst +1/−1
- tst/dh_cert.tst +1/−1
- tst/dhke.tst +1/−1
- tst/dy.tst +1/−1
- tst/encsig.tst +1/−1
- tst/epmo-hash.tst +1/−1
- tst/epmo-key-hash.tst +1/−1
- tst/epmo.tst +1/−1
- tst/epmo_acctnum-key-hash.tst +1/−1
- tst/epmo_acctnum.tst +1/−1
- tst/ffgg.tst +1/−1
- tst/fragile_pruning.tst +1/−1
- tst/hashtest-key-hash.tst +1/−1
- tst/hashtest.tst +1/−1
- tst/isoreject.tst +1/−1
- tst/kelly1.tst +1/−1
- tst/kerberos.tst +1/−1
- tst/mass.tst +1/−1
- tst/mass2.tst +1/−1
- tst/missing_contraction.tst +1/−1
- tst/neuman-stubblebine-reauth.tst +1/−1
- tst/neuman-stubblebine.tst +1/−1
- tst/no_contraction.tst +1/−1
- tst/non_transforming.tst +1/−1
- tst/nonaug-prune.tst +129/−83
- tst/ns.tst +161/−45
- tst/nsl3.tst +1/−1
- tst/nsl4cm1.tst +4/−3
- tst/nslsk.tst +1/−1
- tst/or.tst +1/−1
- tst/pca.tst +1/−1
- tst/pkinit.tst +1/−1
- tst/print.tst +1/−1
- tst/pruning1.tst +1/−1
- tst/sigenc.tst +1/−1
- tst/sorted_epmo_acctnum.tst +1/−1
- tst/targetterms2.tst +1/−1
- tst/targetterms6.tst +1/−1
- tst/targetterms8.tst +1/−1
- tst/timestamping.tst +1/−1
- tst/tor.tst +1/−1
- tst/uncarried_keys.tst +1/−1
- tst/uo.tst +1/−1
- tst/updatetst +2/−11
- tst/wang-hash.tst +1/−1
- tst/wang-key-hash.tst +1/−1
- tst/weird.tst +1/−1
- tst/wide-mouth-frog-scyther.lsp +29/−0
- tst/wide-mouth-frog-scyther.tst +524/−0
- tst/wide-mouth-frog.tst +1/−1
- tst/wonthull.tst +1/−1
- tst/wonthull2.tst +1/−1
- tst/wonthull3.tst +1/−1
- tst/woolam.tst +1/−1
- tst/yahalom-6.3.6.tst +1/−1
- tst/yahalom.tst +1/−1
ChangeLog view
@@ -1,3 +1,23 @@+2012-02-27 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Version): Tagged as version 2.2.8.++2012-02-23 John D. Ramsdell <ramsdell@mitre.org>++ * 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 <ramsdell@mitre.org>++ * doc/cpsa.mk,doc/Make.hs: Removed rules for *.sch files.++2012-02-02 John D. Ramsdell <ramsdell@mitre.org>++ * 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 <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as version 2.2.7.
NEWS view
@@ -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
cpsa.cabal view
@@ -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
doc/Make.hs view
@@ -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
doc/cpsa.mk view
@@ -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 $@ $<
doc/cpsadesign.pdf view
binary file changed (203126 → 203125 bytes)
doc/cpsaoverview.pdf view
binary file changed (75612 → 75613 bytes)
doc/cpsaprimer.pdf view
binary file changed (186155 → 186027 bytes)
doc/cpsasdha.pdf view
binary file changed (130005 → 130006 bytes)
doc/cpsaspec.pdf view
binary file changed (330270 → 330270 bytes)
doc/macros.tex view
@@ -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
setup.bat view
@@ -1,3 +1,3 @@-runghc Setup.hs configure -runghc Setup.hs build +runghc Setup.hs configure+runghc Setup.hs build runghc Setup.hs install
src/CPSA/Lib/Strand.hs view
@@ -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
tst/DH_hack.tst view
@@ -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")
tst/Make.hs view
@@ -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
tst/Makefile view
@@ -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
tst/README view
@@ -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
tst/blanchet.tst view
@@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol" (comment "There is a flaw in this protocol by design")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol crushing basic
tst/dass_simple.tst view
@@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol dass-simple basic
tst/denning-sacco.tst view
@@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol deorig-contract basic
tst/deorig_mesg.scm view
@@ -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))))-
tst/deorig_mesg.tst view
@@ -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
tst/deorig_simple.scm view
@@ -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))))-
tst/deorig_simple.tst view
@@ -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
tst/dh_cert.tst view
@@ -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
tst/dhke.tst view
@@ -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
tst/dy.tst view
@@ -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
tst/encsig.tst view
@@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol mult-keys-enc-sig basic
tst/epmo-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol epmo basic
tst/epmo-key-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol epmo basic
tst/epmo.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol epmo basic
tst/epmo_acctnum-key-hash.tst view
@@ -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")
tst/epmo_acctnum.tst view
@@ -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")
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol" (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol fragile_pruning basic
tst/hashtest-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol hashtest basic
tst/hashtest.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol hashtest basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol missing-contraction basic
tst/neuman-stubblebine-reauth.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol neuman-stubblebine-reauth basic
tst/neuman-stubblebine.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol neuman-stubblebine basic
tst/no_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol no-contraction basic
tst/non_transforming.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol non_transforming basic
tst/nonaug-prune.tst view
@@ -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"))
tst/ns.tst view
@@ -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))))
tst/nsl3.tst view
@@ -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
tst/nsl4cm1.tst view
@@ -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))
tst/nslsk.tst view
@@ -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
tst/or.tst view
@@ -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
tst/pca.tst view
@@ -1,7 +1,7 @@ (herald "Privacy Certificate Authority" (bound 15) (comment "Generation of an Attestation Identity Certificate")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (comment "Strand count bounded at 15")
tst/pkinit.tst view
@@ -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
tst/print.tst view
@@ -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
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol prune basic
tst/sigenc.tst view
@@ -1,7 +1,7 @@ (herald "Signed Encrypted Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol mult-keys-sig-enc basic
tst/sorted_epmo_acctnum.tst view
@@ -4,7 +4,7 @@ "This version uses sorts to avoid confusion" "between a nonce and other data")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (comment "Displacement disabled")
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol targetterms8 basic
tst/timestamping.tst view
@@ -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
tst/tor.tst view
@@ -1,7 +1,7 @@ (herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman) (comment "Achieves unilateral authentication")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol tor diffie-hellman
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol uncarried-keys basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol uniq-orig basic
tst/updatetst view
@@ -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
tst/wang-hash.tst view
@@ -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")
tst/wang-key-hash.tst view
@@ -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")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol weird basic
+ tst/wide-mouth-frog-scyther.lsp view
@@ -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))
+ tst/wide-mouth-frog-scyther.tst view
@@ -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"))
tst/wide-mouth-frog.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol" (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol wonthull basic
tst/wonthull2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol wonthull2 basic
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -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
tst/yahalom-6.3.6.tst view
@@ -4,7 +4,7 @@ "Yahalom Protocol, Section 6.3.6, Page 49") (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")) -(comment "CPSA 2.2.7")+(comment "CPSA 2.2.8") (comment "All input read") (defprotocol yahalom basic
tst/yahalom.tst view
@@ -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