cpsa-4.4.9: src/CPSA/Displayer.hs
-- Displays protocols and preskeletons as S-expressions.
-- Copyright (c) 2009 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 CPSA.Displayer (displayProt, displayPreskel, displayNode,
displayFact, displayForm,
displayOperation, displayStrandMap,
varsContext) where
import qualified Data.List as L
import qualified Data.Set as S
import CPSA.Lib.SExpr
import CPSA.Algebra
import CPSA.Channel
import CPSA.Protocol
import CPSA.Operation
import CPSA.Strand
{--
import System.IO.Unsafe
z :: Show a => a -> b -> b
z x y = unsafePerformIO (print x >> return y)
zz :: Show a => a -> a
zz x = z x x
--}
-- Display of protocols
displayProt :: Prot -> SExpr ()
displayProt p =
L () (S () "defprotocol" : S () (pname p) : S () (alg p) : rs)
where
rs = foldl f ((map displayUserRule (userrules p)) ++
(map displayGenRule (generatedrules p)) ++
pcomment p)
(reverse (roles p))
f rs r = displayRole r : rs
displayRule :: String -> Rule -> SExpr ()
displayRule s r =
L () (S () s :
S () (rlname r) :
displayGoal (rlgoal r) :
rlcomment r)
displayUserRule :: Rule -> SExpr ()
displayUserRule = displayRule "defrule"
displayGenRule :: Rule -> SExpr ()
displayGenRule = displayRule "defgenrule"
displayGoal :: Goal -> SExpr ()
displayGoal g =
L () [S () "forall",
L () (displayVars ctx vars),
displayImpl ctx g]
where
ctx = varsContext vars
vars = uvars g
displayImpl :: Context -> Goal -> SExpr ()
displayImpl ctx g =
L () [S () "implies",
displayConj ctx (antec g),
displayDisj ctx (consq g) ]
displayDisj :: Context -> [([Term], [AForm])] -> SExpr ()
displayDisj _ [] = L () [S () "false"]
displayDisj ctx [conj] = displayExistential ctx conj
displayDisj ctx disj =
L () (S () "or" : map (displayExistential ctx) disj)
displayExistential :: Context -> ([Term], [AForm]) -> SExpr ()
displayExistential ctx ([], conj) =
displayConj ctx conj
displayExistential ctx (evars, conj) =
L () [S () "exists",
L () (displayVars ctx' evars),
displayConj ctx' conj]
where
ctx' = addToContext ctx evars
displayConj :: Context -> [AForm] -> SExpr ()
-- displayConj _ [] = error "DisplayConj: empty conjunction"
displayConj ctx [form] = displayForm ctx form
displayConj ctx forms = L () (S () "and" : map (displayForm ctx) forms)
displayForm :: Context -> AForm -> SExpr ()
displayForm ctx (Length r s l) =
L () [S () "p", Q () (rname r), displayTerm ctx s, displayTerm ctx l]
displayForm ctx (Param r p _ s t) =
L () [S () "p", Q () (rname r), displayParam r p,
displayTerm ctx s, displayTerm ctx t]
displayForm ctx (Prec (x, i) (y, j)) =
L () [S () "prec", displayTerm ctx x, displayTerm ctx i,
displayTerm ctx y, displayTerm ctx j]
displayForm ctx (Non t) =
L () [S () "non", displayTerm ctx t]
displayForm ctx (Pnon t) =
L () [S () "pnon", displayTerm ctx t]
displayForm ctx (Uniq t) =
L () [S () "uniq", displayTerm ctx t]
displayForm ctx (UniqAt t (s, i)) =
L () [S () "uniq-at", displayTerm ctx t,
displayTerm ctx s, displayTerm ctx i]
displayForm ctx (Ugen t) =
L () [S () "ugen", displayTerm ctx t]
displayForm ctx (UgenAt t (s, i)) =
L () [S () "ugen-at", displayTerm ctx t,
displayTerm ctx s, displayTerm ctx i]
displayForm ctx (GenStV t) =
L () [S () "gen-st", displayTerm ctx t]
displayForm ctx (Conf t) =
L () [S () "conf", displayTerm ctx t]
displayForm ctx (Auth t) =
L () [S () "auth", displayTerm ctx t]
displayForm ctx (AFact name fs) =
L () (S () "fact" : S () name : map (displayTerm ctx) fs)
displayForm ctx (Equals t1 t2) =
L () [S () "=", displayTerm ctx t1, displayTerm ctx t2]
displayForm ctx (Component t1 t2) =
L () [S () "component", displayTerm ctx t1, displayTerm ctx t2]
displayForm ctx (Commpair (i,j) (i',j')) =
L () [S () "comm-pr",
displayTerm ctx i, displayTerm ctx j,
displayTerm ctx i', displayTerm ctx j']
displayForm ctx (SameLocn (i,j) (i',j')) =
L () [S () "same-locn",
displayTerm ctx i, displayTerm ctx j,
displayTerm ctx i', displayTerm ctx j']
displayForm ctx (StateNode (i,j)) =
L () [S () "state-node",
displayTerm ctx i, displayTerm ctx j]
displayForm ctx (Trans (i,j)) =
L () [S () "trans",
displayTerm ctx i, displayTerm ctx j]
displayForm ctx (LeadsTo (i,j) (i',j')) =
L () [S () "leads-to",
displayTerm ctx i, displayTerm ctx j,
displayTerm ctx i', displayTerm ctx j']
displayParam :: Role -> Term -> SExpr ()
displayParam r t =
case displayTerm (varsContext (rvars r)) t of
S () var -> Q () var
_ -> error "displayParam: bad parameter"
-- Display of roles
sansPts :: [Term] -> [Term]
sansPts = filter notPt
sansNestedPts :: [(Maybe Int, Term)] -> [(Maybe Int, Term)]
sansNestedPts = filter (\(_,t) -> notPt t)
sansPtMaplets :: [(Term, Term)] -> [(Term, Term)]
sansPtMaplets = filter (\(v,_) -> notPt v)
displayRole :: Role -> SExpr ()
displayRole r =
L () (S () "defrole" :
S () (rname r) :
L () (S () "vars" : displayVars ctx (sansPts vars)) :
L () (S () "trace" : displayTraceNoPt ctx (rtrace r)) :
displayOptional "non-orig" (displayLenTerms ctx
(sansNestedPts (rnon r)))
(displayOptional "pen-non-orig" (displayLenTerms ctx
(sansNestedPts (rpnon r)))
(displayOptional "uniq-orig" (displayTerms ctx
(sansPts (runique r)))
(displayOptional "uniq-gen" (displayTerms ctx (runiqgen r))
(displayOptional "absent" (displayTermPairs ctx (rabsent r))
(displayOptional "conf" (displayTerms ctx (rconf r))
(displayOptional "auth" (displayTerms ctx (rauth r))
(rcomment r))))))))
where
ctx = varsContext $ rvars r
vars = sansPts $ rvars r
varsContext :: [Term] -> Context
varsContext vars =
addToContext emptyContext vars
displayTerms :: Context -> [Term] -> [SExpr ()]
displayTerms ctx ts = map (displayTerm ctx) (L.sort ts)
displayLenTerms :: Context -> [(Maybe Int, Term)] -> [SExpr ()]
displayLenTerms ctx ts = map (displayLenTerm ctx) (L.sort ts)
displayLenTerm :: Context -> (Maybe Int, Term) -> SExpr ()
displayLenTerm ctx (Nothing, t) = displayTerm ctx t
displayLenTerm ctx (Just len, t) = L () [N () len, displayTerm ctx t]
displayTermPair :: Context -> (Term, Term) -> SExpr ()
displayTermPair ctx (x, y) =
L () [displayTerm ctx x, displayTerm ctx y]
displayTermPairs :: Context -> [(Term, Term)] -> [SExpr ()]
displayTermPairs ctx ts = map (displayTermPair ctx) (L.sort ts)
displayOptional :: String -> [SExpr ()] -> [SExpr ()] -> [SExpr ()]
displayOptional _ [] rest = rest
displayOptional key value rest =
L () (S () key : value) : rest
displayTrace :: Context -> Trace -> [SExpr ()]
displayTrace ctx trace =
map displayDt trace
where
displayDt (In (Plain t)) =
L () [S () "recv", displayTerm ctx t]
displayDt (In (ChMsg ct ch t)) =
case ct == Locn of
True -> L () [S () "load", displayTerm ctx ch, displayTerm ctx t]
False -> L () [S () "recv", displayTerm ctx ch, displayTerm ctx t]
displayDt (Out (Plain t)) =
L () [S () "send", displayTerm ctx t]
displayDt (Out (ChMsg ct ch t)) =
case ct == Locn of
True -> L () [S () "stor", displayTerm ctx ch, displayTerm ctx t]
False -> L () [S () "send", displayTerm ctx ch, displayTerm ctx t]
displayTraceNoPt :: Context -> Trace -> [SExpr ()]
displayTraceNoPt ctx trace =
map displayDt trace
where
displayDt (In (Plain t)) =
L () [S () "recv", displayTerm ctx t]
displayDt (In (ChMsg ct ch t)) =
case ct == Locn of
True -> L () [S () "load", displayTerm ctx ch, displayTermNoPt ctx t]
False -> L () [S () "recv", displayTerm ctx ch, displayTerm ctx t]
displayDt (Out (Plain t)) =
L () [S () "send", displayTerm ctx t]
displayDt (Out (ChMsg ct ch t)) =
case ct == Locn of
True -> L () [S () "stor", displayTerm ctx ch, displayTermNoPt ctx t]
False -> L () [S () "send", displayTerm ctx ch, displayTerm ctx t]
-- Display of preskeletons
displayPreskel :: Preskel -> [SExpr ()] -> SExpr ()
displayPreskel k rest =
L () (S () "defskeleton" :
S () (pname (protocol k)) :
L () (S () "vars" : displayVars ctx vars ) :
-- (sansPts vars) lets
-- try printing points
foldr f (displayRest k ctx rest) (insts k))
where
ctx = varsContext vars
vars = kfvars k ++ kvars k
f i rest = displayInst ctx i : rest
-- Display the remainder of a preskeleton
displayRest :: Preskel -> Context -> [SExpr ()] -> [SExpr ()]
displayRest k ctx rest =
(displayOptional "precedes" (displayOrdering (orderings k))
(displayOptional "non-orig" (displayTerms ctx (sansPts (knon k)))
(displayOptional "pen-non-orig" (displayTerms ctx (sansPts (kpnon k)))
(displayOptional "uniq-orig" (displayTerms ctx (sansPts (kunique k)))
(displayOptional "uniq-gen" (displayTerms ctx (kuniqgen k))
(displayOptional "absent" (displayTermPairs ctx (kabsent k))
(displayOptional "precur" (displayNodes (kprecur k))
(displayOptional "gen-st" (displayTerms ctx (kgenSt k))
(displayOptional "conf" (displayTerms ctx (kconf k))
(displayOptional "auth" (displayTerms ctx (kauth k))
(displayOptional "facts" (displayFacts ctx (kfacts k))
(displayOptional "leads-to" (displayOrdering (nodePairsOfSkel k))
(displayOptional "priority" priorities
(kcomment k ++
(displayOptional "rule" (L.sort (map (S ()) (krules k)))
(displayOperation k ctx
(displayStrandMap k
(displayOptional "traces" traces rest))))))))))))))))))
where
priorities = map displayPriority (kpriority k)
traces = map (L () . displayTrace ctx . trace) (insts k)
{--
displayPOV :: Maybe Preskel -> [SExpr ()]
displayPOV Nothing = [S () "None"]
displayPOV (Just _) = [S () "Some"]
--}
displayFacts :: Context -> [Fact] -> [SExpr ()]
displayFacts ctx =
foldr
(\(Fact name fs) soFar ->
case name of
"trans" -> soFar
_ -> (L () (S () name : map (displayFterm ctx) fs)) : soFar)
[]
displayFact :: Context -> Fact -> SExpr ()
displayFact ctx (Fact name fs) =
L () (S () name : map (displayFterm ctx) fs)
displayFterm :: Context -> FTerm -> SExpr ()
displayFterm _ (FSid s) = N () s
displayFterm ctx (FTerm t) = displayTerm ctx t
displayPriority :: (Node, Int) -> SExpr ()
displayPriority (n, p) =
L () [displayNode n, N () p]
displayInst :: Context -> Instance -> SExpr ()
displayInst ctx s =
case listenerTerm s of
Just t -> L () [S () "deflistener", displayTerm ctx t]
Nothing ->
L () (S () "defstrand" :
S () (rname r) :
N () (height s) :
map (displayMaplet rctx ctx) maplets)
where
r = role s
domain = rvars r
maplets = L.sort (sansPtMaplets (reify domain (env s)))
rctx = varsContext domain
displayMaplet :: Context -> Context -> (Term, Term) -> SExpr ()
displayMaplet domain range (x, t)=
L () [displayTerm domain x, displayTerm range t]
displayOrdering :: [Pair] -> [SExpr ()]
displayOrdering orderings =
map displayPair (L.sort orderings)
displayPair :: Pair -> SExpr ()
displayPair (n0, n1) =
L () [displayNode n0, displayNode n1]
displayNode :: Node -> SExpr ()
displayNode (s, p) = L () [N () s, N () p]
displayNodes :: [Node] -> [SExpr ()]
displayNodes ns = map displayNode (L.sort ns)
-- Display the reason the preskeleton was created
displayOperation :: Preskel -> Context -> [SExpr ()] -> [SExpr ()]
displayOperation k ctx rest =
case operation k of
New -> rest
Contracted _ subst cause ->
let substitution = displaySubst ctx subst in
displayCause (L () (S () "contracted" : substitution)) cause
Displaced _ s s' role height cause ->
displayCause
(L () [S () "displaced", N () s, N () s', S () role, N () height])
cause
AddedStrand _ role height cause ->
displayCause
(L () [S () "added-strand", S () role, N () height]) cause
AddedListener _ t cause ->
displayCause
(L () [S () "added-listener", displayOpCmt ctx $ CM $ Plain t]) cause
AddedAbsence _ t1 t2 cause ->
displayCause (L () [S () "added-absence", displayOpCmt ctx $ TM t1,
displayOpCmt ctx $ TM t2]) cause
Generalized _ method ->
let desc = displayMethod ctx method in
L () (S () "operation" : S () "generalization" : desc) : rest
Collapsed _ s s' ->
let desc = [N () s, N () s'] in
L () (S () "operation" : S () "collapsed" : desc) : rest
AppliedRules _ -> L () (S () "operation" : [(S () "applied-rules")]) : rest
where
displayCause op (Cause dir node critical escape) =
L () (S () "operation" :
displayDirection dir :
op :
displayOpCmt ctx critical :
displayNode node :
displayOpCmts ctx (S.toList escape)) : rest
displayDirection Encryption = S () "encryption-test"
displayDirection Nonce = S () "nonce-test"
displayDirection Channel = S () "channel-test"
displayMethod _ (Deleted node) =
[S () "deleted", displayNode node]
displayMethod _ (Weakened (n0, n1)) =
[S () "weakened", L () [displayNode n0, displayNode n1] ]
displayMethod ctx (Separated t) =
[S () "separated", displayOpCmt ctx $ TM t]
displayMethod ctx (Forgot t) =
[S () "forgot", displayOpCmt ctx $ TM t]
-- Terms in the operation field may contain variables not in the skeleton
displayOpCmt :: Context -> CMT -> SExpr ()
displayOpCmt ctx cm = displayCmt (addToContext ctx $ cmtTerms cm) cm
displayOpCmts :: Context -> [CMT] -> [SExpr ()]
displayOpCmts ctx ts =
map (displayCmt $ addToContext ctx ts') (L.sort ts)
where
ts' = concatMap cmtTerms ts
displayCmt :: Context -> CMT -> SExpr ()
displayCmt ctx (CM (Plain t)) = displayTerm ctx t
displayCmt ctx (CM (ChMsg _ ch t)) =
L () [S () "ch-msg", displayTerm ctx ch, displayTerm ctx t]
displayCmt ctx (TM t) = displayTerm ctx t
-- Display the strand map
displayStrandMap :: Preskel -> [SExpr ()] -> [SExpr ()]
displayStrandMap k rest =
case getStrandMap $ operation k of
[] -> rest
sm -> L () (S () "strand-map" : map (N ()) sm) : rest