scyther-proof-0.4.0: src/Scyther/Facts.hs
{-# LANGUAGE CPP, FlexibleContexts, DeriveDataTypeable #-}
-- | Conjunctions of the logical facts needed during a proof using decryption chain reasoning.
module Scyther.Facts (
module Scyther.Protocol
, module Scyther.Typing
, module Scyther.Message
, module Scyther.Event
, module Scyther.Formula
-- * Facts
, Facts
, protocol
-- ** Construction
, empty
, freshTID
, freshArbMsgId
, quantifyTID
, quantifyArbMsgId
, conjoinAtoms
, setTyping
-- ** Queries
, nullFacts
, freeVariableMappings
, proveFacts
, proveFalse
, proveAtom
, proveFormula
, toAtoms
, nextTID
, nextArbMsgId
, quantifiedTIDs
-- ** Substitution under the equalities of the facts
, substEv
, threadRole
, eqsToMapping
, applyMapping
-- ** Rule applications
, oldestOpenMessages
, chainRuleFacts
, saturateFacts
, exploitTypingFacts
, exploitLongTermKeySecrecy
, splittableEqs
, splitEqFacts
-- * Output
, isaFacts
, sptFacts
) where
import Debug.Trace
import Extension.Prelude
import Safe
import Data.List
import Data.Maybe
-- workaround new Monoid operator <>
#if __GLASGOW_HASKELL__ < 704
import Data.Monoid
#else
import Data.Monoid hiding ((<>))
#endif
import Data.Foldable (foldMap)
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.Message
import qualified Scyther.Typing as T
import Scyther.Typing hiding (substTypeAnn)
import qualified Scyther.Equalities as E
import Scyther.Equalities hiding (solve, substTID, threadRole, substMVar, substAVar, substMsg, substAnyEq, substAMID, empty, null)
import Scyther.Event hiding (substEv, substEvOrd)
import qualified Scyther.Event as E
import Scyther.Formula hiding (substAtom)
import qualified Scyther.Formula as F
-- | A convenient abbreviation for `mappend`.
(><) :: Monoid m => m -> m -> m
(><) = mappend
------------------------------------------------------------------------------
-- Facts
------------------------------------------------------------------------------
-- | A conjunction of logical facts.
--
-- Invariants that hold for a value @facts = Facts _ evs evord co uc eqs@:
--
-- 1. All facts are invariant under their corresponding substitution. This
-- excludes the quantifiers, as they are no facts.
--
-- 2. All trivial learn events are removed (or split in case of a pair).
--
-- 3. All arbitrary messages are annotated with a type.
--
-- We assume that all thread identifiers that are assigned to a role are
-- locally quantified. The kind of quantification depends on the context. If
-- the set of facts models the premises of a proof state then this would be
-- universal quantification. If the set of facts models an authentication
-- conclusion this would be existential quantification.
--
data Facts = Facts {
events :: S.Set Event -- ^ Statements about events that must have happened.
, eventOrd :: EventOrder -- ^ Statements about the order of events that happened.
, compromised :: S.Set Message -- ^ Statements about agents being compromised.
, uncompromised :: S.Set Message -- ^ Statements about agents being uncompromised.
, equalities :: E.Equalities -- ^ All equalities that must hold.
, tidQuantifiers :: S.Set TID -- ^ All thread IDs occurring in the facts.
, amQuantifiers :: S.Set ArbMsgId -- ^ All arbitrary-message IDs ocurring in the facts.
, optTyping :: Maybe Typing -- ^ The typing if there is any that the
-- current state satisfies.
-- NOTE: The Maybe is used for facts that don't have a typing.
, typeAnns :: S.Set TypeAnn -- ^ Type annotations on messages.
, covered :: S.Set Message -- ^ The messages that have already been used in a
-- case distinction.
, protocol :: Protocol -- ^ The protocol that the current state
-- is a reachable state of.
}
deriving( Eq, Ord, Show, Data, Typeable )
------------------------------------------------------------------------------
-- Queries
------------------------------------------------------------------------------
-- | True if no premises apart from state reachability and the optional
-- well-typedness claim are present. Note that there may be quantifiers and
-- covered goals.
nullFacts :: Facts -> Bool
nullFacts facts =
S.null (events facts) &&
S.null (eventOrd facts) &&
S.null (compromised facts) &&
S.null (uncompromised facts) &&
S.null (typeAnns facts) &&
E.null (equalities facts)
------------------------------------------------------------------------------
-- Construction
------------------------------------------------------------------------------
-- | Empty set of facts; logically equivalent to true.
empty :: Protocol -> Facts
empty = Facts S.empty S.empty S.empty S.empty E.empty S.empty S.empty Nothing S.empty S.empty
-- | Set the protocol.
--
-- PRE: Setting a protocol is the identity iff the new protocol agrees with the
-- existing one.
--
-- Uses 'fail' for error reporting.
setProtocol :: Monad m => Protocol -> Facts -> m Facts
setProtocol proto facts
| proto == protocol facts = return facts
| otherwise = fail $ "setProtocol: '" ++ show proto ++ "' /= '"
++ show (protocol facts) ++ "'"
-- | Set the typing.
--
-- PRE: There mustn't be a different existing typing.
--
-- Uses 'fail' for error reporting.
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 }
-- | Create a mapping from the equalities of the facts.
eqsToMapping :: Facts -> Mapping
eqsToMapping = Mapping . equalities
-- Quantifiers
--------------
-- | Tries to quantify the given thread identifier. If it is already quantified
-- `fail` is called in the given monad.
quantifyTID :: Monad m => TID -> Facts -> m Facts
quantifyTID tid facts
| null (tidQuantified facts tid) =
fail $ "quantifyTID: " ++ show tid ++ " already quantified."
| otherwise =
return $ facts { tidQuantifiers = S.insert tid $ tidQuantifiers facts }
-- | Tries to quantify the given agent identifier. If it is already quantified
-- `fail` is called in the given monad.
quantifyArbMsgId :: Monad m => ArbMsgId -> Facts -> m Facts
quantifyArbMsgId aid facts
| null (arbMsgIdQuantified facts aid) =
fail $ "quantifyArbMsgId: " ++ show aid ++ " already quantified."
| otherwise =
return $ facts { amQuantifiers = S.insert aid $ amQuantifiers facts }
-- | Get a fresh TID and the updated set of facts.
freshTID :: Facts -> (TID, Facts)
freshTID facts =
(tid, facts { tidQuantifiers = S.insert tid $ tidQuantifiers facts })
where tid = nextTID facts
-- | Get a fresh ArbMsgId and the updated set of facts.
freshArbMsgId :: Facts -> (ArbMsgId, Facts)
freshArbMsgId facts =
(aid, facts { amQuantifiers = S.insert aid $ amQuantifiers facts })
where aid = nextArbMsgId facts
-- | The list of thread ids that are quantified.
quantifiedTIDs :: Facts -> [TID]
quantifiedTIDs = S.toList . tidQuantifiers
-- Certification
----------------
-- | A value certified to be satisfy. This is a type level construct
-- helping the implementor to discern between values from the outside and
-- values with their invariants checked.
--
-- What is missing is the binding between the context and the checked value. It
-- is up to the user to not mix this up.
newtype Cert a = Cert { certified :: a }
deriving( Eq, Ord, Show )
-- | The results denotes the list of certification errors. If it is empty, then
-- certification succeeded.
type CertResult = [String]
-- | The successful certification result.
certSuccess :: CertResult
certSuccess = []
-- | Conditionally return a certification error.
certErrorIf :: Bool -> String -> CertResult
certErrorIf True msg = [msg]
certErrorIf False _ = certSuccess
-- | Changed the certified value. Note that you have to guarantee that the
-- required invariants are not violated.
mapCertified :: (a -> b) -> Cert a -> Cert b
mapCertified f (Cert x) = Cert (f x)
-- | Check if a TID is quantified in these facts
tidQuantified :: Facts -> TID -> CertResult
tidQuantified facts tid =
certErrorIf (tid `S.notMember` tidQuantifiers facts) $
"unquantified tid: " ++ show tid
-- | Check if a agent id is quantified in these facts
arbMsgIdQuantified :: Facts -> ArbMsgId -> CertResult
arbMsgIdQuantified facts aid =
certErrorIf (aid `S.notMember` amQuantifiers facts) $
"unquantified aid: " ++ show aid
-- | Check if all logical variables in an local id are quantified.
lidQuantified :: Facts -> LocalId -> CertResult
lidQuantified facts = tidQuantified facts . lidTID
-- | Check if all logical variables in an agent variable are quantified.
avarQuantified :: Facts -> AVar -> CertResult
avarQuantified facts = lidQuantified facts . getAVar
-- | Check if all logical variables in an message variable are quantified.
mvarQuantified :: Facts -> MVar -> CertResult
mvarQuantified facts = lidQuantified facts . getMVar
-- | Check if all logical variables in an message are quantified.
msgQuantified :: Facts -> Message -> CertResult
msgQuantified facts m =
foldMap (tidQuantified facts) (msgTIDs m) ><
foldMap (arbMsgIdQuantified facts) (msgAMIDs m)
-- | Check if all logical variables in an event are quantified.
evQuantified :: Facts -> Event -> CertResult
evQuantified facts (Learn m) = msgQuantified facts m
evQuantified facts (Step tid _) = tidQuantified facts tid
-- | Check if all logical variables in an event order are quantified.
evOrdQuantified :: Facts -> (Event, Event) -> CertResult
evOrdQuantified facts (e1, e2) = evQuantified facts e1 >< evQuantified facts e2
-- | Check if all logical variables in a type annotation are quantified.
typeAnnQuantified :: Facts -> TypeAnn -> CertResult
typeAnnQuantified facts (m, _, tid) =
msgQuantified facts m >< tidQuantified facts tid
-- | Check if an equality contains only quantified logical variables.
anyEqQuantified :: Facts -> E.AnyEq -> CertResult
anyEqQuantified facts eq = case eq of
E.TIDEq (tid1, tid2) -> tidQuantified facts tid1 >< tidQuantified facts tid2
E.TIDRoleEq (tid, _) -> tidQuantified facts tid
E.RoleEq _ -> certSuccess
E.ArbMsgEq (aid, rhs) -> arbMsgIdQuantified facts aid >< msgQuantified 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
-- | Check if an atom contains only quantified logical variables.
atomQuantified :: Facts -> Atom -> CertResult
atomQuantified facts atom = case atom of
AFalse -> certSuccess
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 tya -> typeAnnQuantified facts tya
ATyping _ -> certSuccess
AReachable _ -> certSuccess
-- | Certification of a value with respect to a check and a morphism required
-- to establish the required invariants in the context of a set of facts.
certify :: Show a => (Facts -> a -> CertResult) -> (Facts -> a -> b)
-> Facts -> a -> Cert b
certify check conv facts x =
case check facts x of
[] -> x'
-- FIXME: Somehow bidirectional shared keys lead in some cases to an
-- unquantified thread identifier error. However, all of these cases
-- dealt with proofs that failed (i.e., attackable security
-- properties). Therfore, we have not yet debugged this to its full
-- extent.
errs -> trace
(unlines $
("warning: internal check failed for '" ++ show x ++ "' because of") :
(map (" "++) $ errs)
)
x'
where
x' = Cert $ conv facts x
-- | Certify a message.
certMsg :: Facts -> Message -> Cert Message
certMsg = certify msgQuantified substMsg
-- | Certify an event.
-- certEv :: Facts -> Event -> Cert Event
-- certEv = certify evQuantified substEv
-- | Certify an event order.
certEvOrd :: Facts -> (Event, Event) -> Cert (Event, Event)
certEvOrd = certify evOrdQuantified substEvOrd
-- | Certify an equality.
certAnyEq :: Facts -> E.AnyEq -> Cert E.AnyEq
certAnyEq = certify anyEqQuantified substAnyEq
-- | Certify an atom: All logical variables are quantified under the given
-- facts and all values are invariant under the equalities associated with the
-- facts.
certAtom :: Facts -> Atom -> Cert Atom
certAtom = certify atomQuantified substAtom
-- | Certify an a type annotation.
certTypeAnn :: Facts -> TypeAnn -> Cert TypeAnn
certTypeAnn = certify typeAnnQuantified substTypeAnn
-- Equalities
-------------
-- | Lift a substitutition.
liftSubst :: (E.Equalities -> a -> b) -> Facts -> a -> b
liftSubst subst facts = subst (equalities facts)
-- | Substitute a TID.
substTID :: Facts -> TID -> TID
substTID = liftSubst E.substTID
-- TODO: Remove if not used anymore.
-- | Substitute an agent variale.
-- substAVar :: Facts -> AVar -> AVar
-- substAVar = liftSubst E.substAVar
-- | Substitute an message variale.
-- substMVar :: Facts -> MVar -> Message
-- substMVar = liftSubst E.substMVar
-- | Substitute an message variale.
substAMID :: Facts -> ArbMsgId -> Message
substAMID = liftSubst E.substAMID
-- | Substitute an message variale.
-- substArbMsgEqRHS :: Facts -> E.ArbMsgEqRHS -> E.ArbMsgEqRHS
-- substArbMsgEqRHS = liftSubst E.substArbMsgEqRHS
-- | Substitute a message.
substMsg :: Facts -> Message -> Message
substMsg = liftSubst E.substMsg
-- | Substitute an equality.
substAnyEq :: Facts -> E.AnyEq -> E.AnyEq
substAnyEq = liftSubst E.substAnyEq
-- | Substitute an atom.
substAtom :: Facts -> Atom -> Atom
substAtom = liftSubst F.substAtom
-- | Substitute an event.
substEv :: Facts -> Event -> Event
substEv = liftSubst E.substEv
-- | Substitute an event order.
substEvOrd :: Facts -> (Event, Event) -> (Event, Event)
substEvOrd = liftSubst E.substEvOrd
-- | Substitute a type annotation.
substTypeAnn :: Facts -> TypeAnn -> TypeAnn
substTypeAnn = liftSubst T.substTypeAnn
-- | The role assigned to a thread.
threadRole :: TID -> Facts -> Maybe Role
threadRole tid = E.threadRole tid . equalities
-- | Remove thread identifier and agent identifiers equalities and the
-- quantifiers that were mapped by them.
--
-- This operation is logically safe iff there are no references to the mapped
-- logical variables outside the facts.
trimQuantifiers :: Facts -> Facts
trimQuantifiers facts = facts {
equalities = eqs'
, tidQuantifiers = S.filter (`notElem` tids) $ tidQuantifiers facts
, amQuantifiers = S.filter (`notElem` aids) $ amQuantifiers facts
}
where
(tids, (aids, eqs')) = second E.trimArbMsgEqs . E.trimTIDEqs $ equalities facts
-- | Solve the equations in the context of the given facts and update all facts
-- accordingly.
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
, amQuantifiers = amQuantifiers facts
, typeAnns = S.map (T.substTypeAnn eqs) (typeAnns facts)
, covered = S.map (E.substMsg eqs) (covered facts)
}
-- Compromised agents
---------------------
-- | Mark an message as being a compromised agent name.
compromise :: Message -> Facts -> Facts
compromise m facts =
facts { compromised = S.insert (certified m') (compromised facts) }
where m' = certMsg facts m
-- | Mark an message as not being a compromised agent name.
uncompromise :: Message -> Facts -> Facts
uncompromise m facts =
facts { uncompromised = S.insert (certified m') (uncompromised facts) }
where m' = certMsg facts m
-- Incremental construction
---------------------------
-- | Inserts an event fact.
insertEv :: Cert Event -> Facts -> Facts
insertEv ev prems = prems { events = S.insert (certified ev) (events prems) }
-- | Delete an event fact.
deleteEv :: Cert Event -> Facts -> Facts
deleteEv ev prems = prems { events = S.delete (certified ev) (events prems) }
-- | Insert a learn event fact.
insertLearn :: Cert Message -> Facts -> Facts
insertLearn m = insertEv (mapCertified Learn m)
-- | Inserts an event order fact.
insertEvOrd :: Cert (Event, Event) -> Facts -> Facts
insertEvOrd ord prems =
prems { eventOrd = S.insert (certified ord) (eventOrd prems) }
-- | Delete an event order fact.
deleteEvOrd :: Cert (Event, Event) -> Facts -> Facts
deleteEvOrd ord prems =
prems { eventOrd = S.delete (certified ord) (eventOrd prems) }
-- | Insert a thread identifier to role assignment. This will fail with
-- an error iff this assignment conflicts with an existing assignment of
-- the same thread identifier to a different role.
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"
-- | Annotate a message with a type interpreted with respect to a specific
-- thread.
insertTypeAnn:: Cert TypeAnn -> Facts -> Facts
insertTypeAnn tya prems =
prems { typeAnns = S.insert (certified tya) (typeAnns prems) }
-- | Build the conjunction of the atoms and the facts; a result of 'Nothing'
-- means that the conjunction is logically equivalent to False. This will occur
-- in case 'AFalse' is conjoined or an equality that cannot be unified.
--
-- PRE: The atom must pass certification under the given facts.
--
-- PRE: The atom must not be a 'AHasTyp' or a 'ATyping' atom, as they are not
-- representable by 'Facts'
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
-- FIXME: repeated calls to solve may be a bit expensive due to duplicated
-- work of 'removeTrivialFacts'.
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
AHasType tya -> return . Just $ insertTypeAnn (Cert tya) facts
-- Combined construction and application of inference rules
-----------------------------------------------------------
-- | Inserts an event order fact and both event facts implied by the presence
-- of this event oder fact.
insertEvOrdAndEvs :: Cert (Event, Event) -> Facts -> Facts
insertEvOrdAndEvs ord =
insertEv (mapCertified fst ord) .
insertEv (mapCertified snd ord) . insertEvOrd ord
-- | Insert all non-trivial events implied by the given event.
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
-- | Insert all event orders which are non-trivial in their first argument
-- implied by the given event order.
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
-- | Insert an executed role step and all non-trivial facts implied by the
-- Input rule.
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
-- | Insert an executed role step and all non-trivial facts implied by the
-- Input and Role rules.
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)
-- | Insert an event an all non-trivial facts implied by the Input and Role
-- rules.
insertEvSaturated :: Cert Event -> Facts -> Facts
insertEvSaturated ev = case certified ev of
(Learn _ ) -> insertEvNonTrivial ev
(Step tid step) -> insertStepPrefixClosed (Cert (tid, step))
-- | Derive all non-trivial facts implied by the splitting rules and remove
-- remove trivial facts.
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 ()
-- | Saturate facts modulo removal of trivial facts; i.e. apply all rules
-- except the chain rule eagerly and remove trivial facts.
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')
-- | Make use of the typing assumption by checking for instantiated message variables
-- if their instantiation does not agree with the structural type and hence they must
-- be known before the given step.
--
-- Is equal to 'mzero' in case the facts don't contain a typing.
exploitTypingFacts :: MonadPlus m => Facts -> m Facts
exploitTypingFacts facts0 = return facts0 -- TODO: implement this check.
{- cf. the one for weak atomicity below:
do
-- WeaklyAtomic -> foldl' weaklyAtomic facts0 . E.getMVarEqs . equalities $ 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
-}
------------------------------------------------------------------------------
-- Queries
------------------------------------------------------------------------------
-- | The next free thread identifier
nextTID :: Facts -> TID
nextTID = maybe 0 (succ . fst) . S.maxView . tidQuantifiers
-- | The next free agent identifier
nextArbMsgId :: Facts -> ArbMsgId
nextArbMsgId = maybe 0 (succ . fst) . S.maxView . amQuantifiers
-- | Try to retrieve the typing; equal to 'mzero' if there is none.
getTyping :: MonadPlus m => Facts -> m Typing
getTyping = maybe mzero return . optTyping
-- | Check if a set of facts is trivially contradictory.
--
-- NOTE: This is not the same as trying to prove the atom AFalse under these
-- premises. The checks are separated due to efficiency reasons.
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 (MArbMsg _) = False
noAgent _ = True
-- | True iff the facts imply the validity of the given atom. Note that this check
-- is incomplete; i.e. there may be atoms that would be true under these facts,
-- but are not detected as such.
--
-- PRE: Trivial learn events must be split. You may achieve this using
-- 'removeTrivialFacts'.
proveAtom :: Facts -> Atom -> Bool
proveAtom facts = checkAtom . certified . certAtom facts
where
-- PRE: atom is fully substituted
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 tya -> hasType tya
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
hasType (m0, ty0, tid0) =
go m0 ty0
where
go (MAVar _) (AgentT) = True
go (MConst i) (ConstT i') = i == i'
go (MFresh (Fresh (LocalId (i, tid)))) (NonceT role i') =
i == i' && threadRole tid facts == Just role
go (MHash m) (HashT ty) = go m ty
go (MEnc m1 m2) (EncT ty1 ty2) = go m1 ty1 && go m2 ty2
go (MTup m1 m2) (TupT ty1 ty2) = go m1 ty1 && go m2 ty2
go (MSymK m1 m2) (SymKT ty1 ty2) = go m1 ty1 && go m2 ty2
go (MAsymPK m) (AsymPKT ty) = go m ty
go (MAsymSK m) (AsymSKT ty) = go m ty
go m (KnownT step) = checkAtom (AEvOrd (Learn m, Step tid0 step))
go m (SumT ty1 ty2) = go m ty1 || go m ty2
go m ty = or $ do
(m', ty', tid') <- S.toList $ typeAnns facts
guard (m == m')
return $ (ty', tid') `subType` (ty, tid0)
-- ty `subType` ty' holds iff every instance of ty is also an instance of ty'.
subType (ty0, tid) (ty'0, tid') =
go ty0 ty'0
where
go (EncT ty1 ty2) (EncT ty'1 ty'2) = go ty1 ty'1 && go ty2 ty'2
go (TupT ty1 ty2) (TupT ty'1 ty'2) = go ty1 ty'1 && go ty2 ty'2
go (SymKT ty1 ty2) (SymKT ty'1 ty'2) = go ty1 ty'1 && go ty2 ty'2
go (AsymPKT ty) (AsymPKT ty') = go ty ty'
go (AsymSKT ty) (AsymSKT ty') = go ty ty'
-- NOTE: SumT handling results in an under-approximation for nested
-- SumTs. The left-hand SumTs should be pushed outwards first; such
-- that they are taken apart before the right-hand SumTs.
go (SumT ty1 ty2) ty' = go ty1 ty' && go ty2 ty'
go ty (SumT ty'1 ty'2) = go ty ty'1 || go ty ty'2
go (KnownT step) (KnownT step') =
-- every message before step is also before step'
checkAtom (AEvOrd (Step tid step, Step tid' step'))
go ty ty' = ty == ty'
-- | Try to prove that the formula holds under these facts.
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)
-- the mappings assign witnesses to the existentially quantified variables.
mkMappings (Left tid) = map (E.addTIDMapping tid) (S.toList $ tidQuantifiers facts)
mkMappings (Right aid) = map (E.addArbMsgIdMapping aid) (S.toList $ amQuantifiers facts)
-- | Try to find a long-term-key that must be secret due to the
-- uncompromisedness assumptions, but is claimed to be known to the intruder;
-- i.e. if this method returns a message, then the premises are contradictory.
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
-- Deconstruction
-----------------
-- | Represent the facts as a set of atoms.
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)
, AHasType <$> S.toList (typeAnns facts)
]
------------------------------------------------------------------------------
-- Chain Rule Application
------------------------------------------------------------------------------
-- | Compute the set of messages that have no given previous event.
--
-- PRE: Assumes all events in the event order are also part of the
-- set of events.
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 (MArbMsg _) = False
okGoal (MAsymPK _) = False
okGoal (MInvKey _) = False
okGoal m = not (trivial m) && (m `S.notMember` covered prems)
-- | Sort open messages ascending with respect to the maximal thread id.
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 ]
-- | A data type to represent the state of the chain rule computation.
data ChainRuleState = ChainRuleState
{ crsCaseName :: [String]
, crsNewVars :: [Either TID ArbMsgId]
, crsFacts :: Facts
, crsFinalEq :: Maybe E.MsgEq
}
type ChainRuleM = StateT ChainRuleState []
-- | Add a fragment of the case name.
addCaseFragment :: String -> ChainRuleM ()
addCaseFragment name = modify $ \crs -> crs { crsCaseName = crsCaseName crs ++ [name] }
-- | Add a newly quantified variable.
addNewVar :: Either TID ArbMsgId -> ChainRuleM ()
addNewVar v = modify $ \crs -> crs { crsNewVars = crsNewVars crs ++ [v] }
-- | Change the facts of the chain rule computation state.
modifyFacts :: (Facts -> Facts) -> ChainRuleM ()
modifyFacts f = modify $ \crs -> crs { crsFacts = f $ crsFacts crs }
-- | Gets a component of the facts.
getsFacts :: (Facts -> a) -> ChainRuleM a
getsFacts f = gets (f . crsFacts)
-- | Set the equality that has to be solved for the case to be complete.
setFinalEq :: E.MsgEq -> ChainRuleM ()
setFinalEq eq = modify $ \crs -> crs { crsFinalEq = Just eq }
-- try to unify the two messages in the context of the current facts;
-- this function will always succeed, but the facts may be Nothing
unify :: Message -> Message -> ChainRuleM ()
unify m m'
| m == m' = return () -- performance optimization
| otherwise = do
crs <- get
maybe mzero (modifyFacts . const) $
solve [certAnyEq (crsFacts crs) $ E.MsgEq (m', m)] (crsFacts crs)
-- | Get a fresh thread identifier and update the facts accordingly
getFreshTID :: ChainRuleM TID
getFreshTID = do
(tid, facts) <- getsFacts freshTID
modifyFacts (const facts)
addNewVar (Left tid)
return tid
-- | Get a fresh thread arbitrary-message id and update the facts accordingly
getFreshAMID :: ChainRuleM ArbMsgId
getFreshAMID = do
(aid, facts) <- getsFacts freshArbMsgId
modifyFacts (const facts)
addNewVar (Right aid)
return aid
-- | Add a type annotation.
addTypeAnn :: TypeAnn -> ChainRuleM ()
addTypeAnn tya = modifyFacts $
\facts -> insertTypeAnn (certTypeAnn facts tya) facts
-- | Delete the given type annotation. Logically, this means forgetting
-- the corresponding assumption.
deleteTypeAnn :: TypeAnn -> ChainRuleM ()
deleteTypeAnn tya = modifyFacts $
\facts -> facts { typeAnns = S.delete tya (typeAnns facts) }
-- | Add a type annotation in expanded form. Expansion stops at SumT types
-- to avoid introducing unnecessary case distionctions.
addExpandedTypeAnn :: TypeAnn -> ChainRuleM ()
addExpandedTypeAnn (m, ty0, tid) = do
m' <- expand (return m) ty0
unify m m'
where
-- The first argument allows us to be lazy for creating new
-- message-variables
expand :: ChainRuleM Message -> Type -> ChainRuleM Message
expand mkV AgentT = do
v <- mkV
addTypeAnn (v, AgentT, tid)
return v
expand _ (NonceT role n) = do
nTid <- getFreshTID
modifyFacts $ insertRole nTid role
return $ MFresh (Fresh (LocalId (n, nTid)))
expand mkV ty@(SumT _ _) = do
v <- mkV
addTypeAnn (v, ty, tid)
return v
expand mkV ty@(KnownT _) = do
v <- mkV
addTypeAnn (v, ty, tid)
return v
expand _ (ConstT c) = return (MConst c)
expand _ (HashT ty) = MHash <$> expand arb ty
expand _ (EncT ty1 ty2) = MEnc <$> expand arb ty1 <*> expand arb ty2
expand _ (TupT ty1 ty2) = MTup <$> expand arb ty1 <*> expand arb ty2
expand _ (SymKT ty1 ty2) = MSymK <$> expand arb ty1 <*> expand arb ty2
expand _ (AsymPKT ty) = MAsymPK <$> expand arb ty
expand _ (AsymSKT ty) = MAsymSK <$> expand arb ty
arb :: ChainRuleM Message
arb = MArbMsg <$> getFreshAMID
-- | Get the type annotation of a message.
--
-- PRE: The message must be normalized with respect to the current facts.
getTypeAnn :: Message -> ChainRuleM TypeAnn
getTypeAnn m = do
tyas <- gets (typeAnns . crsFacts)
return $ headNote ("getTypeAnn: unannotated message '" ++ show m ++ "'")
[ tya | tya@(m', _, _) <- S.toList tyas, m == m' ]
-- number cases such that duplicates get numbered individually
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}
-- TODO: Remove this magic number (0) hack
-- | Extract the actual cases that result in new facts the other cases were
-- just there to compute the name
extractCase :: [E.AnyEq] -> ChainRuleState -> Maybe ((String, [Either TID ArbMsgId]), Facts)
extractCase delayedEqs0 crs = do
let facts0 = crsFacts crs
unmappedTID tid
| substTID facts0 tid == tid = return (Left tid)
| otherwise = mzero
unmappedAMID aid
| substAMID facts0 aid == MArbMsg aid = return (Right aid)
| otherwise = mzero
newVars = concatMap (either unmappedTID unmappedAMID) $ crsNewVars crs
delayedEqs = maybe [] (return . E.MsgEq) (crsFinalEq crs) ++ delayedEqs0
-- NOTE we are careful here to certify the equalities again. This should be a
-- no-op, but we'll leave it in for debugging purposes.
facts <- solve (map (certAnyEq facts0) delayedEqs) facts0
-- NOTE that at this point the case name is stored in complete form in the
-- head fragment. Trivial facts need to be removed as they could have been
-- introduced due to unification.
return ( (head $ crsCaseName crs, newVars)
, removeTrivialFacts . trimQuantifiers $ facts)
-- | Cases stemming from the initial intruder knowledge
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
-- fake
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 ++ "'"
-- | Apply the chain rule to a message in the context of a protocol and a set
-- of established facts. Returns the list of facts corresponding to the
-- disjunctions in the conclusion of the chain rule, which are not trivially
-- false due to syntactic inequality.
chainRuleFacts :: MonadPlus m => Message -> Facts -> m [((String, [Either TID ArbMsgId]), 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`
-- send steps
do tid <- getFreshTID
proto <- getsFacts protocol
msum $ map (roleChains typ tid) $ protoRoles proto
-- don't output cases where the facts are already contradictory without
-- the context. This caters for messages that are received and sent in
-- exactly the same form.
finalFacts <- gets crsFacts
guard (not $ proveFalse finalFacts)
)
where
facts1 = facts0 { equalities = E.empty
, covered = S.insert m $ covered facts0 }
delayedEqs = E.toAnyEqs $ equalities facts0
-- insert a list of previous events
insertPrevious :: [Event] -> Event -> ChainRuleM ()
insertPrevious prev ev = modifyFacts $
\facts -> foldl' insertSingle facts prev
where
insertSingle p prevEv = insertEvOrdNonTrivial (certEvOrd p (prevEv, ev)) p
-- enumerate chainRuleFacts starting from the given role
roleChains :: Typing -> TID -> Role -> ChainRuleM ()
roleChains typ 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
-- trace ("stepChains: " ++ roleName role ++"_"++getLabel l) (return ())
modifyFacts $ insertStepPrefixClosed (Cert (tid, step))
addCaseFragment $ stepLabel step
mapM_ annotateMVarType $ S.toList $ patFMV pt
msgChains [(Step tid step)] (inst tid pt)
where
-- annotating message variables with their type
annotateMVarType mv =
case M.lookup (mv, role) typ of
Nothing -> error $ "stepChains: no type provided for '"++show v++"'"
Just ty -> addExpandedTypeAnn (v, ty, tid)
where
v = MMVar (MVar (LocalId (mv, tid)))
-- case naming
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 (MArbMsg _) = "someAgent"
msgName (MInvKey _) = "invKey"
lidName = getId . fst . getLocalId
-- chain enumeration
msgChains :: [Event] -> Message -> ChainRuleM ()
msgChains _ (MAVar _) = mzero
msgChains _ (MConst _) = mzero
msgChains prev v@(MArbMsg _) = typChains prev v
msgChains prev v@(MMVar _) = do
addCaseFragment (msgName v)
typChains prev v
msgChains prev m'@(MEnc m1 m2) =
do insertPrevious prev (Learn m')
( do -- trace ("msgChains: unify " ++ show m' ++ " =?= " ++ show m) (return ())
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'
-- here we have to unify, as Isabelle is also doing it early
unify m' m
-- the m' is an atomic message: just unify and be done with it.
msgChains prev m' = do
insertPrevious prev (Learn m')
addCaseFragment $ msgName m'
setFinalEq (m', m)
-- exploiting type annotations.
typChains :: [Event] -> Message -> ChainRuleM ()
typChains prev v = do
v' <- getsFacts (`substMsg` v)
if v /= v'
then msgChains prev v'
else do
tya <- getTypeAnn v
case tya of
(_,tyaTy,tyaTid) -> case tyaTy of
KnownT _ -> mzero -- protocol wellformedness checks that KnownT implies cyclicity
AgentT -> mzero -- we already know the agent names
SumT ty1 ty2 -> do
deleteTypeAnn tya
(addFastExpandedTypeAnn (v, ty1, tyaTid) <|>
addFastExpandedTypeAnn (v, ty2, tyaTid))
msgChains prev v
-- all other type annotations should have been expanded already.
_ -> error $ "msgChains: unexpanded type annotation: " ++ show tya
-- fast expansion of type annotations: exploits that KnownT _ is guaranteed to be cyclic
addFastExpandedTypeAnn (_, KnownT _, _) = mzero
addFastExpandedTypeAnn tya = addExpandedTypeAnn tya
------------------------------------------------------------------------------
-- Message Equality Splitting to deal with 'MShrK a b = MShrK x y' eqs
------------------------------------------------------------------------------
-- | Equalities that can be splitted.
splittableEqs :: Facts -> [MsgEq]
splittableEqs facts =
do eq@(MShrK _ _, MShrK _ _) <- getPostEqs $ equalities facts
guard (not $ uncurry (==) eq)
return eq
-- | Split an equality between bi-directional symmetric shared keys.
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 ++ "'"
------------------------------------------------------------------------------
-- Resolution
------------------------------------------------------------------------------
proveFacts :: Facts -- ^ From these premises
-> Facts -- ^ Show the these conclusion
-> Mapping -- ^ Mapping the free variables of the conclusion to the premises.
-> Bool
proveFacts prems concl mapping =
all (proveAtom prems . F.substAtom (getMappingEqs mapping)) (toAtoms concl)
-- | Possible unifiers making the first set of facts provable under the second
-- set of facts. resulting equalities describe the mapping from all logical
-- variables of the first set of facts logical variables of the second set of
-- facts.
--
-- NOTE: You may want to use 'trimQuantifiers' before using this function to
-- avoid getting superfluous unifiers.
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 mkArbMsgIdMapping M.empty . S.toList $ amQuantifiers from
return $ E.mkMapping tideqs agnteqs
mkTIDMapping eqs tidF = do
tidT <- msum . map return . S.toList $ tidQuantifiers to
return $ M.insert tidF tidT eqs
mkArbMsgIdMapping eqs aidF = do
aidT <- msum . map return . S.toList $ amQuantifiers to
return $ M.insert aidF aidT eqs
-- | Apply the mapping of agent and thread equalities to the facts.
--
-- TODO: Improve error handling. Currently, 'error' is called if the facts
-- are contradictory after the substitution.
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 (quantifyArbMsgId . extractArbMsgId . E.substAMID eqs)
quantifyTIDs facts = foldM qTID facts $ S.toList $ tidQuantifiers facts0
quantifyAIDs facts = foldM qAID facts $ S.toList $ amQuantifiers facts0
addAtoms = conjoinAtoms atoms
atoms = map (F.substAtom (getMappingEqs mapping)) . toAtoms $ facts0
extractArbMsgId (MArbMsg aid) = aid
extractArbMsgId m = error $
"applyMapping: arbitrary-message id mapped to '" ++ show m ++ "'"
------------------------------------------------------------------------------
-- Pretty Printing
------------------------------------------------------------------------------
-- Helper functions
-------------------
isReprEq :: E.AnyEq -> Bool
isReprEq (TIDEq _) = False
isReprEq (ArbMsgEq _) = False
isReprEq _ = True
ppSet :: (a -> b) -> S.Set a -> [b]
ppSet ppElem = map ppElem . S.toList
-- To Isar
----------
-- | Pretty print the facts in Isar format.
isaFacts :: IsarConf -> Facts
-> ([Doc],[Doc],[Doc]) -- ^ Quantified variables, representable facts, and non-representable facts
isaFacts conf facts =
( ppSet (isar conf) (tidQuantifiers facts) ++
ppSet (isar conf) (amQuantifiers 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
-- To a security protocol theory
--------------------------------
-- | Pretty print the facts in security protocol theory format.
sptFacts :: Facts
-> ([Doc],[Doc],[Doc]) -- ^ Quantified variables, representable facts, and non-representable facts
sptFacts facts =
( ppSet sptTID (tidQuantifiers facts) ++
ppSet sptArbMsgId (amQuantifiers 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 (sptTypeAnn (`threadRole` facts)) $ S.toList $ typeAnns 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]
{-
sptSimpleFacts :: Facts -> Doc
sptSimpleFacts facts = case sptFacts facts of
(ds1, ds2, ds3) -> vcat $ map vcat [ds1, [text ""], ds2, [text ""], ds3]
-}
-- | Compute a list of transitive chains representing an abbreviated version of
-- the given binary relation.
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