cpsa 3.6.2 → 3.6.3

raw patch · 60 files changed

+470/−153 lines, 60 filesdep +directorydep ~basenew-component:exe:cpsainit

Dependencies added: directory

Dependency ranges changed: base

Files

ChangeLog +69/−0
NEWS +7/−0
cpsa.cabal +11/−1
doc/cpsamanual.pdf binary
doc/init/Makefile +12/−0
doc/init/template.lisp +39/−0
src/CPSA/Init/Main.hs +112/−0
src/CPSA/Lib/Cohort.hs +3/−3
src/CPSA/Lib/Displayer.hs +5/−12
src/CPSA/Lib/Loader.hs +20/−25
src/CPSA/Lib/Protocol.hs +4/−3
src/CPSA/Lib/Reduction.hs +2/−2
src/CPSA/Lib/State.hs +17/−24
src/CPSA/Lib/Strand.hs +112/−39
src/CPSA/SAS/SAS.hs +13/−0
src/ocaml/expand.ml +1/−1
src/ocaml/pp.ml +1/−1
tst/aik.tst +1/−1
tst/axiom2.tst +1/−1
tst/blanchet.tst +1/−1
tst/bltk_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/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/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/reflect.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/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,72 @@+2019-08-26  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version): Tagged as 3.6.3++2019-08-22  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (doRewritesLoop): Fixed the code that+	counts rewrite rules applied so it is accurate.  This allows the+	rewrite rule limit to be correctly enforced.++2019-08-21  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (runiqAt): Ensured that rewriting with+	uniq-at fails when the index is greater than the strand length.++2019-08-19  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Init/Main.hs (main): Added program cpsainit.  The+	programs copies the files Makefile, cpsa4.mk, Make4.hs, and+	template.lisp from the CPSA data directory to the current+	directory, thereby easing the task of starting a CPSA project.++2019-07-15  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/State.hs: Removed the label field in a transition.+	The field was always ignored, and it causes confusion on input.++2019-06-26  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (multiset): Used multisets of trace+	briefs to reduce the number of full permutation isomorphism+	checks.++2019-06-21  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (brief): Added a summary of trace that+	reduces the need for matching during isomorphism checking.++2019-06-04  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Reduction.hs (begin): Reversed todo list after+	running rules so as to get the output order correct.++2019-05-20  Joshua D. Guttman  <guttman@mitre.org>++	* src/CPSA/Lib/Strand.hs (tryPerm): Fixed bug in isomorphism+	checking.  Checking of facts used wrong environment.++2019-05-17  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/SAS/SAS.hs (leadstoKey):  Added support for leadsto in+	shape analysis sentences.++	* src/CPSA/Lib/Strand.hs (kfactVars):  Allow message variables in+	facts that occur nowhere else.+	(useFactVars):  Add flag that disables message variable in facts+	that occur nowhere else and disable it, because isomorphism+	checking is broken.++	* src/CPSA/Strand.hs (doRewriteOne):  Values associated with+	existential variables in rules are freshly generated so that+	parameter terms can be compound.++2019-04-03  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (verbosePreskelWellFormed): Added a check+	that ensures the every variable that occurs in a fact also occurs+	in some strand.+ 2019-03-18  John D. Ramsdell  <ramsdell@mitre.org>  	* cpsa.cabal (Version): Tagged as 3.6.2

NEWS view

@@ -1,5 +1,12 @@ CPSA NEWS +  August 2019:++* Release 3.6.3 adds the cpsainit program and fixes bugs.  The+  cpsainit program copies files from the CPSA data directory into a+  fresh CPSA project directory.  The files ease the task of automating+  the use of the various CPSA tools.+   March, 2019:  * Release 3.6.2 adds the leads-to predicate to the rule language, adds

cpsa.cabal view

@@ -1,5 +1,5 @@ Name:			cpsa-Version:		3.6.2+Version:		3.6.3 Maintainer:		mliskov@mitre.org Cabal-Version:		>= 1.6 License:		BSD3@@ -71,6 +71,7 @@   examples/fluffy_draft03_gske.scm   examples/fluffy_draft03_improving_pske.scm   examples/fluffy_draft03_pske.scm examples/eq_test.scm+  init/Makefile init/template.lisp   examples/eq_test.xhtml Data-Dir:	    	doc Extra-Source-Files:@@ -233,3 +234,12 @@     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Match.Match     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra++Executable cpsainit+  Main-Is:		CPSA/Init/Main.hs+  Build-Depends:	base, directory+  GHC-Options:+    -Wall -fno-warn-name-shadowing -fwarn-unused-imports+  Hs-Source-Dirs:	src+  Other-Modules:+    Paths_cpsa

doc/cpsamanual.pdf view

binary file changed (904636 → 1025619 bytes)

+ doc/init/Makefile view

