packages feed

cpsa 3.6.0 → 3.6.1

raw patch · 50 files changed

+154/−74 lines, 50 files

Files

ChangeLog view
@@ -1,3 +1,32 @@+2018-08-29  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version): Tagged as 3.6.1++2018-08-22  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Strand.hs (doRewrites): Added a limit on the number of+	rules that can be applied after solving an authentication test.++2018-08-20  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (cleansPreskel): Cleansed facts from a+	skeleton purged of a strand.  This changes fixes a nasty display+	bug that occurred when a variable in a fact did not occur in any+	strand.++2018-08-06  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Loader.hs (loadConclusion):  Removed mode flag as+	this routine should always be using mode RoleSpec.  This resolves+	a bug in which CPSA could not load a Shape Analysis Sentence as+	rule because equality was before the protocol specific formulas.++	* src/CPSA/Lib/Strand.hs (newPreskel):  Changed newPreskel so that+	it removed duplicates in the leadsto field when creating a new+	preskeleton.  This resolved a bug in which CPSA produced to shapes+	that appeared to be isomorphic, but instead, one shape had+	duplicates in its leadsto field.+ 2018-06-25  John D. Ramsdell  <ramsdell@mitre.org>  	* cpsa.cabal (Version): Tagged as 3.6.0
NEWS view
@@ -1,5 +1,10 @@ CPSA NEWS +  August, 2018:++* Release 3.6.1 is a bug fix release.  It includes updates to the CPSA+  manual.  There are no user visible changes.+   June, 2018:  * Release 3.6.0 adds rules and facts.  Rules are associated with
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		3.6.0+Version:		3.6.1 Maintainer:		mliskov@mitre.org Cabal-Version:		>= 1.6 License:		BSD3
doc/cpsamanual.pdf view

binary file changed (900410 → 904514 bytes)

