cpsa 3.6.1 → 3.6.2
raw patch · 99 files changed
+1414/−142 lines, 99 files
Files
- ChangeLog +38/−0
- NEWS +9/−0
- cpsa.cabal +7/−1
- doc/cpsamanual.pdf binary
- doc/examples/blanchet.xhtml +4/−2
- doc/examples/bltk_or.xhtml +2/−2
- doc/examples/dh_mim.xhtml too large to diff
- doc/examples/envelope.xhtml +4/−2
- doc/examples/eq_test.xhtml +3/−2
- doc/examples/ffgg.xhtml +3/−2
- doc/examples/fnof_test.xhtml +4/−2
- doc/examples/fnof_yahalom.xhtml +2/−2
- doc/examples/goals.xhtml +6/−3
- doc/examples/iadh_um.xhtml too large to diff
- doc/examples/kerb.xhtml +4/−2
- doc/examples/lt_test.xhtml +2/−2
- doc/examples/neq_test.xhtml +2/−2
- doc/examples/ns.xhtml +2/−2
- doc/examples/or.xhtml +2/−2
- doc/examples/pkinit.xhtml +5/−2
- doc/examples/plaindh.xhtml +2/−2
- doc/examples/priority_test.xhtml +2/−2
- doc/examples/station.xhtml +2/−2
- doc/examples/subsort_test.xhtml +2/−2
- doc/examples/woolam.xhtml +2/−2
- doc/examples/yahalom.xhtml +2/−2
- src/CPSA/Lib/Characteristic.hs +8/−1
- src/CPSA/Lib/Cohort.hs +4/−4
- src/CPSA/Lib/Displayer.hs +3/−0
- src/CPSA/Lib/Entry.hs +1/−1
- src/CPSA/Lib/Expand.hs +1/−1
- src/CPSA/Lib/Loader.hs +25/−3
- src/CPSA/Lib/Main.hs +1/−1
- src/CPSA/Lib/Printer.hs +41/−11
- src/CPSA/Lib/Protocol.hs +25/−0
- src/CPSA/Lib/Reduction.hs +37/−17
- src/CPSA/Lib/Strand.hs +31/−0
- src/CPSA/SAS/SAS.hs +12/−12
- src/ocaml/Makefile +25/−0
- src/ocaml/README +5/−0
- src/ocaml/cpsa.d.itarget +1/−0
- src/ocaml/cpsa.itarget +5/−0
- src/ocaml/cpsa.mllib +5/−0
- src/ocaml/cpsa.mltop +4/−0
- src/ocaml/cpsa.odocl +3/−0
- src/ocaml/expand.ml +152/−0
- src/ocaml/main.ml +73/−0
- src/ocaml/main.mli +24/−0
- src/ocaml/pp.ml +13/−0
- src/ocaml/reader.ml +58/−0
- src/ocaml/reader.mli +24/−0
- src/ocaml/scanner.mll +21/−0
- src/ocaml/sexpr.ml +84/−0
- src/ocaml/sexpr.mli +109/−0
- src/ocaml/sexpr_type.ml +5/−0
- tst/aik.tst +1/−1
- tst/axiom2.tst +3/−1
- tst/blanchet.tst +10/−1
- tst/bltk_test.tst +5/−1
- tst/dh-ca.tst +33/−1
- tst/dh_mim.tst +1/−1
- tst/dh_mim2.tst +1/−1
- tst/dh_sig.tst +1/−1
- tst/dh_test.tst +1/−1
- tst/dhnsl_basic.tst +12/−1
- tst/dhnsl_use.tst +77/−1
- tst/enrich.tst +1/−1
- tst/envelope.tst +40/−1
- tst/ffgg.tst +2/−1
- tst/fnof_or.tst +1/−1
- tst/fnof_test.tst +5/−1
- tst/fnof_woolam.tst +1/−1
- tst/fnof_yahalom.tst +3/−1
- tst/goals.scm +14/−0
- tst/goals.tst +191/−8
- tst/iadh_um.tst too large to diff
- tst/injection.tst +1/−1
- tst/kerb.tst +4/−1
- tst/kerberos++.tst +13/−1
- tst/lt_test.tst +3/−1
- tst/neq_test.tst +3/−1
- tst/ns.tst +1/−1
- tst/or.tst +1/−1
- tst/owang.tst +3/−1
- tst/owat.tst +1/−1
- tst/pkinit.tst +8/−1
- tst/plaindh.tst +1/−1
- tst/priority_test.tst +1/−1
- tst/reflect.tst +1/−1
- tst/staticdh.tst +3/−1
- tst/station.tst +11/−1
- tst/station2.tst +1/−1
- tst/subsort_test.tst +2/−1
- tst/test_small.tst +1/−1
- tst/unilateral.tst +1/−1
- tst/uniq-gen-test.tst +2/−1
- tst/woolam.tst +1/−1
- tst/wrap_decrypt.tst +22/−1
- tst/yahalom.tst +15/−1
ChangeLog view
@@ -1,3 +1,41 @@+2019-03-18 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Version): Tagged as 3.6.2++2019-02-22 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Reduction.hs (addAnnoKey): Added structured+ annotations to skeleton output to facilitate post processing+ programs besides cpsagraph. The new keys are (aborted),+ (satisfied-all), and (dead).++2019-02-04 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Reduction.hs (step): Changed default depth bound+ to zero representing no bound and ignored the check when the bound+ is not positive. This matches what is documented in the manual.++2019-01-31 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Loader.hs (badKey): Added checks for bad keys in+ alists for skeletons ("defstrand" and "deflistener") and protocols+ ("defrole" and "defrule").++2018-11-28 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Protocol.hs (AForm): Added the leads-to predicate+ to the goal language.++2018-11-19 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Printer.hs (formula): Added special pretty+ printing rules for formulas in defgoal and defrule.++2018-11-09 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/SAS/SAS.hs (loadPOV): Use a preskeleton as a POV+ instead of insisting on using a skeleton.+ 2018-08-29 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.1
NEWS view
@@ -1,5 +1,14 @@ CPSA NEWS + March, 2019:++* Release 3.6.2 adds the leads-to predicate to the rule language, adds+ better checks for malformed input, and fixes a bug so that now the+ default depth is infinite as is specified in the manual. It adds+ structured annotations to skeleton output to facilitate post+ processing programs besides cpsagraph. The sources for OCaml+ programs for processing CPSA input and output are now included.+ August, 2018: * Release 3.6.1 is a bug fix release. It includes updates to the CPSA
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 3.6.1+Version: 3.6.2 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.6 License: BSD3@@ -77,6 +77,12 @@ Makefile ChangeLog README.txt NEWS ghci cpsatst setup.bat src/cpsa.el src/cpsaops.scm src/cpsa.pl src/pp.pl src/sexpr.pl src/ghcmemlimit src/cpsajson.py src/split.py+ src/ocaml/Makefile src/ocaml/README src/ocaml/cpsa.d.itarget+ src/ocaml/cpsa.itarget src/ocaml/cpsa.mllib src/ocaml/cpsa.mltop+ src/ocaml/cpsa.odocl src/ocaml/expand.ml src/ocaml/main.ml+ src/ocaml/main.mli src/ocaml/pp.ml src/ocaml/reader.ml+ src/ocaml/reader.mli src/ocaml/scanner.mll src/ocaml/sexpr.ml+ src/ocaml/sexpr.mli src/ocaml/sexpr_type.ml tst/checktst tst/updatetst tst/graphtst tst/Makefile tst/Make.hs tst/README tst/axiom2.scm tst/axiom2.tst tst/blanchet.scm tst/blanchet.tst
doc/cpsamanual.pdf view
binary file changed (904514 → 904636 bytes)
doc/examples/blanchet.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Blanchet's Simple Example Protocol</title>@@ -12,7 +12,7 @@ <pre>(herald "Blanchet's Simple Example Protocol" (comment "There is a flaw in this protocol by design"))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from blanchet.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t4">4</a> <a href="#t6">6</a> <a href="#t11">11</a> <a href="#t14">14</a> <a href="#t18">18</a> <a href="#t23">23</a> <a href="#t25">25</a>.</p>@@ -852,6 +852,7 @@ (comment "From the responders's perspective, is the secret leaked?") (label 11) (unrealized (0 0) (1 0))+ (origs (d (0 1))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -1816,6 +1817,7 @@ (comment "From the responders's perspective, is the secret leaked?") (label 25) (unrealized (0 0) (1 0))+ (origs (d (0 1))) (preskeleton) (comment "Not a skeleton"))</pre>
doc/examples/bltk_or.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Otway-Rees Protocol</title>@@ -13,7 +13,7 @@ <pre>(herald "Otway-Rees Protocol" (comment "Standard version using variables of sort mesg") (algebra diffie-hellman))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from bltk_or.scm")</pre> <p id="t0">Tree 0.</p>
doc/examples/dh_mim.xhtml view
file too large to diff
doc/examples/envelope.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Envelope Protocol</title>@@ -11,7 +11,7 @@ <body> <pre>(herald "Envelope Protocol" (bound 20))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from envelope.scm") (comment "Strand count bounded at 20")</pre> @@ -495,6 +495,7 @@ (uniq-orig v n tno esk) (label 0) (unrealized (0 0) (1 0) (2 5))+ (origs (esk (2 0)) (n (2 2)) (tno (2 2)) (v (2 6))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -14919,6 +14920,7 @@ (uniq-orig v n tno esk) (label 59) (unrealized (0 0) (1 5))+ (origs (esk (1 0)) (n (1 2)) (tno (1 2)) (v (1 6))) (preskeleton) (comment "Not a skeleton"))</pre>
doc/examples/eq_test.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Equality constraint test protocol</title>@@ -13,7 +13,7 @@ <pre>(herald "Equality constraint test protocol" (comment "First skeleton should have a shape," "second, and hird should be dead."))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from eq_test.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t4">4</a>.</p>@@ -295,6 +295,7 @@ (uniq-orig n1 n2) (label 4) (unrealized (0 1))+ (origs (n1 (0 0)) (n2 (0 0))) (preskeleton) (comment "Not a skeleton"))</pre>
doc/examples/ffgg.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>The ffgg Protocol</title>@@ -12,7 +12,7 @@ <pre>(herald "The ffgg Protocol" (comment "From A Necessarily Parallel Attack by Jon K. Millen"))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from ffgg.scm")</pre> <p id="t0">Tree 0.</p>@@ -110,6 +110,7 @@ (uniq-orig m) (label 0) (unrealized (1 0))+ (origs (m (0 2))) (preskeleton) (comment "Not a skeleton"))</pre>
doc/examples/fnof_test.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Function constraint test protocol</title>@@ -12,7 +12,7 @@ <pre>(herald "Function constraint test protocol" (comment "Skeletons 2, 4, and 7 should have no shapes."))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from fnof_test.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t3">3</a> <a href="#t5">5</a> <a href="#t6">6</a> <a href="#t8">8</a> <a href="#t10">10</a>.</p>@@ -248,6 +248,7 @@ (uniq-orig n1) (label 3) (unrealized)+ (origs (n1 (0 0))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -350,6 +351,7 @@ (uniq-orig n1) (label 5) (unrealized)+ (origs (n1 (0 0))) (comment "Input cannot be made into a skeleton--nothing to do"))</pre> <p id="t6">Tree <a href="#top">6</a>.</p>
doc/examples/fnof_yahalom.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function</title>@@ -13,7 +13,7 @@ <pre>(herald "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function" (bound 12))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from fnof_yahalom.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t4">4</a> <a href="#t10">10</a> <a href="#t15">15</a>.</p>
doc/examples/goals.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>goals</title>@@ -11,7 +11,7 @@ <body> <pre>(herald goals)-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from goals.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t4">4</a> <a href="#t6">6</a> <a href="#t8">8</a> <a href="#t17">17</a> <a href="#t19">19</a> <a href="#t21">21</a> <a href="#t23">23</a> <a href="#t26">26</a> <a href="#t28">28</a> <a href="#t33">33</a> <a href="#t41">41</a>.</p>@@ -297,7 +297,7 @@ (parent 2) (unrealized) (shape)- (satisfies (no (b b) (n1 n1) (z0 0)))+ (satisfies yes) (maps ((0) ((b b) (n1 n1) (a a) (n2 n2)))) (origs (n1 (0 0))))</pre> @@ -729,6 +729,7 @@ "Secrecy goal: nonce n1 not revealed") (label 8) (unrealized (0 0) (1 1))+ (origs (n1 (1 0))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -2212,6 +2213,7 @@ "Failed secrecy goal: nonce n2 not revealed") (label 28) (unrealized (0 0) (1 2))+ (origs (n2 (1 1))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -3235,6 +3237,7 @@ (comment "Shows typeflaw in typeless NSL") (label 41) (unrealized (0 0))+ (origs (n2 (1 1))) (preskeleton) (comment "Not a skeleton"))</pre>
doc/examples/iadh_um.xhtml view
file too large to diff
doc/examples/kerb.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>kerb-flawed</title>@@ -10,7 +10,7 @@ </head> <body> -<pre>(comment "CPSA 3.6.0")+<pre>(comment "CPSA 3.6.2") (comment "All input read from kerb.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t5">5</a>.</p>@@ -112,6 +112,7 @@ (uniq-orig m n) (label 0) (unrealized (0 1) (1 0))+ (origs (n (0 0)) (m (0 2))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -483,6 +484,7 @@ (uniq-orig m n) (label 5) (unrealized (0 1) (1 0))+ (origs (n (0 0)) (m (0 2))) (preskeleton) (comment "Not a skeleton"))</pre>
doc/examples/lt_test.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Less-than constraint test protocol</title>@@ -13,7 +13,7 @@ <pre>(herald "Less-than constraint test protocol" (comment "First and third skeletons should have a shape," "second and fourth should be dead."))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from lt_test.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t3">3</a> <a href="#t5">5</a>.</p>
doc/examples/neq_test.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Inequality constraint test protocol</title>@@ -13,7 +13,7 @@ <pre>(herald "Inequality constraint test protocol" (comment "First skeleton should have a shape," "second, and hird should be dead."))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from neq_test.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t3">3</a>.</p>
doc/examples/ns.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Needham-Schroeder Public-Key Protocol</title>@@ -13,7 +13,7 @@ <pre>(herald "Needham-Schroeder Public-Key Protocol" (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe."))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from ns.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t3">3</a>.</p>
doc/examples/or.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Otway-Rees Protocol</title>@@ -12,7 +12,7 @@ <pre>(herald "Otway-Rees Protocol" (comment "Standard version using variables of sort mesg"))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from or.scm")</pre> <p id="t0">Tree 0.</p>
doc/examples/pkinit.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Kerberos PKINIT</title>@@ -11,7 +11,7 @@ <body> <pre>(herald "Kerberos PKINIT")-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from pkinit.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t8">8</a> <a href="#t13">13</a> <a href="#t16">16</a> <a href="#t23">23</a>.</p>@@ -1143,6 +1143,7 @@ (non (privk c))) (= c c-0)))) (label 13) (unrealized (1 1))+ (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -1418,6 +1419,7 @@ (non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2))))) (label 16) (unrealized (1 1))+ (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (preskeleton) (comment "Not a skeleton"))</pre> @@ -1978,6 +1980,7 @@ (non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2))))) (label 23) (unrealized (1 1))+ (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (preskeleton) (comment "Not a skeleton"))</pre>
doc/examples/plaindh.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Plain diffie-hellman protocol with challenge-response</title>@@ -12,7 +12,7 @@ <pre>(herald "Plain diffie-hellman protocol with challenge-response" (algebra diffie-hellman))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from plaindh.scm")</pre> <p id="t0">Tree 0.</p>
doc/examples/priority_test.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Receive priority test protocol</title>@@ -11,7 +11,7 @@ <body> <pre>(herald "Receive priority test protocol")-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from priority_test.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t3">3</a>.</p>
doc/examples/station.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Station-to-station protocol</title>@@ -11,7 +11,7 @@ <body> <pre>(herald "Station-to-station protocol" (algebra diffie-hellman))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from station.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t10">10</a> <a href="#t20">20</a> <a href="#t23">23</a>.</p>
doc/examples/subsort_test.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Subsort constraint test protocol</title>@@ -13,7 +13,7 @@ <pre>(herald "Subsort constraint test protocol" (comment "First, third, and fourth skeletons should have a shape," "second should be dead."))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from subsort_test.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t3">3</a> <a href="#t5">5</a>.</p>
doc/examples/woolam.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Woo-Lam Protocol</title>@@ -11,7 +11,7 @@ <body> <pre>(herald "Woo-Lam Protocol")-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from woolam.scm")</pre> <p id="t0">Tree 0.</p>
doc/examples/yahalom.xhtml view
@@ -1,5 +1,5 @@ <?xml version="1.0"?>-<!-- CPSA 3.6.0 -->+<!-- CPSA 3.6.2 --> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title>Yahalom Protocol with Forwarding Removed</title>@@ -12,7 +12,7 @@ <pre>(herald "Yahalom Protocol with Forwarding Removed" (algebra diffie-hellman) (bound 12))-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.2") (comment "All input read from yahalom.scm")</pre> <p id="top">Trees: <a href="#t0">0</a> <a href="#t52">52</a>.</p>
src/CPSA/Lib/Characteristic.hs view
@@ -144,6 +144,7 @@ mkSkel pos p goals nmap g insts as comment = do let o = foldr (mkPrec nmap) [] as+ let lto = foldr (mkLeadsTo nmap) [] as let nr = foldr mkNon [] as let ar = foldr mkPnon [] as let ur = foldr mkUniq [] as@@ -151,7 +152,7 @@ let decls = mkDcls nr ar ur gr let fs = foldr (mkFact nmap) [] as let prios = []- let k = mkPreskel g p goals insts o [] decls fs comment prios Nothing []+ let k = mkPreskel g p goals insts o lto decls fs comment prios Nothing [] mapM_ (checkUniqAt nmap k) as case termsWellFormed $ (termsInDlist decls) ++ kterms k of False -> fail (shows pos "Terms in skeleton not well formed")@@ -168,6 +169,12 @@ mkPrec nmap (_, Prec n n') o = (nMapLookup n nmap, nMapLookup n' nmap) : o mkPrec _ _ o = o++mkLeadsTo :: Eq t => [(t, Sid)] ->+ (Pos, AForm t) -> [Pair] -> [Pair]+mkLeadsTo nmap (_, LeadsTo n n') o =+ (nMapLookup n nmap, nMapLookup n' nmap) : o+mkLeadsTo _ _ o = o mkDcls :: [t] -> [t] -> [t] -> [t] -> SkelDeclList t mkDcls nr ar ur gr =
src/CPSA/Lib/Cohort.hs view
@@ -134,12 +134,12 @@ -- pos = p -- ek = encription key if ct is an encyption else nothing -- escape = esc(k, v, t)--- k' = k--- (s, p) = v and n+-- k = k'+-- n = v -- subst = sigma solved :: Algebra t p g s e c => t -> p -> [t] -> Set t -> Preskel t g s e -> Node -> s -> [(t,t)] -> Bool-solved ct pos eks escape k (s, p) subst absent =+solved ct pos eks escape k n subst absent = -- Condition 1 isAncestorInSet escape' t pos || derivable a escape' ct' || -- Condition 2@@ -155,7 +155,7 @@ -- Condition 6: hack! length (kabsent k) > length absent where- v = vertex k (s, p) -- Look up vertex in k+ v = vertex k n -- Look up vertex in k t = evt id erro errs (event v) -- Term at v erro = const $ assertError "Cohort.solved: got an outbound term" errs = const $ assertError "Cohort.solved: got a state synchronization term"
src/CPSA/Lib/Displayer.hs view
@@ -84,6 +84,9 @@ displayForm ctx (Prec (x, i) (y, j)) = L () [S () "prec", displayTerm ctx x, N () i, displayTerm ctx y, N () j]+displayForm ctx (LeadsTo (x, i) (y, j)) =+ L () [S () "leads-to", displayTerm ctx x, N () i,+ displayTerm ctx y, N () j] displayForm ctx (Non t) = L () [S () "non", displayTerm ctx t] displayForm ctx (Pnon t) =
src/CPSA/Lib/Entry.hs view
@@ -99,7 +99,7 @@ optGoalsSat = False, optLimit = 2000, optBound = 12,- optDepth = 32,+ optDepth = 0, optMargin = 72, optIndent = 2 }
src/CPSA/Lib/Expand.hs view
@@ -114,7 +114,7 @@ macroExpand :: Monad m => [Macro] -> Pos -> Int -> SExpr Pos -> m (SExpr Pos) macroExpand _ pos limit _- | limit <= 0 = fail (shows pos "Expansion limit exceded")+ | limit <= 0 = fail (shows pos "Expansion limit exceeded") macroExpand macs pos limit sexpr@(L _ (S _ sym : xs)) = case macroExpand1 macs sym xs of Nothing -> return sexpr -- Nothing to do
src/CPSA/Lib/Loader.hs view
@@ -311,7 +311,8 @@ t2 <- loadTerm vars False x2 p <- loadIntMax height x3 return (declInstAux [t1,t2] [p] stag)-loadRoleTermPairPlusMaybeOneLoc _ _ _ _ = fail ("Malformed pair of terms")+loadRoleTermPairPlusMaybeOneLoc _ _ _ x = fail+ (shows (annotation x) "Malformed pair of terms") loadSkelTermPair :: (Algebra t p g s e c, Monad m) => [t] -> String -> SExpr Pos -> m (SkelDeclInst t)@@ -320,7 +321,8 @@ t1 <- loadTerm vars False x1 t2 <- loadTerm vars False x2 return (declInstAux [t1,t2] [] stag)-loadSkelTermPair _ _ _ = fail ("Malformed pair of terms")+loadSkelTermPair _ _ x = fail+ (shows (annotation x) "Malformed pair of terms") loadRolePriority :: Monad m => Int -> SExpr Pos -> m (Int, Int) loadRolePriority n (L _ [N _ i, N _ p])@@ -344,7 +346,7 @@ (g, xs) <- loadVars g [L pos [S pos "x", S pos "mesg"]] case xs of [x] -> return (g, mkRole "" [x] [In x, Out x] [] [] [] False)- _ -> fail "Loader.mkListenerRole: Expection one variable"+ _ -> fail (shows pos "Loader.mkListenerRole: Expecting one term") -- Protocol Rules @@ -355,8 +357,11 @@ (g, r) <- loadRule prot g pos x (g, rs, comment) <- loadRules prot g xs return (g, r : rs, comment)+loadRules _ _ (L pos (S _ "defrole" : S _ name : _) : _) =+ fail (shows pos ("defrole " ++ name ++ " misplaced")) loadRules _ g xs = do+ badKey ["defrole", "defrule"] xs comment <- alist [] xs -- Ensure remaining is an alist return (g, [], comment) @@ -412,6 +417,14 @@ f (L _ (S _ head : _)) = head == key f _ = False +-- Complain if alist has a bad key+badKey :: Monad m => [String] -> [SExpr Pos] -> m ()+badKey keys (L _ (S pos key : _) : xs)+ | elem key keys =+ fail (shows pos (key ++ " declaration too late in enclosing form"))+ | otherwise = badKey keys xs+badKey _ _ = return ()+ loadTrace :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [Event t] loadTrace vars xs = mapM (loadEvt vars) xs@@ -565,6 +578,7 @@ fail (shows pos "Malformed deflistener") loadInsts top p kvars gen insts xs = do+ badKey ["defstrand", "deflistener"] xs _ <- alist [] xs -- Check syntax of xs others <- loadGenSkelDecls heights kvars (assocDecls xs) predefs <- loadAllPredefSkelDecls heights kvars xs@@ -1069,6 +1083,11 @@ t <- loadNodeTerm kvars w x t' <- loadNodeTerm kvars y z return (pos, Prec t t')+loadPrimary _ _ kvars (L pos [S _ "leads-to", w, x, y, z]) =+ do+ t <- loadNodeTerm kvars w x+ t' <- loadNodeTerm kvars y z+ return (pos, LeadsTo t t') loadPrimary _ p kvars (L pos [S _ "p", Q _ name, x, N _ h]) = do r <- lookupRole pos p name@@ -1150,6 +1169,9 @@ roleSpecific unbound (pos, Prec (z, _) (z', _)) | L.notElem z unbound && L.notElem z' unbound = return unbound | otherwise = fail (shows pos "Unbound variable in prec")+roleSpecific unbound (pos, LeadsTo (z, _) (z', _))+ | L.notElem z unbound && L.notElem z' unbound = return unbound+ | otherwise = fail (shows pos "Unbound variable in leadsto") roleSpecific unbound (pos, Non t) | allBound unbound t = return unbound | otherwise = fail (shows pos "Unbound variable in non")
src/CPSA/Lib/Main.hs view
@@ -214,7 +214,7 @@ Option ['b'] ["bound"] (ReqArg Bound "INT") ("strand count bound (default " ++ show defaultStrandBound ++ ")"), Option ['d'] ["depth"] (ReqArg Depth "INT")- ("tree depth bound (default " ++ show defaultDepthBound ++ ")"),+ ("tree depth bound (default unbounded)"), Option ['m'] ["margin"] (ReqArg Margin "INT") ("set output margin (default " ++ show (optMargin defaultOptions) ++ ")"), Option ['e'] ["expand"] (NoArg Expand)
src/CPSA/Lib/Printer.hs view
@@ -23,30 +23,60 @@ -- occur, all breaks are forced. Also, breaks are only placed before -- strings and lists. CPSA protocols are handled specially. Each -- defrole is handled as are top-level lists.++-- Update: there are special layout rules for formulas in defgoal's+-- and defrule's. pretty :: Printer a pretty indent (L _ (x@(S _ "defprotocol") : xs)) = loop [block indent x, str "("] xs where loop es [] = grp indent (reverse (str ")" : es))- loop es (x@(S _ _):xs) = loop (block indent x : str " " : es) xs- loop es (x@(Q _ _):xs) = loop (block indent x : brk 1 : es) xs- loop es (x@(N _ _):xs) = loop (block indent x : str " " : es) xs- loop es (x@(L _ (S _ "defrole": _)):xs) =+ loop es (x@(S _ _) : xs) = loop (block indent x : str " " : es) xs+ loop es (x@(Q _ _) : xs) = loop (block indent x : brk 1 : es) xs+ loop es (x@(N _ _) : xs) = loop (block indent x : str " " : es) xs+ loop es (x@(L _ (S _ "defrole" : _)) : xs) = loop (group indent x : brk 1 : es) xs- loop es (x@(L _ _):xs) = loop (block indent x : brk 1 : es) xs-pretty indent x@(L _ (S _ "defmacro" : _)) = block indent x+ loop es ((L _ (x@(S _ "defrule") : forms)) : xs) =+ loop (formula indent x forms : brk 1 : es) xs+ loop es (x@(L _ _) : xs) = loop (block indent x : brk 1 : es) xs+pretty indent (L _ (x@(S _ "defgoal") : forms)) = formula indent x forms+pretty indent x@(L _ (S _ "defmacro" : _)) = group indent x pretty indent x@(L _ (S _ "herald" : _)) = block indent x pretty indent x = group indent x +formula :: Int -> SExpr a -> [SExpr a] -> Pretty+formula indent x xs =+ loop [block indent x, str "("] xs+ where+ loop es [] = grp indent (reverse (str ")" : es))+ loop es (L _ [S _ "forall", decs,+ L _ [S _ "implies", antec, concl]] : xs) =+ loop+ (blo indent+ [str "(forall", brk 1, block indent decs, brk 1,+ grp indent+ [str "(implies", brk 1,+ block indent antec, brk 1,+ disj indent concl],+ str "))"] : brk 1 : es)+ xs+ loop es (x@(S _ _) : xs) = loop (block indent x : str " " : es) xs+ loop es (x@(N _ _) : xs) = loop (block indent x : str " " : es) xs+ loop es (x : xs) = loop (block indent x : brk 1 : es) xs++disj :: Int -> SExpr a -> Pretty+disj indent x@(L _ (S _ "or" : _)) = group indent x+disj indent x = block indent x+ group :: Printer a group indent (L _ (x:xs)) = loop [block indent x, str "("] xs where loop es [] = grp indent (reverse (str ")" : es))- loop es (x@(S _ _):xs) = loop (block indent x : str " " : es) xs- loop es (x@(Q _ _):xs) = loop (block indent x : brk 1 : es) xs- loop es (x@(N _ _):xs) = loop (block indent x : str " " : es) xs- loop es (x@(L _ _):xs) = loop (block indent x : brk 1 : es) xs+ loop es (x@(S _ _) : xs) = loop (block indent x : str " " : es) xs+ loop es (x@(Q _ _) : xs) = loop (block indent x : brk 1 : es) xs+ loop es (x@(N _ _) : xs) = loop (block indent x : str " " : es) xs+ loop es (x@(L _ _) : xs) = loop (block indent x : brk 1 : es) xs group indent x = block indent x -- A pretty printer for interior lists using block style breaking.@@ -55,7 +85,7 @@ block _ (Q _ s) = str (showQuoted s "") block _ (N _ n) = str (show n) block _ (L _ []) = str "()"-block indent (L _ (x:xs)) =+block indent (L _ (x : xs)) = loop [block indent x, str "("] xs where loop es [] = blo indent (reverse (str ")" : es))
src/CPSA/Lib/Protocol.hs view
@@ -395,6 +395,7 @@ = Length (Role t) t Int | Param (Role t) t Int t t -- role param first-height strand value | Prec (NodeTerm t) (NodeTerm t)+ | LeadsTo (NodeTerm t) (NodeTerm t) | Non t | Pnon t | Uniq t@@ -419,6 +420,7 @@ aFormOrder (Length _ _ _) (Length _ _ _) = EQ aFormOrder (Length _ _ _) (Param _ _ _ _ _) = LT aFormOrder (Length _ _ _) (Prec _ _) = LT+aFormOrder (Length _ _ _) (LeadsTo _ _) = LT aFormOrder (Length _ _ _) (Non _) = LT aFormOrder (Length _ _ _) (Pnon _) = LT aFormOrder (Length _ _ _) (Uniq _) = LT@@ -430,6 +432,7 @@ aFormOrder (Param _ _ _ _ _) (Length _ _ _) = GT aFormOrder (Param _ _ _ _ _) (Param _ _ _ _ _) = EQ aFormOrder (Param _ _ _ _ _) (Prec _ _) = LT+aFormOrder (Param _ _ _ _ _) (LeadsTo _ _) = LT aFormOrder (Param _ _ _ _ _) (Non _) = LT aFormOrder (Param _ _ _ _ _) (Pnon _) = LT aFormOrder (Param _ _ _ _ _) (Uniq _) = LT@@ -441,6 +444,7 @@ aFormOrder (Prec _ _) (Length _ _ _) = GT aFormOrder (Prec _ _) (Param _ _ _ _ _) = GT aFormOrder (Prec _ _) (Prec _ _) = EQ+aFormOrder (Prec _ _) (LeadsTo _ _) = LT aFormOrder (Prec _ _) (Non _) = LT aFormOrder (Prec _ _) (Pnon _) = LT aFormOrder (Prec _ _) (Uniq _) = LT@@ -449,9 +453,22 @@ aFormOrder (Prec _ _) (Ugen _) = LT aFormOrder (Prec _ _) (AFact _ _) = LT aFormOrder (Prec _ _) (Equals _ _) = LT+aFormOrder (LeadsTo _ _) (Length _ _ _) = GT+aFormOrder (LeadsTo _ _) (Param _ _ _ _ _) = GT+aFormOrder (LeadsTo _ _) (Prec _ _) = GT+aFormOrder (LeadsTo _ _) (LeadsTo _ _) = EQ+aFormOrder (LeadsTo _ _) (Non _) = LT+aFormOrder (LeadsTo _ _) (Pnon _) = LT+aFormOrder (LeadsTo _ _) (Uniq _) = LT+aFormOrder (LeadsTo _ _) (UniqAt _ _) = LT+aFormOrder (LeadsTo _ _) (UgenAt _ _) = LT+aFormOrder (LeadsTo _ _) (Ugen _) = LT+aFormOrder (LeadsTo _ _) (AFact _ _) = LT+aFormOrder (LeadsTo _ _) (Equals _ _) = LT aFormOrder (Non _) (Length _ _ _) = GT aFormOrder (Non _) (Param _ _ _ _ _) = GT aFormOrder (Non _) (Prec _ _) = GT+aFormOrder (Non _) (LeadsTo _ _) = GT aFormOrder (Non _) (Non _) = EQ aFormOrder (Non _) (Pnon _) = LT aFormOrder (Non _) (Uniq _) = LT@@ -463,6 +480,7 @@ aFormOrder (Pnon _) (Length _ _ _) = GT aFormOrder (Pnon _) (Param _ _ _ _ _) = GT aFormOrder (Pnon _) (Prec _ _) = GT+aFormOrder (Pnon _) (LeadsTo _ _) = GT aFormOrder (Pnon _) (Non _) = GT aFormOrder (Pnon _) (Pnon _) = EQ aFormOrder (Pnon _) (Uniq _) = LT@@ -474,6 +492,7 @@ aFormOrder (Uniq _) (Length _ _ _) = GT aFormOrder (Uniq _) (Param _ _ _ _ _) = GT aFormOrder (Uniq _) (Prec _ _) = GT+aFormOrder (Uniq _) (LeadsTo _ _) = GT aFormOrder (Uniq _) (Non _) = GT aFormOrder (Uniq _) (Pnon _) = GT aFormOrder (Uniq _) (Uniq _) = EQ@@ -485,6 +504,7 @@ aFormOrder (UniqAt _ _) (Length _ _ _) = GT aFormOrder (UniqAt _ _) (Param _ _ _ _ _) = GT aFormOrder (UniqAt _ _) (Prec _ _) = GT+aFormOrder (UniqAt _ _) (LeadsTo _ _) = GT aFormOrder (UniqAt _ _) (Non _) = GT aFormOrder (UniqAt _ _) (Pnon _) = GT aFormOrder (UniqAt _ _) (Uniq _) = GT@@ -496,6 +516,7 @@ aFormOrder (UgenAt _ _) (Length _ _ _) = GT aFormOrder (UgenAt _ _) (Param _ _ _ _ _) = GT aFormOrder (UgenAt _ _) (Prec _ _) = GT+aFormOrder (UgenAt _ _) (LeadsTo _ _) = GT aFormOrder (UgenAt _ _) (Non _) = GT aFormOrder (UgenAt _ _) (Pnon _) = GT aFormOrder (UgenAt _ _) (Uniq _) = GT@@ -507,6 +528,7 @@ aFormOrder (Ugen _) (Length _ _ _) = GT aFormOrder (Ugen _) (Param _ _ _ _ _) = GT aFormOrder (Ugen _) (Prec _ _) = GT+aFormOrder (Ugen _) (LeadsTo _ _) = GT aFormOrder (Ugen _) (Non _) = GT aFormOrder (Ugen _) (Pnon _) = GT aFormOrder (Ugen _) (Uniq _) = GT@@ -518,6 +540,7 @@ aFormOrder (AFact _ _) (Length _ _ _) = GT aFormOrder (AFact _ _) (Param _ _ _ _ _) = GT aFormOrder (AFact _ _) (Prec _ _) = GT+aFormOrder (AFact _ _) (LeadsTo _ _) = GT aFormOrder (AFact _ _) (Non _) = GT aFormOrder (AFact _ _) (Pnon _) = GT aFormOrder (AFact _ _) (Uniq _) = GT@@ -529,6 +552,7 @@ aFormOrder (Equals _ _) (Length _ _ _) = GT aFormOrder (Equals _ _) (Param _ _ _ _ _) = GT aFormOrder (Equals _ _) (Prec _ _) = GT+aFormOrder (Equals _ _) (LeadsTo _ _) = GT aFormOrder (Equals _ _) (Non _) = GT aFormOrder (Equals _ _) (Pnon _) = GT aFormOrder (Equals _ _) (Uniq _) = GT@@ -542,6 +566,7 @@ aFreeVars vars (Length _ z _) = addVars vars z aFreeVars vars (Param _ _ _ z t) = addVars (addVars vars z) t aFreeVars vars (Prec (x, _) (y, _)) = addVars (addVars vars x) y+aFreeVars vars (LeadsTo (x, _) (y, _)) = addVars (addVars vars x) y aFreeVars vars (Non t) = addVars vars t aFreeVars vars (Pnon t) = addVars vars t aFreeVars vars (Uniq t) = addVars vars t
src/CPSA/Lib/Reduction.hs view
@@ -138,7 +138,7 @@ [] -> -- Input cannot be made into a skeleton do let lk = LPreskel k n 0 Nothing- wrt p h (commentPreskel lk [] (unrealized k) Ordinary+ wrt p h (commentPreskel lk [] (unrealized k) Ordinary Nada "Input cannot be made into a skeleton--nothing to do") solve p h ks (n + 1) ks' ->@@ -150,8 +150,8 @@ do let lk = LPreskel k n (-1) Nothing let ks'' = L.nubBy (\k1 k2 -> isomorphic (gist k1) (gist k2)) ks'- wrt p h (commentPreskel lk [] (unrealized k) Ordinary- "Not a skeleton")+ wrt p h (commentPreskel lk [] (unrealized k) Ordinary + Preskeleton "Not a skeleton") let lk_nums = zip [(n+1) .. (n+length(ks'))] ks'' let lks' = map (\(n', k')-> withParent k' n' lk) lk_nums begin p h ks (n + optLimit p) (n+length(ks'')+1)@@ -173,7 +173,7 @@ Just kids -> do wrt p h (commentPreskel lk [] (unrealized k) Ordinary- "Not closed under rules")+ Nada "Not closed under rules") let (n', seen', todo', _) = foldl (next lk) (n, seen, todo, []) kids loop n' seen' todo' lks@@ -256,7 +256,7 @@ do let ns = unrealized (content lk) let shape = if null ns then Shape else Fringe- wrt p h (commentPreskel lk [] ns shape "satisfies all")+ wrt p h (commentPreskel lk [] ns shape SatisfiesAll "satisfies all") step p h ks m oseen n seen todo tobig reducts | size <= 0 = -- Interpret empty reducts do@@ -264,12 +264,13 @@ let shape = if null ns then Shape else Ordinary let live = null $ thresholdUnrealized (content lk) wrt p h (commentPreskel lk [] ns shape+ (if live then Nada else Dead) (if live then "" else "empty cohort")) step p h ks m oseen n seen todo tobig reducts- | depth lk >= optDepth p =+ | optDepth p > 0 && depth lk >= optDepth p = do let ns = unrealized (content lk)- wrt p h (commentPreskel lk [] ns Fringe "")+ wrt p h (commentPreskel lk [] ns Fringe Nada "") step p h ks m oseen n seen todo tobig reducts | otherwise = do@@ -279,7 +280,7 @@ let u = size - length dups' let msg = shows size $ showString " in cohort - " $ shows u " not yet seen"- wrt p h (commentPreskel lk (reverse dups') ns Ordinary msg)+ wrt p h (commentPreskel lk (reverse dups') ns Ordinary Nada msg) step p h ks m oseen n' seen' todo' tobig reducts -- Expands one branch in the derivation tree.@@ -356,7 +357,7 @@ let ks' = reduce (mkMode p) (content lk) let msg = show (length ks') ++ " in cohort" let shape = if null ns then Shape else Ordinary- wrt p h (commentPreskel lk [] ns shape msg)+ wrt p h (commentPreskel lk [] ns shape Nada msg) let (n', todo') = foldl (children lk) (n, []) ks' fast p h ks m n' (todo ++ reverse todo') @@ -375,22 +376,22 @@ dump p h (lk : lks) msg = do let ns = unrealized $ content lk- wrt p h (commentPreskel lk [] ns Ordinary "aborted")+ wrt p h (commentPreskel lk [] ns Aborted Nada "aborted") dump p h lks msg -- Add a label, maybe a parent, a list of seen preskeletons isomorphic -- to some members of this skeleton's cohort, and a list of unrealized -- nodes. If it's a shape, note this fact. Add a comment if present. commentPreskel :: Algebra t p g s e c => LPreskel t g s e ->- [Int] -> [Node] -> Kind -> String -> SExpr ()-commentPreskel lk seen unrealized kind msg =+ [Int] -> [Node] -> Kind -> Anno -> String -> SExpr ()+commentPreskel lk seen unrealized kind anno msg = displayPreskel k $ addKeyValues "label" [N () (label lk)] $ maybeAddVKeyValues "parent" (\p -> [N () (label p)]) (parent lk) $ condAddKeyValues "seen" (not $ null seen) (map (N ()) (L.sort (L.nub seen))) $ addKeyValues "unrealized" (map displayNode $ L.sort unrealized) $- addKindKey kind $+ addKindKey kind $ addAnnoKey anno $ condAddKeyValues "satisfies" (kind == Shape && (not $ null $ kgoals k)) (satisfies k) $ -- Structure preserving maps@@ -402,15 +403,13 @@ -- Messages case msg of "" -> []- -- Preskeleton key added for cpsasas program- "Not a skeleton" -> addKeyValues "preskeleton" [] [comment msg] _ -> [comment msg] where- fringe = kind /= Ordinary+ fringe = isFringe kind k = content lk starter k = -- True for the POV skeleton and case pov k of -- just a few others- Nothing -> False+ Nothing -> True Just k' -> nstrands k == nstrands k' addKeyValues :: String -> [SExpr ()] -> [SExpr ()] -> [SExpr ()]@@ -434,12 +433,33 @@ = Ordinary | Shape | Fringe+ | Aborted deriving (Eq, Show) addKindKey :: Kind -> [SExpr ()] -> [SExpr ()] addKindKey Ordinary xs = xs addKindKey Shape xs = addKeyValues "shape" [] xs addKindKey Fringe xs = addKeyValues "fringe" [] xs+addKindKey Aborted xs = addKeyValues "aborted" [] xs++isFringe :: Kind -> Bool+isFringe Ordinary = False+isFringe Shape = True+isFringe Fringe = True+isFringe Aborted = False++-- Skeleton annotations+data Anno+ = Nada+ | Preskeleton+ | SatisfiesAll+ | Dead++addAnnoKey :: Anno -> [SExpr ()] -> [SExpr ()]+addAnnoKey Nada xs = xs+addAnnoKey Preskeleton xs = addKeyValues "preskeleton" [] xs+addAnnoKey SatisfiesAll xs = addKeyValues "satisfies-all" [] xs+addAnnoKey Dead xs = addKeyValues "dead" [] xs -- Variable assignments and security goals
src/CPSA/Lib/Strand.hs view
@@ -2637,6 +2637,7 @@ satisfy (UgenAt t n) = gugenAt t n satisfy (Ugen t) = gugen t satisfy (Prec n n') = gprec n n'+satisfy (LeadsTo n n') = gleadsTo n n' satisfy (Length r n i) = glength r n i satisfy (Param r v f n t) = gparam r v f n t @@ -2767,6 +2768,18 @@ where tc = map graphPair $ graphClose $ graphEdges $ strands k +-- Node leads to+gleadsTo :: Algebra t p g s e c => NodeTerm t -> NodeTerm t -> Sem t g s e+gleadsTo n n' k (g, e) =+ case (nodeLookup e n, nodeLookup e n') of+ (Just p, Just p')+ | inSkel k p && inSkel k p' && elem (p, p') (leadsto k) -> [(g, e)]+ _ ->+ do+ (p, p') <- leadsto k+ (g, e) <- nodeMatch n p (g, e)+ nodeMatch n' p' (g, e)+ -- Length predicate -- r and h determine the predicate, which has arity one. glength :: Algebra t p g s e c => Role t -> t -> Int -> Sem t g s e@@ -2952,6 +2965,7 @@ rwt _ (Length r z h) = rlength r z h rwt rule (Param r v i z t) = rparam rule r v i z t rwt rule (Prec n n') = rprec rule n n'+rwt rule (LeadsTo n n') = rleadsTo rule n n' rwt rule (Non t) = rlnon rule t rwt rule (Pnon t) = rlpnon rule t rwt rule (Uniq t) = rluniq rule t@@ -3102,6 +3116,23 @@ badIndex :: Algebra t p g s e c => Preskel t g s e -> Sid -> Int -> Bool badIndex k s i = i >= height (strandInst k s)++rleadsTo :: Algebra t p g s e c => String -> NodeTerm t ->+ NodeTerm t -> Rewrite t g s e+rleadsTo name (z, i) (z', i') k (g, e) =+ case (strdLookup e z, strdLookup e z') of+ (Just s, Just s')+ | elem ((s, i), (s', i')) (leadsto k) -> [(k, (g, e))]+ | badIndex k s i || badIndex k s' i' -> []+ | otherwise ->+ do -- Add one ordering+ let leadsto' = ((s, i), (s', i')) : leadsto k+ let k' = newPreskel g (shared k) (insts k) (orderings k)+ leadsto' (decls k) (kfacts k) (operation k)+ (prob k) (kpriority k) (pov k)+ return (k', (gen k, e))+ _ ->+ error ("In rule " ++ name ++ ", leads to did not get a strand") withNewDecl :: Algebra t p g s e c => Preskel t g s e -> SkelDeclarations t -> Preskel t g s e
src/CPSA/SAS/SAS.hs view
@@ -52,8 +52,8 @@ do p <- findProt pos ps xs k <- loadPreskel pos p (pgen p) xs- case (isSkeleton k, isFringe k) of- (True, False) ->+ case (isFringe k) of+ False -> do -- Found POV origCheck pos k -- Ensure uniqs originate return ((ps, [k]), Nothing)@@ -264,7 +264,6 @@ origs :: [(t, (t, Int))], -- ugen, ugenAt missing! facts :: [Fact t],- isSkeleton :: Bool, isFringe :: !Bool, -- Always looked at, so make it strict homomorphisms :: [SExpr Pos], -- Loaded later varmap :: VM t }@@ -297,7 +296,6 @@ uniqs = uniqs, origs = map g origs, facts = facts,- isSkeleton = not $ hasKey preskeletonKey xs, isFringe = hasKey shapeKey xs || hasKey fringeKey xs, homomorphisms = assoc mapsKey xs, varmap = varmap})@@ -473,7 +471,7 @@ loadMap pov k (L _ [L _ strandMap, L _ algebraMap]) = do perm <- mapM loadPerm strandMap -- Load the strand map- let nh = map (loadStrandEq k perm) (M.assocs $ varmap pov)+ nh <- mapM (loadStrandEq k perm) (M.assocs $ varmap pov) -- Load the algebra part of the homomorphism ah <- mapM (loadMaplet (kvars k) (kvars pov)) algebraMap return (nh, ah)@@ -484,11 +482,17 @@ loadPerm x = fail (shows (annotation x) "Expecting a natural number") -- Applies a strand permutation to a strand.--- Hope the strand map is valid, or !! will blow up.-loadStrandEq :: Preskel t g c -> [Int] -> (Strand, t) -> (t, t)+loadStrandEq :: Monad m => Preskel t g c -> [Int] -> (Strand, t) -> m (t, t) loadStrandEq k perm (z, v) =- (v, slookup (perm !! z) (varmap k))+ do+ z <- index perm z+ return (v, slookup z (varmap k)) +index :: Monad m => [a] -> Int -> m a+index (x : _) 0 = return x+index (_ : xs) i | i > 0 = index xs (i - 1)+index _ _ = fail "Bad strand map"+ -- Association lists -- Lookup value in alist, appending values with the same key@@ -502,10 +506,6 @@ hasKey :: String -> [SExpr a] -> Bool hasKey key alist = any (keyPred key) alist---- The key used to identify a non-skeleton-preskeletonKey :: String-preskeletonKey = "preskeleton" -- The key used to identify a shape shapeKey :: String
+ src/ocaml/Makefile view
@@ -0,0 +1,25 @@+# OCaml Makefile that relies on ocamlbuild+#+# Type "make cpsa.d.otarget" to make a debugable executable+#+# Enable warnings by adding to OCFLAGS: -cflags "-w +A-4"++OCFLAGS = -classic-display -use-ocamlfind -cflags "-w +A-4"+OCB = ocamlbuild+# Define DEBUG during development+# DEBUG = d.+TARGET = cpsa.$(DEBUG)otarget++all:+ $(OCB) $(OCFLAGS) $(TARGET)++clean:+ $(OCB) $(OCFLAGS) -clean++Makefile:+ @echo make $@++%: force+ $(OCB) $(OCFLAGS) $@++.PHONY: all clean force
+ src/ocaml/README view
@@ -0,0 +1,5 @@+This directory contains ocaml code for reading and writing CPSA+S-expressions. See sexpr.mli for exported functions on S-expressions.+Module Main provides a top-level loop for writing simple filters.+Module Pp is a simple example of using Main to pretty print+the S-expressions in a file.
+ src/ocaml/cpsa.d.itarget view
@@ -0,0 +1,1 @@+cpsa.d.cma
+ src/ocaml/cpsa.itarget view
@@ -0,0 +1,5 @@+pp.native+expand.native+cpsa.cma+cpsa.docdir/index.html+# cpsa.top
+ src/ocaml/cpsa.mllib view
@@ -0,0 +1,5 @@+Sexpr_type+Reader+Scanner+Sexpr+Main
+ src/ocaml/cpsa.mltop view
@@ -0,0 +1,4 @@+Sexpr_type+Reader+Scanner+Sexpr
+ src/ocaml/cpsa.odocl view
@@ -0,0 +1,3 @@+Sexpr+Reader+Main
+ src/ocaml/expand.ml view
@@ -0,0 +1,152 @@+(* Expand macros as is done by CPSA *)++open Lexing+open Sexpr+open Reader+open Main++(* The macro expand loop limit *)+let limit = 1000++(* Include depth bound *)+let bound = 16++type macro = {+ name: string;+ args: string list;+ body: position sexpr;+ }++(**** Define a macro ****)++let symbol = function+ | S (_, s) -> s+ | x -> failwith_msg (annotation x) "Expecting a symbol"++let defmacro pos = function+ | [L (_, name :: args); body] ->+ {+ name = symbol name;+ args = List.map symbol args;+ body = body;+ }+ | _ -> failwith_msg pos "Malformed macro"++(**** Expand macros ****)++(* lookup key in association list with default *)++let rec lookup default x = function+ | [] -> default+ | (s, y) :: _ when s = x -> y+ | _ :: xs -> lookup default x xs++let rec subst env = function+ | S (_, s) as x -> lookup x s env+ | L (pos, xs) -> L (pos, List.map (subst env) xs)+ | x -> x++let rec zip xs ys =+ match (xs, ys) with+ | (x :: xs, y :: ys) -> (x, y) :: zip xs ys+ | _ -> []++let apply mac args =+ subst (zip mac.args args) mac.body++let rec expand_one macs sym xs =+ match macs with+ | [] -> None+ | mac :: _ when mac.name = sym &&+ List.length mac.args = List.length xs ->+ Some (apply mac xs)+ | _ :: macs -> expand_one macs sym xs++let rec limited_expand macs pos limit = function+ | L (_, S (_, sym) :: xs) as x when limit > 0 ->+ (match expand_one macs sym xs with+ | Some y -> limited_expand macs pos (limit - 1) y+ | None -> x)+ | _ when limit <= 0 ->+ failwith_msg pos "Expansion limit exceeded"+ | x -> x++(* Splice sexprs that start with splice symbol. The splice symbol is+ ^. *)++let rec splice = function+ | [] -> []+ | L (_, S (_, keyword) :: xs) :: ys when keyword = "^" ->+ let rec loop xs ys =+ match xs with+ | [] -> splice ys+ | x :: xs -> x :: loop xs ys in+ loop xs ys+ | x :: xs -> x :: splice xs++let rec expand_all macs x =+ match limited_expand macs (annotation x) limit x with+ | L (pos, xs) ->+ let ys = List.map (expand_all macs) xs in+ L (pos, splice ys)+ | x -> x++let need_newline = ref false++let expand o macs x =+ if !need_newline+ then print_newline ();+ print_sexpr o (expand_all macs x);+ need_newline := true++(**** Include the contents of a file ****)++let read_sexprs ch =+ let rec loop xs =+ try+ let x = read_sexpr ch in+ loop (x :: xs)+ with+ | End_of_file ->+ List.rev xs in+ loop []++(**** Main loop ****)++(* o is the output channel+ bound is the include bound+ macs is the current list of defined macros *)++let rec loop o bound macs = function+ | [] -> macs (* Return the collected macros *)+ | x :: xs -> dispatch o bound macs xs x++ and dispatch o bound macs xs = function+ | L (pos, (S (_, keyword) :: rest)) when keyword = "defmacro" ->+ loop o bound (defmacro pos rest :: macs) xs+ | L (pos, (S (_, keyword) :: rest)) when keyword = "include" ->+ loop o bound (incl o bound macs pos rest) xs+ | x ->+ expand o macs x;+ loop o bound macs xs++ and incl o bound macs pos = function+ | [Q (_, f)] when bound > 0 ->+ let i =+ try+ open_in f+ with Sys_error s -> failwith s+ in+ let lb = read_lexbuf f i in+ let xs = read_sexprs lb in+ loop o (bound - 1) macs xs+ | [Q (_, f)] when bound <= 0 ->+ failwith_msg pos ("Include depth exceeded with file " ^ f)+ | _ -> failwith_msg pos "Malformed include directive"++let start o xs =+ let _ = loop o bound [] xs in+ ()++let () =+ main start
+ src/ocaml/main.ml view
@@ -0,0 +1,73 @@+(* Main entry point *)++open Sexpr++let read_sexprs ch =+ let rec loop xs =+ try+ let x = read_sexpr ch in+ loop (x :: xs)+ with+ | End_of_file ->+ List.rev xs in+ loop []++let go run f i ofile =+ let lb = read_lexbuf f i in+ let xs = read_sexprs lb in+ close_in i;+ let o =+ if ofile = "" then+ stdout+ else+ open_out ofile in+ run o xs++(* Command-line processing using Arg *)++let help = ref false+let output = ref ""+let input = ref ""++let usage =+ "Usage: " ^ Sys.argv.(0) ^ " [OPTIONS] [INPUT]\n" ^+ "Options:"++let speclist =+[("-o", Arg.Set_string(output), "output to file (default is standard output)");+ ("-h", Arg.Set(help), "print this message")]++let anon s =+ if !input = "" then+ input := s+ else+ begin+ prerr_endline "Bad command-line argument count\n";+ exit 1+ end++let start run =+ Arg.parse speclist anon usage;+ if !help then+ begin+ Arg.usage speclist usage;+ exit 0+ end+ else+ let (in_name, in_ch) =+ match !input with+ | "" -> ("", stdin)+ | f ->+ try+ (f, open_in f)+ with Sys_error s -> failwith s+ in+ go run in_name in_ch !output++let main run =+ try+ start run+ with+ | Failure s ->+ prerr_endline s;+ exit 1
+ src/ocaml/main.mli view
@@ -0,0 +1,24 @@+(** A main routine for processing S-expressions *)++(** Build a program that processes S-expressions. The program++{[ let () = main f]}++reads an input file containing a sequence of S-expressions, and opens+an output file. It then invokes function [f] with the output channel+and the list of S-expressions read.++If the name of the program is [prog], the input file and the output+file is specified on the command line as++{[ $ prog -o OUTPUT INPUT]}++where standard input is used when [INPUT] is omitted, and standard+output is used when [-o OUTPUT] is omitted.++Function [f] is invoked in a context that catches {!exception:Failure}+exceptions, prints the failure message to standard error, and then+exits with error code 1. Function {!val:Reader.failwith_msg} raises+{!exception:Failure} exceptions after adding position information to+an error message. *)+val main : (out_channel -> Lexing.position Sexpr.sexpr list -> unit) -> unit
+ src/ocaml/pp.ml view
@@ -0,0 +1,13 @@+open Sexpr+open Main++let need_newline = ref false++let filter o x =+ if !need_newline+ then print_newline ();+ print_sexpr o x;+ need_newline := true++let () =+ main (fun o xs -> List.iter (filter o) xs)
+ src/ocaml/reader.ml view
@@ -0,0 +1,58 @@+open Sexpr_type+open Lexing++type token =+ | SYM of string+ | STR of string+ | NUM of int+ | LPAR+ | RPAR+ | EOF++let error_msg pos msg =+ Printf.sprintf "%s:%d:%d: %s\n" pos.pos_fname pos.pos_lnum+ (pos.pos_cnum - pos.pos_bol + 1) msg++let failwith_msg pos msg =+ failwith (error_msg pos msg)++let parse_err = failwith_msg++let rec parse_list lexfun lexbuf lpos list =+ let tok = lexfun lexbuf in+ let pos = lexeme_start_p lexbuf in+ match tok with+ | SYM s -> parse_list lexfun lexbuf lpos (S (pos, s) :: list)+ | STR s -> parse_list lexfun lexbuf lpos (Q (pos, s) :: list)+ | NUM n -> parse_list lexfun lexbuf lpos (N (pos, n) :: list)+ | LPAR ->+ let x = parse_list lexfun lexbuf pos [] in+ parse_list lexfun lexbuf lpos (x :: list)+ | RPAR -> L (lpos, List.rev list)+ | EOF -> parse_err pos "End of file in list"++let top lexfun lexbuf =+ let tok = lexfun lexbuf in+ let pos = lexeme_start_p lexbuf in+ match tok with+ | SYM s -> S (pos, s)+ | STR s -> Q (pos, s)+ | NUM n -> N (pos, n)+ | LPAR -> parse_list lexfun lexbuf pos []+ | RPAR -> parse_err pos "Unmatched right parenthesis"+ | EOF -> raise End_of_file++let one lexfun lexbuf =+ let tok = lexfun lexbuf in+ let pos = lexeme_start_p lexbuf in+ let x =+ match tok with+ | SYM s -> S (pos, s)+ | STR s -> Q (pos, s)+ | NUM n -> N (pos, n)+ | LPAR -> parse_list lexfun lexbuf pos []+ | RPAR -> parse_err pos "Unmatched right parenthesis"+ | EOF -> parse_err pos "Nothing in string" in+ match lexfun lexbuf with+ | EOF -> x+ | _ -> parse_err (lexeme_start_p lexbuf) "Trailing garbage in string"
+ src/ocaml/reader.mli view
@@ -0,0 +1,24 @@+(** Operations on positions produced by {!val:Sexpr.read_sexpr} *)++open Sexpr_type+open Lexing++(**/**)++type token = SYM of string | STR of string | NUM of int | LPAR | RPAR | EOF++(**/**)++(** Add position information to a message. *)+val error_msg : position -> string -> string++(** Add position information to a message and fail.+ @raise Failure always *)+val failwith_msg : position -> string -> 'a++(**/**)++val parse_err : position -> string -> 'a++val top : (lexbuf -> token) -> lexbuf -> position sexpr+val one : (lexbuf -> token) -> lexbuf -> position sexpr
+ src/ocaml/scanner.mll view
@@ -0,0 +1,21 @@+{+open Reader+open Lexing++let parse_error pos =+ parse_err pos "Bad token"+}+let special = ['*' '/' '<' '=' '>' '!' '?' ':' '$' '%' '_' '&' '~' '^']+let start = ['a' - 'z' 'A' - 'Z'] | special+let part = start | ['-' '+' '0' - '9']+rule token = parse+ [' ' '\t'] { token lexbuf }+ | '\n' { new_line lexbuf; token lexbuf }+ | ';' [^ '\n']* { token lexbuf }+ | start part* as s { SYM(s) }+ | ['-' '+']? ['0'-'9']+ as n { NUM(int_of_string n) }+ | '"' ([^ '\\' '"']* as s) '"' { STR(s) }+ | '(' { LPAR }+ | ')' { RPAR }+ | eof { EOF }+ | _ { parse_error (lexeme_start_p lexbuf) }
+ src/ocaml/sexpr.ml view
@@ -0,0 +1,84 @@+include Sexpr_type+open Lexing+open Format++let annotation = function+ | S (a, _) -> a+ | Q (a, _) -> a+ | N (a, _) -> a+ | L (a, _) -> a++let read_lexbuf fname ch =+ let lexbuf = Lexing.from_channel ch in+ lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fname };+ lexbuf++let read_sexpr lexbuf =+ Reader.top Scanner.token lexbuf++let read_sexpr_from_string ch =+ let lexbuf = Lexing.from_string ch in+ Reader.one Scanner.token lexbuf++let rec sexpr_printer f x =+ match x with+ | S (_, s) -> pp_print_string f s+ | Q (_, s) ->+ pp_print_char f '"';+ pp_print_string f s;+ pp_print_char f '"'+ | N (_, n) -> pp_print_int f n+ | L (_, xs) -> print_list f xs+and print_list f x =+ match x with+ | [] -> pp_print_string f "()"+ | x :: xs ->+ pp_open_box f 2;+ pp_print_string f "(";+ sexpr_printer f x;+ print_rest f xs+and print_rest f x =+ match x with+ | [] ->+ pp_print_string f ")";+ pp_close_box f ()+ | x :: xs ->+ pp_print_space f ();+ sexpr_printer f x;+ print_rest f xs++let print_sexpr ch x =+ let f = formatter_of_out_channel ch in+ sexpr_printer f x;+ pp_print_newline f ()++let sym x = S ((), x)+let quo x = Q ((), x)+let num x = N ((), x)+let lst x = L ((), x)++let rec strip = function+ | S (_, s) -> sym s+ | Q (_, s) -> quo s+ | N (_, i) -> num i+ | L (_, l) -> lst (List.map strip l)++let assoc key alist =+ let rec loop acc = function+ | [] -> acc+ | L (_, S (_, head) :: rest) :: l when key = head ->+ loop (acc @ rest) l+ | _ :: l -> loop acc l in+ loop [] alist++let rec has_key key = function+ | [] -> false+ | L (_, S (_, head) :: _) :: _ when key = head -> true+ | _ :: l -> has_key key l++let rem_keys keys xs =+ let f xs x =+ match x with+ | L (_, S (_, head) :: _) when List.mem head keys -> xs+ | _ -> x :: xs in+ List.rev (List.fold_left f [] xs)
+ src/ocaml/sexpr.mli view
@@ -0,0 +1,109 @@+(** S-expressions++This module provides a data structure for S-expressions, and a reader.+The reader records the position in the file at which items that make+up the list are located.++The S-expressions used are restricted so that most dialects of Lisp+can read them, and characters within symbols and strings never need+quoting. Every list is proper. An atom is either a symbol, an integer,+or a string. The characters that make up a symbol are the letters, the+digits, and these special characters.++{[ +-*\/\<=>!?:$%_&~^]}++A symbol may not begin with a digit or a sign followed by a digit. The+characters that make up a string are the printing characters omitting+double quote and backslash. Double quotes delimit a string. A comment+begins with a semicolon and continues to the end of the current line.++ *)++open Lexing+open Format++(** S-expression datatype *)+type 'a sexpr =+ | S of 'a * string (** Symbol *)+ | Q of 'a * string (** String *)+ | N of 'a * int (** Number (integer) *)+ | L of 'a * 'a sexpr list (** Proper list *)++(** Extract the annotation associated with an S-expression. *)+val annotation : 'a sexpr -> 'a++(** {1 Input} *)++(** Given a file name and its channel, return a {!val:Lexer.lexbuf}+ for use by the reader. Use the empty string as the file name for+ {!val:Sys.stdin}. *)+val read_lexbuf : string -> in_channel -> lexbuf++(** Read an S-expression from a file annotated with the position of+ the datum in the file. See module {!module:Reader} for functions+ that use positions to construct informative error messages.++ @raise End_of_file on end of file+ @raise Failure on malformed input *)+val read_sexpr : lexbuf -> position sexpr++(** Read an S-expression from a string annotated with the position of+ the datum in the string. *)+val read_sexpr_from_string : string -> position sexpr++(** {1 Output} *)++(** Pretty print an S-expression *)+val print_sexpr : out_channel -> 'a sexpr -> unit++(** An S-expression printer that can be installed as a printer in a+ toplevel system using++{[ install_printer Sexpr.sexpr_printer]}+ *)+val sexpr_printer : formatter -> 'a sexpr -> unit++(** {1 List Builders} *)++(** Construct a symbol *)+val sym : string -> unit sexpr++(** Construct a string *)+val quo : string -> unit sexpr++(** Construct an integer *)+val num : int -> unit sexpr++(** Construct a list *)+val lst : unit sexpr list -> unit sexpr++(** {1 List Operations} *)++(** Replace all annotations in a list with the unit value. *)+val strip : 'a sexpr -> unit sexpr++(** {2 Association Lists}++ An association list is a list of lists, in which the first element+ of each interior list is a symbol. The symbol is call a key. The+ list of values associated with a key is the result of appending+ all interior lists that are headed by the key after removing the+ key. Thus, the list of values [(a b c d)] is associated with key+ [k] in the following association list++{[ ((k a b)+ (x y z)+ (k c d))]}++ An interior list that does not begin with a symbol is silently+ ignored. *)++(** Return the values associated with a key. *)+val assoc : string -> 'a sexpr list -> 'a sexpr list++(** Does an association list have an interior list headed with the+ given key? *)+val has_key : string -> 'a sexpr list -> bool++(** Remove interior lists if their key is in a given list. *)+val rem_keys : string list -> 'a sexpr list -> 'a sexpr list
+ src/ocaml/sexpr_type.ml view
@@ -0,0 +1,5 @@+type 'a sexpr =+ | S of 'a * string+ | Q of 'a * string+ | N of 'a * int+ | L of 'a * 'a sexpr list
tst/aik.tst view
@@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from aik.scm") (defprotocol aikprot basic
tst/axiom2.tst view
@@ -1,6 +1,6 @@ (herald "Axiom 2 Protocol" (bound 20)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from axiom2.scm") (comment "Strand count bounded at 20") @@ -112,6 +112,7 @@ (label 6) (parent 5) (unrealized (0 1))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -229,6 +230,7 @@ (label 13) (parent 12) (unrealized (0 1))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
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.1")+(comment "CPSA 3.6.2") (comment "All input read from blanchet.scm") (defprotocol blanchet basic@@ -55,6 +55,7 @@ (label 2) (parent 0) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton blanchet@@ -176,6 +177,7 @@ (label 8) (parent 6) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton blanchet@@ -214,6 +216,7 @@ (label 10) (parent 9) (unrealized (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -241,6 +244,7 @@ (label 11) (unrealized (0 0) (1 0)) (preskeleton)+ (origs (d (0 1))) (comment "Not a skeleton")) (defskeleton blanchet@@ -331,6 +335,7 @@ (label 16) (parent 14) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton blanchet-corrected@@ -409,6 +414,7 @@ (label 20) (parent 18) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton blanchet-corrected@@ -447,6 +453,7 @@ (label 22) (parent 21) (unrealized (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -517,6 +524,7 @@ (label 25) (unrealized (0 0) (1 0)) (preskeleton)+ (origs (d (0 1))) (comment "Not a skeleton")) (defskeleton blanchet-corrected@@ -568,6 +576,7 @@ (label 28) (parent 27) (unrealized (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/bltk_test.tst view
@@ -1,6 +1,6 @@ (herald "bltk Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from bltk_test.scm") (defprotocol test diffie-hellman@@ -40,6 +40,7 @@ (label 1) (unrealized (1 0)) (preskeleton)+ (origs (n (0 0))) (comment "Not a skeleton")) (defskeleton test@@ -54,6 +55,7 @@ (label 2) (parent 1) (unrealized (1 0))+ (dead) (origs (n (0 0))) (comment "empty cohort")) @@ -76,6 +78,7 @@ (label 3) (unrealized (1 0)) (preskeleton)+ (origs (n (0 0))) (comment "Not a skeleton")) (defskeleton test@@ -90,6 +93,7 @@ (label 4) (parent 3) (unrealized (1 0))+ (dead) (origs (n (0 0))) (comment "empty cohort"))
tst/dh-ca.tst view
@@ -1,6 +1,6 @@ (herald dhca (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from dh-ca.scm") (defprotocol dhca diffie-hellman@@ -528,6 +528,7 @@ (label 15) (parent 8) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -586,6 +587,7 @@ (label 17) (parent 9) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -618,6 +620,7 @@ (label 18) (parent 9) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -879,6 +882,7 @@ (label 25) (parent 16) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -924,6 +928,7 @@ (label 26) (parent 19) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -988,6 +993,7 @@ (label 28) (parent 20) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -1023,6 +1029,7 @@ (label 29) (parent 20) (unrealized (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -1227,6 +1234,7 @@ (label 34) (parent 23) (unrealized (6 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -1262,6 +1270,7 @@ (label 35) (parent 24) (unrealized (4 0) (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -1296,6 +1305,7 @@ (label 36) (parent 24) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -1330,6 +1340,7 @@ (label 37) (parent 24) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -1368,6 +1379,7 @@ (label 38) (parent 24) (unrealized (4 0) (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -1402,6 +1414,7 @@ (label 39) (parent 27) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2033,6 +2046,7 @@ (label 57) (parent 50) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2093,6 +2107,7 @@ (label 59) (parent 51) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2126,6 +2141,7 @@ (label 60) (parent 51) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2395,6 +2411,7 @@ (label 67) (parent 58) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2441,6 +2458,7 @@ (label 68) (parent 61) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2507,6 +2525,7 @@ (label 70) (parent 62) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2543,6 +2562,7 @@ (label 71) (parent 62) (unrealized (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2758,6 +2778,7 @@ (label 76) (parent 65) (unrealized (6 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2794,6 +2815,7 @@ (label 77) (parent 66) (unrealized (4 0) (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2829,6 +2851,7 @@ (label 78) (parent 66) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2864,6 +2887,7 @@ (label 79) (parent 66) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2903,6 +2927,7 @@ (label 80) (parent 66) (unrealized (4 0) (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -2938,6 +2963,7 @@ (label 81) (parent 69) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -3088,6 +3114,7 @@ (label 84) (unrealized (0 1) (0 3) (1 1) (1 2) (1 4)) (preskeleton)+ (origs (n (1 3))) (comment "Not a skeleton")) (defskeleton dhca@@ -3548,6 +3575,7 @@ (label 95) (parent 93) (unrealized (0 1) (6 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -3591,6 +3619,7 @@ (label 96) (parent 94) (unrealized (0 1) (4 0) (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -3633,6 +3662,7 @@ (label 97) (parent 94) (unrealized (0 1) (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -3675,6 +3705,7 @@ (label 98) (parent 94) (unrealized (0 1) (5 0))+ (dead) (comment "empty cohort")) (defskeleton dhca@@ -3720,6 +3751,7 @@ (label 99) (parent 94) (unrealized (0 1) (4 0) (5 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
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.1")+(comment "CPSA 3.6.2") (comment "All input read from 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.1")+(comment "CPSA 3.6.2") (comment "All input read from dh_mim2.scm") (defprotocol dh_mim diffie-hellman
tst/dh_sig.tst view
@@ -1,6 +1,6 @@ (herald "Signed DH exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from 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.1")+(comment "CPSA 3.6.2") (comment "All input read from dh_test.scm") (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.1")+(comment "CPSA 3.6.2") (comment "All input read from dhnsl_basic.scm") (defprotocol dhnsl diffie-hellman@@ -147,6 +147,7 @@ (label 5) (parent 2) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -235,6 +236,7 @@ (label 9) (parent 4) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -364,6 +366,7 @@ (label 14) (parent 6) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -388,6 +391,7 @@ (label 15) (parent 7) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -411,6 +415,7 @@ (label 16) (parent 8) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -438,6 +443,7 @@ (label 17) (parent 10) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -468,6 +474,7 @@ (label 18) (parent 11) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -525,6 +532,7 @@ (label 20) (parent 13) (unrealized (4 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -627,6 +635,7 @@ (label 24) (parent 23) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -746,6 +755,7 @@ (label 29) (parent 26) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -770,6 +780,7 @@ (label 30) (parent 27) (unrealized (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/dhnsl_use.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from dhnsl_use.scm") (defprotocol dhnsl diffie-hellman@@ -156,6 +156,7 @@ (label 5) (parent 2) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -181,6 +182,7 @@ (label 6) (parent 2) (unrealized (0 1) (0 3) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -224,6 +226,7 @@ (label 8) (parent 2) (unrealized (0 1) (0 3) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -297,6 +300,7 @@ (label 11) (parent 4) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -322,6 +326,7 @@ (label 12) (parent 4) (unrealized (0 1) (0 3) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -352,6 +357,7 @@ (label 13) (parent 4) (unrealized (0 1) (0 3) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -405,6 +411,7 @@ (label 15) (parent 4) (unrealized (0 1) (0 3) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -430,6 +437,7 @@ (label 16) (parent 7) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -576,6 +584,7 @@ (label 21) (parent 18) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -636,6 +645,7 @@ (label 23) (parent 18) (unrealized (1 2) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -696,6 +706,7 @@ (label 25) (parent 18) (unrealized (1 2) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -724,6 +735,7 @@ (label 26) (parent 19) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -751,6 +763,7 @@ (label 27) (parent 19) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -782,6 +795,7 @@ (label 28) (parent 19) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -809,6 +823,7 @@ (label 29) (parent 19) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -839,6 +854,7 @@ (label 30) (parent 19) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -868,6 +884,7 @@ (label 31) (parent 22) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -902,6 +919,7 @@ (label 32) (parent 24) (unrealized (1 2) (2 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -1103,6 +1121,7 @@ (label 39) (parent 35) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1151,6 +1170,7 @@ (label 41) (parent 35) (unrealized (0 2) (0 4) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1176,6 +1196,7 @@ (label 42) (parent 35) (unrealized (0 2) (0 4) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1273,6 +1294,7 @@ (label 45) (parent 40) (unrealized (0 4) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1311,6 +1333,7 @@ (label 46) (parent 43) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1387,6 +1410,7 @@ (label 48) (parent 43) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1458,6 +1482,7 @@ (label 50) (parent 43) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1497,6 +1522,7 @@ (label 51) (parent 43) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1527,6 +1553,7 @@ (label 52) (parent 44) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1556,6 +1583,7 @@ (label 53) (parent 44) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1589,6 +1617,7 @@ (label 54) (parent 44) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1618,6 +1647,7 @@ (label 55) (parent 44) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1650,6 +1680,7 @@ (label 56) (parent 44) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1686,6 +1717,7 @@ (label 57) (parent 47) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhnsl@@ -1727,6 +1759,7 @@ (label 58) (parent 49) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -1883,6 +1916,7 @@ (label 64) (parent 61) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -1908,6 +1942,7 @@ (label 65) (parent 61) (unrealized (0 1) (0 3) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -1951,6 +1986,7 @@ (label 67) (parent 61) (unrealized (0 1) (0 3) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2024,6 +2060,7 @@ (label 70) (parent 63) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2049,6 +2086,7 @@ (label 71) (parent 63) (unrealized (0 1) (0 3) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2079,6 +2117,7 @@ (label 72) (parent 63) (unrealized (0 1) (0 3) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2132,6 +2171,7 @@ (label 74) (parent 63) (unrealized (0 1) (0 3) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2157,6 +2197,7 @@ (label 75) (parent 66) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2303,6 +2344,7 @@ (label 80) (parent 77) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2363,6 +2405,7 @@ (label 82) (parent 77) (unrealized (1 2) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2423,6 +2466,7 @@ (label 84) (parent 77) (unrealized (1 2) (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2451,6 +2495,7 @@ (label 85) (parent 78) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2478,6 +2523,7 @@ (label 86) (parent 78) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2509,6 +2555,7 @@ (label 87) (parent 78) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2536,6 +2583,7 @@ (label 88) (parent 78) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2566,6 +2614,7 @@ (label 89) (parent 78) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2595,6 +2644,7 @@ (label 90) (parent 81) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2629,6 +2679,7 @@ (label 91) (parent 83) (unrealized (1 2) (2 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -2830,6 +2881,7 @@ (label 98) (parent 94) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2878,6 +2930,7 @@ (label 100) (parent 94) (unrealized (0 2) (0 4) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -2903,6 +2956,7 @@ (label 101) (parent 94) (unrealized (0 2) (0 4) (1 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3038,6 +3092,7 @@ (label 105) (parent 102) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3113,6 +3168,7 @@ (label 107) (parent 102) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3147,6 +3203,7 @@ (label 108) (parent 102) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3183,6 +3240,7 @@ (label 109) (parent 102) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3222,6 +3280,7 @@ (label 110) (parent 102) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3252,6 +3311,7 @@ (label 111) (parent 103) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3281,6 +3341,7 @@ (label 112) (parent 103) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3314,6 +3375,7 @@ (label 113) (parent 103) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3343,6 +3405,7 @@ (label 114) (parent 103) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3375,6 +3438,7 @@ (label 115) (parent 103) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3506,6 +3570,7 @@ (label 119) (parent 106) (unrealized (2 1) (3 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3622,6 +3687,7 @@ (label 122) (parent 120) (unrealized (3 1) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3702,6 +3768,7 @@ (label 124) (parent 120) (unrealized (3 1) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3739,6 +3806,7 @@ (label 125) (parent 120) (unrealized (3 1) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3778,6 +3846,7 @@ (label 126) (parent 120) (unrealized (3 1) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3819,6 +3888,7 @@ (label 127) (parent 120) (unrealized (3 1) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3851,6 +3921,7 @@ (label 128) (parent 121) (unrealized (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3882,6 +3953,7 @@ (label 129) (parent 121) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3917,6 +3989,7 @@ (label 130) (parent 121) (unrealized (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3948,6 +4021,7 @@ (label 131) (parent 121) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -3982,6 +4056,7 @@ (label 132) (parent 121) (unrealized (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton dhns@@ -4020,6 +4095,7 @@ (label 133) (parent 123) (unrealized (3 1) (4 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/enrich.tst view
@@ -1,6 +1,6 @@ (herald enrich) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from enrich.scm") (defprotocol enrich basic
tst/envelope.tst view
@@ -1,6 +1,6 @@ (herald "Envelope Protocol" (bound 20)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from envelope.scm") (comment "Strand count bounded at 20") @@ -78,6 +78,7 @@ (label 0) (unrealized (0 0) (1 0) (2 5)) (preskeleton)+ (origs (esk (2 0)) (n (2 2)) (tno (2 2)) (v (2 6))) (comment "Not a skeleton")) (defskeleton envelope@@ -149,6 +150,7 @@ (label 2) (parent 1) (unrealized (0 0) (3 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -230,6 +232,7 @@ (label 4) (parent 3) (unrealized (0 0) (1 0) (4 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -305,6 +308,7 @@ (label 6) (parent 5) (unrealized (0 0) (4 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -388,6 +392,7 @@ (label 8) (parent 7) (unrealized (0 0) (5 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -894,6 +899,7 @@ (label 15) (parent 12) (unrealized (0 0) (6 2) (8 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -1030,6 +1036,7 @@ (label 17) (parent 13) (unrealized (0 0) (7 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -1420,6 +1427,7 @@ (label 22) (parent 16) (unrealized (7 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -1496,6 +1504,7 @@ (label 23) (parent 18) (unrealized (0 0) (8 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -1974,6 +1983,7 @@ (label 28) (parent 24) (unrealized (0 0) (6 2) (10 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -2075,6 +2085,7 @@ (label 29) (parent 25) (unrealized (0 0) (6 2) (10 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -2247,6 +2258,7 @@ (label 31) (parent 26) (unrealized (0 0) (10 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -2517,6 +2529,7 @@ (label 34) (parent 30) (unrealized (0 0) (6 0) (10 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -2695,6 +2708,7 @@ (label 36) (parent 32) (unrealized (0 0) (11 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -3105,6 +3119,7 @@ (label 40) (parent 35) (unrealized (0 0) (6 0) (11 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -3202,6 +3217,7 @@ (label 41) (parent 37) (unrealized (0 0) (12 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -3336,6 +3352,7 @@ (label 42) (parent 38) (unrealized (9 2) (11 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -4079,6 +4096,7 @@ (label 48) (parent 45) (unrealized (9 2) (13 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -4208,6 +4226,7 @@ (label 49) (parent 46) (unrealized (9 2) (13 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -4437,6 +4456,7 @@ (label 51) (parent 47) (unrealized (13 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -4669,6 +4689,7 @@ (label 53) (parent 50) (unrealized (9 0) (13 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -4906,6 +4927,7 @@ (label 55) (parent 52) (unrealized (14 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -5148,6 +5170,7 @@ (label 57) (parent 54) (unrealized (9 0) (14 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -5273,6 +5296,7 @@ (label 58) (parent 56) (unrealized (15 1))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -5347,6 +5371,7 @@ (label 59) (unrealized (0 0) (1 5)) (preskeleton)+ (origs (esk (1 0)) (n (1 2)) (tno (1 2)) (v (1 6))) (comment "Not a skeleton")) (defskeleton envelope@@ -5410,6 +5435,7 @@ (label 61) (parent 60) (unrealized (2 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -5483,6 +5509,7 @@ (label 63) (parent 62) (unrealized (0 0) (3 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -5549,6 +5576,7 @@ (label 65) (parent 64) (unrealized (3 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -5623,6 +5651,7 @@ (label 67) (parent 66) (unrealized (4 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -6094,6 +6123,7 @@ (label 74) (parent 71) (unrealized (5 2) (7 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -6226,6 +6256,7 @@ (label 76) (parent 72) (unrealized (6 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -6525,6 +6556,7 @@ (label 80) (parent 77) (unrealized (7 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -6898,6 +6930,7 @@ (label 84) (parent 81) (unrealized (5 2) (9 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -6993,6 +7026,7 @@ (label 85) (parent 82) (unrealized (5 2) (9 3))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -7153,6 +7187,7 @@ (label 87) (parent 83) (unrealized (9 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -7316,6 +7351,7 @@ (label 89) (parent 86) (unrealized (5 0) (9 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -7484,6 +7520,7 @@ (label 91) (parent 88) (unrealized (10 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -7658,6 +7695,7 @@ (label 93) (parent 90) (unrealized (5 0) (10 1))+ (dead) (comment "empty cohort")) (defskeleton envelope@@ -7750,6 +7788,7 @@ (label 94) (parent 92) (unrealized (11 1))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
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.1")+(comment "CPSA 3.6.2") (comment "All input read from ffgg.scm") (defprotocol ffgg basic@@ -29,6 +29,7 @@ (label 0) (unrealized (1 0)) (preskeleton)+ (origs (m (0 2))) (comment "Not a skeleton")) (defskeleton ffgg
tst/fnof_or.tst view
@@ -2,7 +2,7 @@ (comment "Version using variables of sort mesg, with ltk function emulated.")) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from 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.1")+(comment "CPSA 3.6.2") (comment "All input read from fnof_test.scm") (defprotocol fnoftest basic@@ -56,6 +56,7 @@ (traces ((send (cat n0 (enc an0 an1 n0 n1 k))) (recv n1))) (label 2) (unrealized (0 1))+ (dead) (origs (n0 (0 0)) (n1 (0 0))) (comment "empty cohort")) @@ -78,6 +79,7 @@ (label 3) (unrealized) (preskeleton)+ (origs (n1 (0 0))) (comment "Not a skeleton")) (defskeleton fnoftest@@ -113,6 +115,7 @@ (traces ((send (cat n1 (enc an0 an1 n1 n1 k))) (recv n1))) (label 5) (unrealized)+ (origs (n1 (0 0))) (comment "Input cannot be made into a skeleton--nothing to do")) (defprotocol fnoftest2 basic@@ -221,6 +224,7 @@ (traces ((send (cat n0 (enc bn0 bn1 an0 an1 n0 n1 k))) (recv n1))) (label 10) (unrealized (0 1))+ (dead) (origs (n0 (0 0)) (n1 (0 0))) (comment "empty cohort"))
tst/fnof_woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol, using fnof to emulate ltk function") -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from 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.1")+(comment "CPSA 3.6.2") (comment "All input read from fnof_yahalom.scm") (defprotocol yahalom basic@@ -268,6 +268,7 @@ (label 8) (parent 6) (unrealized (1 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -297,6 +298,7 @@ (label 9) (parent 7) (unrealized (1 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/goals.scm view
@@ -214,6 +214,20 @@ (= z z-0)))) (comment "Double initiator point of view")) +;;; Double initiator point of view+(defskeleton ns+ (vars (a b name) (n1 n1-0 text))+ (defstrand init 3 (a a) (b b) (n1 n1))+ (defstrand init 3 (a a) (b b) (n1 n1-0))+ (non-orig (privk b) (privk a))+ (uniq-orig n1 n1-0)+ (goals+ (forall ((z z-0 strd))+ (implies+ (and (p "init" z 3) (p "init" z-0 3))+ (= z z-0))))+ (comment "Double initiator point of view 2"))+ (defprotocol nsl-typeless basic (defrole init (vars (a b name) (n1 text) (n2 mesg))
tst/goals.tst view
@@ -1,6 +1,6 @@ (herald goals) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from goals.scm") (defprotocol ns basic@@ -260,6 +260,7 @@ (label 8) (unrealized (0 0) (1 1)) (preskeleton)+ (origs (n1 (1 0))) (comment "Not a skeleton")) (defskeleton ns@@ -427,6 +428,7 @@ (label 16) (parent 14) (unrealized (0 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -754,6 +756,7 @@ (label 28) (unrealized (0 0) (1 2)) (preskeleton)+ (origs (n2 (1 1))) (comment "Not a skeleton")) (defskeleton ns@@ -1037,6 +1040,184 @@ (comment "Nothing left to do") +(defprotocol ns basic+ (defrole init+ (vars (a b name) (n1 n2 text))+ (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+ (send (enc n2 (pubk b)))))+ (defrole resp+ (vars (b a name) (n2 n1 text))+ (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+ (recv (enc n2 (pubk b)))))+ (comment "Needham-Schroeder with no role origination assumptions"))++(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))+ (non-orig (privk a) (privk b))+ (uniq-orig n1 n1-0)+ (subgoals+ (forall ((z z-0 strd))+ (implies (and (p "init" z 3) (p "init" z-0 3)) (= z z-0))))+ (comment "Double initiator point of view 2")+ (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)))))+ (label 41)+ (unrealized (0 1) (1 1))+ (origs (n1 (0 0)) (n1-0 (1 0)))+ (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+ (vars (n1 n2 text) (a b name))+ (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+ (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)))))+ (label 42)+ (parent 41)+ (unrealized (0 1))+ (comment "1 in cohort - 1 not yet seen"))++(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-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 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))))+ ((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 43)+ (parent 41)+ (unrealized (0 1) (1 1))+ (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+ (vars (n1 n2 n2-0 text) (a b name))+ (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+ (defstrand resp 2 (n2 n2-0) (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 (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))))+ ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+ (label 44)+ (parent 42)+ (unrealized (0 1))+ (origs (n1 (0 0)))+ (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 45)+ (parent 43)+ (unrealized (0 1))+ (comment "1 in cohort - 1 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)))+ (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 46)+ (parent 44)+ (unrealized)+ (shape)+ (satisfies yes)+ (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 47)+ (parent 45)+ (unrealized (0 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-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 48)+ (parent 47)+ (unrealized)+ (shape)+ (satisfies (no (z 0) (z-0 1)))+ (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 "Nothing left to do")+ (defprotocol nsl-typeless basic (defrole init (vars (a b name) (n1 text) (n2 mesg))@@ -1063,9 +1244,10 @@ (comment "Shows typeflaw in typeless NSL") (traces ((recv n2)) ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))))- (label 41)+ (label 49) (unrealized (0 0)) (preskeleton)+ (origs (n2 (1 1))) (comment "Not a skeleton")) (defskeleton nsl-typeless@@ -1084,8 +1266,8 @@ (comment "Shows typeflaw in typeless NSL") (traces ((recv n2)) ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))))- (label 42)- (parent 41)+ (label 50)+ (parent 49) (unrealized (0 0)) (origs (n2 (1 1))) (comment "2 in cohort - 2 not yet seen"))@@ -1104,9 +1286,10 @@ ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))) ((send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a))) (send (enc n2 (pubk b)))))- (label 43)- (parent 42)+ (label 51)+ (parent 50) (unrealized (0 0))+ (dead) (comment "empty cohort")) (defskeleton nsl-typeless@@ -1123,8 +1306,8 @@ ((recv (enc a a-0 (pubk b))) (send (enc a-0 n2 b (pubk a)))) ((recv (enc a-0 n2 b (pubk a))) (send (enc (cat n2 b) n2-0 a (pubk a-0)))))- (label 44)- (parent 42)+ (label 52)+ (parent 50) (unrealized) (shape) (satisfies (no (n2 n2) (a a) (b b) (z 1) (z-0 0)))
tst/iadh_um.tst view
file too large to diff
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.1")+(comment "CPSA 3.6.2") (comment "All input read from injection.scm") (defprotocol ns diffie-hellman
tst/kerb.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from kerb.scm") (defprotocol kerb-flawed basic@@ -30,6 +30,7 @@ (label 0) (unrealized (0 1) (1 0)) (preskeleton)+ (origs (n (0 0)) (m (0 2))) (comment "Not a skeleton")) (defskeleton kerb-flawed@@ -112,6 +113,7 @@ (label 4) (parent 3) (unrealized (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -143,6 +145,7 @@ (label 5) (unrealized (0 1) (1 0)) (preskeleton)+ (origs (n (0 0)) (m (0 2))) (comment "Not a skeleton")) (defskeleton kerb-flawed2
tst/kerberos++.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from kerberos++.scm") (defprotocol kerberos basic@@ -150,6 +150,7 @@ (label 3) (parent 1) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -201,6 +202,7 @@ (label 4) (parent 2) (unrealized (2 0) (3 3))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -286,6 +288,7 @@ (label 6) (parent 2) (unrealized (2 0) (3 1))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -327,6 +330,7 @@ (label 7) (parent 2) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -690,6 +694,7 @@ (label 15) (parent 10) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -787,6 +792,7 @@ (label 17) (parent 11) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -846,6 +852,7 @@ (label 18) (parent 12) (unrealized (3 0) (4 1))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -906,6 +913,7 @@ (label 19) (parent 12) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -963,6 +971,7 @@ (label 20) (parent 13) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -1013,6 +1022,7 @@ (label 21) (parent 14) (unrealized (5 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -1138,6 +1148,7 @@ (label 24) (parent 23) (unrealized (2 3))+ (dead) (comment "empty cohort")) (defskeleton kerberos@@ -1203,6 +1214,7 @@ (label 26) (parent 23) (unrealized (2 0))+ (dead) (comment "empty cohort")) (defskeleton kerberos
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.1")+(comment "CPSA 3.6.2") (comment "All input read from lt_test.scm") (defprotocol lttest basic@@ -55,6 +55,7 @@ (traces ((send (cat n1 (enc n1 n2 k))) (recv n2))) (label 2) (unrealized (0 1))+ (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort")) @@ -114,6 +115,7 @@ (traces ((send n) (send (cat n1 (enc n1 n2 k))) (recv n2))) (label 5) (unrealized (0 2))+ (dead) (origs (n1 (0 1)) (n2 (0 1))) (comment "empty cohort"))
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.1")+(comment "CPSA 3.6.2") (comment "All input read from neq_test.scm") (defprotocol neqtest basic@@ -55,6 +55,7 @@ (traces ((send (cat n1 (enc n1 n2 k))) (recv n2))) (label 2) (unrealized (0 1))+ (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort")) @@ -76,6 +77,7 @@ (traces ((send (cat n1 (enc n1 n2 n3 k))) (recv n2))) (label 3) (unrealized (0 1))+ (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort"))
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.1")+(comment "CPSA 3.6.2") (comment "All input read from 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.1")+(comment "CPSA 3.6.2") (comment "All input read from or.scm") (defprotocol or basic
tst/owang.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from owang.scm") (defprotocol wang basic@@ -294,6 +294,7 @@ (label 0) (unrealized (1 0)) (preskeleton)+ (origs (m (0 0)) (k (0 0))) (comment "Not a skeleton")) (defskeleton wang@@ -795,6 +796,7 @@ (label 7) (unrealized (1 0)) (preskeleton)+ (origs (m (0 0)) (k (0 0))) (comment "Not a skeleton")) (defskeleton wang
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.1")+(comment "CPSA 3.6.2") (comment "All input read from owat.scm") (defprotocol owa diffie-hellman
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PKINIT") -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from pkinit.scm") (defprotocol pkinit-flawed basic@@ -254,6 +254,7 @@ (label 7) (parent 6) (unrealized (2 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -422,6 +423,7 @@ (label 12) (parent 11) (unrealized (2 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -470,6 +472,7 @@ (label 13) (unrealized (1 1)) (preskeleton)+ (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (comment "Not a skeleton")) (defskeleton pkinit-flawed@@ -583,6 +586,7 @@ (label 16) (unrealized (1 1)) (preskeleton)+ (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (comment "Not a skeleton")) (defskeleton pkinit-fix1@@ -755,6 +759,7 @@ (label 22) (parent 20) (unrealized (0 0) (2 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -810,6 +815,7 @@ (label 23) (unrealized (1 1)) (preskeleton)+ (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (comment "Not a skeleton")) (defskeleton pkinit-fix2@@ -972,6 +978,7 @@ (label 28) (parent 27) (unrealized (2 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/plaindh.tst view
@@ -1,7 +1,7 @@ (herald "Plain diffie-hellman protocol with challenge-response" (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from plaindh.scm") (defprotocol plaindh diffie-hellman
tst/priority_test.tst view
@@ -1,6 +1,6 @@ (herald "Receive priority test protocol") -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from priority_test.scm") (defprotocol priority_test basic
tst/reflect.tst view
@@ -1,6 +1,6 @@ (herald reflect) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from reflect.scm") (defprotocol reflect basic
tst/staticdh.tst view
@@ -1,6 +1,6 @@ (herald "Static DH key exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from staticdh.scm") (defprotocol staticdh1 diffie-hellman@@ -569,6 +569,7 @@ (label 18) (parent 9) (unrealized (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton staticdh1@@ -600,6 +601,7 @@ (label 19) (parent 9) (unrealized (3 0) (4 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/station.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from station.scm") (defprotocol station-to-station diffie-hellman@@ -217,6 +217,7 @@ (label 5) (parent 4) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -253,6 +254,7 @@ (label 6) (parent 4) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -289,6 +291,7 @@ (label 7) (parent 4) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -328,6 +331,7 @@ (label 8) (parent 4) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -372,6 +376,7 @@ (label 9) (parent 4) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")@@ -599,6 +604,7 @@ (label 15) (parent 14) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -636,6 +642,7 @@ (label 16) (parent 14) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -676,6 +683,7 @@ (label 17) (parent 14) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -713,6 +721,7 @@ (label 18) (parent 14) (unrealized (3 0))+ (dead) (comment "empty cohort")) (defskeleton station-to-station@@ -757,6 +766,7 @@ (label 19) (parent 14) (unrealized (2 0) (3 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/station2.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from station2.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.1")+(comment "CPSA 3.6.2") (comment "All input read from subsort_test.scm") (defprotocol subsorttest basic@@ -55,6 +55,7 @@ (traces ((send (cat n1 (enc n1 n2 k))) (recv n2))) (label 2) (unrealized (0 1))+ (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort"))
tst/test_small.tst view
@@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from test_small.scm") (defprotocol test diffie-hellman
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from 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.1")+(comment "CPSA 3.6.2") (comment "All input read from uniq-gen-test.scm") (defprotocol uniqgentest basic@@ -133,6 +133,7 @@ (label 7) (parent 5) (unrealized (1 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from woolam.scm") (defprotocol woolam basic
tst/wrap_decrypt.tst view
@@ -1,6 +1,6 @@ (herald wrap-decrypt (bound 10)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from wrap_decrypt.lsp") (comment "Strand count bounded at 10") @@ -51,6 +51,7 @@ (label 0) (unrealized (1 2) (3 0) (4 0) (5 2) (5 3)) (preskeleton)+ (origs) (comment "Not a skeleton")) (defskeleton wrap-decrypt@@ -345,6 +346,7 @@ (label 10) (parent 6) (unrealized (1 2) (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -470,6 +472,7 @@ (label 14) (parent 8) (unrealized (1 2) (3 0) (4 0))+ (dead) (origs) (comment "empty cohort")) @@ -664,6 +667,7 @@ (label 20) (parent 12) (unrealized (1 2) (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -821,6 +825,7 @@ (label 26) (parent 16) (unrealized (1 2) (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1059,6 +1064,7 @@ (label 33) (parent 19) (unrealized (1 2) (8 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1257,6 +1263,7 @@ (label 39) (parent 25) (unrealized (1 2) (7 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1326,6 +1333,7 @@ (label 41) (parent 28) (unrealized (1 2) (3 0) (4 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1433,6 +1441,7 @@ (label 45) (parent 32) (unrealized (8 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1606,6 +1615,7 @@ (label 51) (parent 38) (unrealized (7 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1713,6 +1723,7 @@ (label 57) (parent 48) (unrealized (8 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1750,6 +1761,7 @@ (label 58) (parent 49) (unrealized (8 0))+ (dead) (comment "empty cohort")) (defskeleton wrap-decrypt@@ -1787,6 +1799,7 @@ (label 60) (parent 52) (unrealized (8 0))+ (dead) (comment "empty cohort")) (comment "Strand bound exceeded--aborting run")@@ -1827,6 +1840,7 @@ (label 22) (parent 12) (unrealized (1 2) (3 0) (4 0) (9 0))+ (aborted) (comment "aborted")) (defskeleton wrap-decrypt@@ -1866,6 +1880,7 @@ (label 44) (parent 31) (unrealized (1 2) (9 0))+ (aborted) (comment "aborted")) (defskeleton wrap-decrypt@@ -1905,6 +1920,7 @@ (label 47) (parent 34) (unrealized (1 2) (9 0))+ (aborted) (comment "aborted")) (defskeleton wrap-decrypt@@ -1944,6 +1960,7 @@ (label 54) (parent 42) (unrealized (9 0))+ (aborted) (comment "aborted")) (defskeleton wrap-decrypt@@ -1983,6 +2000,7 @@ (label 55) (parent 43) (unrealized (9 0))+ (aborted) (comment "aborted")) (defskeleton wrap-decrypt@@ -2022,6 +2040,7 @@ (label 56) (parent 46) (unrealized (9 0))+ (aborted) (comment "aborted")) (defskeleton wrap-decrypt@@ -2061,6 +2080,7 @@ (label 59) (parent 50) (unrealized (1 2) (9 0))+ (aborted) (comment "aborted")) (defskeleton wrap-decrypt@@ -2100,4 +2120,5 @@ (label 61) (parent 53) (unrealized (1 2) (9 0))+ (aborted) (comment "aborted"))
tst/yahalom.tst view
@@ -1,7 +1,7 @@ (herald "Yahalom Protocol with Forwarding Removed" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.1")+(comment "CPSA 3.6.2") (comment "All input read from yahalom.scm") (defprotocol yahalom diffie-hellman@@ -277,6 +277,7 @@ (label 11) (parent 5) (unrealized (0 3) (2 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -329,6 +330,7 @@ (label 13) (parent 7) (unrealized (0 3) (3 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -598,6 +600,7 @@ (label 22) (parent 15) (unrealized (4 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -963,6 +966,7 @@ (label 33) (parent 21) (unrealized (5 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1065,6 +1069,7 @@ (label 36) (parent 25) (unrealized (2 1) (4 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1138,6 +1143,7 @@ (label 38) (parent 27) (unrealized (3 1) (5 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1315,6 +1321,7 @@ (label 43) (parent 31) (unrealized (6 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1350,6 +1357,7 @@ (label 44) (parent 32) (unrealized (2 1) (5 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1414,6 +1422,7 @@ (label 46) (parent 35) (unrealized (2 1) (5 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1452,6 +1461,7 @@ (label 47) (parent 37) (unrealized (3 1) (6 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1521,6 +1531,7 @@ (label 49) (parent 41) (unrealized (7 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1559,6 +1570,7 @@ (label 50) (parent 42) (unrealized (2 1) (6 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1703,6 +1715,7 @@ (label 56) (parent 54) (unrealized (0 3) (1 0))+ (dead) (comment "empty cohort")) (defskeleton yahalom@@ -1725,6 +1738,7 @@ (label 57) (parent 55) (unrealized (0 3) (1 0))+ (dead) (comment "empty cohort")) (comment "Nothing left to do")