@@ -0,0 +1,12 @@+CPSAFLAGS = +RTS -M512m -N1 -RTS+CPSATIME = time++SRCS := $(wildcard *.scm) $(wildcard *.lsp)++include cpsa.mk++all:    $(SRCS:%.scm=%_shapes.xhtml) $(SRCS:%.scm=%.xhtml) \+        $(SRCS:%.lsp=%_shapes.xhtml) $(SRCS:%.lsp=%.xhtml)++clean:+	-rm *.txt *.xhtml

+ doc/init/template.lisp view

@@ -0,0 +1,39 @@+;; This is a minimal template for a CPSA input file.++;; Replace <TITLE> with the desired title and <PROTONAME>+;; with the desired name of your project.++;; The defrole template below may be copied and used as+;; a starting point for the roles of your protocol.+;; Change the <ROLENAME> field in each copy as desired.+;; Roles must have distinct names.++;; The basic cryptoalgebra is selected by default. If+;; your project requires the diffie-hellman algebra,+;; delete "basic" on the defprotocol line, uncomment+;; "diffie-hellman" on this same line and uncomment+;; the "(algebra diffie-hellman)" statement in the+;; herald.++;; Refer to the CPSA manual for more information+;; about syntax and additional features.++(herald "<TITLE>"+	;; (algebra diffie-hellman)+	)++(defprotocol <PROTONAME> basic ;; diffie-hellman++  (defrole <ROLENAME>+    (vars )+    (trace++     )+    )++  )++(defskeleton <PROTONAME>+  (vars )+  (defstrand )+  )

+ src/CPSA/Init/Main.hs view

@@ -0,0 +1,112 @@+--  Copies important files from the CPSA data directory to the current+--  directory.++-- Copyright (c) 2019 The MITRE Corporation+--+-- This program is free software: you can redistribute it and/or+-- modify it under the terms of the BSD License as published by the+-- University of California.++module Main (main) where++import System.IO+import System.Environment+import System.Console.GetOpt+import System.Exit+import System.Directory (copyFile, doesFileExist)+import Data.List (elemIndex)+import Data.Version+import Paths_cpsa++main :: IO ()+main =+  do+    argv <- getArgs+    (flags, _) <- opts options argv+    interp flags+    copy ["init/Makefile", "cpsa.mk", "Make.hs", "init/template.lisp"]++-- Copy the file only if it does not already exist++copy :: [String] -> IO ()+copy [] = return ()+copy (f : fs) =+  do+    let b = basename f+    exist <- doesFileExist b+    case exist of+      True ->+        hPutStrLn stderr ("File " ++ b ++ " exists, not overwriting")+      False ->+        do+          fp <- getDataFileName f+          copyFile fp b+          hPutStrLn stderr ("Created " ++ b)+    copy fs++basename :: String -> String+basename f =+  case elemIndex '/' f of+    Nothing -> f+    Just i -> basename (drop (i + 1) f)++-- Command-line options++data Flag+    = Help                      -- Help+    | Info                      -- Version information+      deriving Show++options :: [OptDescr Flag]+options =+    [ Option ['h'] ["help"]     (NoArg Help)           "show help message",+      Option ['v'] ["version"]  (NoArg Info)           "show version number" ]++opts :: [OptDescr a] -> [String] -> IO ([a], [String])+opts options argv =+    case getOpt RequireOrder options argv of+      (o, n, []) -> return (o, n)+      (_, _, errs) ->+          do+            msg <- use options errs+            abort msg++use :: [OptDescr a] -> [String] -> IO String  -- Return usage string+use options errs =+    do+      name <- getProgName+      datadir <- getDataDir+      let header = "Usage: " ++ name ++ " [OPTIONS]"+      let footer = "\nDocumentation directory: " ++ datadir+      return (concat errs ++ usageInfo header options ++ footer)++-- Interpret option flags++interp :: [Flag] -> IO ()+interp flags =+    loop flags+    where+      loop [] = return ()+      loop (Info : _) =+          success cpsaVersion+      loop (Help : _) =+          do                    -- Show help then exit with success+            msg <- use options []+            success msg++-- From CPSA.Lib.Entry++cpsaVersion :: String+cpsaVersion = showString "CPSA " (showVersion version)++abort :: String -> IO a         -- Print message then exit with failure+abort msg =+    do+      hPutStrLn stderr msg+      exitFailure++success :: String -> IO a       -- Print message then exit with success+success msg =+    do+      hPutStrLn stderr msg+      exitWith ExitSuccess

src/CPSA/Lib/Cohort.hs view

