module Scyther.Facts (
module Scyther.Protocol
, module Scyther.Typing
, module Scyther.Message
, module Scyther.Event
, module Scyther.Formula
, Facts
, protocol
, empty
, freshTID
, freshAgentId
, quantifyTID
, quantifyAgentId
, conjoinAtoms
, setTyping
, nullFacts
, freeVariableMappings
, proveFacts
, proveFalse
, proveAtom
, proveFormula
, toAtoms
, nextTID
, nextAgentId
, quantifiedTIDs
, substEv
, threadRole
, eqsToMapping
, applyMapping
, oldestOpenMessages
, chainRuleFacts
, saturateFacts
, exploitTypingFacts
, exploitLongTermKeySecrecy
, splittableEqs
, splitEqFacts
, isaFacts
, sptFacts
) where
import Extension.Prelude
import Safe
import Data.List
import Data.Maybe
import Data.Monoid
import qualified Data.Set as S
import qualified Data.Map as M
import Data.Data
import Control.Arrow ( second, (***) )
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.State
import Text.Isar
import Scyther.Protocol
import Scyther.Typing
import Scyther.Message
import qualified Scyther.Equalities as E
import Scyther.Equalities hiding (solve, substTID, threadRole, substMVar, substAVar, substMsg, substAnyEq, empty)
import Scyther.Event hiding (substEv, substEvOrd)
import qualified Scyther.Event as E
import Scyther.Formula hiding (substAtom)
import qualified Scyther.Formula as F
data Facts = Facts {
events :: S.Set Event
, eventOrd :: EventOrder
, compromised :: S.Set Message
, uncompromised :: S.Set Message
, equalities :: E.Equalities
, tidQuantifiers :: S.Set TID
, aidQuantifiers :: S.Set AgentId
, optTyping :: Maybe Typing
, covered :: S.Set Message
, protocol :: Protocol
}
deriving( Eq, Ord, Show, Data, Typeable )
nullFacts :: Facts -> Bool
nullFacts facts =
S.null (events facts) &&
S.null (eventOrd facts) &&
S.null (compromised facts) &&
S.null (uncompromised facts) &&
E.null (equalities facts)
empty :: Protocol -> Facts
empty = Facts S.empty S.empty S.empty S.empty E.empty S.empty S.empty Nothing S.empty
setProtocol :: Monad m => Protocol -> Facts -> m Facts
setProtocol proto facts
| proto == protocol facts = return facts
| otherwise = fail $ "setProtocol: '" ++ show proto ++ "' /= '"
++ show (protocol facts) ++ "'"
setTyping :: Monad m => Typing -> Facts -> m Facts
setTyping typ facts = case optTyping facts of
Just typ' | typ /= typ' -> fail $ "setTyping: '" ++ show typ ++ "' /= '"
++ show typ' ++ "'"
_ -> return $ facts { optTyping = Just typ }
eqsToMapping :: Facts -> Mapping
eqsToMapping = Mapping . equalities
quantifyTID :: Monad m => TID -> Facts -> m Facts
quantifyTID tid facts
| tidQuantified facts tid = fail $ "quantifyTID: " ++ show tid ++ " already quantified."
| otherwise =
return $ facts { tidQuantifiers = S.insert tid $ tidQuantifiers facts }
quantifyAgentId :: Monad m => AgentId -> Facts -> m Facts
quantifyAgentId aid facts
| agentIdQuantified facts aid =
fail $ "quantifyAgentId: " ++ show aid ++ " already quantified."
| otherwise =
return $ facts { aidQuantifiers = S.insert aid $ aidQuantifiers facts }
freshTID :: Facts -> (TID, Facts)
freshTID facts =
(tid, facts { tidQuantifiers = S.insert tid $ tidQuantifiers facts })
where tid = nextTID facts
freshAgentId :: Facts -> (AgentId, Facts)
freshAgentId facts =
(aid, facts { aidQuantifiers = S.insert aid $ aidQuantifiers facts })
where aid = nextAgentId facts
quantifiedTIDs :: Facts -> [TID]
quantifiedTIDs = S.toList . tidQuantifiers
newtype Cert a = Cert { certified :: a }
deriving( Eq, Ord, Show )
mapCertified :: (a -> b) -> Cert a -> Cert b
mapCertified f (Cert x) = Cert (f x)
tidQuantified :: Facts -> TID -> Bool
tidQuantified facts = (`S.member` tidQuantifiers facts)
agentIdQuantified :: Facts -> AgentId -> Bool
agentIdQuantified facts = (`S.member` aidQuantifiers facts)
lidQuantified :: Facts -> LocalId -> Bool
lidQuantified facts = tidQuantified facts . lidTID
avarQuantified :: Facts -> AVar -> Bool
avarQuantified facts = lidQuantified facts . getAVar
mvarQuantified :: Facts -> MVar -> Bool
mvarQuantified facts = lidQuantified facts . getMVar
agentEqRHSQuantified :: Facts -> E.AgentEqRHS -> Bool
agentEqRHSQuantified facts = either (agentIdQuantified facts) (avarQuantified facts)
msgQuantified :: Facts -> Message -> Bool
msgQuantified facts m =
all (tidQuantified facts) (msgTIDs m) &&
all (agentIdQuantified facts) (msgAgentIds m)
evQuantified :: Facts -> Event -> Bool
evQuantified facts (Learn m) = msgQuantified facts m
evQuantified facts (Step tid _) = tidQuantified facts tid
evOrdQuantified :: Facts -> (Event, Event) -> Bool
evOrdQuantified facts (e1, e2) = evQuantified facts e1 && evQuantified facts e2
anyEqQuantified :: Facts -> E.AnyEq -> Bool
anyEqQuantified facts eq = case eq of
E.TIDEq (tid1, tid2) -> tidQuantified facts tid1 && tidQuantified facts tid2
E.TIDRoleEq (tid, _) -> tidQuantified facts tid
E.RoleEq _ -> True
E.AgentEq (aid, rhs) -> agentIdQuantified facts aid && agentEqRHSQuantified facts rhs
E.AVarEq (av1, av2) -> avarQuantified facts av1 && avarQuantified facts av2
E.MVarEq (mv, m) -> mvarQuantified facts mv && msgQuantified facts m
E.MsgEq (m1, m2) -> msgQuantified facts m1 && msgQuantified facts m2
atomQuantified :: Facts -> Atom -> Bool
atomQuantified facts atom = case atom of
AFalse -> True
AEq eq -> anyEqQuantified facts eq
AEv ev -> evQuantified facts ev
AEvOrd ord -> evOrdQuantified facts ord
ACompr m -> msgQuantified facts m
AUncompr m -> msgQuantified facts m
AHasType mv _ -> mvarQuantified facts mv
ATyping _ -> True
AReachable _ -> True
certify :: Show a => (Facts -> a -> Bool) -> (Facts -> a -> b) -> Facts -> a -> Cert b
certify check conv facts x
| check facts x = Cert $ conv facts x
| otherwise = error $ "certify: check failed for '" ++ show x ++ "'"
certMsg :: Facts -> Message -> Cert Message
certMsg = certify msgQuantified substMsg
certEvOrd :: Facts -> (Event, Event) -> Cert (Event, Event)
certEvOrd = certify evOrdQuantified substEvOrd
certAnyEq :: Facts -> E.AnyEq -> Cert E.AnyEq
certAnyEq = certify anyEqQuantified substAnyEq
certAtom :: Facts -> Atom -> Cert Atom
certAtom = certify atomQuantified substAtom
liftSubst :: (E.Equalities -> a -> b) -> Facts -> a -> b
liftSubst subst facts = subst (equalities facts)
substTID :: Facts -> TID -> TID
substTID = liftSubst E.substTID
substMVar :: Facts -> MVar -> Message
substMVar = liftSubst E.substMVar
substMsg :: Facts -> Message -> Message
substMsg = liftSubst E.substMsg
substAnyEq :: Facts -> E.AnyEq -> E.AnyEq
substAnyEq = liftSubst E.substAnyEq
substAtom :: Facts -> Atom -> Atom
substAtom = liftSubst F.substAtom
substEv :: Facts -> Event -> Event
substEv = liftSubst E.substEv
substEvOrd :: Facts -> (Event, Event) -> (Event, Event)
substEvOrd = liftSubst E.substEvOrd
threadRole :: TID -> Facts -> Maybe Role
threadRole tid = E.threadRole tid . equalities
trimQuantifiers :: Facts -> Facts
trimQuantifiers facts = facts {
equalities = eqs'
, tidQuantifiers = S.filter (`notElem` tids) $ tidQuantifiers facts
, aidQuantifiers = S.filter (`notElem` aids) $ aidQuantifiers facts
}
where
(tids, (aids, eqs')) = second E.trimAgentEqs . E.trimTIDEqs $ equalities facts
solve :: Monad m => [Cert E.AnyEq] -> Facts -> m Facts
solve ueqs facts = do
eqs <- E.solve (map certified ueqs) $ equalities facts
return . removeTrivialFacts $ facts {
events = S.map (E.substEv eqs) (events facts)
, eventOrd = S.map (E.substEvOrd eqs) (eventOrd facts)
, compromised = S.map (E.substMsg eqs) (compromised facts)
, uncompromised = S.map (E.substMsg eqs) (uncompromised facts)
, equalities = eqs
, tidQuantifiers = tidQuantifiers facts
, aidQuantifiers = aidQuantifiers facts
, covered = S.map (E.substMsg eqs) (covered facts)
}
compromise :: Message -> Facts -> Facts
compromise m facts =
facts { compromised = S.insert (certified m') (compromised facts) }
where m' = certMsg facts m
uncompromise :: Message -> Facts -> Facts
uncompromise m facts =
facts { uncompromised = S.insert (certified m') (uncompromised facts) }
where m' = certMsg facts m
insertEv :: Cert Event -> Facts -> Facts
insertEv ev prems = prems { events = S.insert (certified ev) (events prems) }
deleteEv :: Cert Event -> Facts -> Facts
deleteEv ev prems = prems { events = S.delete (certified ev) (events prems) }
insertLearn :: Cert Message -> Facts -> Facts
insertLearn m = insertEv (mapCertified Learn m)
insertEvOrd :: Cert (Event, Event) -> Facts -> Facts
insertEvOrd ord prems =
prems { eventOrd = S.insert (certified ord) (eventOrd prems) }
deleteEvOrd :: Cert (Event, Event) -> Facts -> Facts
deleteEvOrd ord prems =
prems { eventOrd = S.delete (certified ord) (eventOrd prems) }
insertRole :: TID -> Role -> Facts -> Facts
insertRole tid role facts = maybe err id $
solve [certAnyEq facts $ E.TIDRoleEq (tid, role)] facts
where
err = error $ "insertRole: failed to insert role"
conjoinAtoms :: Monad m => [Atom] -> Facts -> m (Maybe Facts)
conjoinAtoms atoms facts0 = foldM conjoinAtom (Just facts0) atoms
where
conjoinAtom Nothing _ = return Nothing
conjoinAtom (Just facts) atom = case certified $ certAtom facts atom of
AFalse -> return Nothing
AEq eq -> return $ solve [Cert eq] facts
AEv ev -> return . Just $ insertEvNonTrivial (Cert ev) facts
AEvOrd ord -> return . Just $ insertEvOrdNonTrivial (Cert ord) facts
ACompr m -> return . Just $ compromise m facts
AUncompr m -> return . Just $ uncompromise m facts
AReachable p -> Just `liftM` setProtocol p facts
ATyping typ -> Just `liftM` setTyping typ facts
_ -> error $ "conjoinAtoms: atom '" ++ show atom ++ "' not supported."
insertEvOrdAndEvs :: Cert (Event, Event) -> Facts -> Facts
insertEvOrdAndEvs ord =
insertEv (mapCertified fst ord) .
insertEv (mapCertified snd ord) . insertEvOrd ord
insertEvNonTrivial :: Cert Event -> Facts -> Facts
insertEvNonTrivial ev prems = case certified ev of
Learn m -> foldl' (flip (insertLearn . Cert)) prems (splitNonTrivial m)
Step _ _ -> insertEv ev prems
insertEvOrdNonTrivial :: Cert (Event, Event) -> Facts -> Facts
insertEvOrdNonTrivial ord prems = case certified ord of
(Learn m, to) -> foldl' (insertLearnBefore to) prems (splitNonTrivial m)
_ -> insertEvOrdAndEvs ord prems
where
insertLearnBefore to p m = insertEvOrdAndEvs (Cert (Learn m, to)) p
insertStepInputClosed :: Cert (TID, RoleStep) -> Facts -> Facts
insertStepInputClosed s prems = case certified s of
(tid, step@(Recv _ pt)) ->
let m = substMsg prems (inst tid pt) in
insertEvOrdNonTrivial (Cert (Learn m, Step tid step)) prems
(tid, step@(Send _ _)) -> insertEv (Cert (Step tid step)) prems
insertStepPrefixClosed :: Cert (TID, RoleStep) -> Facts -> Facts
insertStepPrefixClosed s = case certified s of
(tid, step) -> execState $ do
let err = error $ "insertStepPrefixClosed: no role assigned to thread " ++ show tid
role <- gets (fromMaybe err . threadRole tid)
let prefix = takeWhile (/= step) (roleSteps role) ++ [step]
insertStepOrd = modify . insertEvOrdAndEvs . Cert . (Step tid *** Step tid)
mapM_ (modify . insertStepInputClosed . (Cert . ((,) tid))) prefix
mapM_ insertStepOrd $ zip prefix (tail prefix)
insertEvSaturated :: Cert Event -> Facts -> Facts
insertEvSaturated ev = case certified ev of
(Learn _ ) -> insertEvNonTrivial ev
(Step tid step) -> insertStepPrefixClosed (Cert (tid, step))
removeTrivialFacts :: Facts -> Facts
removeTrivialFacts = execState $ do
evs <- S.toList <$> gets events
mapM_ checkEv evs
evord <- S.toList <$> gets eventOrd
mapM_ checkEvOrd evord
where
checkEv ev@(Learn m)
| trivial m = modify (insertEvNonTrivial (Cert ev) . deleteEv (Cert ev))
| otherwise = return ()
checkEv _ = return ()
checkEvOrd ord@(Learn m, _)
| trivial m = modify (insertEvOrdNonTrivial (Cert ord) . deleteEvOrd (Cert ord))
| otherwise = return ()
checkEvOrd _ = return ()
saturateFacts :: Facts -> Facts
saturateFacts = execState $ do
modify removeTrivialFacts
evs <- gets events
evord <- gets eventOrd
let evs' = (evs `S.union` S.map fst evord) `S.union` S.map snd evord
mapM_ (modify . insertEvSaturated . Cert) (S.toList evs')
exploitTypingFacts :: MonadPlus m => Facts -> m Facts
exploitTypingFacts facts0 = do
typ <- getTyping facts0
return $ case typ of
WeaklyAtomic -> foldl' weaklyAtomic facts0 . E.getMVarEqs . equalities $ facts0
Typing _ -> facts0
where
weaklyAtomic :: Facts -> (MVar, Message) -> Facts
weaklyAtomic facts (_, MMVar _ ) = facts
weaklyAtomic facts (_, MFresh _) = facts
weaklyAtomic facts (MVar (LocalId (i, tid)), m ) =
case threadRole tid facts of
Nothing -> error $ "exploitTypingFacts: no role assigned to '"++show tid++"'"
Just role ->
case find (S.member i . stepFMV) (roleSteps role) of
Nothing ->
error $ "exploitTypingFacts: variable '"++show i++"' does not occur in role."
Just step ->
insertEvOrdNonTrivial (Cert (Learn m, Step tid step)) facts
nextTID :: Facts -> TID
nextTID = maybe 0 (succ . fst) . S.maxView . tidQuantifiers
nextAgentId :: Facts -> AgentId
nextAgentId = maybe 0 (succ . fst) . S.maxView . aidQuantifiers
getTyping :: MonadPlus m => Facts -> m Typing
getTyping = maybe mzero return . optTyping
proveFalse :: Facts -> Bool
proveFalse prems =
not (S.null (compromised prems `S.intersection` uncompromised prems)) ||
any noAgent (S.toList (compromised prems)) ||
cyclic (eventOrd prems)
where
noAgent (MMVar _) = False
noAgent (MAVar _) = False
noAgent (MAgent _) = False
noAgent _ = True
proveAtom :: Facts -> Atom -> Bool
proveAtom facts = checkAtom . certified . certAtom facts
where
checkAtom atom = case atom of
AFalse -> False
AEq eq -> E.reflexive eq
AEv (Learn m) -> all checkLearn (splitNonTrivial m)
AEv ev -> ev `S.member` events facts
AEvOrd (Learn m, e2) -> all (checkLearnBefore e2) (splitNonTrivial m)
AEvOrd (e1, e2) -> before (eventOrd facts) e1 e2
ACompr m -> m `S.member` compromised facts
AUncompr m -> m `S.member` uncompromised facts
AHasType mv Nothing -> weaklyAtomic mv (substMVar facts mv)
AHasType mv (Just ty) -> checkType (substMVar facts mv) ty
ATyping typ -> Just typ == optTyping facts
AReachable proto -> proto == protocol facts
checkLearn m = Learn m `S.member` events facts
checkLearnBefore to m = before (eventOrd facts) (Learn m) to
weaklyAtomic mv (MMVar mv') = mv /= mv'
weaklyAtomic _ m = checkAtom (AEv (Learn m))
checkType (MAVar _) (AgentT) = True
checkType (MAgent _) (AgentT) = True
checkType (MConst i) (ConstT i') = i == i'
checkType (MFresh (Fresh (LocalId (i, tid)))) (NonceT role i') =
i == i' && threadRole tid facts == Just role
checkType (MHash m) (HashT ty) = checkType m ty
checkType (MEnc m1 m2) (EncT ty1 ty2) = checkType m1 ty1 && checkType m2 ty2
checkType (MTup m1 m2) (TupT ty1 ty2) = checkType m1 ty1 && checkType m2 ty2
checkType (MSymK m1 m2) (SymKT ty1 ty2) = checkType m1 ty1 && checkType m2 ty2
checkType (MAsymPK m) (AsymPKT ty) = checkType m ty
checkType (MAsymSK m) (AsymSKT ty) = checkType m ty
checkType m (KnownT step) = checkAtom (AEv (Learn m))
checkType m (SumT ty1 ty2) = checkType m ty1 || checkType m ty2
checkType _ _ = False
proveFormula :: Facts -> Formula -> Bool
proveFormula facts = prove (Mapping E.empty)
where
prove mapping (FAtom atom) = proveAtom facts (F.substAtom (getMappingEqs mapping) atom)
prove mapping (FConj f1 f2) = prove mapping f1 && prove mapping f2
prove mapping (FExists v f) = any (\mk -> prove (mk mapping) f) (mkMappings v)
mkMappings (Left tid) = map (E.addTIDMapping tid) (S.toList $ tidQuantifiers facts)
mkMappings (Right aid) = map (E.addAgentIdMapping aid) (S.toList $ aidQuantifiers facts)
exploitLongTermKeySecrecy :: Facts -> Maybe Message
exploitLongTermKeySecrecy facts = msum . map check . S.toList $ events facts
where
check (Learn key@(MSymK m1 m2)) = do
guard (all (`S.member` uncompromised facts) [m1, m2])
return key
check (Learn key@(MShrK m1 m2)) = do
guard (all (`S.member` uncompromised facts) [m1, m2])
return key
check (Learn key@(MAsymSK m)) = do
guard (m `S.member` uncompromised facts)
return key
check _ = mzero
toAtoms :: Facts -> [Atom]
toAtoms facts = mconcat [
AEq <$> E.toAnyEqs (equalities facts)
, AUncompr <$> S.toList (uncompromised facts)
, ACompr <$> S.toList (compromised facts)
, AEv <$> S.toList (events facts)
, AEvOrd <$> S.toList (eventOrd facts)
]
openMessages :: Facts -> [Message]
openMessages prems = nub $ filter okGoal $ catMaybes
[ case e of Learn m -> Just m; _ -> Nothing
| e <- S.toList $ events prems `S.difference` S.map snd (eventOrd prems) ]
where
okGoal (MMVar _) = False
okGoal (MAgent _) = False
okGoal (MAsymPK _) = False
okGoal (MInvKey _) = False
okGoal m = not (trivial m) && (m `S.notMember` covered prems)
oldestOpenMessages :: Facts -> [Message]
oldestOpenMessages prems =
map fst . sortOn snd . mapMaybe score $ ms
where
ms = openMessages prems
co = compromised prems
ltkLocalIds (MAsymSK m@(MAVar a))
| m `S.member` co = []
| otherwise = [getAVar a]
ltkLocalIds (MSymK ma@(MAVar a) mb@(MAVar b))
| ma `S.member` co || mb `S.member` co = []
| otherwise = [getAVar a, getAVar b]
ltkLocalIds (MShrK ma@(MAVar a) mb@(MAVar b))
| ma `S.member` co || mb `S.member` co = []
| otherwise = [getAVar a, getAVar b]
ltkLocalIds _ = []
score m = fmap (\x->(m,x)) . maximumMay $
[ tid | MVar (LocalId (_,tid)) <- msgFMV m ] ++
[ tid | Fresh (LocalId (_,tid)) <- msgFresh m ] ++
[ tid | LocalId (_,tid) <- ltkLocalIds m ]
data ChainRuleState = ChainRuleState
{ crsCaseName :: [String]
, crsNewVars :: [Either TID AgentId]
, crsFacts :: Facts
, crsFinalEq :: Maybe E.MsgEq
}
type ChainRuleM = StateT ChainRuleState []
addCaseFragment :: String -> ChainRuleM ()
addCaseFragment name = modify $ \crs -> crs { crsCaseName = crsCaseName crs ++ [name] }
addNewVar :: Either TID AgentId -> ChainRuleM ()
addNewVar v = modify $ \crs -> crs { crsNewVars = crsNewVars crs ++ [v] }
modifyFacts :: (Facts -> Facts) -> ChainRuleM ()
modifyFacts f = modify $ \crs -> crs { crsFacts = f $ crsFacts crs }
getsFacts :: (Facts -> a) -> ChainRuleM a
getsFacts f = gets (f . crsFacts)
setFinalEq :: E.MsgEq -> ChainRuleM ()
setFinalEq eq = modify $ \crs -> crs { crsFinalEq = Just eq }
unify :: Message -> Message -> ChainRuleM ()
unify m m' = do
crs <- get
maybe mzero (modifyFacts . const) $
solve [certAnyEq (crsFacts crs) $ E.MsgEq (m', m)] (crsFacts crs)
getFreshTID :: ChainRuleM TID
getFreshTID = do
(tid, facts) <- getsFacts freshTID
modifyFacts (const facts)
addNewVar (Left tid)
return tid
expandType :: Type -> ChainRuleM Message
expandType (AgentT) = do
(aid, facts) <- getsFacts freshAgentId
modifyFacts (const facts)
addNewVar (Right aid)
return $ MAgent aid
expandType (ConstT c) = return $ MConst c
expandType (NonceT role n) = do
nTid <- getFreshTID
modifyFacts (insertRole nTid role)
return $ MFresh (Fresh (LocalId (n, nTid)))
expandType (HashT ty) = MHash <$> expandType ty
expandType (EncT ty1 ty2) = MEnc <$> expandType ty1 <*> expandType ty2
expandType (TupT ty1 ty2) = MTup <$> expandType ty1 <*> expandType ty2
expandType (SymKT ty1 ty2) = MSymK <$> expandType ty1 <*> expandType ty2
expandType (AsymPKT ty) = MAsymPK <$> expandType ty
expandType (AsymSKT ty) = MAsymSK <$> expandType ty
expandType (SumT (KnownT _) ty) = expandType ty
expandType (KnownT _) = mzero
expandType ty = error $ "expandType: '" ++ ppTy ++ "' not supported"
where ppTy = show . render $ sptType Nothing ty
numberCases :: [ChainRuleState] -> [ChainRuleState]
numberCases cases = (`evalState` M.empty) . forM cases $ \ crs -> do
let name = concat . intersperse "_" . map head . group $ crsCaseName crs
counter <- get
let i = M.findWithDefault (0::Int) name counter
put $ M.insert name (succ i) counter
return $ crs {crsCaseName = return $ if i == 0 then name else name ++ "_" ++ show i}
extractCase :: [E.AnyEq] -> ChainRuleState -> Maybe ((String, [Either TID AgentId]), Facts)
extractCase delayedEqs0 crs = do
let facts0 = crsFacts crs
unmappedTID tid
| substTID facts0 tid == tid = return (Left tid)
| otherwise = mzero
newVars = concatMap (either unmappedTID (return . Right)) $ crsNewVars crs
delayedEqs = maybe [] (return . E.MsgEq) (crsFinalEq crs) ++ delayedEqs0
facts <- solve (map (certAnyEq facts0) delayedEqs) facts0
return ( (head $ crsCaseName crs, newVars)
, removeTrivialFacts . trimQuantifiers $ facts)
initialIntruderKnowledge :: Message -> ChainRuleM ()
initialIntruderKnowledge m = do
facts <- getsFacts id
case m of
MSymK a b -> do
addCaseFragment "ik0"
( (modifyFacts $ compromise a) `mplus` (modifyFacts $ compromise b) )
MShrK a b -> do
addCaseFragment "ik0"
( (modifyFacts $ compromise a) `mplus` (modifyFacts $ compromise b) )
MAsymSK a -> do
addCaseFragment "ik0"
modifyFacts $ compromise a
MHash m1 -> do
addCaseFragment "fake"
modifyFacts $ insertEvOrdNonTrivial (certEvOrd facts (Learn m1, Learn m))
MEnc m1 m2 -> do
addCaseFragment "fake"
modifyFacts
( insertEvOrdNonTrivial (certEvOrd facts (Learn m1, Learn m))
. insertEvOrdNonTrivial (certEvOrd facts (Learn m2, Learn m)))
MTup m1 m2 -> do
addCaseFragment "fake"
modifyFacts
( insertEvOrdNonTrivial (certEvOrd facts (Learn m1, Learn m))
. insertEvOrdNonTrivial (certEvOrd facts (Learn m2, Learn m)))
MFresh _ -> mzero
_ -> error $ "initialIntruderKnowledge: message not supported '" ++ show m ++ "'"
chainRuleFacts :: MonadPlus m => Message -> Facts -> m [((String, [Either TID AgentId]), Facts)]
chainRuleFacts (MAVar _ ) _ = error $ "chainRuleFacts: application to agent variables not supported."
chainRuleFacts (MConst _) _ = error $ "chainRuleFacts: application to global constants not supported."
chainRuleFacts (MInvKey _) _ = error $ "chainRuleFacts: application to symbolically inverted keys not supported."
chainRuleFacts (MAsymPK _) _ = error $ "chainRuleFacts: no support for public keys."
chainRuleFacts (MTup _ _) _ = error $ "chainRuleFacts: no support for tuples."
chainRuleFacts m facts0
| proveAtom facts0 (F.AEv (Learn m)) = assembleCases `liftM` getTyping facts0
| otherwise = error $ "chainRuleFacts: could not prove that '" ++ show m ++ "' is known to the intruder."
where
assembleCases typ =
mapMaybe (extractCase delayedEqs) . numberCases .
flip execStateT (ChainRuleState [] [] facts1 Nothing) $ (
initialIntruderKnowledge m
`mplus`
do tid <- getFreshTID
proto <- getsFacts protocol
msum $ map (roleChains typ tid) $ protoRoles proto
finalFacts <- gets crsFacts
guard (not $ proveFalse finalFacts)
)
where
facts1 = facts0 { equalities = E.empty
, covered = S.insert m $ covered facts0 }
delayedEqs = E.toAnyEqs $ equalities facts0
insertPrevious :: [Event] -> Event -> ChainRuleM ()
insertPrevious prev ev = modifyFacts $
\facts -> foldl' insertSingle facts prev
where
insertSingle p prevEv = insertEvOrdNonTrivial (certEvOrd p (prevEv, ev)) p
roleChains :: Typing -> TID -> Role -> ChainRuleM ()
roleChains genTyp tid role = do
modifyFacts $ insertRole tid role
addCaseFragment $ roleName role
msum . map stepChains $ roleSteps role
where
stepChains :: RoleStep -> ChainRuleM ()
stepChains (Recv _ _) = mzero
stepChains step@(Send _ pt) = do
modifyFacts $ insertStepPrefixClosed (Cert (tid, step))
addCaseFragment $ stepLabel step
msgChains [(Step tid step)] (inst tid pt)
where
msgName (MConst i) = getId i
msgName (MFresh fr) = lidName . getFresh $ fr
msgName (MAVar av) = lidName . getAVar $ av
msgName (MMVar mv) = lidName . getMVar $ mv
msgName (MHash _) = "hash"
msgName (MEnc _ _) = "enc"
msgName (MTup _ _) = "tup"
msgName (MSymK _ _) = "K_ud"
msgName (MShrK _ _) = "K_bd"
msgName (MAsymPK _) = "pk"
msgName (MAsymSK _) = "sk"
msgName (MAgent _) = "someAgent"
msgName (MInvKey _) = "invKey"
lidName = getId . fst . getLocalId
msgChains :: [Event] -> Message -> ChainRuleM ()
msgChains _ (MAVar _) = mzero
msgChains _ (MAgent _) = mzero
msgChains _ (MConst _) = mzero
msgChains prev v@(MMVar mv) = do
addCaseFragment $ msgName v
case genTyp of
WeaklyAtomic -> do
case m of MMVar _ -> return (); MFresh _ -> return (); _ -> mzero
insertPrevious prev (Learn v)
setFinalEq (v, m)
Typing typ ->
case M.lookup (lidId $ getMVar mv, role) typ of
Nothing -> error $ "msgChains: no type provided for '"++show mv++"'"
Just vty -> do
vm <- expandType vty
unify v vm
msgChains prev vm
msgChains prev m'@(MEnc m1 m2) =
do insertPrevious prev (Learn m')
( do
addCaseFragment $ msgName m'
setFinalEq (m', m)
`mplus`
msgChains [Learn m', Learn (MInvKey m2)] m1 )
msgChains prev (MTup m1 m2) = msgChains prev m1 `mplus` msgChains prev m2
msgChains prev m'@(MFresh _) = do
insertPrevious prev (Learn m')
addCaseFragment $ msgName m'
unify m' m
msgChains prev m' = do
insertPrevious prev (Learn m')
addCaseFragment $ msgName m'
setFinalEq (m', m)
splittableEqs :: Facts -> [MsgEq]
splittableEqs facts =
do eq@(MShrK _ _, MShrK _ _) <- getPostEqs $ equalities facts
guard (not $ uncurry (==) eq)
return eq
splitEqFacts :: MsgEq -> Facts -> [Maybe Facts]
splitEqFacts (MShrK a b, MShrK x y) facts =
[ addEqs [MsgEq (a,x), MsgEq (b,y)]
, addEqs [MsgEq (b,x), MsgEq (a,y)]
]
where
addEqs eqs = solve (map (certAnyEq facts) eqs) facts
splitEqFacts eq _ =
error $ "splitEqFacts: cannot split equality '" ++ show eq ++ "'"
proveFacts :: Facts
-> Facts
-> Mapping
-> Bool
proveFacts prems concl mapping =
all (proveAtom prems . F.substAtom (getMappingEqs mapping)) (toAtoms concl)
freeVariableMappings :: Facts -> Facts -> [Mapping]
freeVariableMappings from to = do
mapping <- quantifierMappings
return mapping
where
quantifierMappings = do
tideqs <- foldM mkTIDMapping M.empty . S.toList $ tidQuantifiers from
agnteqs <- foldM mkAgentIdMapping M.empty . S.toList $ aidQuantifiers from
return $ E.mkMapping tideqs agnteqs
mkTIDMapping eqs tidF = do
tidT <- msum . map return . S.toList $ tidQuantifiers to
return $ M.insert tidF tidT eqs
mkAgentIdMapping eqs aidF = do
aidT <- msum . map return . S.toList $ aidQuantifiers to
return $ M.insert aidF aidT eqs
applyMapping :: Mapping -> Facts -> Facts
applyMapping mapping facts0 = case newFacts of
Just (Just facts) -> facts
_ -> error "applyMapping: failed to reconstruct facts after mapping"
where
p = protocol facts0
newFacts = addAtoms =<< quantifyAIDs =<< quantifyTIDs (empty p)
eqs = getMappingEqs mapping
qTID = flip (quantifyTID . E.substTID eqs)
qAID = flip (quantifyAgentId . either id err . E.substAgentId eqs)
err = error "applyMapping: mapping does not map agent ids to agent ids"
quantifyTIDs facts = foldM qTID facts $ S.toList $ tidQuantifiers facts0
quantifyAIDs facts = foldM qAID facts $ S.toList $ aidQuantifiers facts0
addAtoms = conjoinAtoms atoms
atoms = map (F.substAtom (getMappingEqs mapping)) . toAtoms $ facts0
isReprEq :: E.AnyEq -> Bool
isReprEq (TIDEq _) = False
isReprEq (AgentEq _) = False
isReprEq _ = True
ppSet :: (a -> b) -> S.Set a -> [b]
ppSet ppElem = map ppElem . S.toList
isaFacts :: IsarConf -> Facts
-> ([Doc],[Doc],[Doc])
isaFacts conf facts =
( ppSet (isar conf) (tidQuantifiers facts) ++
ppSet (isar conf) (aidQuantifiers facts)
, map (isar conf) reprEqs ++
ppSet (isaUncompr conf) (uncompromised facts) ++
ppSet (isaCompr conf) (compromised facts) ++
ppSet (isaEventOrd conf (Mapping eqs)) (eventOrd facts) ++
ppSet (isaEvent conf (Mapping eqs)) (events facts)
, map (isar conf) nonReprEqs
)
where
eqs = equalities facts
(reprEqs, nonReprEqs) = partition isReprEq $ E.toAnyEqs eqs
sptFacts :: Facts
-> ([Doc],[Doc],[Doc])
sptFacts facts =
( ppSet sptTID (tidQuantifiers facts) ++
ppSet sptAgentId (aidQuantifiers facts)
, map sptAnyEq reprEqs ++
ppComprInfo "uncompromised" (uncompromised facts) ++
ppComprInfo "compromised" (compromised facts) ++
(map (sptEventOrd (Mapping eqs)) $ transitiveChains $ S.toList $ eventOrd facts) ++
ppSet (sptEvent (Mapping eqs)) (events facts)
, map sptAnyEq nonReprEqs ++
(map ppCovered $ S.toList $ covered facts)
)
where
eqs = equalities facts
(reprEqs, nonReprEqs) = partition isReprEq $ E.toAnyEqs eqs
ppCovered m = text "covered" <> parens (sptMessage m)
ppComprInfo setName set
| S.null set = mzero
| otherwise = return . fsep $
(text setName <> lparen : (map (nest 2) . punctuate comma)
(ppSet sptMessage set)) ++ [rparen]
transitiveChains :: Ord a => [(a,a)] -> [[a]]
transitiveChains = sortOn head . foldl' insertEdge []
where
findChain sel x cs = case break ((x ==) . sel) cs of
(_,[]) -> (cs, [x])
(cs1, c:cs2) -> (cs1 ++ cs2, c)
insertEdge chains0 (from,to) =
let (chains1, prefix) = findChain last from chains0
(chains2, suffix) = findChain head to chains1
in (prefix ++ suffix) : chains2