cpsa 3.6.4 → 3.6.5
raw patch · 55 files changed
+70/−58 lines, 55 files
Files
- ChangeLog +12/−0
- NEWS +5/−0
- cpsa.cabal +1/−1
- src/CPSA/Lib/Strand.hs +2/−7
- tst/aik.tst +1/−1
- tst/attest.tst +1/−1
- tst/axiom2.tst +1/−1
- tst/blanchet.tst +1/−1
- tst/bltk_test.tst +1/−1
- tst/comp_test.tst +1/−1
- tst/dh-ca.tst +1/−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 +1/−1
- tst/dhnsl_use.tst +1/−1
- tst/enrich.tst +1/−1
- tst/envelope.tst +1/−1
- tst/ffgg.tst +1/−1
- tst/fluffy_draft03_gske.tst +1/−1
- tst/fnof_or.tst +1/−1
- tst/fnof_test.tst +1/−1
- tst/fnof_woolam.tst +1/−1
- tst/fnof_yahalom.tst +1/−1
- tst/goals.tst +1/−1
- tst/iadh_um.tst too large to diff
- tst/injection.tst +1/−1
- tst/kerb.tst +1/−1
- tst/kerberos++.tst +1/−1
- tst/lt_test.tst +1/−1
- tst/neq_test.tst +1/−1
- tst/ns.tst +1/−1
- tst/or.tst +1/−1
- tst/ordered.tst +1/−1
- tst/owang.tst +1/−1
- tst/owat.tst +1/−1
- tst/pkinit.tst +1/−1
- tst/plaindh.tst +1/−1
- tst/priority_test.tst +1/−1
- tst/prottrans.tst +1/−1
- tst/reflect.tst +1/−1
- tst/role_uniq.tst +1/−1
- tst/rule-order.tst +1/−1
- tst/staticdh.tst +1/−1
- tst/station.tst +1/−1
- tst/station2.tst +1/−1
- tst/subsort_test.tst +1/−1
- tst/test_small.tst +1/−1
- tst/trust-anchor.tst +1/−1
- tst/unilateral.tst +1/−1
- tst/uniq-gen-test.tst +1/−1
- tst/woolam.tst +1/−1
- tst/wrap_decrypt.tst +1/−1
- tst/yahalom.tst +1/−1
ChangeLog view
@@ -1,3 +1,15 @@+2019-11-12 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Version): Tagged as 3.6.5++ * src/CPSA/Lib/Strand.hs (tryPermProb): Rewrote tryPermProb so+ that it uses tryPerm.++2019-11-08 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Strand.hs (tryPermProb): Added missing invperm to+ the third line of tryPermProb, and reenabled multistrand thinning.+ 2019-10-21 John D. Ramsdell <ramsdell@gootoo.mitre.org> * cpsa.cabal (Version): Tagged as 3.6.4
NEWS view
@@ -1,5 +1,10 @@ CPSA NEWS + November 2019:++* Release 3.6.5 is a bug fix release. There are no user visible+ changes.+ October 2019: * Release 3.6.4 adds support for the latest version of the GHC
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 3.6.4+Version: 3.6.5 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.6 License: BSD3
src/CPSA/Lib/Strand.hs view
@@ -884,13 +884,8 @@ tryPermProb :: Algebra t p g s e c => Gist t g -> Gist t g -> [Sid] -> [Sid] -> ((g, e), (g, e), [Sid]) -> Bool tryPermProb g g' prob prob' (fenv, renv, perm) =- checkOrigs g g' fenv perm &&- checkOrigs g' g renv perm &&- checkFacts g g' fenv perm &&- checkFacts g' g renv (invperm perm) &&- containsMapped (permutePair perm) (gorderings g') (gorderings g) &&- containsMapped (permutePair perm) (gleadsto g') (gleadsto g) &&- all (\n -> perm !! (prob !! n) == prob' !! n) [0..((length prob)-1)]+ all (\n -> perm !! (prob !! n) == prob' !! n) [0..((length prob)-1)] &&+ tryPerm g g' (fenv, renv, perm) invperm :: [Int] -> [Int] invperm p = map snd (L.sortOn fst (zip p [0..]))
tst/aik.tst view
@@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from aik.scm") (defprotocol aikprot basic
tst/attest.tst view
@@ -1,6 +1,6 @@ (herald attest-door) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from attest.scm") (defprotocol attest-door basic
tst/axiom2.tst view
@@ -1,6 +1,6 @@ (herald "Axiom 2 Protocol" (bound 20)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from axiom2.scm") (comment "Strand count bounded at 20")
tst/blanchet.tst view
@@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol" (comment "There is a flaw in this protocol by design")) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from blanchet.scm") (defprotocol blanchet basic
tst/bltk_test.tst view
@@ -1,6 +1,6 @@ (herald "bltk Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from bltk_test.scm") (defprotocol test diffie-hellman
tst/comp_test.tst view
@@ -1,6 +1,6 @@ (herald "Main Example") -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from comp_test.scm") (defprotocol main-ex-src basic
tst/dh-ca.tst view
@@ -1,6 +1,6 @@ (herald dhca (algebra diffie-hellman)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from dh-ca.scm") (defprotocol dhca diffie-hellman
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.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from dhnsl_basic.scm") (defprotocol dhnsl diffie-hellman
tst/dhnsl_use.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from dhnsl_use.scm") (defprotocol dhnsl diffie-hellman
tst/enrich.tst view
@@ -1,6 +1,6 @@ (herald enrich) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from envelope.scm") (comment "Strand count bounded at 20")
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.4")+(comment "CPSA 3.6.5") (comment "All input read from ffgg.scm") (defprotocol ffgg basic
tst/fluffy_draft03_gske.tst view
@@ -3,7 +3,7 @@ (comment "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt")) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from fluffy_draft03_gske.scm") (defprotocol fluffy basic
tst/fnof_or.tst view
@@ -2,7 +2,7 @@ (comment "Version using variables of sort mesg, with ltk function emulated.")) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from fnof_test.scm") (defprotocol fnoftest basic
tst/fnof_woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol, using fnof to emulate ltk function") -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from fnof_yahalom.scm") (defprotocol yahalom basic
tst/goals.tst view
@@ -1,6 +1,6 @@ (herald goals) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from goals.scm") (defprotocol ns basic
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.4")+(comment "CPSA 3.6.5") (comment "All input read from injection.scm") (defprotocol ns diffie-hellman
tst/kerb.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from kerb.scm") (defprotocol kerb-flawed basic
tst/kerberos++.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from kerberos++.scm") (defprotocol kerberos basic
tst/lt_test.tst view
@@ -2,7 +2,7 @@ (comment "First and third skeletons should have a shape," "second and fourth should be dead.")) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from lt_test.scm") (defprotocol lttest basic
tst/neq_test.tst view
@@ -2,7 +2,7 @@ (comment "First skeleton should have a shape," "second, and hird should be dead.")) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from neq_test.scm") (defprotocol neqtest basic
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.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from or.scm") (defprotocol or basic
tst/ordered.tst view
@@ -1,6 +1,6 @@ (herald ordered) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from ordered.scm") (defprotocol ordered basic
tst/owang.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from owang.scm") (defprotocol wang basic
tst/owat.tst view
@@ -1,7 +1,7 @@ (herald "One-way Authentication Test with bltk keys" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from pkinit.scm") (defprotocol pkinit-flawed basic
tst/plaindh.tst view
@@ -1,7 +1,7 @@ (herald "Plain diffie-hellman protocol with challenge-response" (algebra diffie-hellman)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from priority_test.scm") (defprotocol priority_test basic
tst/prottrans.tst view
@@ -1,6 +1,6 @@ (herald "Protocol Transformations With Rules") -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from prottrans.scm") (defprotocol ns basic
tst/reflect.tst view
@@ -1,6 +1,6 @@ (herald reflect) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from reflect.scm") (defprotocol reflect basic
tst/role_uniq.tst view
@@ -1,6 +1,6 @@ (herald "Role Unique Origination") -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from role_uniq.scm") (defprotocol blanchet basic
tst/rule-order.tst view
@@ -1,6 +1,6 @@ (herald rule-order) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from rule-order.scm") (defprotocol rule-order basic
tst/staticdh.tst view
@@ -1,6 +1,6 @@ (herald "Static DH key exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from staticdh.scm") (defprotocol staticdh1 diffie-hellman
tst/station.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from station.scm") (defprotocol station-to-station diffie-hellman
tst/station2.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from subsort_test.scm") (defprotocol subsorttest basic
tst/test_small.tst view
@@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from test_small.scm") (defprotocol test diffie-hellman
tst/trust-anchor.tst view
@@ -1,7 +1,7 @@ (herald trust-anchor (comment "Tests rule application on initial skeleton")) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from trust-anchor.scm") (defprotocol trust-anchor basic
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from uniq-gen-test.scm") (defprotocol uniqgentest basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (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.4")+(comment "CPSA 3.6.5") (comment "All input read from wrap_decrypt.lsp") (comment "Strand count bounded at 10")
tst/yahalom.tst view
@@ -1,7 +1,7 @@ (herald "Yahalom Protocol with Forwarding Removed" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.4")+(comment "CPSA 3.6.5") (comment "All input read from yahalom.scm") (defprotocol yahalom diffie-hellman