cpsa 3.3.0 → 3.3.1
raw patch · 13 files changed
+154/−125 lines, 13 filesbinary-added
Files
- ChangeLog +23/−0
- NEWS +13/−0
- cpsa.cabal +2/−2
- doc/cpsamanual.pdf binary
- doc/examples/IKE_variants.tar.gz binary
- src/CPSA/Basic/Algebra.hs +12/−23
- src/CPSA/DiffieHellman/Algebra.hs +12/−32
- src/CPSA/Lib/Algebra.hs +6/−10
- src/CPSA/Lib/Cohort.hs +6/−17
- src/CPSA/Lib/Entry.hs +2/−0
- src/CPSA/Lib/Main.hs +19/−0
- src/CPSA/Lib/Reduction.hs +51/−37
- src/CPSA/SAS/SAS.hs +8/−4
ChangeLog view
@@ -1,3 +1,26 @@+2016-06-03 Moses D. Liskov <mliskov@mitre.org>++ * doc/examples/IKE_variants.tar.gz: Added this compressed archive+ of IKEv1 and IKEv2 variant input files.+ +2016-03-30 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/SAS/SAS.hs: Added support for fringe skeletons so that+ cpassas makes use of depth limited output. When a tree depth+ limit is exceeded, a fringe labeled skeleton is printed. cpsasas+ produces a sentence with a right-hand-side that encodes both the+ shapes and the fringe. Thus, when cpsa is running the a tree+ depth limit of one, cpsasas computes a cohort analysis sentence.++2016-03-29 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Reduction.hs (LPreskel): Added a depth field, so+ that CPSA aborts when the depth of one branch exceeds a bound.++ * src/CPSA/Lib/Algebra.hs: Added escapeSet to Term class and remove+ protectors, thus computing the escape set in a more+ straightforward way.+ 2015-11-23 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/SAS/Main.hs (main): Changed start up so that the herald
NEWS view
@@ -1,5 +1,18 @@ CPSA NEWS + June, 2016:++* New feature: depth limit. When a depth limit is specified, analysis of+ skeletons will proceed as long as the skeleton's depth in the search tree+ is below the limit. Skeletons not analyzed are marked as "(fringe)" to+ indicate the incomplete nature of those branches of the analysis. Unlike+ hitting a strand bound, the tool does not exit with an error when the depth+ limit is reached.++* IKE_variants.tar.gz added: This is an archive of over 30 variants of+ IKEv1 and IKEv2 protocols modeled in CPSA. The archive can be found in the+ doc/examples directory.+ February, 2016: CPSA version 3 released to the public. Version 3 of CPSA is a major update to the tool including many new features.
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 3.3.0+Version: 3.3.1 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.6 License: BSD3@@ -60,7 +60,7 @@ examples/plaindh.scm examples/plaindh.xhtml examples/priority_test.scm examples/priority_test.xhtml examples/station.scm examples/station.xhtml examples/subsort_test.scm examples/woolam.scm examples/yahalom.scm- examples/yahalom.xhtml+ examples/yahalom.xhtml examples/IKE_variants.tar.gz Data-Dir: doc Extra-Source-Files: Makefile ChangeLog README.txt NEWS ghci cpsatst setup.bat
doc/cpsamanual.pdf view
binary file changed (870621 → 871671 bytes)
+ doc/examples/IKE_variants.tar.gz view
binary file changed (absent → 18502 bytes)
src/CPSA/Basic/Algebra.hs view
@@ -423,28 +423,17 @@ | x `elem` xs = xs | otherwise = x : xs --- Returns the encryptions that carry the target. If the target is--- carried outside all encryptions, or is exposed because a decription--- key is derivable, Nothing is returned.-protectors :: Set Term -> Set Term -> Term -> Term -> Maybe [Term]-protectors avoid sent target source =- do- ts <- bare source S.empty- return $ S.elems ts- where- bare source _- | source == target = Nothing- bare (F Cat [t, t']) acc =- maybe Nothing (bare t') (bare t acc)- bare t@(F Enc [t', key]) acc =- if target `carriedBy` t' then- if (derivable avoid sent) (inv key) then- bare t' acc- else- Just (S.insert t acc)- else- Just acc- bare _ acc = Just acc+escapeSet :: Set Term -> Set Term -> Term -> Maybe (Set Term)+escapeSet ts a ct =+ if buildable ts a ct then+ Nothing+ else+ Just $ S.filter f ts+ where+ f (F Enc [t, key]) =+ carriedBy ct t &&+ not (buildable ts a (inv key))+ f _ = False instance C.Term Term where derivable = derivable@@ -466,7 +455,7 @@ decompose = decompose buildable = buildable encryptions = encryptions- protectors = protectors+ escapeSet = escapeSet loadTerm = loadTerm2 -- Places
src/CPSA/DiffieHellman/Algebra.hs view
@@ -958,37 +958,17 @@ indicatorBasis = S.fold mul M.empty numAvoid indicator _ t = error ("Algebra.hs: indicator called on a non-base " ++ show t) --- Returns the encryptions that carry something relevant to the target.--- If something relevant to the target is carried outside all encryptions,--- or is exposed because a decription key is derivable, Nothing is returned.-protectors :: Set Term -> Set Term -> Term -> Term -> Maybe [Term]-protectors avoid sent target source =--- z ("protectors", avoid, sent, target, source) $- do- ts <- bare source S.empty- return $ S.elems ts- where- bare source acc- | source == target = Nothing- | relevant avoid source target =- case (getBase source == getBase target) of- True -> Nothing- False -> Just (S.insert source acc)- bare (F Cat [t, t']) acc =- maybe Nothing (bare t') (bare t acc)- bare t@(F Enc [t', key]) acc =- if relevantCarriedBy avoid target t' then- if (derivable avoid sent) (inv key) then- bare t' acc- else- Just (S.insert t acc)- else- Just acc- bare t acc =- if relevant avoid target t then- Just (S.insert t acc)- else- Just acc+escapeSet :: Set Term -> Set Term -> Term -> Maybe (Set Term)+escapeSet ts a ct =+ if buildable ts a ct then+ Nothing+ else+ Just $ S.filter f ts+ where+ f (F Enc [t, key]) =+ relevantCarriedBy a ct t &&+ not (buildable ts a (inv key))+ f t = relevant a ct t instance C.Term Term where derivable = derivable@@ -1010,7 +990,7 @@ decompose = decompose buildable = buildable encryptions = encryptions- protectors = protectors+ escapeSet = escapeSet loadTerm = loadTerm -- Places
src/CPSA/Lib/Algebra.hs view
@@ -81,16 +81,12 @@ -- later in the list. encryptions :: t -> [(t,[t])] - -- protectors derivable target source returns Nothing if target is- -- carried by the source outside of an encryption, where derivable- -- is used to determine if a decryption key can be used to expose- -- the target. Otherwise, it returns the list of encryptions in- -- the source that carry the target and have underivable- -- decryption keys, with duplicates eliminated. If two- -- encryptions protect the target, only the outside one is- -- returned. The inside encryption is the one that is carried by- -- the outside encryption.- protectors :: Set t -> Set t -> t -> t -> Maybe [t]+ -- Assume (ts, a) is the output of decomposable, that is ts is a+ -- set of encriptions and a is the reduced avoidance set.+ -- escapeSet ts a ct = Nothing if buildable ts a ct = True.+ -- Otherwise, escapeSet ts a ct = Just es, where es is the escape+ -- set.+ escapeSet :: Set t -> Set t -> t -> Maybe (Set t) -- Given a list of variables, load a term from an S-expression. loadTerm :: Monad m => [t] -> Bool -> SExpr Pos -> m t
src/CPSA/Lib/Cohort.hs view
@@ -8,7 +8,6 @@ module CPSA.Lib.Cohort (Mode(..), reduce, unrealized, minPriority) where -import Control.Monad import qualified Data.Set as S import Data.Set (Set) import qualified Data.List as L@@ -215,9 +214,10 @@ testNode mode k a n = case event n of In t ->- let ts = transmissionsBefore S.empty n in -- Public messages- if derivable a ts t then Nothing- else Just $ solveNode mode k a ts (graphNode n) t+ let ts = transmissionsBefore S.empty n -- Public messages+ (ts', a') = decompose ts a in+ if buildable ts' a' t then Nothing+ else Just $ solveNode mode k a' ts' (graphNode n) t Sync t | not (explainable k n (leadsto k)) -> Just $ solveSyncNode mode k (graphNode n) (now t) _ -> Nothing@@ -231,7 +231,7 @@ where loop [] = assertError ("Cohort.solveNode missing test at " ++ show n) loop ((ct, eks) : cts) =- case escapeSet a ts ct of+ case escapeSet ts a ct of Nothing -> loop cts Just escape -> places (carriedPlaces ct t)@@ -256,22 +256,11 @@ g (_, []) = False -- An encryption test must have g _ = True -- at least one non-derivable key -- Dump derivable encryption keys- h (ct, eks) = (ct, filter (not . (derivable a ts)) eks)+ h (ct, eks) = (ct, filter (not . (buildable ts a)) eks) ff a (t, _) = any (nonTrivIndicator t) (S.elems a) nonTrivIndicator t e = case indicator t e of Just n -> n /= 0 Nothing -> False---- Compute the relevant escape set-escapeSet :: Algebra t p g s e c => Set t ->- Set t -> t -> Maybe (Set t)-escapeSet a ts ct =- foldM f S.empty (S.toList ts)- where- f e t =- do- es <- protectors a ts ct t- return (foldl (flip S.insert) e es) --carriedOnlyWithin :: Algebra t p g s e c => t -> Set t -> t -> Bool --carriedOnlyWithin target escape source =
src/CPSA/Lib/Entry.hs view
@@ -80,6 +80,7 @@ optGoalsSat :: Bool , -- True when goals satisfied stops tree expansion optLimit :: Int, -- Step count limit optBound :: Int, -- Strand cound bound+ optDepth :: Int, -- Tree depth bound optMargin :: Int, -- Output line length optIndent :: Int } -- Pretty printing indent deriving Show@@ -96,6 +97,7 @@ optGoalsSat = False, optLimit = 2000, optBound = 12,+ optDepth = 32, optMargin = 72, optIndent = 2 }
src/CPSA/Lib/Main.hs view
@@ -30,6 +30,10 @@ defaultStrandBound :: Int defaultStrandBound = optBound defaultOptions +-- Default limit on the number of depths is a skeleton.+defaultDepthBound :: Int+defaultDepthBound = optDepth defaultOptions+ -- Default algebra defaultAlgebra :: String defaultAlgebra = optAlg defaultOptions@@ -136,6 +140,10 @@ True -> writeComment h m $ "Strand count bounded at " ++ show (optBound opts) False -> return ()+ case optDepth opts /= defaultDepthBound of+ True -> writeComment h m $+ "Tree depth bounded at " ++ show (optDepth opts)+ False -> return () case optCheckNoncesFirst opts of True -> writeComment h m "Nonces checked first" False -> return ()@@ -168,6 +176,7 @@ = Output String -- Output file name | Limit String -- Step count limit | Bound String -- Strand count bound+ | Depth String -- Tree depth bound | Margin String -- Output line length | Expand -- Expand macros only | NoIsoChk -- Disable isomorphism checks@@ -188,6 +197,8 @@ ("step count limit (default " ++ show defaultStepLimit ++ ")"), Option ['b'] ["bound"] (ReqArg Bound "INT") ("strand count bound (default " ++ show defaultStrandBound ++ ")"),+ Option ['d'] ["depth"] (ReqArg Depth "INT")+ ("tree depth bound (default " ++ show defaultDepthBound ++ ")"), Option ['m'] ["margin"] (ReqArg Margin "INT") ("set output margin (default " ++ show (optMargin defaultOptions) ++ ")"), Option ['e'] ["expand"] (NoArg Expand)@@ -232,6 +243,14 @@ _ -> do msg <- usage options ["Bad value for strand bound\n"]+ abort msg+ loop (Depth value : flags) opts =+ case readDec value of+ [(depth, "")] ->+ loop flags $ opts { optDepth = depth }+ _ ->+ do+ msg <- usage options ["Bad value for depth bound\n"] abort msg loop (Margin value : flags) opts = case readDec value of
src/CPSA/Lib/Reduction.hs view
@@ -38,9 +38,15 @@ data LPreskel t g s e = LPreskel { content :: Preskel t g s e, label :: Int,+ depth :: Int, parent :: Maybe (LPreskel t g s e) } deriving Show +withParent :: Algebra t p g s e c => Preskel t g s e ->+ Int -> LPreskel t g s e -> LPreskel t g s e+withParent k label parent =+ LPreskel k label (1 + depth parent) (Just parent)+ -- A skeleton that has been seen before need not be reanalyzed. -- Instead, one looks up the label of the skeleton seen before, and -- returns it. What follows is the data structure used to store@@ -85,7 +91,7 @@ -- last position is used to hold the reverse of the labels of the -- seen children data Reduct t g s e =- Reduct !(LPreskel t g s e) !Int !Bool ![Preskel t g s e] ![Int]+ Reduct !(LPreskel t g s e) !Int ![Preskel t g s e] ![Int] parMap :: (a -> b) -> [a] -> [b] parMap _ [] = []@@ -103,6 +109,7 @@ -} -- Entry point for analysis+-- n is the step count solve :: Algebra t p g s e c => Options -> Handle -> [Preskel t g s e] -> Int -> IO () solve _ h [] _ = -- Done@@ -113,21 +120,21 @@ case firstSkeleton k of [] -> -- Input cannot be made into a skeleton do- let lk = LPreskel k n Nothing- wrt p h (commentPreskel lk [] (unrealized k) False False+ let lk = LPreskel k n 0 Nothing+ wrt p h (commentPreskel lk [] (unrealized k) Ordinary "Input cannot be made into a skeleton--nothing to do") solve p h ks (n + 1) [k'] -> if isomorphic (gist k) (gist k') then -- Input was a skeleton- let lk' = LPreskel k' n Nothing in+ let lk' = LPreskel k' n 0 Nothing in begin p h ks (n + optLimit p) (n + 1) (hist (gist k', n)) [lk'] else -- Input was not a skeleton do- let lk = LPreskel k n Nothing- wrt p h (commentPreskel lk [] (unrealized k) False False+ let lk = LPreskel k n (-1) Nothing+ wrt p h (commentPreskel lk [] (unrealized k) Ordinary "Not a skeleton")- let lk' = LPreskel k' (n + 1) (Just lk)+ let lk' = withParent k' (n + 1) lk begin p h ks (n + optLimit p) (n + 2) (hist (gist k', n + 1)) [lk'] _ -> error "Main.solve: can't handle more than one skeleton"@@ -209,25 +216,29 @@ do wrt p h (comment "Step limit exceeded--aborting run") dump p h (mktodo reducts todo tobig) "Step limit exceeded"-step p h ks m oseen n seen todo tobig (Reduct lk _ _ _ _ : reducts)+step p h ks m oseen n seen todo tobig (Reduct lk _ _ _ : reducts) | nstrands (content lk) >= optBound p = -- Check strand count step p h ks m oseen n seen todo (lk : tobig) reducts-step p h ks m oseen n seen todo tobig (Reduct lk size cols kids dups : reducts)+step p h ks m oseen n seen todo tobig (Reduct lk size kids dups : reducts) | optGoalsSat p && satCheck lk = -- Stop if goals satisfied mode? do let ns = unrealized (content lk)- let shape = null ns- wrt p h (commentPreskel lk [] ns shape False- "satisfies all")+ let shape = if null ns then Shape else Fringe+ wrt p h (commentPreskel lk [] ns shape "satisfies all") step p h ks m oseen n seen todo tobig reducts | size <= 0 = -- Interpret empty reducts do let ns = unrealized (content lk)- let shape = null ns+ let shape = if null ns then Shape else Ordinary let live = null $ thresholdUnrealized (content lk)- wrt p h (commentPreskel lk [] ns shape False+ wrt p h (commentPreskel lk [] ns shape (if live then "" else "empty cohort")) step p h ks m oseen n seen todo tobig reducts+ | depth lk >= optDepth p =+ do+ let ns = unrealized (content lk)+ wrt p h (commentPreskel lk [] ns Fringe "")+ step p h ks m oseen n seen todo tobig reducts | otherwise = do let (n', seen', todo', dups') =@@ -236,18 +247,17 @@ 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 cols False msg)+ wrt p h (commentPreskel lk (reverse dups') ns Ordinary msg) step p h ks m oseen n' seen' todo' tobig reducts -- Expands one branch in the derivation tree. branch :: Algebra t p g s e c => Options -> Seen t g s e -> LPreskel t g s e -> Reduct t g s e branch p seen lk =- Reduct lk (length kids) cols+ Reduct lk (length kids) (seqList $ reverse unseen) (seqList dups) where kids = reduce (mkMode p) (content lk)- cols = all collapsed kids (unseen, dups) = foldl (duplicates seen) ([], []) kids @@ -258,13 +268,6 @@ visitOldStrandsFirst = optTryOldStrandsFirst p, reverseNodeOrder = optTryYoungNodesFirst p} --- Is preskeleton the result of a collapsing operation?-collapsed :: Algebra t p g s e c => Preskel t g s e -> Bool-collapsed k =- case operation k of- Collapsed _ _ -> True- _ -> False- duplicates :: Algebra t p g s e c => Seen t g s e -> ([Preskel t g s e], [Int]) -> Preskel t g s e -> ([Preskel t g s e], [Int])@@ -278,7 +281,7 @@ [LPreskel t g s e] -> [LPreskel t g s e] -> [LPreskel t g s e] mktodo reducts todo tobig =- map (\(Reduct lk _ _ _ _) -> lk) reducts ++ reverse todo ++ reverse tobig+ map (\(Reduct lk _ _ _) -> lk) reducts ++ reverse todo ++ reverse tobig type Next t p g s e c = (Int, Seen t g s e, [LPreskel t g s e], [Int])@@ -295,7 +298,7 @@ Nothing -> (n + 1, remember (g, n) seen, lk : todo, dups) where- lk = LPreskel k n (Just p) -- Label a preskeleton here+ lk = withParent k n p -- Label a preskeleton here -- This function reduces without checking for isomorphisms fast :: Algebra t p g s e c => Options -> Handle ->@@ -320,7 +323,8 @@ let ns = unrealized (content lk) let ks' = reduce (mkMode p) (content lk) let msg = show (length ks') ++ " in cohort"- wrt p h (commentPreskel lk [] ns (null ns) False msg)+ let shape = if null ns then Shape else Ordinary+ wrt p h (commentPreskel lk [] ns shape msg) let (n', todo') = foldl (children lk) (n, []) ks' fast p h ks m n' (todo ++ reverse todo') @@ -328,7 +332,7 @@ (Int, [LPreskel t g s e]) -> Preskel t g s e -> (Int, [LPreskel t g s e]) children p (n, todo) k = -- Label a preskeleton here- (n + 1, LPreskel k n (Just p) : todo)+ (n + 1, withParent k n p : todo) -- Print partial results in a form that works with analysis tools dump :: Algebra t p g s e c => Options -> Handle ->@@ -340,32 +344,30 @@ dump p h (lk : lks) msg = do let ns = unrealized $ content lk- wrt p h (commentPreskel lk [] ns False True "aborted")+ wrt p h (commentPreskel lk [] ns Ordinary "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] -> Bool -> Bool -> String -> SExpr ()-commentPreskel lk seen unrealized shape _ msg =+ [Int] -> [Node] -> Kind -> String -> SExpr ()+commentPreskel lk seen unrealized kind 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) $--- addKeyValues "unrealized-todo" (map displayNode $ L.sort (filter (\n -> priority k n >= minPriority) unrealized)) $- condAddKeyValues "shape" shape [] $- condAddKeyValues "satisfies" (shape && (not $ null $ kgoals k))+ addKindKey kind $+ condAddKeyValues "satisfies" (kind == Shape && (not $ null $ kgoals k)) (satisfies k) $ -- Structure preserving maps -- Added for cpsasas program- condAddKeyValues "maps" shape (maps k) $+ condAddKeyValues "maps" fringe (maps k) $ -- Nodes of origination -- Added for cpsasas program- condAddKeyValues "origs" (starter k || shape) (origs k) $- -- condAddKeyValues "ugens" (starter k || shape) (ugens k) $+ condAddKeyValues "origs" (starter k || fringe) (origs k) $ -- Messages case msg of "" -> []@@ -373,6 +375,7 @@ "Not a skeleton" -> addKeyValues "preskeleton" [] [comment msg] _ -> [comment msg] where+ fringe = kind /= Ordinary k = content lk starter k = -- True for the POV skeleton and case pov k of -- just a few others@@ -395,6 +398,17 @@ rest maybeAddVKeyValues key f (Just x) rest = addKeyValues key (f x) rest++data Kind+ = Ordinary+ | Shape+ | Fringe+ deriving (Eq, Show)++addKindKey :: Kind -> [SExpr ()] -> [SExpr ()]+addKindKey Ordinary xs = xs+addKindKey Shape xs = addKeyValues "shape" [] xs+addKindKey Fringe xs = addKeyValues "fringe" [] xs -- Variable assignments and security goals
src/CPSA/SAS/SAS.hs view
@@ -46,7 +46,7 @@ do p <- findProt pos ps xs k <- loadPreskel pos p (pgen p) xs- case (isSkeleton k, isShape k) of+ case (isSkeleton k, isFringe k) of (True, False) -> do -- Found POV origCheck pos k -- Ensure uniqs originate@@ -66,7 +66,7 @@ p <- findProt pos ps xs let g = kgen (last ks) -- Make sure vars in skeleton are k <- loadPreskel pos p g xs -- distinct from the ones in the POV- case isShape k of+ case isFringe k of True -> do -- Found shape origCheck pos k -- Ensure uniqs originate@@ -251,7 +251,7 @@ uniqs :: [t], origs :: [(t, t)], isSkeleton :: Bool,- isShape :: !Bool, -- Always looked at, so make it strict+ isFringe :: !Bool, -- Always looked at, so make it strict homomorphisms :: [SExpr Pos], -- Loaded later varmap :: VM t } @@ -282,7 +282,7 @@ uniqs = uniqs, origs = map g origs, isSkeleton = not $ hasKey preskeletonKey xs,- isShape = hasKey shapeKey xs,+ isFringe = hasKey shapeKey xs || hasKey fringeKey xs, homomorphisms = assoc mapsKey xs, varmap = varmap}) loadPreskel pos _ _ _ = fail (shows pos "Malformed skeleton")@@ -503,6 +503,10 @@ -- The key used to identify a shape shapeKey :: String shapeKey = "shape"++-- The key used to identify a non-shape fringe+fringeKey :: String+fringeKey = "fringe" -- The key used to extract the list of homomorphisms mapsKey :: String