@@ -63,7 +63,7 @@         case derivable (avoid k) ts t of           True -> (acc, ns')           False -> (graphNode n : acc, ns')-    Sync (Tran (Just _, _, _))+    Sync (Tran (Just _, _))       | not (explainable k n (leadsto k)) ->           (graphNode n : acc, ns)     _ -> (acc, ns)@@ -688,9 +688,9 @@       loop (ht + 1) acc c     loop ht acc (Out _ : c) =       loop (ht + 1) acc c-    loop ht acc (Sync (Tran (_, Nothing, _)) : c) =+    loop ht acc (Sync (Tran (_, Nothing)) : c) =       loop (ht + 1) acc c-    loop ht acc (Sync (Tran (_, Just next, _)) : c) =+    loop ht acc (Sync (Tran (_, Just next)) : c) =       loop (ht + 1) acc' c       where         acc' = nextNodeA now g role ht next acc

src/CPSA/Lib/Displayer.hs view

@@ -52,7 +52,7 @@ displayImpl ctx g =   L () [S () "implies",         displayConj ctx (antec g),-        displayDisj ctx (zip (evars g) (concl g)) ]+        displayDisj ctx (consq g) ]  displayDisj :: Algebra t p g s e c => c -> [([t], [AForm t])] -> SExpr () displayDisj _ [] = L () [S () "false"]@@ -180,20 +180,13 @@       displayDt (Sync t) = L () (displayTran ctx t)  displayTran :: Algebra t p g s e c => c -> Tran t -> [SExpr ()]-displayTran ctx (Tran(Just now, Just next, Nothing)) =+displayTran ctx (Tran(Just now, Just next)) =   [S () "tran", displayTerm ctx now,  displayTerm ctx next]-displayTran ctx (Tran(Just now, Just next, Just label)) =-  [S () "tran", displayTerm ctx now,  displayTerm ctx next,-                displayTerm ctx label]-displayTran ctx (Tran(Just now, Nothing, Nothing)) =+displayTran ctx (Tran(Just now, Nothing)) =   [S () "obsv", displayTerm ctx now]-displayTran ctx (Tran(Just now, Nothing, Just label)) =-  [S () "obsv", displayTerm ctx now, displayTerm ctx label]-displayTran ctx (Tran(Nothing, Just next, Nothing)) =+displayTran ctx (Tran(Nothing, Just next)) =   [S () "init", displayTerm ctx next]-displayTran ctx (Tran(Nothing, Just next, Just label)) =-  [S () "init", displayTerm ctx next, displayTerm ctx label]-displayTran _ (Tran(Nothing, Nothing, _)) =+displayTran _ (Tran(Nothing, Nothing)) =   assertError("Displayer.displayTran: encountered sync node with current or next state")  -- Display of preskeletons

src/CPSA/Lib/Loader.hs view

@@ -424,7 +424,7 @@       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@@ -443,31 +443,15 @@     do       t0 <- loadTerm vars True t0       t1 <- loadTerm vars True t1-      return $ Sync $ Tran (Just t0, Just t1, Nothing)-loadEvt vars (L _ [S _ "tran", t0, t1, t2]) =-    do-      t0 <- loadTerm vars True t0-      t1 <- loadTerm vars True t1-      t2 <- loadTerm vars True t2-      return $ Sync $ Tran (Just t0, Just t1, Just t2)+      return $ Sync $ Tran (Just t0, Just t1) loadEvt vars (L _ [S _ "obsv", t0]) =     do       t0 <- loadTerm vars True t0-      return $ Sync $ Tran (Just t0, Nothing, Nothing)-loadEvt vars (L _ [S _ "obsv", t0, t1]) =-    do-      t0 <- loadTerm vars True t0-      t1 <- loadTerm vars True t1-      return $ Sync $ Tran (Just t0, Nothing, Just t1)+      return $ Sync $ Tran (Just t0, Nothing) loadEvt vars (L _ [S _ "init", t0]) =     do       t0 <- loadTerm vars True t0-      return $ Sync $ Tran (Nothing, Just t0, Nothing)-loadEvt vars (L _ [S _ "init", t0, t1]) =-    do-      t0 <- loadTerm vars True t0-      t1 <- loadTerm vars True t1-      return $ Sync $ Tran (Nothing, Just t0, Just t1)+      return $ Sync $ Tran (Nothing, Just t0) loadEvt _ (L pos [S _ dir, _]) =     fail (shows pos $ "Malformed direction: " ++ dir) loadEvt _ x = fail (shows (annotation x) "Malformed event")@@ -612,7 +596,7 @@     | otherwise =         case trace (insts !! s) !! i of           Out _ -> fail (shows pos "Priority declaration disallowed on sending")-          Sync (Tran (Nothing, _, _))+          Sync (Tran (Nothing, _))             -> fail (shows pos                      "Priority declaration disallowed on initializers")           _ -> do@@ -937,12 +921,13 @@   do     antec <- loadCheckedConj md pos prot vars vars a     (g, vc) <- loadConclusion pos prot g vars c-    let (evars, concl) = unzip vc+    let f (evars, form) = (evars, map snd form)+    let consq = map f vc        -- Expunge position info     let goal =           Goal { uvars = vars,                  antec = map snd antec,-                 evars = evars,-                 concl = map (map snd) concl }+                 consq = consq,+                 concl = map snd consq }     return (g, goal, antec) loadImplication _ pos _ _ _ _ = fail (shows pos "Malformed goal implication") @@ -999,7 +984,11 @@   do     as <- loadConjunction pos prot vars x     let as' = L.sortBy (\(_, x) (_, y) -> aFormOrder x y) as-    unbound <- foldM roleSpecific unbound as'+    let unbound' =+          if useFactVars+          then foldl factSpecific unbound as'+          else unbound+    unbound <- foldM roleSpecific unbound' as'     case unbound of       [] -> return as'       (v : _) -> fail (shows (annotation x) ("Malformed defgoal: " ++ showst v " not used"))@@ -1202,3 +1191,9 @@   | isStrdVar t' = fail (shows pos "Type mismatch in equals")   | allBound unbound t && allBound unbound t' = return unbound   | otherwise = fail (shows pos "Unbound variable in equals")++-- Remove unbound message variables that occur in a fact+factSpecific :: Algebra t p g s e c => [t] -> (Pos, AForm t) -> [t]+factSpecific unbound (_, AFact _ fs) =+  unbound L.\\ foldl addVars [] (L.filter (not . isStrdVar) fs)+factSpecific unbound _ = unbound