src/CPSA/Lib/Loader.hs view
@@ -922,7 +922,7 @@ loadImplication md _ prot g vars (L pos [S _ "implies", a, c]) =   do     antec <- loadCheckedConj md pos prot vars vars a-    (g, vc) <- loadConclusion md pos prot g vars c+    (g, vc) <- loadConclusion pos prot g vars c     let (evars, concl) = unzip vc     let goal =           Goal { uvars = vars,@@ -935,35 +935,35 @@ -- The conclusion must be a disjunction.  Each disjunct may introduce -- existentially quantified variables. -loadConclusion :: (Algebra t p g s e c, Monad m) => Mode -> Pos -> Prot t g ->+loadConclusion :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->                   g -> [t] -> SExpr Pos -> m (g, [([t], Conj t)])-loadConclusion _ _ _ g _ (L _ [S _ "false"]) = return (g, [])-loadConclusion md _ prot g vars (L pos (S _ "or" : xs)) =-  loadDisjuncts md pos prot g vars xs []-loadConclusion md pos prot g vars x =+loadConclusion _ _ g _ (L _ [S _ "false"]) = return (g, [])+loadConclusion _ prot g vars (L pos (S _ "or" : xs)) =+  loadDisjuncts pos prot g vars xs []+loadConclusion pos prot g vars x =   do-    (g, a) <- loadExistential md pos prot g vars x+    (g, a) <- loadExistential pos prot g vars x     return (g, [a]) -loadDisjuncts :: (Algebra t p g s e c, Monad m) => Mode -> Pos ->+loadDisjuncts :: (Algebra t p g s e c, Monad m) => Pos ->                  Prot t g -> g -> [t] -> [SExpr Pos] ->                  [([t], Conj t)] -> m (g, [([t], Conj t)])-loadDisjuncts _ _ _ g _ [] rest = return (g, reverse rest)-loadDisjuncts md pos prot g vars (x : xs) rest =+loadDisjuncts _ _ g _ [] rest = return (g, reverse rest)+loadDisjuncts pos prot g vars (x : xs) rest =   do-    (g, a) <- loadExistential md pos prot g vars x-    loadDisjuncts md pos prot g vars xs (a : rest)+    (g, a) <- loadExistential pos prot g vars x+    loadDisjuncts pos prot g vars xs (a : rest) -loadExistential :: (Algebra t p g s e c, Monad m) => Mode -> Pos -> Prot t g ->+loadExistential :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->                    g -> [t] -> SExpr Pos -> m (g, ([t], Conj t))-loadExistential md _ prot g vars (L pos [S _ "exists", L _ vs, x]) =+loadExistential _ prot g vars (L pos [S _ "exists", L _ vs, x]) =   do     (g, evars) <- loadVars g vs-    as <- loadCheckedConj md pos prot (evars ++ vars) evars x+    as <- loadCheckedConj RoleSpec pos prot (evars ++ vars) evars x     return (g, (evars, as))-loadExistential md pos prot g vars x =+loadExistential pos prot g vars x =   do-    as <- loadCheckedConj md pos prot vars [] x+    as <- loadCheckedConj RoleSpec pos prot vars [] x     return (g, ([], as))  -- Load a conjunction and check the result as determined by the mode@@ -1090,7 +1090,7 @@           Nothing ->             fail (shows pos ("parameter " ++ x ++ " not in role " ++ name)) loadPrimary _ _ _ (L pos (S _ "p" : Q _ name : _)) =-  fail (shows pos ("Malformed role specific formula for role " ++ name))+  fail (shows pos ("Malformed protocol specific formula for role " ++ name)) loadPrimary _ _ _ (L pos (S _ pred : _)) =   fail (shows pos ("Malformed formula for predicate " ++ pred)) loadPrimary pos _ _ _ = fail (shows pos "Bad formula")
src/CPSA/Lib/Reduction.hs view
@@ -39,7 +39,7 @@  -- Set when debugging an exception so that buffered results get out. useFlush :: Bool-useFlush = True                -- False+useFlush = False                -- True  -- Parameter driven S-expression printer wrt :: Options -> Handle -> SExpr a -> IO ()
src/CPSA/Lib/Strand.hs view
@@ -517,6 +517,7 @@ newPreskel gen shared insts orderings leadsto decls            facts oper prob kpriority pov =     let orderings' = L.nub orderings+        leadsto' = L.nub leadsto         g = graph trace height insts orderings'         strands = gstrands g         decls' = declsNub decls@@ -528,7 +529,7 @@                       insts = insts,                       strands = strands,                       orderings = orderings',-                      leadsto = leadsto,+                      leadsto = leadsto',                       edges = edges,                       decls = decls',                       extraDecls = mkDecls [],@@ -835,6 +836,7 @@     checkOrigs g g' fenv perm &&     checkOrigs g' g renv (invperm perm) &&     checkFacts g g' fenv perm &&+    checkFacts g' g fenv (invperm perm) &&     containsMapped (permutePair perm) (gorderings g') (gorderings g) &&     containsMapped (permutePair perm) (gleadsto g') (gleadsto g) @@ -844,6 +846,7 @@     checkOrigs g g' fenv perm &&     checkOrigs g' g renv perm &&     checkFacts g g' fenv perm &&+    checkFacts g' g fenv (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)]@@ -1048,7 +1051,7 @@               (updateProb perm (prob k))               (updatePriority perm (kpriority k))               (pov k)-      k'' <- wellFormedPreskel $ k'+      k'' <- wellFormedPreskel $ cleansPreskel k'       return (k0, k'', permuteNode perm n, map (perm !!) phi, hsubst)  -- Forward orderings from strand s@@ -1063,6 +1066,22 @@           | s1 == s = []        -- Dump edges to strand s           | otherwise = [p]     -- Pass thru other edges +-- Cleans facts in a skeleton+cleansPreskel :: Algebra t p g s e c => Preskel t g s e ->  Preskel t g s e+cleansPreskel k =+  newPreskel+  (gen k)+  (shared k)+  (insts k)+  (orderings k)+  (leadsto k)+  (decls k)+  (cleansFacts (kvars k) (kfacts k))+  (operation k)+  (prob k)+  (kpriority k)+  (pov k)+ matchTraces :: Algebra t p g s e c => Trace t ->                Trace t -> (g, e) -> [(g, e)] matchTraces [] _ env = [env]    -- Pattern can be shorter@@ -1531,6 +1550,8 @@                Preskel t g s e -> [Sid] -> e -> Bool validateEnv k k' mapping env =   validateDeclEnv k k' mapping env &&+  all (flip elem (kfacts k'))+  (map (instUpdateFact env (mapping !!)) (kfacts k)) &&   all (flip elem (tc k')) (permuteOrderings mapping (orderings k))  -- Given a realized skeleton k, generate candidates for minimization.@@ -2551,20 +2572,30 @@ -}  {-- For debugging-factVars :: Fact -> [Term] -> [Term]+factVars :: Algebra t p g s e c => Fact t -> [t] -> [t] factVars (Fact _ ts) vs =   foldr f vs ts   where     f (FSid _) vs = vs     f (FTerm t) vs = addVars vs t -chkFVars :: Preskel -> Preskel+chkFVars :: Algebra t p g s e c => Preskel t g s e -> Preskel t g s e chkFVars k =   foldl f k (foldr factVars [] (kfacts k))   where     f k v       | elem v (kvars k) = k       | otherwise = error ("Bad var in fact " ++ show v)+        -- ++ "\n\n" ++ show k)++chkFVarsS :: Algebra t p g s e c => String -> Preskel t g s e -> Preskel t g s e+chkFVarsS s k =+  foldl f k (foldr factVars [] (kfacts k))+  where+    f k v+      | elem v (kvars k) = k+      | otherwise = error (s ++ ": Bad var in fact " ++ show v)+        -- ++ "\n\n" ++ show k) --}  {-@@ -2613,6 +2644,12 @@ -- eliminate error cases. geq :: Algebra t p g s e c => t -> t -> Sem t g s e geq t t' _ (g, e)+  -- Ensure all variables in t and t' are in the domain of e.+  -- This always happens for goals because they must be role specific+  -- but it is not always true for rules.+  | not (matched e t) || not (matched e t') =+      error ("In a rule equality check, " +++             "cannot find a binding for some variable")   | ti == ti' = [(g, e)]   | otherwise = []   where@@ -2721,12 +2758,14 @@   case (nodeLookup e n, nodeLookup e n') of     (Just p, Just p')       | inSkel k p && inSkel k p' &&-        (strandPrec p p' || elem (p, p') (tc k)) -> [(g, e)]+        (strandPrec p p' || elem (p, p') tc) -> [(g, e)]     _ ->       do-        (p, p') <- tc k+        (p, p') <- tc         (g, e) <- nodeMatch n p (g, e)         nodeMatch n' p' (g, e)+  where+    tc = map graphPair $ graphClose $ graphEdges $ strands k  -- Length predicate -- r and h determine the predicate, which has arity one.@@ -2843,7 +2882,7 @@         if null vas then           loop rs               -- Rule does not apply         else-          Just $ doRewrites prules k r vas+          Just $ doRewrites 0 prules k r vas  -- Returns the environments that show satifaction of the antecedent -- but fail to be extendable to show satifaction of one of the@@ -2856,10 +2895,17 @@     conclusion e = all (disjunct e) $ concl $ rlgoal r     disjunct e a = null $ conjoin a k e +ruleLimit :: Int+ruleLimit = 500+ -- Repeatedly applies rules until no rule applies.-doRewrites :: Algebra t p g s e c => [Rule t] -> Preskel t g s e ->+doRewrites :: Algebra t p g s e c => Int -> [Rule t] -> Preskel t g s e ->               Rule t -> [(g, e)] -> [Preskel t g s e]-doRewrites rules k r vas =+doRewrites lim _ _ _ _+  | lim >= ruleLimit =+    error ("Aborting after applying " ++ show ruleLimit +++           " rules and more are applicable")+doRewrites lim rules k r vas =   concatMap f (doRewrite k r vas)   where     f k = loop rules@@ -2870,7 +2916,7 @@             if null vas then               loop rs           -- Rule does not apply             else-              doRewrites rules k r vas+              doRewrites (lim + 1) rules k r vas  -- Apply rewrite rule at all assignments doRewrite :: Algebra t p g s e c => Preskel t g s e ->@@ -3049,7 +3095,7 @@                    (prob k) (kpriority k) (pov k)           return (k', (gen k, e))     _ ->-      error ("In rule " ++ name ++ ", precidence did not get a strand")+      error ("In rule " ++ name ++ ", precedence did not get a strand")   where     tc = map graphPair $ graphClose $ graphEdges $ strands k
tst/aik.tst view
@@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 3.6.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (comment "All input read from bltk_test.scm")  (defprotocol test diffie-hellman
tst/dh-ca.tst view
@@ -1,6 +1,6 @@ (herald dhca (algebra diffie-hellman)) -(comment "CPSA 3.6.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (comment "All input read from ffgg.scm")  (defprotocol ffgg 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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (comment "All input read from goals.scm")  (defprotocol ns basic@@ -108,7 +108,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))))
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.0")+(comment "CPSA 3.6.1") (comment "All input read from injection.scm")  (defprotocol ns diffie-hellman
tst/kerb.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.1") (comment "All input read from kerb.scm")  (defprotocol kerb-flawed basic
tst/kerberos++.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (comment "All input read from or.scm")  (defprotocol or basic
tst/owang.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (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.0")+(comment "CPSA 3.6.1") (comment "All input read from yahalom.scm")  (defprotocol yahalom diffie-hellman