cpsa 3.6.10 → 3.6.11
raw patch · 95 files changed
+109/−96 lines, 95 files
Files
- ChangeLog +9/−0
- NEWS +4/−0
- README.txt +2/−2
- cpsa.cabal +1/−1
- src/CPSA/Annotations/Main.hs +1/−1
- src/CPSA/Graph/Main.hs +5/−5
- src/CPSA/Lib/Entry.hs +1/−1
- src/CPSA/Match/Main.hs +1/−1
- src/CPSA/SAS/Main.hs +1/−1
- src/CPSA/Shapes/Main.hs +1/−1
- tst/aik.tst +1/−1
- tst/attest.tst +1/−1
- tst/axiom2.tst +1/−1
- tst/blanchet.tst +1/−1
- tst/bltk_or.tst +1/−1
- tst/bltk_test.tst +1/−1
- tst/comment.tst +1/−1
- tst/comp_test.tst +1/−1
- tst/dh-ca.tst +1/−1
- tst/dh_group_sig.tst +1/−1
- tst/dh_mim.tst +1/−1
- tst/dh_mim2.tst +1/−1
- tst/dh_mim_nobase.tst +1/−1
- tst/dh_sig.tst +1/−1
- tst/dh_test.tst +1/−1
- tst/dhcr_um.tst +1/−1
- tst/dhcr_um3.tst +1/−1
- tst/dhcr_umx.tst +1/−1
- tst/dhnsl_basic.tst +1/−1
- tst/dhnsl_use.tst +1/−1
- tst/doorsep.tst +1/−1
- tst/doorsep2invk.tst +1/−1
- tst/eadh_um.tst too large to diff
- tst/enrich.tst +1/−1
- tst/envelope.tst +1/−1
- tst/envelope_short.tst +1/−1
- tst/eq_test.tst +1/−1
- tst/ffgg.tst +1/−1
- tst/fluffy_draft03_gske.tst +1/−1
- tst/fnof_or.tst +1/−1
- tst/fnof_test.tst +1/−1
- tst/fnof_woolam.tst +1/−1
- tst/fnof_yahalom.tst +1/−1
- tst/goals.tst +1/−1
- tst/iadh_um.tst too large to diff
- tst/iadh_um_eq.tst +1/−1
- tst/iadh_um_joshua.tst +1/−1
- tst/iadh_umx.tst +1/−1
- tst/injection.tst +1/−1
- tst/kerb.tst +1/−1
- tst/kerberos++.tst +1/−1
- tst/lt_test.tst +1/−1
- tst/neq_test.tst +1/−1
- tst/nh-ca-w-dh.tst +1/−1
- tst/nh-ca.tst +1/−1
- tst/nhcr_um.tst +1/−1
- tst/nhcr_um3.tst +1/−1
- tst/nhcr_umx.tst +1/−1
- tst/ns.tst +1/−1
- tst/or.tst +1/−1
- tst/ordered.tst +1/−1
- tst/owang.tst +1/−1
- tst/owat.tst +1/−1
- tst/pkinit.tst +1/−1
- tst/plaindh.tst +1/−1
- tst/precursor.tst +1/−1
- tst/priority_test.tst +1/−1
- tst/prottrans.tst +1/−1
- tst/reflect.tst +1/−1
- tst/reflect_dh.tst +1/−1
- tst/role_uniq.tst +1/−1
- tst/rule-order.tst +1/−1
- tst/staticdh.tst +1/−1
- tst/station.tst +1/−1
- tst/station2.tst +1/−1
- tst/station_newhope.tst +1/−1
- tst/station_nobase.tst +1/−1
- tst/stationbase.tst +1/−1
- tst/subsort_test.tst +1/−1
- tst/tag_test.tst +1/−1
- tst/target.tst +1/−1
- tst/test_g.tst +1/−1
- tst/test_small.tst +1/−1
- tst/thinning.tst +1/−1
- tst/trust-anchor.tst +1/−1
- tst/ugen_test.tst +1/−1
- tst/unilateral.tst +1/−1
- tst/uniq-gen-test.tst +1/−1
- tst/uniq_orig_doesnt_fail.tst +1/−1
- tst/wd-goalssat.tst +1/−1
- tst/wd-gs-simple.tst +1/−1
- tst/woolam.tst +1/−1
- tst/wrap_decrypt.tst +1/−1
- tst/yahalom.tst +1/−1
- tst/yolo.tst +1/−1
ChangeLog view
@@ -1,3 +1,12 @@+2022-06-15 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Version): Tagged as 3.6.11++2022-04-07 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/{Graph,SAS,Shapes}/Main.hs: Removed extra quotes in+ error messages.+ 2022-03-20 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.10
NEWS view
@@ -1,5 +1,9 @@ CPSA NEWS + June 2022:++* Release 3.6.11 removes extra quotes in some error messages.+ March 2022: * Release 3.6.10 allows double quote and backslash in S-expressions so
README.txt view
@@ -44,7 +44,7 @@ Build and install with: $ cabal build-$ cabal install+$ cabal install --overwrite-policy=always : To find the directory containing documentation and samples, type: $ cpsa4 -h @@ -72,7 +72,7 @@ C:\...> cabal update C:\...> cabal install parallel C:\...> cabal build-C:\...> cabal install+C:\...> cabal install --overwrite-policy=always Documentation and samples are in the directory given by C:\...> cpsa -h
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 3.6.10+Version: 3.6.11 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.10 License: BSD3
src/CPSA/Annotations/Main.hs view
@@ -68,4 +68,4 @@ writeLnSExpr output margin sexpr return ps Left err ->- abort (show err)+ abort err
src/CPSA/Graph/Main.hs view
@@ -49,7 +49,7 @@ do preskels <- tryIO (loadDefs p) case preskels of- Left err -> abort (show err)+ Left err -> abort err Right (cmts, preskels) -> do h <- outputHandle (file params)@@ -89,7 +89,7 @@ do preskel <- tryIO (loadFirst p) case preskel of- Left err -> abort (show err)+ Left err -> abort err Right (cmts, preskel, state) -> do h <- outputHandle (file params)@@ -100,7 +100,7 @@ ans <- tryIO (treelessView h conf (margin params) cmts preskel state) case ans of- Left err -> abort (show err)+ Left err -> abort err Right () -> return () -- LaTeX graphing.@@ -109,7 +109,7 @@ do preskel <- tryIO (loadFirst p) case preskel of- Left err -> abort (show err)+ Left err -> abort err Right (cmts, preskel, state) -> do h <- outputHandle (file params)@@ -120,7 +120,7 @@ let pp = printer conf ans <- tryIO (latexView h (margin params) pp cmts preskel state) case ans of- Left err -> abort (show err)+ Left err -> abort err Right () -> return () -- Command line option flags
src/CPSA/Lib/Entry.hs view
@@ -268,7 +268,7 @@ return x Left err -> do- hPutStrLn stderr (show err)+ hPutStrLn stderr err return Nothing -- Exception handling for IO errors
src/CPSA/Match/Main.hs view
@@ -63,4 +63,4 @@ writeLnSExpr output margin sexpr return () Left err ->- abort (show err)+ abort err
src/CPSA/SAS/Main.hs view
@@ -96,7 +96,7 @@ x <- tryIO (sas name origin state sexpr) case x of Left err ->- abort (show err)+ abort err Right (acc, Nothing) -> after output margin acc sexpr Right (acc, Just x) ->
src/CPSA/Shapes/Main.hs view
@@ -55,4 +55,4 @@ writeLnSExpr output margin sexpr return acc Left err ->- abort (show err)+ abort err
tst/aik.tst view
@@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/aik.scm") (defprotocol aikprot basic
tst/attest.tst view
@@ -1,6 +1,6 @@ (herald attest-door) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/attest.scm") (defprotocol attest-door basic
tst/axiom2.tst view
@@ -1,6 +1,6 @@ (herald "Axiom 2 Protocol" (bound 20)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/axiom2.scm") (comment "Strand count bounded at 20")
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 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/blanchet.scm") (defprotocol blanchet basic
tst/bltk_or.tst view
@@ -2,7 +2,7 @@ (comment "Standard version using variables of sort mesg") (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/bltk_or.scm") (defprotocol or diffie-hellman
tst/bltk_test.tst view
@@ -1,6 +1,6 @@ (herald "bltk Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/bltk_test.scm") (defprotocol test diffie-hellman
tst/comment.tst view
@@ -1,6 +1,6 @@ (herald comment) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/comment.scm") (defprotocol comment basic
tst/comp_test.tst view
@@ -1,6 +1,6 @@ (herald "Main Example") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/comp_test.scm") (defprotocol main-ex-src basic
tst/dh-ca.tst view
@@ -1,6 +1,6 @@ (herald dhca (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dh-ca.scm") (defprotocol dhca diffie-hellman
tst/dh_group_sig.tst view
@@ -1,6 +1,6 @@ (herald "Signed group DH exchange" (algebra diffie-hellman) (limit 100)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dh_group_sig.scm") (comment "Step count limited to 100")
tst/dh_mim.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dh_mim.scm") (defprotocol dh_mim diffie-hellman
tst/dh_mim2.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dh_mim2.scm") (defprotocol dh_mim diffie-hellman
tst/dh_mim_nobase.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dh_mim_nobase.scm") (defprotocol dh_mim_nobase diffie-hellman
tst/dh_sig.tst view
@@ -1,6 +1,6 @@ (herald "Signed DH exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dh_sig.scm") (defprotocol dh_sig diffie-hellman
tst/dh_test.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dh_test.scm") (comment "Strand count bounded at 20")
tst/dhcr_um.tst view
@@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) original" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dhcr_um.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/dhcr_um3.tst view
@@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) three-part" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dhcr_um3.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/dhcr_umx.tst view
@@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) criss-cross" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dhcr_umx.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/dhnsl_basic.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dhnsl_basic.scm") (defprotocol dhnsl diffie-hellman
tst/dhnsl_use.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/dhnsl_use.scm") (defprotocol dhnsl diffie-hellman
tst/doorsep.tst view
@@ -1,6 +1,6 @@ (herald doorsep (comment "Door Simple Example Protocol")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/doorsep.scm") (defprotocol doorsep basic
tst/doorsep2invk.tst view
@@ -1,6 +1,6 @@ (herald doorsep2invk (comment "Door Simple Example Protocol")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/doorsep2invk.scm") (defprotocol doorsep basic
tst/eadh_um.tst view
file too large to diff
tst/enrich.tst view
@@ -1,6 +1,6 @@ (herald enrich) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/enrich.scm") (defprotocol enrich basic
tst/envelope.tst view
@@ -1,6 +1,6 @@ (herald "Envelope Protocol" (bound 20)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/envelope.scm") (comment "Strand count bounded at 20")
tst/envelope_short.tst view
@@ -1,6 +1,6 @@ (herald "Envelope Protocol" (bound 20)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/envelope_short.scm") (comment "Strand count bounded at 20")
tst/eq_test.tst view
@@ -2,7 +2,7 @@ (comment "First skeleton should have a shape," "second, and hird should be dead.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/eq_test.scm") (defprotocol eqtest basic
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol" (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/ffgg.scm") (defprotocol ffgg basic
tst/fluffy_draft03_gske.tst view
@@ -3,7 +3,7 @@ (comment "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/fluffy_draft03_gske.scm") (defprotocol fluffy basic
tst/fnof_or.tst view
@@ -2,7 +2,7 @@ (comment "Version using variables of sort mesg, with ltk function emulated.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/fnof_or.scm") (defprotocol or basic
tst/fnof_test.tst view
@@ -1,7 +1,7 @@ (herald "Function constraint test protocol" (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/fnof_test.scm") (defprotocol fnoftest basic
tst/fnof_woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol, using fnof to emulate ltk function") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/fnof_woolam.scm") (defprotocol woolam basic
tst/fnof_yahalom.tst view
@@ -2,7 +2,7 @@ "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function" (bound 12)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/fnof_yahalom.scm") (defprotocol yahalom basic
tst/goals.tst view
@@ -1,6 +1,6 @@ (herald goals) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/goals.scm") (defprotocol ns basic
tst/iadh_um.tst view
file too large to diff
tst/iadh_um_eq.tst view
@@ -1,7 +1,7 @@ (herald "IADH: unified model (UM)" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/iadh_um_eq.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/iadh_um_joshua.tst view
@@ -1,7 +1,7 @@ (herald "IADH: unified model (UM)" (bound 20) (limit 2000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/iadh_um_joshua.scm") (comment "Strand count bounded at 20")
tst/iadh_umx.tst view
@@ -1,7 +1,7 @@ (herald "IADH: unified model (UM), criss-cross variant" (bound 20) (limit 2000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/iadh_umx.scm") (comment "Strand count bounded at 20")
tst/injection.tst view
@@ -2,7 +2,7 @@ (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/injection.scm") (defprotocol ns diffie-hellman
tst/kerb.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/kerb.scm") (defprotocol kerb-flawed basic
tst/kerberos++.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/kerberos++.scm") (defprotocol kerberos basic
tst/lt_test.tst view
@@ -2,7 +2,7 @@ (comment "First and third skeletons should have a shape," "second and fourth should be dead.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/lt_test.scm") (defprotocol lttest basic
tst/neq_test.tst view
@@ -2,7 +2,7 @@ (comment "First skeleton should have a shape," "second, and hird should be dead.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/neq_test.scm") (defprotocol neqtest basic
tst/nh-ca-w-dh.tst view
@@ -1,6 +1,6 @@ (herald nhca (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/nh-ca-w-dh.scm") (comment "Strand count bounded at 20")
tst/nh-ca.tst view
@@ -1,6 +1,6 @@ (herald nhca (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/nh-ca.scm") (comment "Strand count bounded at 20")
tst/nhcr_um.tst view
@@ -1,7 +1,7 @@ (herald "NHCR: unified model (UM)" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/nhcr_um.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/nhcr_um3.tst view
@@ -1,7 +1,7 @@ (herald "NHCR: unified model (UM3) original" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/nhcr_um3.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/nhcr_umx.tst view
@@ -1,7 +1,7 @@ (herald "NHCR: unified model (UMX) criss-cross" (bound 20) (limit 8000) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/nhcr_umx.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/ns.tst view
@@ -2,7 +2,7 @@ (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/ns.scm") (defprotocol ns basic
tst/or.tst view
@@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol" (comment "Standard version using variables of sort mesg")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/or.scm") (defprotocol or basic
tst/ordered.tst view
@@ -1,6 +1,6 @@ (herald ordered) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/ordered.scm") (defprotocol ordered basic
tst/owang.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/owang.scm") (defprotocol wang basic
tst/owat.tst view
@@ -1,7 +1,7 @@ (herald "One-way Authentication Test with bltk keys" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/owat.scm") (defprotocol owa diffie-hellman
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PKINIT") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/pkinit.scm") (defprotocol pkinit-flawed basic
tst/plaindh.tst view
@@ -1,7 +1,7 @@ (herald "Plain diffie-hellman protocol with challenge-response" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/plaindh.scm") (defprotocol plaindh diffie-hellman
tst/precursor.tst view
@@ -1,6 +1,6 @@ (herald precursor (algebra diffie-hellman) (bound 6)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/precursor.scm") (comment "Strand count bounded at 6")
tst/priority_test.tst view
@@ -1,6 +1,6 @@ (herald "Receive priority test protocol") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/priority_test.scm") (defprotocol priority_test basic
tst/prottrans.tst view
@@ -1,6 +1,6 @@ (herald "Protocol Transformations With Rules") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/prottrans.scm") (defprotocol ns basic
tst/reflect.tst view
@@ -1,6 +1,6 @@ (herald reflect) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/reflect.scm") (defprotocol reflect basic
tst/reflect_dh.tst view
@@ -1,6 +1,6 @@ (herald reflect (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/reflect_dh.scm") (defprotocol reflect diffie-hellman
tst/role_uniq.tst view
@@ -1,6 +1,6 @@ (herald "Role Unique Origination") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/role_uniq.scm") (defprotocol blanchet basic
tst/rule-order.tst view
@@ -1,6 +1,6 @@ (herald rule-order) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/rule-order.scm") (defprotocol rule-order basic
tst/staticdh.tst view
@@ -1,6 +1,6 @@ (herald "Static DH key exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/staticdh.scm") (defprotocol staticdh1 diffie-hellman
tst/station.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/station.scm") (defprotocol station-to-station diffie-hellman
tst/station2.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/station2.scm") (defprotocol station-to-station diffie-hellman
tst/station_newhope.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/station_newhope.scm") (defprotocol station-to-station diffie-hellman
tst/station_nobase.tst view
@@ -1,7 +1,7 @@ (herald "Station-to-station protocol no base vars" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/station_nobase.scm") (defprotocol station-to-station diffie-hellman
tst/stationbase.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/stationbase.scm") (defprotocol station-to-station diffie-hellman
tst/subsort_test.tst view
@@ -2,7 +2,7 @@ (comment "First, third, and fourth skeletons should have a shape," "second should be dead.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/subsort_test.scm") (defprotocol subsorttest basic
tst/tag_test.tst view
@@ -1,6 +1,6 @@ (herald "Tag Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/tag_test.scm") (defprotocol test diffie-hellman
tst/target.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/target.scm") (defprotocol target-simple basic
tst/test_g.tst view
@@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/test_g.scm") (defprotocol test1 diffie-hellman
tst/test_small.tst view
@@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/test_small.scm") (defprotocol test diffie-hellman
tst/thinning.tst view
@@ -1,6 +1,6 @@ (herald thinning (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/thinning.scm") (defprotocol provision diffie-hellman
tst/trust-anchor.tst view
@@ -1,7 +1,7 @@ (herald trust-anchor (comment "Tests rule application on initial skeleton")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/trust-anchor.scm") (defprotocol trust-anchor basic
tst/ugen_test.tst view
@@ -3,7 +3,7 @@ origination are not always preserved for skeleton uniq-orig assumptions) (algebra diffie-hellman)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/ugen_test.scm") (defprotocol uof diffie-hellman
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/unilateral.scm") (defprotocol unilateral basic
tst/uniq-gen-test.tst view
@@ -1,7 +1,7 @@ (herald "Unique generation test protocols." (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/uniq-gen-test.scm") (defprotocol uniqgentest basic
tst/uniq_orig_doesnt_fail.tst view
@@ -3,7 +3,7 @@ origination are not always preserved for skeleton uniq-orig assumptions)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/uniq_orig_doesnt_fail.scm") (defprotocol uof basic
tst/wd-goalssat.tst view
@@ -1,6 +1,6 @@ (herald "Wrap-Decrypt example" (bound 24) (limit 2000) (goals-sat)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/wd-goalssat.scm") (comment "Strand count bounded at 24") (comment "Stop when goals satisfied")
tst/wd-gs-simple.tst view
@@ -1,7 +1,7 @@ (herald "Wrap-Decrypt example, simplified" (bound 24) (limit 500) (goals-sat)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/wd-gs-simple.scm") (comment "Step count limited to 500") (comment "Strand count bounded at 24")
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/woolam.scm") (defprotocol woolam basic
tst/wrap_decrypt.tst view
@@ -1,6 +1,6 @@ (herald wrap-decrypt (bound 10)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/wrap_decrypt.lsp") (comment "Strand count bounded at 10")
tst/yahalom.tst view
@@ -1,7 +1,7 @@ (herald "Yahalom Protocol with Forwarding Removed" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/yahalom.scm") (defprotocol yahalom diffie-hellman
tst/yolo.tst view
@@ -1,6 +1,6 @@ (herald yolo) -(comment "CPSA 3.6.10")+(comment "CPSA 3.6.11") (comment "All input read from tst/yolo.scm") (defprotocol yolo basic