src/CPSA/Lib/Protocol.hs view

@@ -80,13 +80,13 @@ -- Extract the term in an inbound event. inbnd :: Event t -> Maybe t inbnd (In t) = Just t-inbnd (Sync (Tran (Just t,_,_))) = Just t+inbnd (Sync (Tran (Just t, _))) = Just t inbnd _ = Nothing  -- Extract the term in an outbound event. outbnd :: Event t -> Maybe t outbnd (Out t) = Just t-outbnd (Sync (Tran (_,Just t,_))) = Just t+outbnd (Sync (Tran (_, Just t))) = Just t outbnd _ = Nothing  {-@@ -411,7 +411,8 @@ data Goal t   = Goal { uvars :: [t],          -- Universally quantified variables            antec :: [AForm t],    -- Antecedent-           evars :: [[t]],        -- Existentially quantified variables+           -- Consequent with existentially quantified variables+           consq :: [([t], [AForm t])],            concl :: [[AForm t]] } -- Conclusion   deriving Show

src/CPSA/Lib/Reduction.hs view

@@ -150,7 +150,7 @@                 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 +                  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@@ -176,7 +176,7 @@                        Nada "Not closed under rules")               let (n', seen', todo', _) =                     foldl (next lk) (n, seen, todo, []) kids-              loop n' seen' todo' lks+              loop n' seen' (reverse todo') lks  -- Apply collapse until all possibilities are exhausted. search :: Algebra t p g s e c => Options -> Handle ->

src/CPSA/Lib/State.hs view

@@ -4,47 +4,41 @@ import CPSA.Lib.Algebra import CPSA.Lib.Utilities --- A transition-newtype Tran t = Tran (Maybe t, Maybe t, Maybe t) deriving (Show, Eq, Ord)+-- A transition (pre-state, post-state)+newtype Tran t = Tran (Maybe t, Maybe t) deriving (Show, Eq, Ord)  now :: Tran t -> Maybe t-now (Tran (t, _, _)) = t+now (Tran (t, _)) = t  next :: Tran t -> Maybe t-next (Tran (_, t, _)) = t---- Labels are ignored--- label :: Tran t -> Maybe t--- label (Tran (_, _, t)) = t+next (Tran (_, t)) = t  observer :: Tran t -> Bool-observer (Tran (_, Nothing, _)) = True+observer (Tran (_, Nothing)) = True observer _ = False  path :: Tran t -> Bool path x = not (observer x)  transition :: Tran t -> Bool-transition (Tran (Just _, Just _, _)) = True+transition (Tran (Just _, Just _)) = True transition _ = False  tranTerms :: Tran t -> [t]-tranTerms (Tran (Nothing, Nothing, _)) =+tranTerms (Tran (Nothing, Nothing)) =   assertError ("Encountered sync with no pre- or post-state in State.hs:tranTerms")-tranTerms (Tran (now, next, label)) =-  catMaybes [now, next, label]+tranTerms (Tran (now, next)) =+  catMaybes [now, next]  mapTran :: (t -> t) -> Tran t -> Tran t-mapTran f (Tran (now, next, label)) =-  Tran (maybe Nothing (Just . f) now, maybe Nothing (Just . f) next,-        maybe Nothing (Just . f) label)+mapTran f (Tran (now, next)) =+  Tran (maybe Nothing (Just . f) now, maybe Nothing (Just . f) next)  matchTran :: Algebra t p g s e c => Tran t -> Tran t -> (g, e) -> [(g, e)]-matchTran (Tran (c, n, l)) (Tran (c', n', l')) ge =+matchTran (Tran (c, n)) (Tran (c', n')) ge =   do-    ge0 <- matchNext c c' ge-    ge1 <- matchNext n n' ge0-    matchNext l l' ge1+    ge <- matchNext c c' ge+    matchNext n n' ge  matchNext :: Algebra t p g s e c => Maybe t -> Maybe t -> (g, e) -> [(g, e)] matchNext Nothing Nothing ge = [ge]@@ -52,11 +46,10 @@ matchNext _ _ _ = []  unifyTran :: Algebra t p g s e c => Tran t -> Tran t -> (g, s) -> [(g, s)]-unifyTran (Tran (c, n, l)) (Tran (c', n', l')) gs =+unifyTran (Tran (c, n)) (Tran (c', n')) gs =   do-    gs0 <- unifyNext c c' gs-    gs1 <- unifyNext n n' gs0-    unifyNext l l' gs1+    gs <- unifyNext c c' gs+    unifyNext n n' gs  unifyNext :: Algebra t p g s e c => Maybe t -> Maybe t -> (g, s) -> [(g, s)] unifyNext Nothing Nothing ge = [ge]

src/CPSA/Lib/Strand.hs view

@@ -1,4 +1,4 @@--- on data structures and support functions.+-- Instance and preskeleton data structures and support functions.  -- Copyright (c) 2009 The MITRE Corporation --@@ -9,7 +9,7 @@ module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener,     role, env, trace, height, listenerTerm, Sid, Node, mkPreskel,     firstSkeleton, Pair, Preskel, gen, protocol, kgoals, insts,-    orderings, leadsto, kfacts,+    orderings, leadsto, kfacts, useFactVars,     pov, korig, kcomment, nstrands, kvars, kpriority, kpriorities,     strandids, kterms, avoid, preskelWellFormed, verbosePreskelWellFormed,     Strand, inst, nodes, Vertex, preds, event, kabsent,@@ -74,6 +74,10 @@ useDeOrigination :: Bool useDeOrigination = False -- useThinning +-- Enable variables in facts that do not occur elsewhere in skeletons+useFactVars :: Bool+useFactVars = False -- True+ -- Sanity check: ensure no role variable occurs in a skeleton. useCheckVars :: Bool useCheckVars = False@@ -468,8 +472,8 @@       checkLeadsto [] _ = []       checkLeadsto (((s1,i1),(s2,i2)) : rest) consumed =         case ((trace (insts !! s1)) !! i1) of-          Sync (Tran (_, Just t, _)) -> case ((trace (insts !! s2)) !! i2) of-            Sync (Tran (Just t', nxt, _)) ->+          Sync (Tran (_, Just t)) -> case ((trace (insts !! s2)) !! i2) of+            Sync (Tran (Just t', nxt)) ->                if (t /= t') then error ("Strand.mkPreskel: invalid state edge at " ++ show (s1,i1))                else case nxt of                  Nothing -> (((s1,i1),(s2,i2)) : checkLeadsto rest consumed)@@ -599,9 +603,9 @@ reducedPairWellOrdered (n0, n1) =     case (event n0, event n1) of       (Out _, In _) -> True-      (Sync (Tran (_, Just _, _)), Sync (Tran (Just _, _, _))) ->+      (Sync (Tran (_, Just _)), Sync (Tran (Just _, _))) ->         True-      (Sync (Tran (_, Nothing, _)), Sync (Tran (Just _, Just _, _))) ->+      (Sync (Tran (_, Nothing)), Sync (Tran (Just _, Just _))) ->         True       (Sync _, In _) -> True       (Out _, Sync _) -> True@@ -646,12 +650,14 @@       numbering = dfs preds start'  -- Variables in this preskeleton, excluding ones in roles, and ones--- that only occur in a cause.+-- that only occur in a cause.  The variables in facts are explicitly+-- included. kvars :: Algebra t p g s e c => Preskel t g s e -> [t] kvars k =     S.elems $ foldl addIvars dvars (insts k)     where-      dvars = foldl f S.empty $ declsTerms (decls k)+      factVars = if useFactVars then kfactVars k else S.empty+      dvars = foldl f factVars $ declsTerms (decls k)       f s t = foldVars (flip S.insert) s t  traceBase :: Int@@ -694,6 +700,7 @@       gfacts :: [Fact t],       nvars :: !Int,           -- Number of variables       ntraces :: !Int,         -- Number of traces+      briefs :: [(Int, Int)],  -- Multiset of trace briefs       norderings :: !Int,      -- Number of orderings       nleadsto :: !Int,        -- Number of leadsto pairs       nsndecls :: [Int],       -- Counts of decls@@ -711,12 +718,17 @@            gpatterns = patterns,            nvars = length (kvars k),            ntraces = length gtraces,+           briefs = multiset (map fst gtraces),            norderings = length gorderings,            nleadsto = length gleadsto,            nsndecls = nsds gdecls,            nfacts = length gfacts }     where-      gtraces = map (\i -> (height i, trace i)) (insts k)+      gtraces = map f (insts k)+      -- Old: f i = (height i, trace i)+      f i =+        (brief c, c)+        where c = trace i       gorderings = orderings k       gleadsto = leadsto k       gdecls = decls k@@ -724,6 +736,28 @@       patterns = L.sort (map (tracePattern . trace) (insts k))       nsds decls = [length (dknon decls), length (dkpnon decls), length (dkunique decls)] +-- Summarize a trace so that two traces don't match unless they have+-- the same number.  The summary used to be the height of the trace.+brief :: Algebra t p g s e c => Trace t -> Int+brief [] = 0+brief (In _ : c) = 1 + 4 * brief c+brief (Out _ : c) = 2 + 4 * brief c+brief (Sync _ : c) = 3 + 4 * brief c++-- Convert a list of integers into a sorted multiset representation.+-- The output is a list of pairs, (i, n). Integer n gives the+-- multiplity of integer i in the input list.  List is sorted based on+-- the first element in each pair.+multiset :: [Int] -> [(Int, Int)]+multiset brf =+  L.foldl insert [] brf+  where+    insert [] b = [(b, 1)]+    insert ((k, n) : brf) b+      | k == b = (k, n + 1) : brf+      | k > b = (b, 1) : (k, n) : brf+      | otherwise = (k, n) : insert brf b+ -- Test to see if two preskeletons are isomorphic  -- First, ensure the two preskeletons have:@@ -748,6 +782,7 @@ isomorphic g g' = --    nvars g == nvars g' &&  -- Wrong in DH     ntraces g == ntraces g' &&+    briefs g == briefs g' &&     norderings g == norderings g' &&     gpatterns g == gpatterns g' &&     nleadsto g == nleadsto g' &&@@ -836,7 +871,7 @@     checkOrigs g g' fenv perm &&     checkOrigs g' g renv (invperm perm) &&     checkFacts g g' fenv perm &&-    checkFacts g' g fenv (invperm perm) &&+    checkFacts g' g renv (invperm perm) &&     containsMapped (permutePair perm) (gorderings g') (gorderings g) &&     containsMapped (permutePair perm) (gleadsto g') (gleadsto g) @@ -846,7 +881,7 @@     checkOrigs g g' fenv perm &&     checkOrigs g' g renv perm &&     checkFacts g g' fenv perm &&-    checkFacts g' g fenv (invperm 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)]@@ -2086,6 +2121,7 @@     varSubset (kpnon k) terms &&     all nonCheck (knon k) &&     all uniqueCheck (kunique k) &&+    all factCheck (kfacts k) &&     origNonNullCheck k && ugenNonNullCheck k &&     wellOrdered k && acyclicOrder k &&     roleOrigCheck k && fst (declCheck (decls k))@@ -2094,6 +2130,7 @@       mesgterms = kmesgterms k       nonCheck t = all (not . carriedBy t) mesgterms       uniqueCheck t = any (carriedBy t) mesgterms+      factCheck f = factVarsElem (kvars k) f       origNonNullCheck k = (all (\(_, ns) -> not (null ns)) (korig k))       ugenNonNullCheck k = (all (\(_, ns) -> not (null ns))                             (filter (\(t, _) -> not (isNum t)) (kugen k)))@@ -2118,6 +2155,7 @@                    $ varSubset (kpnon k) terms       mapM_ nonCheck $ knon k       mapM_ uniqueCheck $ kunique k+      mapM_ factCheck $ kfacts k       origNonNullCheck k       uniqgenNonNullCheck k       failwith "ordered pairs not well formed" $ wellOrdered k@@ -2135,6 +2173,9 @@       uniqueCheck t =           failwith (showString "uniq-orig " $ showst t " not carried")                        $ any (carriedBy t) mesgterms+      factCheck f =+          failwith ("a fact var in " ++  factPred f ++ " not in some strand")+                       $ factVarsElem (kvars k) f       origNonNullCheck k =           let ts = filter (\(_, ns) -> null ns) (korig k) in           failwith (showString "uniq-orig " $@@ -2163,7 +2204,7 @@     loop [] _ = True     loop ((n0, (s, i)) : es) ns =       case (trace (insts k !! s) !! i) of-        Sync (Tran (Just _, Just _, _)) ->+        Sync (Tran (Just _, Just _)) ->           S.notMember n0 ns && loop es (S.insert n0 ns)         _ -> loop es ns @@ -2451,7 +2492,7 @@                                                  else acc     f acc _ = acc     xform = filter g es         -- Edges that transform-    g (_, (Sync t@(Tran (_, Just _, _)), Sync t'@(Tran (Just _, Just _, _)))) =+    g (_, (Sync t@(Tran (_, Just _)), Sync t'@(Tran (Just _, Just _)))) =       next t == now t'     g _ = False     h t0 pes =@@ -2520,6 +2561,9 @@   = Fact String [FTerm t]   deriving (Eq, Show) +factPred :: Fact t -> String+factPred (Fact pred _) = pred+ substFTerm :: Algebra t p g s e c => s -> FTerm t -> FTerm t substFTerm s (FTerm t) = FTerm $ substitute s t substFTerm _ t = t@@ -2565,6 +2609,17 @@ cleansFacts vs facts =   L.filter (factVarsElem vs) facts +kfactVars :: Algebra t p g s e c => Preskel t g s e -> Set t+kfactVars k =+  foldl (foldFactTerms $ foldVars $ flip S.insert) S.empty (kfacts k)++foldFactTerms :: Algebra t p g s e c => (a -> t -> a) -> a -> Fact t -> a+foldFactTerms f z (Fact _ ts) =+  foldl g z ts+  where+    g a (FSid _) = a+    g a (FTerm t) = f a t+ {- instvars :: Algebra t p g s e c => [Instance t e] -> [t] instvars insts =@@ -2895,7 +2950,7 @@         if null vas then           loop rs               -- Rule does not apply         else-          Just $ doRewrites 0 prules k r vas+          Just $ doRewrites 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@@ -2912,24 +2967,31 @@ ruleLimit = 500  -- Repeatedly applies rules until no rule applies.-doRewrites :: Algebra t p g s e c => Int -> [Rule t] -> Preskel t g s e ->+doRewrites :: Algebra t p g s e c => [Rule t] -> Preskel t g s e ->               Rule t -> [(g, e)] -> [Preskel t g s e]-doRewrites lim _ _ _ _+doRewrites rules k r vas =+  doRewritesLoop rules k (length vas) (doRewrite k r vas) []++doRewritesLoop :: Algebra t p g s e c => [Rule t] -> Preskel t g s e ->+                  Int -> [Preskel t g s e] -> [Preskel t g s e] ->+                  [Preskel t g s e]+doRewritesLoop _ _ 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)+doRewritesLoop _ _ _ [] ks = reverse ks+doRewritesLoop rules k lim (k' : todo) ks =+  loop rules   where-    f k = loop rules-      where-        loop [] = [k]           -- No rules apply-        loop (r : rs) =-          let vas = tryRule k r in-            if null vas then-              loop rs           -- Rule does not apply-            else-              doRewrites (lim + 1) rules k r vas+    loop [] =                   -- No rules apply+      doRewritesLoop rules k lim todo (k' : ks)+    loop (r : rs) =+      let vas = tryRule k' r in+        if null vas then+          loop rs               -- Rule does not apply+        else+          let new = doRewrite k' r vas in+            doRewritesLoop rules k (lim + length vas) (todo ++ new) ks  -- Apply rewrite rule at all assignments doRewrite :: Algebra t p g s e c => Preskel t g s e ->@@ -2942,8 +3004,9 @@                 Rule t -> (g, e) -> [Preskel t g s e] doRewriteOne k r e =   do-    cl <- concl $ rlgoal r-    (k, _) <- doConj (rlname r) cl k e+    (evars, cl) <- consq $ rlgoal r+    let e' = foldl fresh e evars+    (k, _) <- doConj (rlname r) cl k e'     k <- wellFormedPreskel k     k <- toSkeleton True k     return $ f k                -- Add comment about rule application@@ -2951,6 +3014,16 @@                   L () [S () "rule", S () (rlname r)] :                   kcomment k } +fresh :: Algebra t p g s e c => (g, e) -> t -> (g, e)+fresh (g, e) t+  | isStrdVar t = (g, e)+  | otherwise =+      case match t t' (g', e) of+        e' : _ -> e'+        [] -> error "Strand.fresh: Cannot match logical variable to clone"+    where+      (g', t') = clone g t+ type Rewrite t g s e =   Preskel t g s e -> (g, e) -> [(Preskel t g s e, (g, e))] @@ -3060,30 +3133,29 @@     Just s       | height inst < h -> []       | rname (role inst) == rname r ->-        rParam k (g, e) t t'+        rParam name k (g, e) t t'       | otherwise ->         do           (k, (g, e)) <- rDisplace e k' ns s-          rParam k (g, e) t t'+          rParam name k (g, e) t t'       where         inst = strandInst k s         t' = instantiate (env inst) v         k' = addStrand g k r h         ns = nstrands k     Nothing ->-      error ("In rule " ++ name ++ ", parameter predicate for " ++-             rname r ++ " did not get a strand")+      error ("In rule " ++ name +++             ", parameter predicate did not get a strand") -rParam :: Algebra t p g s e c => Preskel t g s e ->+rParam :: Algebra t p g s e c => String -> Preskel t g s e ->           (g, e) -> t -> t -> [(Preskel t g s e, (g, e))]-rParam k (g, e) t t' =+rParam name k (g, e) t t' =   case matched e t of-    False ->-      do-        (g, e) <- match t t' (g, e)-        return (k, (g, e))     True ->       rUnify k (g, e) (instantiate e t) t'+    False ->+      error ("In rule " ++ name +++             ", parameter predicate did not get a value")  rUnify :: Algebra t p g s e c => Preskel t g s e ->           (g, e) -> t -> t -> [(Preskel t g s e, (g , e))]@@ -3196,6 +3268,7 @@     (True, Just s)       | elem (t', (s, i)) (dkuniqFull $ decls k) -> [(k, (g, e))]       | not $ isAtom t' -> []+      | i >= height (strandInst k s) -> []       | otherwise ->         [(k', (g, e))]         where

src/CPSA/SAS/SAS.hs view

@@ -258,6 +258,7 @@       insts :: [Instance t c],       strands :: [t],           -- A variable for each instance       orderings :: [((t, Int), (t, Int))],+      leadsto :: [((t, Int), (t, Int))],       nons :: [t],       pnons :: [t],       uniqs :: [t],@@ -276,6 +277,7 @@       insts <- loadInsts prot kvars [] xs       let heights = map height insts       orderings <- loadOrderings heights (assoc precedesKey xs)+      leadsto <- loadOrderings heights (assoc leadstoKey xs)       nons <- loadBaseTerms kvars (assoc nonOrigKey xs)       pnons <- loadBaseTerms kvars (assoc pnonOrigKey xs)       uniqs <- loadBaseTerms kvars (assoc uniqOrigKey xs)@@ -291,6 +293,7 @@                         insts = insts,                         strands = M.elems varmap,                         orderings = map f orderings,+                        leadsto = map f leadsto,                         nons = nons,                         pnons = pnons,                         uniqs = uniqs,@@ -523,6 +526,10 @@ precedesKey :: String precedesKey = "precedes" +-- The key used in preskeletons for leadsto orderings+leadstoKey :: String+leadstoKey = "leadsto"+ -- The key used in preskeletons for non-originating atoms nonOrigKey :: String nonOrigKey = "non-orig"@@ -618,6 +625,7 @@       insts = map (mapInst env) (insts k),       strands = zs,       orderings = mapPair (instantiate env) (orderings k),+      leadsto = mapPair (instantiate env) (leadsto k),       nons = map (instantiate env) (nons k),       pnons = map (instantiate env) (pnons k),       uniqs = map (instantiate env) (uniqs k),@@ -666,6 +674,7 @@    map (lengthForm kctx k) (M.assocs (varmap k)) ++    concatMap (paramForm kctx) (zip (strands k) $ insts k) ++    map (precForm kctx) (orderings k) +++   map (leadsToForm kctx) (leadsto k) ++    map (unary "non" kctx) (nons k) ++    map (unary "pnon" kctx) (pnons k) ++    -- Not possible map (unary "uniq" kctx) (noOrigUniqs k) ++@@ -714,6 +723,10 @@ -- Creates the atomic formula used to describe a node ordering relation precForm :: Algebra t p g s e c => c -> ((t, Int), (t, Int)) -> SExpr () precForm = quaternary "prec"++-- Creates the atomic formula used to describe a leads to ordering relation+leadsToForm :: Algebra t p g s e c => c -> ((t, Int), (t, Int)) -> SExpr ()+leadsToForm = quaternary "leads-to"  uniqAtForm :: Algebra t p g s e c => c -> (t, (t, Int)) -> SExpr () uniqAtForm = ternary "uniq-at"

src/ocaml/expand.ml view

@@ -95,7 +95,7 @@  let expand o macs x =   if !need_newline-  then print_newline ();+  then output_char o '\n';   print_sexpr o (expand_all macs x);   need_newline := true

src/ocaml/pp.ml view

@@ -5,7 +5,7 @@  let filter o x =   if !need_newline-  then print_newline ();+  then output_char o '\n';   print_sexpr o x;   need_newline := true

tst/aik.tst view

@@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 3.6.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (comment "All input read from injection.scm")  (defprotocol ns diffie-hellman

tst/kerb.tst view

@@ -1,4 +1,4 @@-(comment "CPSA 3.6.2")+(comment "CPSA 3.6.3") (comment "All input read from kerb.scm")  (defprotocol kerb-flawed basic

tst/kerberos++.tst view

@@ -1,4 +1,4 @@-(comment "CPSA 3.6.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (comment "All input read from or.scm")  (defprotocol or basic

tst/owang.tst view

@@ -1,4 +1,4 @@-(comment "CPSA 3.6.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (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.2")+(comment "CPSA 3.6.3") (comment "All input read from yahalom.scm")  (defprotocol yahalom diffie-hellman