diff --git a/src/Theory/Constraint/Solver/CaseDistinctions.hs b/src/Theory/Constraint/Solver/CaseDistinctions.hs --- a/src/Theory/Constraint/Solver/CaseDistinctions.hs +++ b/src/Theory/Constraint/Solver/CaseDistinctions.hs @@ -19,6 +19,9 @@ -- ** Application , solveWithCaseDistinction + -- ** Redundant cases + , removeRedundantCases + ) where import Prelude hiding (id, (.)) @@ -26,7 +29,6 @@ import Data.Foldable (asum) import qualified Data.Map as M -import Data.Maybe (isJust) import qualified Data.Set as S import Control.Basics @@ -49,6 +51,7 @@ import Theory.Constraint.System import Theory.Model +import Control.Monad.Bind ------------------------------------------------------------------------------ -- Precomputing case distinctions @@ -89,8 +92,14 @@ -> ([a], CaseDistinction) refineCaseDistinction ctxt proofStep th = ( map fst $ getDisj refinement - , set cdCases (snd <$> refinement) th ) + , set cdCases newCases th ) where + newCases = Disj . removeRedundantCases ctxt stableVars snd + . map (second (modify sSubst (restrict stableVars))) + . getDisj $ snd <$> refinement + + stableVars = frees (get cdGoal th) + fs = avoid th refinement = do (names, se) <- get cdCases th @@ -125,6 +134,11 @@ usefulGoal (_, (_, Useful)) = True usefulGoal _ = False + isKDPrem (PremiseG _ fa,_) = isKDFact fa + isKDPrem _ = False + isChainPrem1 (ChainG _ (_,PremIdx 1),_) = True + isChainPrem1 _ = False + solve caseNames = do simplifySystem ctxt <- ask @@ -139,8 +153,10 @@ -- open goal. splitAllowed = noChainGoals && not (null chains) safeGoals = fst <$> filter (safeGoal splitAllowed) goals + kdPremGoals = fst <$> filter (\g -> isKDPrem g || isChainPrem1 g) goals usefulGoals = fst <$> filter usefulGoal goals - nextStep = + nextStep = + ((fmap return . solveGoal) <$> headMay kdPremGoals) <|> ((fmap return . solveGoal) <$> headMay safeGoals) <|> (asum $ map (solveWithCaseDistinction ctxt ths) usefulGoals) case nextStep of @@ -148,53 +164,99 @@ Just step -> solve . (caseNames ++) =<< step + ------------------------------------------------------------------------------ +-- Redundant Case Distinctions -- +------------------------------------------------------------------------------ + +-- | Given a list of stable variables (that are referenced from outside and cannot be simply +-- renamed) and a list containing systems, this function returns a subsequence of the list +-- such that for all removed systems, there is a remaining system that is equal modulo +-- renaming of non-stable variables. +removeRedundantCases :: ProofContext -> [LVar] -> (a -> System) -> [a] -> [a] +removeRedundantCases ctxt stableVars getSys cases0 = + -- usually, redundant cases only occur with the multiset and bilinear pairing theories + if enableBP msig || enableMSet msig then cases else cases0 + where + -- decorate with index and normed version of the system + decoratedCases = map (second addNormSys) $ zip [(0::Int)..] cases0 + -- drop cases where the normed systems coincide + cases = map (fst . snd) . sortOn fst . sortednubOn (snd . snd) $ decoratedCases + + addNormSys = id &&& ((modify sEqStore dropNameHintsBound) . renameDropNameHints . getSys) + + -- this is an ordering that works well in the cases we tried + orderedVars sys = + filter ((/= LSortNode) . lvarSort) $ map fst . sortOn snd . varOccurences $ sys + + -- rename except for stable variables, drop name hints, and import ordered vars first + renameDropNameHints sys = + (`evalFresh` avoid stableVars) . (`evalBindT` stableVarBindings) $ do + _ <- renameDropNamehint (orderedVars sys) + renameDropNamehint sys + where + stableVarBindings = M.fromList (map (\v -> (v, v)) stableVars) + + msig = mhMaudeSig . get pcMaudeHandle $ ctxt + +------------------------------------------------------------------------------ -- Applying precomputed case distinctions ------------------------------------------------------------------------------ --- | Match a precomputed 'CaseDistinction' to a goal. +-- | Match a precomputed 'CaseDistinction' to a goal. Returns the instantiated +-- 'CaseDistinction' with the given goal if possible matchToGoal :: ProofContext -- ^ Proof context used for refining the case distinction. -> CaseDistinction -- ^ Case distinction to use. -> Goal -- ^ Goal to match - -> Maybe (Reduction [String]) - -- ^ A constraint reduction step to apply the resulting case distinction. - -- Note that this step assumes that the theorem has been imported using - -- 'someInst' into the context that this reduction is executed in. - -- - -- FIXME: This is a mess. Factor code such that this inter-dependency - -- between 'applyCaseDistinction' and 'matchToGoal' goes away. -matchToGoal ctxt th goalTerm = + -> Maybe CaseDistinction + -- ^ An adapted version of the case distinction with the given goal +matchToGoal ctxt th0 goalTerm = + if not $ maybeMatcher (goalTerm, get cdGoal th0) then Nothing else case (goalTerm, get cdGoal th) of ( PremiseG (iTerm, premIdxTerm) faTerm ,PremiseG pPat@(iPat, _ ) faPat ) -> - let match = faTerm `matchFact` faPat <> iTerm `matchLVar` iPat in - case runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt) of + case doMatch (faTerm `matchFact` faPat <> iTerm `matchLVar` iPat) of [] -> Nothing - subst:_ -> Just $ genericApply subst $ - -- add the missing edge to each case of the theorem - modify sEdges (substNodePrem pPat (iPat, premIdxTerm)) + subst:_ -> + let refine = do + modM sEdges (substNodePrem pPat (iPat, premIdxTerm)) + refineSubst subst + in Just $ snd $ refineCaseDistinction ctxt refine (set cdGoal goalTerm th) (ActionG iTerm faTerm, ActionG iPat faPat) -> - let match = faTerm `matchFact` faPat <> iTerm `matchLVar` iPat in - case runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt) of + case doMatch (faTerm `matchFact` faPat <> iTerm `matchLVar` iPat) of [] -> Nothing - subst:_ -> Just $ genericApply subst id + subst:_ -> Just $ snd $ refineCaseDistinction ctxt + (refineSubst subst) (set cdGoal goalTerm th) -- No other matches possible, as we only precompute case distinctions for -- premises and KU-actions. _ -> Nothing where - genericApply subst systemModifier = do - void (solveSubstEqs SplitNow subst) - (names, sysTh) <- disjunctionOfList $ getDisj $ get cdCases th - conjoinSystem (systemModifier sysTh) - return names + -- this code reflects the precomputed cases in 'precomputeCaseDistinctions' + maybeMatcher (PremiseG _ faTerm, PremiseG _ faPat) = factTag faTerm == factTag faPat + maybeMatcher ( ActionG _ (Fact KUFact [tTerm]) + , ActionG _ (Fact KUFact [tPat])) = + case (viewTerm tPat, viewTerm tTerm) of + (Lit (Var v),_) | lvarSort v == LSortFresh -> sortOfLNTerm tPat == LSortFresh + (FApp o _, FApp o' _) -> o == o' + _ -> True + maybeMatcher _ = False + th = (`evalFresh` avoid goalTerm) . rename $ th0 + substNodePrem from to = S.map (\ e@(Edge c p) -> if p == from then Edge c to else e) --- | Try to solve a premise goal or 'Ded' action using the first precomputed + doMatch match = runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt) + + refineSubst subst = do + void (solveSubstEqs SplitNow subst) + void substSystem + return ((), []) + +-- | Try to solve a premise goal or 'KU' action using the first precomputed -- case distinction with a matching premise. solveWithCaseDistinction :: ProofContext -> [CaseDistinction] @@ -209,14 +271,16 @@ -> CaseDistinction -- ^ Case distinction theorem. -> Goal -- ^ Required goal -> Maybe (Reduction [String]) -applyCaseDistinction ctxt th goal - | isJust $ matchToGoal ctxt th goal = Just $ do +applyCaseDistinction ctxt th0 goal = case matchToGoal ctxt th0 goal of + Just th -> Just $ do markGoalAsSolved "precomputed" goal - thRenamed <- rename th - fromJustNote "applyCaseDistinction: impossible" $ - matchToGoal ctxt thRenamed goal - - | otherwise = Nothing + (names, sysTh0) <- disjunctionOfList $ getDisj $ get cdCases th + sysTh <- (`evalBindT` keepVarBindings) . someInst $ sysTh0 + conjoinSystem sysTh + return names + Nothing -> Nothing + where + keepVarBindings = M.fromList (map (\v -> (v, v)) (frees goal)) -- | Saturate the case distinctions with respect to each other such that no -- additional splitting is introduced; i.e., only rules with a single or no @@ -283,13 +347,15 @@ absMsgFacts :: [LNTerm] absMsgFacts = asum $ sortednub $ - [ do return $ lit $ Var (LVar "t" LSortFresh 1) - - , [ fAppNonAC (s,k) $ nMsgVars k - | (s,k) <- S.toList . allFunctionSymbols . mhMaudeSig . get sigmMaudeHandle . get pcSignature $ ctxt - , (s,k) `S.notMember` implicitFunSig, k > 0 ] + [ return $ varTerm (LVar "t" LSortFresh 1) + , if enableBP msig then return $ fAppC EMap $ nMsgVars (2::Int) else [] + , [ fAppNoEq o $ nMsgVars k + | o@(_,(k,priv)) <- S.toList . noEqFunSyms $ msig + , NoEq o `S.notMember` implicitFunSig, k > 0 || priv==Private] ] + msig = mhMaudeSig . get pcMaudeHandle $ ctxt + -- | Refine a set of case distinction by exploiting additional typing -- assumptions. refineWithTypingAsms @@ -297,6 +363,8 @@ -> ProofContext -- ^ Proof context to use. -> [CaseDistinction] -- ^ Original, untyped case distinctions. -> [CaseDistinction] -- ^ Refined, typed case distinctions. +refineWithTypingAsms [] _ cases0 = + fmap ((modify cdCases . fmap . second) (set sCaseDistKind TypedCaseDist)) $ cases0 refineWithTypingAsms assumptions ctxt cases0 = fmap (modifySystems removeFormulas) $ saturateCaseDistinctions ctxt $ diff --git a/src/Theory/Constraint/Solver/Contradictions.hs b/src/Theory/Constraint/Solver/Contradictions.hs --- a/src/Theory/Constraint/Solver/Contradictions.hs +++ b/src/Theory/Constraint/Solver/Contradictions.hs @@ -31,7 +31,7 @@ import qualified Data.Foldable as F import Data.List import qualified Data.Map as M -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, listToMaybe) import Data.Monoid import qualified Data.Set as S import Safe (headMay) @@ -47,11 +47,13 @@ import Theory.Constraint.Solver.Types import Theory.Constraint.System import Theory.Model +import Theory.Tools.IntruderRules import Theory.Text.Pretty import Term.Rewriting.Norm (maybeNotNfSubterms, nf') + ------------------------------------------------------------------------------ -- Contradictions ------------------------------------------------------------------------------ @@ -62,6 +64,9 @@ | NonNormalTerms -- ^ Has terms that are not in normal form. -- | NonLastNode -- ^ Has a non-silent node after the last node. | ForbiddenExp -- ^ Forbidden Exp-down rule instance + | ForbiddenBP -- ^ Forbidden bilinear pairing rule instance + | ForbiddenKD -- ^ has forbidden KD-fact + | ImpossibleChain -- ^ has impossible chain | NonInjectiveFactInstance (NodeId, NodeId, NodeId) -- ^ Contradicts that certain facts have unique instances. | IncompatibleEqs -- ^ Incompatible equalities. @@ -85,8 +90,14 @@ [ guard (D.cyclic $ rawLessRel sys) *> pure Cyclic -- CR-rule *N1* , guard (hasNonNormalTerms sig sys) *> pure NonNormalTerms + -- FIXME: add CR-rule + , guard (hasForbiddenKD sys) *> pure ForbiddenKD + -- FIXME: add CR-rule + , guard (hasImpossibleChain sys) *> pure ImpossibleChain -- CR-rule *N7* - , guard (hasForbiddenExp sys) *> pure ForbiddenExp + , guard (enableDH msig && hasForbiddenExp sys) *> pure ForbiddenExp + -- FIXME: add CR-rule + , guard (enableBP msig && hasForbiddenBP sys) *> pure ForbiddenBP -- CR-rules *S_≐* and *S_≈* are implemented via the equation store , guard (eqsIsFalse $ L.get sEqStore sys) *> pure IncompatibleEqs -- CR-rules *S_⟂*, *S_{¬,last,1}*, *S_{¬,≐}*, *S_{¬,≈}* @@ -99,11 +110,25 @@ -- system. (NonInjectiveFactInstance <$> nonInjectiveFactInstances ctxt sys) ++ - -- TODO: Document corresponding constratint reduction rule. + -- TODO: Document corresponding constraint reduction rule. (NodeAfterLast <$> nodesAfterLast sys) where - sig = L.get pcSignature ctxt + sig = L.get pcSignature ctxt + msig = mhMaudeSig . L.get pcMaudeHandle $ ctxt +-- | New normal form condition: +-- We do not allow @KD(t)@ facts if @t@ does not contain +-- any fresh names. +hasForbiddenKD :: System -> Bool +hasForbiddenKD sys = + any isForbiddenKD $ M.elems $ L.get sNodes sys + where + isForbiddenKD ru = fromMaybe False $ do + [conc] <- return $ L.get rConcs ru + (DnK, t) <- kFactView conc + return $ neverContainsFreshPriv t + + -- | True iff there are terms in the node constraints that are not in normal form wrt. -- to 'Term.Rewriting.Norm.norm' (DH/AC). hasNonNormalTerms :: SignatureWithMaude -> System -> Bool @@ -120,51 +145,16 @@ t <- factTerms f maybeNotNfSubterms (mhMaudeSig hnd) t -substCreatesNonNormalTerms :: MaudeHandle -> System -> LNSubstVFresh -> Bool -substCreatesNonNormalTerms hnd se = +substCreatesNonNormalTerms :: MaudeHandle -> System -> LNSubst -> LNSubstVFresh -> Bool +substCreatesNonNormalTerms hnd sys fsubst = \subst -> any (not . nfApply subst) terms - where terms = maybeNonNormalTerms hnd se + where terms = apply fsubst $ maybeNonNormalTerms hnd sys nfApply subst0 t = t == t' || nf' t' `runReader` hnd where tvars = freesList t subst = restrictVFresh tvars subst0 - t' = apply (freshToFreeAvoidingFast subst tvars) t + t' = apply (freshToFreeAvoidingFast subst tvars) t --- | True if there is no @EXP-down@ rule that should be replaced by an --- @EXP-up@ rule. -hasForbiddenExp :: System -> Bool -hasForbiddenExp se = - any (isForbiddenExp) $ M.elems $ L.get sNodes se --- | @isForbiddenExp ru@ returns @True@ if @ru@ is not allowed in --- a normal dependency graph. --- --- > isForbiddenExp (Rule () [undefined, Fact KUFact [undefined, Mult (Inv x1) x2]] --- > [Fact KDFact [expTagToTerm IsExp, Exp p1 (Mult x2 x3)]] []) --- > False --- > isForbiddenExp (Rule () [undefined, Fact KUFact [undefined, Mult (Inv x1) x2]] --- > [Fact KDFact [expTagToTerm IsExp, Exp p1 x2]] []) --- > True --- -isForbiddenExp :: Rule a -> Bool -isForbiddenExp ru = fromMaybe False $ do - [p1,p2] <- return $ L.get rPrems ru - [conc] <- return $ L.get rConcs ru - (DnK, viewTerm2 -> FExp _ _) <- kFactView p1 - (UpK, b ) <- kFactView p2 - (DnK, viewTerm2 -> FExp g c) <- kFactView conc - - -- For a forbidden exp the following conditions must hold: g must be of - -- sort 'pub' and the required inputs for c are already required by b - return $ sortOfLNTerm g == LSortPub - && (inputTerms c \\ inputTerms b == []) - where - -- The required components to construct the message. - inputTerms :: LNTerm -> [LNTerm] - inputTerms (viewTerm2 -> FMult ts) = concatMap inputTerms ts - inputTerms (viewTerm2 -> FInv t1) = inputTerms t1 - inputTerms (viewTerm2 -> FPair t1 t2) = inputTerms t1 ++ inputTerms t2 - inputTerms t = [t] - -- | Compute all contradictions to injective fact instances. -- -- Formally, they are computed as follows. Let 'f' be a fact symbol with @@ -214,14 +204,193 @@ guard (j /= i && isInTrace sys j) return (i, j) +-- | Detect impossible chains early by checking if +-- it is possible to deduce the chain-end from the +-- chain-start by extending the chain or replacing +-- it with an edge. +hasImpossibleChain :: System -> Bool +hasImpossibleChain sys = + any impossibleChain [ (c,p) | ChainG c p <- M.keys $ L.get sGoals sys ] + where + impossibleChain (c,p) = fromMaybe False $ do + (DnK, t_start) <- kFactView $ nodeConcFact c sys + (DnK, t_end) <- kFactView $ nodePremFact p sys + -- the root symbol of the chain-end if it can be determined + req_end_sym <- rootSym t_end + -- the possible root symbols after applying deconstruction + -- rules to the chain-start if they can be determined + poss_end_syms <- possibleRootSyms t_start + -- the chain is impossible if both the required root-symbol + -- and the possible root0symbols for the chain-end can be + -- determined and the required symbol in not possible. + return $ not (req_end_sym `elem` poss_end_syms) + rootSym :: LNTerm -> Maybe (Either LSort FunSym) + rootSym t = + case viewTerm t of + FApp sym _ -> return $ Right sym + Lit _ | sortOfLNTerm t == LSortMsg -> Nothing + -- we cannot determine the root symbols of a message-variable + | otherwise -> return $ Left (sortOfLNTerm t) + -- a public or fresh name or variable + + possibleRootSyms :: LNTerm -> Maybe [Either LSort FunSym] + possibleRootSyms t | neverContainsFreshPriv t = return [] + -- this is an 'isForbiddenDeconstruction' + possibleRootSyms t = case viewTerm2 t of + FExp a _b -> -- cannot obtain a subterm of the exponents @_b@ + ((Right (NoEq expSym)):) <$> possibleRootSyms a + FPMult _b a -> -- cannot obtain a subterm of the scalars @_b@ + ((Right <$> [NoEq expSym, NoEq pmultSym, C EMap])++) <$> possibleRootSyms a + FEMap _ _ -> return [Right (C EMap)] + _ -> case viewTerm t of + Lit _ -> (:[]) <$> rootSym t + FApp o args -> ((Right o):) . concat <$> mapM possibleRootSyms args + + +-- Diffie-Hellman and Bilinear Pairing +-------------------------------------- + +-- | 'True' if there is a @Exp-down@ rule that is not allowed in +-- a normal dependency graph. +hasForbiddenExp :: System -> Bool +hasForbiddenExp sys = + any forbiddenDExp $ M.toList $ L.get sNodes sys + where + forbiddenDExp (i,ru) = fromMaybe False $ do + [p1,p2] <- return $ L.get rPrems ru + [conc] <- return $ L.get rConcs ru + (DnK, viewTerm2 -> FExp _ _) <- kFactView p1 + (UpK, b ) <- kFactView p2 + case kFactView conc of + Just (DnK, viewTerm2 -> FExp g c) -> + -- For a forbidden dexp, the following conditions must hold: g does not + -- contain fresh names/vars, all msg vars in g must be KU-known earlier, + -- and the factors of c are already factors of b + return $ (isSimpleTerm g && allMsgVarsKnownEarlier i (varTerm <$> frees g)) + && (niFactors c \\ niFactors b == []) + Just (DnK, g) -> + return $ isSimpleTerm g && allMsgVarsKnownEarlier i (varTerm <$> frees g) + _ -> return False + + allMsgVarsKnownEarlier i args = + all (`elem` earlierMsgVars) (filter isMsgVar args) + where earlierMsgVars = do (j, _, t) <- allKUActions sys + guard $ isMsgVar t && alwaysBefore sys j i + return t + +-- | 'True' if there is a @Pmult-down@ or @Em-down@ rule that +-- is not allowed in a normal dependency graph. +hasForbiddenBP :: System -> Bool +hasForbiddenBP sys = + (any isForbiddenDPMult $ M.elems $ L.get sNodes sys) || + (any (isForbiddenDEMap sys) $ M.toList $ L.get sNodes sys) || + (any (isForbiddenDEMapOrder sys) $ M.toList $ L.get sNodes sys) + +-- | @isForbiddenDPMult ru@ returns @True@ if @ru@ is not allowed in +-- a normal dependency graph. +isForbiddenDPMult :: Rule a -> Bool +isForbiddenDPMult ru = fromMaybe False $ do + [p1,p2] <- return $ L.get rPrems ru + [conc] <- return $ L.get rConcs ru + (DnK, viewTerm2 -> FPMult _ _) <- kFactView p1 + (UpK, b ) <- kFactView p2 + (DnK, viewTerm2 -> FPMult c p) <- kFactView conc + + -- For a forbidden dpmult, the following conditions must hold: p does not + -- contain fresh names and the factors of c are already factors of b + return $ neverContainsFreshPriv p + && (niFactors c \\ niFactors b == []) + +-- | We detect many scenarios where a 'dem' rule followed +-- by a 'dexp' rule can be replaced by simpler variants. +-- As an example consider: +-- +-- [s]P [r]Q P [r]Q +-- -------------- dem ------------ dem +-- em(P,Q)^(s*r) ==> em(P,Q)^r +-- | ke=inv(s)*ke' | ke' +-- ------------------------------ dexp ----------------- dexp +-- em(P,Q)^r*ke' em(P,Q)^r*ke' +-- +-- It is also possible that r is removed or that s is added a second time +-- to the exponent. +-- FIXME: This requires a new normal-form condition +isForbiddenDEMap :: System -> (NodeId, RuleACInst) -> Bool +isForbiddenDEMap sys (i, ruExp) = fromMaybe False $ do + guard (isDExpRule ruExp) + + ke_f <- resolveNodePremFact (i, PremIdx 1) sys + (UpK, ke) <- kFactView ke_f + + ruEMap <- flip nodeRule sys <$> + listToMaybe [ ns | Edge (ns,_) (nt,pit) <- S.toList (L.get sEdges sys) + , nt == i, pit == PremIdx 0 ] + guard (isDEMapRule ruEMap) + + [sP_f, rQ_f] <- return $ L.get rPrems ruEMap + (DnK, viewTerm2 -> FPMult s p) <- kFactView sP_f + (DnK, viewTerm2 -> FPMult r q) <- kFactView rQ_f + + return (overComplicated s p ke || overComplicated r q ke) + where + overComplicated scalar point ke = + (niFactors scalar \\ niFactors ke == []) && neverContainsFreshPriv point + +-- | We enforce that if both premises of the @Emap-down@ rule +-- KD([s]p), KD([r]q) --> KD(em(p,q)^(s*r) (where s,r are not +-- products) are provided by @IRecv@ and protocol rules @P1@ and +-- @P2@, then the factTags of @P1@ cannot be greater than the +-- factTags of @P2@. +-- This requires another normal-form condition. +isForbiddenDEMapOrder :: System -> (NodeId, RuleACInst) -> Bool +isForbiddenDEMapOrder sys (i, ruDEMap) = fromMaybe False $ do + guard (isDEMapRule ruDEMap) + + -- ensure that ruDEMap is instance of the right rule + [f_p0, f_p1] <- return $ L.get rPrems ruDEMap + [f_c0] <- return $ L.get rConcs ruDEMap + (DnK, viewTerm2 -> FPMult s p) <- kFactView f_p0 + (DnK, viewTerm2 -> FPMult r q) <- kFactView f_p1 + (DnK, viewTerm2 -> FExp (viewTerm2 -> FEMap p' q') (viewTerm2 -> FMult as)) <- kFactView f_c0 + guard (((p,q) == (p',q') || (p,q) == (q',p')) && as \\ [s,r] == []) + + -- there must be at least one rule (IRecv) between 'i' and the + -- protocol rules + j1 <- lookupPremProvider (i,PremIdx 0) + j2 <- lookupPremProvider (i,PremIdx 1) + + ruProto1 <- flip nodeRule sys <$> lookupPremProvider (j1, PremIdx 0) + ruProto2 <- flip nodeRule sys <$> lookupPremProvider (j2, PremIdx 0) + -- ensure that both are protocol rules + guard (isStandRule ruProto1 && isStandRule ruProto2) + + return $ (factTags ruProto1) > (factTags ruProto2) + where + lookupPremProvider (k,prem) = + listToMaybe [ ns | Edge (ns,_) (nt,pit) <- S.toList (L.get sEdges sys) + , nt == k, pit == prem ] + + factTags ru = map (map factTag) [L.get rPrems ru, L.get rConcs ru, L.get rActs ru] + + isStandRule ru = ruleInfo (isStandName . L.get praciName) (const False) $ L.get rInfo ru + isStandName (StandRule _) = True + isStandName _ = False + + +-- Pretty printing +------------------ + -- | Pretty-print a 'Contradiction'. prettyContradiction :: Document d => Contradiction -> d prettyContradiction contra = case contra of Cyclic -> text "cyclic" IncompatibleEqs -> text "incompatible equalities" NonNormalTerms -> text "non-normal terms" - ForbiddenExp -> text "non-normal exponentiation instance" + ForbiddenExp -> text "non-normal exponentiation rule instance" + ForbiddenBP -> text "non-normal bilinear pairing rule instance" + ForbiddenKD -> text "forbidden KD-fact" + ImpossibleChain -> text "impossible chain" NonInjectiveFactInstance cex -> text $ "non-injective facts " ++ show cex FormulasFalse -> text "from formulas" SuperfluousLearn m v -> @@ -240,6 +409,8 @@ foldFrees f (NonInjectiveFactInstance x) = foldFrees f x foldFrees f (NodeAfterLast x) = foldFrees f x foldFrees _ _ = mempty + + foldFreesOcc _ _ = const mempty mapFrees f (SuperfluousLearn t v) = SuperfluousLearn <$> mapFrees f t <*> mapFrees f v mapFrees f (NonInjectiveFactInstance x) = NonInjectiveFactInstance <$> mapFrees f x diff --git a/src/Theory/Constraint/Solver/Goals.hs b/src/Theory/Constraint/Solver/Goals.hs --- a/src/Theory/Constraint/Solver/Goals.hs +++ b/src/Theory/Constraint/Solver/Goals.hs @@ -41,9 +41,9 @@ import Theory.Constraint.Solver.Reduction import Theory.Constraint.Solver.Types import Theory.Constraint.System +import Theory.Tools.IntruderRules (mkDUnionRule, isDExpRule, isDPMultRule, isDEMapRule) import Theory.Model - ------------------------------------------------------------------------------ -- Extracting Goals ------------------------------------------------------------------------------ @@ -79,7 +79,7 @@ || isMsgVar m || sortOfLNTerm m == LSortPub -- handled by 'insertAction' || isPair m || isInverse m || isProduct m - || isNullaryFunction m + || isUnion m || isNullaryPublicFunction m ActionG _ _ -> not solved PremiseG _ _ -> not solved -- Technically the 'False' disj would be a solvable goal. However, we @@ -89,8 +89,10 @@ ChainG c _ -> case kFactView (nodeConcFact c sys) of - Just (DnK, m) | isMsgVar m -> False - | otherwise -> not solved + Just (DnK, viewTerm2 -> FUnion args) -> + not solved && allMsgVarsKnownEarlier c args + Just (DnK, m) | isMsgVar m -> False + | otherwise -> not solved fa -> error $ "openChainGoals: impossible fact: " ++ show fa -- FIXME: Split goals may be duplicated, we always have to check @@ -116,21 +118,22 @@ checkTermLits :: (LSort -> Bool) -> LNTerm -> Bool checkTermLits p = Mono.getAll . foldMap (Mono.All . p . sortOfLit) - where - sortOfLit (Con n) = sortOfName n - sortOfLit (Var v) = lvarSort v -- KU goals of messages that are likely to be constructible by the -- adversary. These are terms that do not contain a fresh name or a fresh -- name variable. For protocols without loops they are very likely to be -- constructible. For protocols with loops, such terms have to be given -- similar priority as loop-breakers. - probablyConstructible = checkTermLits (LSortFresh /=) + probablyConstructible m = checkTermLits (LSortFresh /=) m + && not (containsPrivate m) -- KU goals of messages that are currently deducible. Either because they - -- are composed of public names only or because they can be extracted from - -- a sent message using unpairing or inversion only. - currentlyDeducible i m = checkTermLits (LSortPub ==) m || extractible i m + -- are composed of public names only and do not contain private function + -- symbols or because they can be extracted from a sent message using + -- unpairing or inversion only. + currentlyDeducible i m = (checkTermLits (LSortPub ==) m + && not (containsPrivate m)) + || extractible i m extractible i m = or $ do (j, ru) <- M.toList $ get sNodes sys @@ -145,12 +148,17 @@ return $ m `elem` derivedMsgs && not (D.cyclic ((j, i) : existingDeps)) - toplevelTerms t@(destPair -> Just (t1, t2)) = + toplevelTerms t@(viewTerm2 -> FPair t1 t2) = t : toplevelTerms t1 ++ toplevelTerms t2 - toplevelTerms t@(destInverse -> Just t1) = t : toplevelTerms t1 + toplevelTerms t@(viewTerm2 -> FInv t1) = t : toplevelTerms t1 toplevelTerms t = [t] + allMsgVarsKnownEarlier (i,_) args = + all (`elem` earlierMsgVars) (filter isMsgVar args) + where earlierMsgVars = do (j, _, t) <- allKUActions sys + guard $ isMsgVar t && alwaysBefore sys j i + return t ------------------------------------------------------------------------------ @@ -229,32 +237,59 @@ solveChain rules (c, p) = do faConc <- gets $ nodeConcFact c (do -- solve it by a direct edge + cRule <- gets $ nodeRule (nodeConcNode c) + pRule <- gets $ nodeRule (nodePremNode p) faPrem <- gets $ nodePremFact p + contradictoryIf (forbiddenEdge cRule pRule) insertEdges [(c, faConc, faPrem, p)] - let m = case kFactView faConc of - Just (DnK, m') -> m' - _ -> error $ "solveChain: impossible" + let mPrem = case kFactView faConc of + Just (DnK, m') -> m' + _ -> error $ "solveChain: impossible" caseName (viewTerm -> FApp o _) = showFunSymName o caseName t = show t - return $ caseName m + return $ caseName mPrem `disjunction` - do -- extend it with one step - cRule <- gets $ nodeRule (nodeConcNode c) - (i, ru) <- insertFreshNode rules - -- contradicts normal form condition: - -- no edge from dexp to dexp KD premise - -- (this condition replaces the exp/noexp tags) - contradictoryIf (isDexpRule cRule && isDexpRule ru) - (v, faPrem) <- disjunctionOfList $ enumPrems ru + -- extend it with one step + case kFactView faConc of + Just (DnK, viewTerm2 -> FUnion args) -> + do -- If the chain starts at a union message, we + -- compute the applicable destruction rules directly. + i <- freshLVar "vr" LSortNode + let rus = map (ruleACIntrToRuleACInst . mkDUnionRule args) + (filter (not . isMsgVar) args) + -- NOTE: We rely on the check that the chain is open here. + ru <- disjunctionOfList rus + modM sNodes (M.insert i ru) + -- FIXME: Do we have to add the PremiseG here so it + -- marked as solved? + let v = PremIdx 0 + faPrem <- gets $ nodePremFact (i,v) + extendAndMark i ru v faPrem faConc + _ -> + do -- If the chain does not start at a union message, + -- the usual *DG2_chain* extension is perfomed. + cRule <- gets $ nodeRule (nodeConcNode c) + (i, ru) <- insertFreshNode rules + contradictoryIf (forbiddenEdge cRule ru) + -- This requires a modified chain constraint def: + -- path via first destruction premise of rule ... + (v, faPrem) <- disjunctionOfList $ take 1 $ enumPrems ru + extendAndMark i ru v faPrem faConc + ) + where + extendAndMark i ru v faPrem faConc = do insertEdges [(c, faConc, faPrem, (i, v))] markGoalAsSolved "directly" (PremiseG (i, v) faPrem) insertChain (i, ConcIdx 0) p return $ showRuleCaseName ru - ) - where - isDexpRule ru = case get rInfo ru of - IntrInfo (DestrRule n) | n == expSymString -> True - _ -> False + + -- contradicts normal form condition: + -- no edge from dexp to dexp KD premise, no edge from dpmult + -- to dpmult KD premise, and no edge from dpmult to demap KD premise + -- (this condition replaces the exp/noexp tags) + forbiddenEdge cRule pRule = isDExpRule cRule && isDExpRule pRule || + isDPMultRule cRule && isDPMultRule pRule || + isDPMultRule cRule && isDEMapRule pRule -- | Solve an equation split. There is no corresponding CR-rule in the rule -- system on paper because there we eagerly split over all variants of a rule. diff --git a/src/Theory/Constraint/Solver/ProofMethod.hs b/src/Theory/Constraint/Solver/ProofMethod.hs --- a/src/Theory/Constraint/Solver/ProofMethod.hs +++ b/src/Theory/Constraint/Solver/ProofMethod.hs @@ -37,6 +37,7 @@ import qualified Data.Label as L import Data.List import qualified Data.Map as M +import Data.Maybe (catMaybes) import Data.Monoid import Data.Ord (comparing) import qualified Data.Set as S @@ -44,7 +45,6 @@ import Control.Basics import Control.DeepSeq -import Control.Monad.Bind import qualified Control.Monad.Trans.PreciseFresh as Precise import Theory.Constraint.Solver.CaseDistinctions @@ -57,7 +57,6 @@ import Theory.Model import Theory.Text.Pretty - ------------------------------------------------------------------------------ -- Utilities ------------------------------------------------------------------------------ @@ -108,6 +107,8 @@ foldFrees f (Contradiction c) = foldFrees f c foldFrees _ _ = mempty + foldFreesOcc _ _ = const mempty + mapFrees f (SolveGoal g) = SolveGoal <$> mapFrees f g mapFrees f (Contradiction c) = Contradiction <$> mapFrees f c mapFrees _ method = pure method @@ -126,7 +127,6 @@ execProofMethod :: ProofContext -> ProofMethod -> System -> Maybe (M.Map CaseName System) execProofMethod ctxt method sys = - M.map cleanupSystem <$> case method of Sorry _ -> return M.empty Solved @@ -134,9 +134,9 @@ | otherwise -> Nothing SolveGoal goal | goal `M.member` L.get sGoals sys -> execSolveGoal goal - | otherwise -> Nothing - Simplify -> singleCase (/=) simplifySystem - Induction -> execInduction + | otherwise -> Nothing + Simplify -> singleCase simplifySystem + Induction -> M.map cleanupSystem <$> execInduction Contradiction _ | null (contradictions ctxt sys) -> Nothing | otherwise -> Just M.empty @@ -146,25 +146,27 @@ -- simplifySystem). We also reset the variable indices here. cleanupSystem = (`Precise.evalFresh` Precise.nothingUsed) - . (`evalBindT` noBindings) - . someInst + . renamePrecise . set sSubst emptySubst -- expect only one or no subcase in the given case distinction - singleCase check m = - case map fst $ getDisj $ execReduction m ctxt sys (avoid sys) of - [] -> return $ M.empty - [sys'] | check sys sys' -> return $ M.singleton "" sys' - | otherwise -> mzero - syss -> + singleCase m = + case removeRedundantCases ctxt [] id . map cleanupSystem + . map fst . getDisj $ execReduction m ctxt sys (avoid sys) of + [] -> return $ M.empty + [sys'] | check sys' -> return $ M.singleton "" sys' + | otherwise -> mzero + syss -> return $ M.fromList (zip (map show [(1::Int)..]) syss) + where check sys' = cleanupSystem sys /= sys' -- solve the given goal -- PRE: Goal must be valid in this system. - execSolveGoal goal = do - return $ makeCaseNames $ map fst $ getDisj $ - runReduction solver ctxt sys (avoid sys) + execSolveGoal goal = + return . makeCaseNames . removeRedundantCases ctxt [] snd + . map (second cleanupSystem) . map fst . getDisj + $ runReduction solver ctxt sys (avoid sys) where ths = L.get pcCaseDists ctxt solver = do name <- maybe (solveGoal goal) @@ -229,12 +231,12 @@ -- | Use a 'GoalRanking' to sort a list of 'AnnotatedGoal's stemming from the -- given constraint 'System'. -rankGoals :: GoalRanking -> System -> [AnnotatedGoal] -> [AnnotatedGoal] -rankGoals ranking = case ranking of +rankGoals :: ProofContext -> GoalRanking -> System -> [AnnotatedGoal] -> [AnnotatedGoal] +rankGoals ctxt ranking = case ranking of GoalNrRanking -> \_sys -> goalNrRanking UsefulGoalNrRanking -> \_sys -> sortOn (\(_, (nr, useless)) -> (useless, nr)) - SmartRanking useLoopsBreakers -> smartRanking useLoopsBreakers + SmartRanking useLoopsBreakers -> smartRanking ctxt useLoopsBreakers -- | Use a 'GoalRanking' to generate the ranked, list of possible -- 'ProofMethod's and their corresponding results in this 'ProofContext' and @@ -249,7 +251,7 @@ AvoidInduction -> [(Simplify, ""), (Induction, "")] UseInduction -> [(Induction, ""), (Simplify, "")] ) - <|> (solveGoalMethod <$> (rankGoals ranking sys $ openGoals sys)) + <|> (solveGoalMethod <$> (rankGoals ctxt ranking sys $ openGoals sys)) case execProofMethod ctxt m sys of Just cases -> return (m, (cases, expl)) Nothing -> [] @@ -318,12 +320,20 @@ -- | A ranking function tuned for the automatic verification of -- classical security protocols that exhibit a well-founded protocol premise -- fact flow. -smartRanking :: Bool -- True if PremiseG loop-breakers should not be delayed +smartRanking :: ProofContext + -> Bool -- True if PremiseG loop-breakers should not be delayed -> System -> [AnnotatedGoal] -> [AnnotatedGoal] -smartRanking allowPremiseGLoopBreakers sys = +smartRanking ctxt allowPremiseGLoopBreakers sys = sortOnUsefulness . unmark . sortDecisionTree solveFirst . goalNrRanking where + oneCaseOnly = catMaybes . map getMsgOneCase . L.get pcCaseDists $ ctxt + + getMsgOneCase cd = case msgPremise (L.get cdGoal cd) of + Just (viewTerm -> FApp o _) + | length (getDisj (L.get cdCases cd)) == 1 -> Just o + _ -> Nothing + sortOnUsefulness = sortOn (tagUsefulness . snd . snd) tagUsefulness Useful = 0 :: Int @@ -342,8 +352,10 @@ , isDisjGoal . fst , isNonLoopBreakerProtoFactGoal , isStandardActionGoal . fst + , isPrivateKnowsGoal . fst , isFreshKnowsGoal . fst , isSplitGoalSmall . fst + , isMsgOneCaseGoal . fst , isDoubleExpGoal . fst , isNoLargeSplitGoal . fst ] -- move the rest (mostly more expensive KU-goals) before expensive @@ -351,7 +363,7 @@ -- FIXME: This small split goal preferral is quite hacky when using -- induction. The problem is that we may end up solving message premise - -- goals all the time instead performing a necessary split. We should make + -- goals all the time instead of performing a necessary split. We should make -- sure that a split does not get too old. smallSplitGoalSize = 3 @@ -364,6 +376,14 @@ isFreshKnowsGoal goal = case msgPremise goal of Just (viewTerm -> Lit (Var lv)) | lvarSort lv == LSortFresh -> True _ -> False + + isMsgOneCaseGoal goal = case msgPremise goal of + Just (viewTerm -> FApp o _) | o `elem` oneCaseOnly -> True + _ -> False + + isPrivateKnowsGoal goal = case msgPremise goal of + Just t -> isPrivateFunction t + _ -> False isDoubleExpGoal goal = case msgPremise goal of Just (viewTerm2 -> FExp _ (viewTerm2 -> FMult _)) -> True diff --git a/src/Theory/Constraint/Solver/Reduction.hs b/src/Theory/Constraint/Solver/Reduction.hs --- a/src/Theory/Constraint/Solver/Reduction.hs +++ b/src/Theory/Constraint/Solver/Reduction.hs @@ -1,4 +1,5 @@ {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} -- | -- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier @@ -289,6 +290,9 @@ Just (UpK, viewTerm2 -> FMult ms) -> mapM_ requiresKU ms *> return Changed + Just (UpK, viewTerm2 -> FUnion ms) -> + mapM_ requiresKU ms *> return Changed + _ -> return Unchanged where goal = ActionG i fa @@ -534,7 +538,7 @@ changes <- forM goals $ \(goal, status) -> case goal of -- Look out for KU-actions that might need to be solved again. ActionG i fa@(kFactView -> Just (UpK, m)) - | (isMsgVar m || isProduct m) && (apply subst m /= m) -> + | (isMsgVar m || isProduct m || isUnion m) && (apply subst m /= m) -> insertAction i (apply subst fa) _ -> do modM sGoals $ M.insertWith' combineGoalStatus (apply subst goal) status @@ -659,7 +663,7 @@ (eqs, splitId) <- addRuleVariants eqConstr <$> getM sEqStore insertGoal (SplitG splitId) False -- do not use expensive substCreatesNonNormalTerms here - setM sEqStore =<< simp hnd (const False) eqs + setM sEqStore =<< simp hnd (const (const False)) eqs noContradictoryEqStore solveRuleConstraints Nothing = return () diff --git a/src/Theory/Constraint/Solver/Simplify.hs b/src/Theory/Constraint/Solver/Simplify.hs --- a/src/Theory/Constraint/Solver/Simplify.hs +++ b/src/Theory/Constraint/Solver/Simplify.hs @@ -196,7 +196,11 @@ ruleActions = [ (tag, length ts) | ru <- rules, Fact tag ts <- get rActs ru ] - isUnique (Fact tag ts) = (tag, length ts) `elem` uniqueActions + isUnique (Fact tag ts) = + (tag, length ts) `elem` uniqueActions + -- multiset union leads to case-splits because there + -- are multiple unifiers + && null [ () | t <- ts, FUnion _ <- return (viewTerm2 t) ] trySolve (i, fa) | isUnique fa = solveGoal (ActionG i fa) >> return Changed @@ -322,26 +326,36 @@ impliedFormulas hnd sys gf0 = case openGuarded gf `evalFresh` avoid gf of Just (All, _vs, antecedent, succedent) -> do - let (actions, otherAtoms) = partitionEithers $ map prepare antecedent - succedent' = gall [] otherAtoms succedent - subst <- candidateSubsts emptySubst actions + let (actionsEqs, otherAtoms) = first sortGAtoms . partitionEithers $ + map prepare antecedent + succedent' = gall [] otherAtoms succedent + subst <- candidateSubsts emptySubst actionsEqs return $ unskolemizeLNGuarded $ applySkGuarded subst succedent' _ -> [] where gf = skolemizeGuarded gf0 - prepare (Action i fa) = Left (i, fa) + prepare (Action i fa) = Left (GAction (i,fa)) + prepare (EqE s t) = Left (GEqE (s,t)) prepare ato = Right (fmap (fmapTerm (fmap Free)) ato) sysActions = do (i, fa) <- allActions sys return (skolemizeTerm (varTerm i), skolemizeFact fa) - candidateSubsts subst [] = do - return subst - candidateSubsts subst (a:as) = do + candidateSubsts subst [] = return subst + candidateSubsts subst ((GAction a):as) = do sysAct <- sysActions subst' <- (`runReader` hnd) $ matchAction sysAct (applySkAction subst a) candidateSubsts (compose subst' subst) as + candidateSubsts subst ((GEqE eq):as) = do + let (s,t) = applySkTerm subst <$> eq + (term,pat) | frees s == [] = (s,t) + | frees t == [] = (t,s) + | otherwise = error $ "impliedFormulas: impossible, " + ++ "equality not guarded as checked" + ++"by 'Guarded.formulaToGuarded'." + subst' <- (`runReader` hnd) $ matchTerm term pat + candidateSubsts (compose subst' subst) as ------------------------------------------------------------------------------ @@ -451,6 +465,13 @@ matchAction :: (SkTerm, SkFact) -> (SkTerm, SkFact) -> WithMaude [SkSubst] matchAction (i1, fa1) (i2, fa2) = solveMatchLTerm sortOfSkol (i1 `matchWith` i2 <> fa1 `matchFact` fa2) + where + sortOfSkol (SkName n) = sortOfName n + sortOfSkol (SkConst v) = lvarSort v + +matchTerm :: SkTerm -> SkTerm -> WithMaude [SkSubst] +matchTerm s t = + solveMatchLTerm sortOfSkol (s `matchWith` t) where sortOfSkol (SkName n) = sortOfName n sortOfSkol (SkConst v) = lvarSort v diff --git a/src/Theory/Constraint/Solver/Types.hs b/src/Theory/Constraint/Solver/Types.hs --- a/src/Theory/Constraint/Solver/Types.hs +++ b/src/Theory/Constraint/Solver/Types.hs @@ -43,6 +43,8 @@ , cdGoal , cdCases + , prettyCaseDistinction + ) where import Prelude hiding (id, (.)) @@ -60,6 +62,7 @@ import Logic.Connectives import Theory.Constraint.System +import Theory.Text.Pretty import Theory.Model @@ -134,8 +137,21 @@ foldFrees f (L.get cdGoal th) `mappend` foldFrees f (L.get cdCases th) + foldFreesOcc _ _ = const mempty + mapFrees f th = CaseDistinction <$> mapFrees f (L.get cdGoal th) <*> mapFrees f (L.get cdCases th) + +-- Pretty printing +------------------ + +-- | Pretty print a case distinction +prettyCaseDistinction :: HighlightDocument d => CaseDistinction -> d +prettyCaseDistinction th = vcat $ + [ prettyGoal $ L.get cdGoal th ] + ++ map combine (zip [(1::Int)..] $ map snd . getDisj $ (L.get cdCases th)) + where + combine (i, sys) = fsep [keyword_ ("Case " ++ show i) <> colon, nest 2 (prettySystem sys)] -- NFData diff --git a/src/Theory/Constraint/System.hs b/src/Theory/Constraint/System.hs --- a/src/Theory/Constraint/System.hs +++ b/src/Theory/Constraint/System.hs @@ -174,7 +174,7 @@ , _sNextGoalNr :: Integer , _sCaseDistKind :: CaseDistKind } - -- NOTE: Don't forget the update 'substSystem' in + -- NOTE: Don't forget to update 'substSystem' in -- "Constraint.Solver.Reduction" when adding further fields to the -- constraint system. deriving( Eq, Ord ) @@ -380,8 +380,6 @@ isLast :: System -> NodeId -> Bool isLast sys i = Just i == L.get sLastAtom sys - - ------------------------------------------------------------------------------ -- Pretty printing -- ------------------------------------------------------------------------------ @@ -426,7 +424,6 @@ | otherwise = "" return $ prettyGoal goal <-> lineComment_ ("nr: " ++ show nr ++ loopBreaker) - -- Additional instances ----------------------- @@ -437,10 +434,12 @@ instance HasFrees CaseDistKind where foldFrees = const mempty + foldFreesOcc _ _ = const mempty mapFrees = const pure instance HasFrees GoalStatus where foldFrees = const mempty + foldFreesOcc _ _ = const mempty mapFrees = const pure instance HasFrees System where @@ -456,6 +455,20 @@ foldFrees fun i `mappend` foldFrees fun j `mappend` foldFrees fun k + + foldFreesOcc fun ctx (System a _b _c _d _e _f _g _h _i _j _k) = + foldFreesOcc fun ("a":ctx') a {- `mappend` + foldFreesCtx fun ("b":ctx') b `mappend` + foldFreesCtx fun ("c":ctx') c `mappend` + foldFreesCtx fun ("d":ctx') d `mappend` + foldFreesCtx fun ("e":ctx') e `mappend` + foldFreesCtx fun ("f":ctx') f `mappend` + foldFreesCtx fun ("g":ctx') g `mappend` + foldFreesCtx fun ("h":ctx') h `mappend` + foldFreesCtx fun ("i":ctx') i `mappend` + foldFreesCtx fun ("j":ctx') j `mappend` + foldFreesCtx fun ("k":ctx') k -} + where ctx' = "system":ctx mapFrees fun (System a b c d e f g h i j k) = System <$> mapFrees fun a diff --git a/src/Theory/Constraint/System/Constraints.hs b/src/Theory/Constraint/System/Constraints.hs --- a/src/Theory/Constraint/System/Constraints.hs +++ b/src/Theory/Constraint/System/Constraints.hs @@ -81,6 +81,7 @@ instance HasFrees Edge where foldFrees f (Edge x y) = foldFrees f x `mappend` foldFrees f y + foldFreesOcc f c (Edge x y) = foldFreesOcc f ("edge":c) (x, y) mapFrees f (Edge x y) = Edge <$> mapFrees f x <*> mapFrees f y @@ -143,6 +144,11 @@ ChainG c p -> foldFrees f c <> foldFrees f p SplitG i -> foldFrees f i DisjG x -> foldFrees f x + + foldFreesOcc f c goal = case goal of + ActionG i fa -> foldFreesOcc f ("ActionG":c) (i, fa) + ChainG co p -> foldFreesOcc f ("ChainG":c) (co, p) + _ -> mempty mapFrees f goal = case goal of ActionG i fa -> ActionG <$> mapFrees f i <*> mapFrees f fa diff --git a/src/Theory/Constraint/System/Guarded.hs b/src/Theory/Constraint/System/Guarded.hs --- a/src/Theory/Constraint/System/Guarded.hs +++ b/src/Theory/Constraint/System/Guarded.hs @@ -18,6 +18,7 @@ Guarded(..) , LGuarded , LNGuarded + , GAtom(..) -- ** Smart constructors , gfalse @@ -37,6 +38,9 @@ , mapGuardedAtoms + , atomToGAtom + , sortGAtoms + -- ** Queries , isConjunction , isDisjunction @@ -116,6 +120,7 @@ isAllGuarded (GGuarded All _ _ _) = True isAllGuarded _ = False + -- | Check whether the guarded formula is closed and does not contain an -- existential quantifier. This under-approximates the question whether the -- formula is a safety formula. A safety formula @phi@ has the property that a @@ -139,6 +144,28 @@ getTags _qua _ss atos inner = mconcat [ D.singleton tag | Action _ (Fact tag _) <- atos ] <> inner + +-- | Atoms that are allowed as guards. +data GAtom t = GEqE (t,t) | GAction (t,Fact t) + deriving (Eq, Show, Ord) + +isGAction :: GAtom t -> Bool +isGAction (GAction _) = True +isGAction _ = False + +-- | Convert 'Atom's to 'GAtom's, if possible. +atomToGAtom :: Show t => Atom t -> GAtom t +atomToGAtom = conv + where conv (EqE s t) = GEqE (s,t) + conv (Action i f) = GAction (i,f) + conv a = error $ "atomsToGAtom: "++ show a + ++ "is not a guarded atom." + +-- | Stable sort that ensures that actions occur before equations. +sortGAtoms :: [GAtom t] -> [GAtom t] +sortGAtoms = uncurry (++) . partition isGAction + + ------------------------------------------------------------------------------ -- Folding ------------------------------------------------------------------------------ @@ -215,8 +242,9 @@ (\qua ss as gf -> GGuarded qua ss <$> traverse (traverse (traverseTerm (traverse (traverse f)))) as <*> gf) instance Ord c => HasFrees (Guarded (String, LSort) c LVar) where - foldFrees f = foldMap (foldFrees f) - mapFrees f = traverseGuarded (mapFrees f) + foldFrees f = foldMap (foldFrees f) + foldFreesOcc _ _ = const mempty + mapFrees f = traverseGuarded (mapFrees f) -- FIXME: remove name hints for variables for saturation? @@ -279,7 +307,7 @@ ------------------------------------------------------------------------------ -- | @openGuarded gf@ returns @Just (qua,vs,ats,gf')@ if @gf@ is a guarded --- clause and @Nothing@ otherwise. In the first case, @quao@ is the quantifier, +-- clause and @Nothing@ otherwise. In the first case, @qua@ is the quantifier, -- @vs@ is a list of fresh variables, @ats@ is the antecedent, and @gf'@ is the -- succedent. In both antecedent and succedent, the bound variables are -- replaced by @vs@. @@ -351,7 +379,7 @@ gfs | any (gtrue ==) gfs -> gtrue -- FIXME: Consider using 'sortednub' here. This yields stronger -- normalizaton for formulas. However, it also means that we loose - -- invariance under renaming free variables, as the order changes, + -- invariance under renaming of free variables, as the order changes, -- when they are renamed. | otherwise -> GDisj $ Disj $ nub gfs where @@ -440,35 +468,50 @@ , ppFormula f0 ] - conjActions (Conn And f1 f2) = conjActions f1 ++ conjActions f2 - conjActions (Ato a@(Action _ _)) = [Left $ bvarToLVar a] - conjActions f = [Right f] + conjActionsEqs (Conn And f1 f2) = conjActionsEqs f1 ++ conjActionsEqs f2 + conjActionsEqs (Ato a@(Action _ _)) = [Left $ bvarToLVar a] + conjActionsEqs (Ato e@(EqE _ _)) = [Left $ bvarToLVar e] + conjActionsEqs f = [Right f] + -- Given a list of unguarded variables and a list of atoms, compute the + -- remaining unguarded variables that are not guarded by the given atoms. + remainingUnguarded ug0 atoms = + go ug0 (sortGAtoms . map atomToGAtom $ atoms) + where go ug [] = ug + go ug ((GAction a) :gatoms) = go (ug \\ frees a) gatoms + -- FIXME: We do not consider the terms, e.g., for ug=[x,y], + -- s=pair(x,a), and t=pair(b,y), we could define ug'=[]. + go ug ((GEqE (s,t)):gatoms) = go ug' gatoms + where ug' | covered s ug = ug \\ frees t + | covered t ug = ug \\ frees s + | otherwise = ug + covered a vs = frees a `intersect` vs == [] + convEx qua = do (xs,_,f) <- openFormulaPrefix f0 - case partitionEithers $ conjActions f of - (as, fs) -> do - -- all existentially quantified variables must be guarded - noUnguardedVars (xs \\ frees as) - -- convert all other formulas - gf <- (if polarity then gdisj else gconj) - <$> mapM (convert polarity) fs - return $ closeGuarded qua xs as gf - where + let (as_eqs, fs) = partitionEithers $ conjActionsEqs f + -- all existentially quantified variables must be guarded + noUnguardedVars (remainingUnguarded xs as_eqs) + -- convert all other formulas + gf <- (if polarity then gdisj else gconj) + <$> mapM (convert polarity) fs + return $ closeGuarded qua xs (as_eqs) gf + convAll qua = do (xs,_,f) <- openFormulaPrefix f0 case f of - Conn Imp ante suc -> case partitionEithers $ conjActions ante of - (as, fs) -> do + Conn Imp ante suc -> do + let (as_eqs, fs) = partitionEithers $ conjActionsEqs ante + -- all universally quantified variables must be guarded - noUnguardedVars (xs \\ frees as) + noUnguardedVars (remainingUnguarded xs (as_eqs)) -- negate formulas in antecedent and combine with body gf <- (if polarity then gconj else gdisj) <$> sequence ( map (convert (not polarity)) fs ++ [convert polarity suc] ) - return $ closeGuarded qua xs as gf + return $ closeGuarded qua xs as_eqs gf _ -> throwError $ text "universal quantifier without toplevel implication" $-$ @@ -484,7 +527,7 @@ -- | Negate a guarded formula. gnot :: (Ord s, Ord c, Ord v) - => Guarded s c v -> Guarded s c v + => Guarded s c v -> Guarded s c v gnot = go where @@ -535,7 +578,7 @@ -- | Try to prove the formula by applying induction over the trace. -- Returns @'Left' errMsg@ if this is not possible. Returns a tuple of --- formulas: one formalzing the proof obligation of the base-case and one +-- formulas: one formalizing the proof obligation of the base-case and one -- formalizing the proof obligation of the step-case. ginduct :: Ord c => LGuarded c -> Either String (LGuarded c, LGuarded c) ginduct gf = do @@ -587,7 +630,7 @@ annAtos = (\x -> (x, valuation =<< unbindAtom x)) <$> atos -- Note that existentials without quantifiers are already eliminated by - -- 'gex'. Moreover, we dealay simplification inside guarded all + -- 'gex'. Moreover, we delay simplification inside guarded all -- quantification and guarded existential quantifiers. Their body will be -- simplified once the quantifiers are gone. simp fm@(GGuarded _ _ _ _) = fm diff --git a/src/Theory/Model/Atom.hs b/src/Theory/Model/Atom.hs --- a/src/Theory/Model/Atom.hs +++ b/src/Theory/Model/Atom.hs @@ -44,7 +44,7 @@ import Data.DeriveTH import Data.Foldable (Foldable, foldMap) import Data.Generics -import Data.Monoid (mappend) +import Data.Monoid (mappend, mempty) import Data.Traversable import Term.LTerm @@ -100,6 +100,7 @@ instance HasFrees t => HasFrees (Atom t) where foldFrees f = foldMap (foldFrees f) + foldFreesOcc _ _ = const mempty -- we ignore occurences in atoms for now mapFrees f = traverse (mapFrees f) instance Apply LNAtom where diff --git a/src/Theory/Model/Fact.hs b/src/Theory/Model/Fact.hs --- a/src/Theory/Model/Fact.hs +++ b/src/Theory/Model/Fact.hs @@ -128,6 +128,7 @@ instance HasFrees t => HasFrees (Fact t) where foldFrees f = foldMap (foldFrees f) + foldFreesOcc f c fa = foldFreesOcc f ((show $ factTag fa):c) (factTerms fa) mapFrees f = traverse (mapFrees f) instance Apply t => Apply (Fact t) where diff --git a/src/Theory/Model/Formula.hs b/src/Theory/Model/Formula.hs --- a/src/Theory/Model/Formula.hs +++ b/src/Theory/Model/Formula.hs @@ -234,6 +234,7 @@ instance HasFrees LNFormula where foldFrees f = foldMap (foldFrees f) + foldFreesOcc _ _ = const mempty -- we ignore occurences in Formulas for now mapFrees f = traverseFormula (mapFrees f) instance Apply LNFormula where diff --git a/src/Theory/Model/Rule.hs b/src/Theory/Model/Rule.hs --- a/src/Theory/Model/Rule.hs +++ b/src/Theory/Model/Rule.hs @@ -72,6 +72,7 @@ -- ** Conversion , ruleACToIntrRuleAC , ruleACIntrToRuleAC + , ruleACIntrToRuleACInst -- ** Construction , someRuleACInst @@ -176,13 +177,14 @@ instance Functor Rule where fmap f (Rule i ps cs as) = Rule (f i) ps cs as -instance HasFrees i => HasFrees (Rule i) where +instance (Show i, HasFrees i) => HasFrees (Rule i) where foldFrees f (Rule i ps cs as) = (foldFrees f i `mappend`) $ (foldFrees f ps `mappend`) $ (foldFrees f cs `mappend`) $ (foldFrees f as) - + foldFreesOcc f c (Rule i ps cs as) = + foldFreesOcc f ((show i):c) (ps, cs, as) mapFrees f (Rule i ps cs as) = Rule <$> mapFrees f i <*> mapFrees f ps <*> mapFrees f cs <*> mapFrees f as @@ -216,7 +218,7 @@ instance (HasFrees p, HasFrees i) => HasFrees (RuleInfo p i) where foldFrees f = ruleInfo (foldFrees f) (foldFrees f) - + foldFreesOcc _ _ = const mempty mapFrees f = ruleInfo (fmap ProtoInfo . mapFrees f) (fmap IntrInfo . mapFrees f) @@ -265,6 +267,7 @@ instance HasFrees ProtoRuleName where foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty mapFrees _ = pure instance Apply PremIdx where @@ -272,6 +275,7 @@ instance HasFrees PremIdx where foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty mapFrees _ = pure instance Apply ConcIdx where @@ -279,13 +283,14 @@ instance HasFrees ConcIdx where foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty mapFrees _ = pure instance HasFrees ProtoRuleACInfo where foldFrees f (ProtoRuleACInfo na vari breakers) = foldFrees f na `mappend` foldFrees f vari `mappend` foldFrees f breakers - + foldFreesOcc _ _ = const mempty mapFrees f (ProtoRuleACInfo na vari breakers) = ProtoRuleACInfo na <$> mapFrees f vari <*> mapFrees f breakers @@ -296,6 +301,8 @@ foldFrees f (ProtoRuleACInstInfo na breakers) = foldFrees f na `mappend` foldFrees f breakers + foldFreesOcc _ _ = const mempty + mapFrees f (ProtoRuleACInstInfo na breakers) = ProtoRuleACInstInfo na <$> mapFrees f breakers @@ -327,6 +334,10 @@ ruleACIntrToRuleAC :: IntrRuleAC -> RuleAC ruleACIntrToRuleAC (Rule ri ps cs as) = Rule (IntrInfo ri) ps cs as +-- | Converts between these two types of rules. +ruleACIntrToRuleACInst :: IntrRuleAC -> RuleACInst +ruleACIntrToRuleACInst (Rule ri ps cs as) = Rule (IntrInfo ri) ps cs as + -- Instances ------------ @@ -335,6 +346,7 @@ instance HasFrees IntrRuleACInfo where foldFrees _ = const mempty + foldFreesOcc _ _ = const mempty mapFrees _ = pure diff --git a/src/Theory/Proof.hs b/src/Theory/Proof.hs --- a/src/Theory/Proof.hs +++ b/src/Theory/Proof.hs @@ -165,6 +165,7 @@ instance HasFrees a => HasFrees (ProofStep a) where foldFrees f (ProofStep m i) = foldFrees f m `mappend` foldFrees f i + foldFreesOcc _ _ = const mempty mapFrees f (ProofStep m i) = ProofStep <$> mapFrees f m <*> mapFrees f i ------------------------------------------------------------------------------ diff --git a/src/Theory/Text/Parser.hs b/src/Theory/Text/Parser.hs --- a/src/Theory/Text/Parser.hs +++ b/src/Theory/Text/Parser.hs @@ -11,7 +11,7 @@ parseOpenTheory , parseOpenTheoryString , parseLemma - , parseIntruderRulesDH + , parseIntruderRules ) where import Prelude hiding (id, (.)) @@ -51,8 +51,8 @@ parseOpenTheory flags = parseFile (theory flags) -- | Parse DH intruder rules. -parseIntruderRulesDH :: FilePath -> IO [IntrRuleAC] -parseIntruderRulesDH = parseFile (setState dhMaudeSig >> many intrRule) +parseIntruderRules :: MaudeSig -> FilePath -> IO [IntrRuleAC] +parseIntruderRules msig = parseFile (setState msig >> many intrRule) -- | Parse a security protocol theory from a string. parseOpenTheoryString :: [String] -- ^ Defined flags. @@ -73,18 +73,18 @@ -- | Lookup the arity of a non-ac symbol. Fails with a sensible error message -- if the operator is not known. -lookupNonACArity :: String -> Parser Int -lookupNonACArity op = do +lookupArity :: String -> Parser (Int, Privacy) +lookupArity op = do maudeSig <- getState - case lookup (BC.pack op) (S.toList $ allFunctionSymbols maudeSig) of - Nothing -> fail $ "unknown operator `" ++ op ++ "'" - Just k -> return k + case lookup (BC.pack op) (S.toList (noEqFunSyms maudeSig) ++ [(emapSymString, (2,Public))]) of + Nothing -> fail $ "unknown operator `" ++ op ++ "'" + Just (k,priv) -> return (k,priv) -- | Parse an n-ary operator application for arbitrary n. naryOpApp :: Ord l => Parser (Term l) -> Parser (Term l) naryOpApp plit = do op <- identifier - k <- lookupNonACArity op + (k,priv) <- lookupArity op ts <- parens $ if k == 1 then return <$> tupleterm plit else commaSep (multterm plit) @@ -92,18 +92,19 @@ when (k /= k') $ fail $ "operator `" ++ op ++"' has arity " ++ show k ++ ", but here it is used with arity " ++ show k' - return $ fAppNonAC (BC.pack op, k') ts + let app o = if BC.pack op == emapSymString then fAppC EMap else fAppNoEq o + return $ app (BC.pack op, (k,priv)) ts -- | Parse a binary operator written as @op{arg1}arg2@. binaryAlgApp :: Ord l => Parser (Term l) -> Parser (Term l) binaryAlgApp plit = do op <- identifier - k <- lookupNonACArity op + (k,priv) <- lookupArity op arg1 <- braced (tupleterm plit) arg2 <- term plit when (k /= 2) $ fail $ "only operators of arity 2 can be written using the `op{t1}t2' notation" - return $ fAppNonAC (BC.pack op, 2) [arg1, arg2] + return $ fAppNoEq (BC.pack op, (2,priv)) [arg1, arg2] -- | Parse a term. term :: Ord l => Parser (Term l) -> Parser (Term l) @@ -122,19 +123,27 @@ nullaryApp = do maudeSig <- getState -- FIXME: This try should not be necessary. - asum [ try (symbol (BC.unpack sym)) *> pure (fApp (NonAC (sym,0)) []) - | (sym,0) <- S.toList $ allFunctionSymbols maudeSig ] + asum [ try (symbol (BC.unpack sym)) *> pure (fApp (NoEq (sym,(0,priv))) []) + | NoEq (sym,(0,priv)) <- S.toList $ funSyms maudeSig ] -- | A left-associative sequence of exponentations. expterm :: Ord l => Parser (Term l) -> Parser (Term l) -expterm plit = chainl1 (term plit) ((\a b -> fAppExp (a,b)) <$ opExp) +expterm plit = chainl1 (msetterm plit) ((\a b -> fAppExp (a,b)) <$ opExp) -- | A left-associative sequence of multiplications. multterm :: Ord l => Parser (Term l) -> Parser (Term l) multterm plit = do dh <- enableDH <$> getState if dh -- if DH is not enabled, do not accept 'multterm's and 'expterm's - then chainl1 (expterm plit) ((\a b -> fAppMult [a,b]) <$ opMult) + then chainl1 (expterm plit) ((\a b -> fAppAC Mult [a,b]) <$ opMult) + else msetterm plit + +-- | A left-associative sequence of multiset unions. +msetterm :: Ord l => Parser (Term l) -> Parser (Term l) +msetterm plit = do + mset <- enableMSet <$> getState + if mset -- if multiset is not enabled, do not accept 'msetterms's + then chainl1 (term plit) ((\a b -> fAppAC Union [a,b]) <$ opPlus) else term plit -- | A right-associative sequence of tuples. @@ -524,6 +533,10 @@ builtinTheory = asum [ try (symbol "diffie-hellman") *> extendSig dhMaudeSig + , try (symbol "bilinear-pairing") + *> extendSig bpMaudeSig + , try (symbol "multiset") + *> extendSig msetMaudeSig , try (symbol "symmetric-encryption") *> extendSig symEncMaudeSig , try (symbol "asymmetric-encryption") @@ -541,13 +554,14 @@ functionSymbol = do f <- BC.pack <$> identifier <* opSlash k <- fromIntegral <$> natural + priv <- option Public (symbol "[private]" *> pure Private) sig <- getState - case lookup f (S.toList $ allFunctionSymbols sig) of - Just k' | k' /= k -> - fail $ "conflicting arities " ++ - show k' ++ " and " ++ show k ++ + case lookup f [ o | o <- (S.toList $ stFunSyms sig)] of + Just kp' | kp' /= (k,priv) -> + fail $ "conflicting arities/private " ++ + show kp' ++ " and " ++ show (k,priv) ++ " for `" ++ BC.unpack f - _ -> setState (addFunctionSymbol (f,k) sig) + _ -> setState (addFunSym (f,(k,priv)) sig) equations :: Parser () equations = @@ -630,5 +644,3 @@ liftedAddAxiom thy ax = case addAxiom ax thy of Just thy' -> return thy' Nothing -> fail $ "duplicate axiom: " ++ get axName ax - - diff --git a/src/Theory/Text/Parser/Token.hs b/src/Theory/Text/Parser/Token.hs --- a/src/Theory/Text/Parser/Token.hs +++ b/src/Theory/Text/Parser/Token.hs @@ -59,6 +59,7 @@ , opBang , opSlash , opMinus + , opPlus , opLeftarrow , opRightarrow , opLongleftarrow @@ -259,7 +260,6 @@ LSortPub -> void $ char '$' LSortFresh -> void $ char '~' LSortNode -> void $ char '#' - LSortMSet -> void $ char '%' (n, i) <- indexedIdentifier return (LVar n s i) @@ -269,7 +269,7 @@ -- | Parse a non-node variable. msgvar :: Parser LVar -msgvar = sortedLVar [LSortFresh, LSortPub, LSortMsg, LSortMSet] +msgvar = sortedLVar [LSortFresh, LSortPub, LSortMsg] -- | Parse a graph node variable. nodevar :: Parser NodeId @@ -297,6 +297,10 @@ -- | The multiplication operator @*@. opMult :: Parser () opMult = symbol_ "*" + +-- | The multiplication operator @*@. +opPlus :: Parser () +opPlus = symbol_ "+" -- | The timepoint comparison operator @<@. opLess :: Parser () diff --git a/src/Theory/Tools/AbstractInterpretation.hs b/src/Theory/Tools/AbstractInterpretation.hs --- a/src/Theory/Tools/AbstractInterpretation.hs +++ b/src/Theory/Tools/AbstractInterpretation.hs @@ -41,7 +41,7 @@ -- | Higher-order combinator to construct abstract interpreters. interpretAbstractly - :: (Eq s, HasFrees i, Apply i) + :: (Eq s, HasFrees i, Apply i, Show i) => ([Equal LNFact] -> [LNSubstVFresh]) -- ^ Unification of equalities over facts. We assume that facts with -- different tags are never unified. @@ -128,7 +128,7 @@ absTerm t = case viewTerm t of Lit (Con _) -> pure t - FApp (sym@(NonAC (_f,_k))) ts + FApp (sym@(NoEq _)) ts -> fApp sym <$> traverse absTerm ts _ -> importBinding mkVar t (varName t) where diff --git a/src/Theory/Tools/EquationStore.hs b/src/Theory/Tools/EquationStore.hs --- a/src/Theory/Tools/EquationStore.hs +++ b/src/Theory/Tools/EquationStore.hs @@ -36,6 +36,7 @@ -- ** Case splitting , performSplit + , dropNameHintsBound , splits , splitSize @@ -54,6 +55,7 @@ import Theory.Text.Pretty import Control.Monad.Fresh +import Control.Monad.Bind import Control.Monad.Reader import Extension.Prelude import Utils.Misc @@ -121,10 +123,18 @@ eqsIsFalse = any ((S.empty == ) . snd) . getConj . L.get eqsConj -- | The false conjunction. It is always identified with split number -1. -falseEqConstrConj :: Conj (SplitId, S.Set (LNSubstVFresh)) +falseEqConstrConj :: Conj (SplitId, S.Set LNSubstVFresh) falseEqConstrConj = Conj [ (SplitId (-1), S.empty) ] +dropNameHintsBound :: EqStore -> EqStore +dropNameHintsBound = modify eqsConj (Conj . map (second (S.map dropNameHintsLNSubstVFresh)) . getConj) +dropNameHintsLNSubstVFresh :: LNSubstVFresh -> LNSubstVFresh +dropNameHintsLNSubstVFresh subst = + substFromListVFresh $ zip (map fst slist) + ((`evalFresh` nothingUsed) . (`evalBindT` noBindings) $ renameDropNamehint (map snd slist)) + where slist = substToListVFresh subst + -- Instances ------------ @@ -134,6 +144,7 @@ instance HasFrees EqStore where foldFrees f (EqStore subst substs nextSplitId) = foldFrees f subst <> foldFrees f substs <> foldFrees f nextSplitId + foldFreesOcc _ _ = const mempty mapFrees f (EqStore subst substs nextSplitId) = EqStore <$> mapFrees f subst <*> mapFrees f substs @@ -296,7 +307,7 @@ -- names for variables from the underlying 'MonadFresh'. simpDisjunction :: MonadFresh m => MaudeHandle - -> (LNSubstVFresh -> Bool) + -> (LNSubst -> LNSubstVFresh -> Bool) -> Disj LNSubstVFresh -> m (LNSubst, Maybe [LNSubstVFresh]) simpDisjunction hnd isContr disj0 = do @@ -315,7 +326,7 @@ ---------------------------------------------------------------------- -- | @simp eqStore@ simplifies the equation store. -simp :: MonadFresh m => MaudeHandle -> (LNSubstVFresh -> Bool) -> EqStore -> m EqStore +simp :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> EqStore -> m EqStore simp hnd isContr eqStore = execStateT (whileTrue (simp1 hnd isContr)) (trace (show ("eqStore", eqStore)) eqStore) @@ -324,13 +335,13 @@ -- | @simp1@ tries to execute one simplification step -- for the equation store. It returns @True@ if -- the equation store was modified. -simp1 :: MonadFresh m => MaudeHandle -> (LNSubstVFresh -> Bool) -> StateT EqStore m Bool +simp1 :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> StateT EqStore m Bool simp1 hnd isContr = do - s <- MS.get - if eqsIsFalse s + eqs <- MS.get + if eqsIsFalse eqs then return False else do - b1 <- simpMinimize isContr + b1 <- simpMinimize (isContr (L.get eqsSubst eqs)) b2 <- simpRemoveRenamings b3 <- simpEmptyDisj b4 <- foreachDisj hnd simpSingleton diff --git a/src/Theory/Tools/IntruderRules.hs b/src/Theory/Tools/IntruderRules.hs --- a/src/Theory/Tools/IntruderRules.hs +++ b/src/Theory/Tools/IntruderRules.hs @@ -12,7 +12,15 @@ module Theory.Tools.IntruderRules ( subtermIntruderRules , dhIntruderRules + , bpIntruderRules + , multisetIntruderRules + , mkDUnionRule , specialIntruderRules + + -- ** Classifiers + , isDExpRule + , isDEMapRule + , isDPMultRule ) where import Control.Basics @@ -20,6 +28,7 @@ import Data.List import qualified Data.Set as S +import Data.ByteString (ByteString) import Extension.Data.Label @@ -30,6 +39,7 @@ import Term.Rewriting.Norm import Term.SubtermRule import Term.Positions +import Term.Subsumption import Theory.Model @@ -46,20 +56,20 @@ {- These are the special intruder that are always included. -rule (modulo AC) coerce: - [ KD( f_, x ) ] --[ KU( f_, x) ]-> [ KU( f_, x ) ] +rule coerce: + [ KD( x ) ] --[ KU( x ) ]-> [ KU( x ) ] -rule (modulo AC) pub: - [ ] --[ KU( f_, $x) ]-> [ KU( f_, $x ) ] +rule pub: + [ ] --[ KU( $x ) ]-> [ KU( $x ) ] -rule (modulo AC) gen_fresh: - [ Fr( ~x ) ] --[ KU( 'noexp', ~x ) ]-> [ KU( 'noexp', ~x ) ] +rule gen_fresh: + [ Fr( ~x ) ] --[ KU( ~x ) ]-> [ KU( ~x ) ] -rule (modulo AC) isend: - [ KU( f_, x) ] --[ K(x) ]-> [ In(x) ] +rule isend: + [ KU( x) ] --[ K( x ) ]-> [ In( x ) ] -rule (modulo AC) irecv: - [ Out( x) ] --> [ KD( 'exp', x) ] +rule irecv: + [ Out( x) ] --> [ KD( x ) ] -} -- | @specialIntruderRules@ returns the special intruder rules that are @@ -87,7 +97,7 @@ -- | @destuctionRules st@ returns the destruction rules for the given -- subterm rule @st@ destructionRules :: StRule -> [IntrRuleAC] -destructionRules (StRule lhs@(viewTerm -> FApp (NonAC (f,_)) _) (RhsPosition pos)) = +destructionRules (StRule lhs@(viewTerm -> FApp (NoEq (f,_)) _) (RhsPosition pos)) = go [] lhs pos where rhs = lhs `atPos` pos @@ -128,17 +138,17 @@ subtermIntruderRules :: MaudeSig -> [IntrRuleAC] subtermIntruderRules maudeSig = minimizeIntruderRules $ concatMap destructionRules (S.toList $ stRules maudeSig) - ++ constructionRules (functionSymbols maudeSig) + ++ constructionRules (stFunSyms maudeSig) -- | @constructionRules fSig@ returns the construction rules for the given -- function signature @fSig@ -constructionRules :: FunSig -> [IntrRuleAC] +constructionRules :: NoEqFunSig -> [IntrRuleAC] constructionRules fSig = - [ createRule s k | (s,k) <- S.toList fSig ] + [ createRule s k | (s,(k,Public)) <- S.toList fSig ] where createRule s k = Rule (ConstrRule s) (map kuFact vars) [concfact] [concfact] - where vars = take k [ varTerm (LVar "x" LSortMsg i) | i<- [0..] ] - m = fApp (NonAC (s,k)) vars + where vars = take k [ varTerm (LVar "x" LSortMsg i) | i <- [0..] ] + m = fAppNoEq (s,(k,Public)) vars concfact = kuFact m @@ -152,7 +162,7 @@ [ expRule ConstrRule kuFact return , invRule ConstrRule kuFact return ] ++ - concatMap (variantsIntruder hnd) + concatMap (variantsIntruder hnd id) [ expRule DestrRule kdFact (const []) , invRule DestrRule kdFact (const []) ] @@ -172,17 +182,17 @@ Rule (mkInfo invSymString) [bfact] [concfact] (mkAction concfact) where bfact = kudFact x_var_0 - conc = fAppInv x_var_0 + conc = fAppInv x_var_0 concfact = kudFact conc -- | @variantsIntruder mh irule@ computes the deconstruction-variants -- of a given intruder rule @irule@ -variantsIntruder :: MaudeHandle -> IntrRuleAC -> [IntrRuleAC] -variantsIntruder hnd ru = do +variantsIntruder :: MaudeHandle -> ([LNSubstVFresh] -> [LNSubstVFresh]) -> IntrRuleAC -> [IntrRuleAC] +variantsIntruder hnd minimizeVariants ru = do let ruleTerms = concatMap factTerms (get rPrems ru++get rConcs ru++get rActs ru) - fsigma <- computeVariants (fAppList ruleTerms) `runReader` hnd + fsigma <- minimizeVariants $ computeVariants (fAppList ruleTerms) `runReader` hnd let sigma = freshToFree fsigma `evalFreshAvoiding` ruleTerms ruvariant = normRule' (apply sigma ru) `runReader` hnd guard (frees (get rConcs ruvariant) /= [] && @@ -196,10 +206,99 @@ case concatMap factTerms $ get rConcs ruvariant of [viewTerm -> FApp (AC Mult) _] -> fail "Rules with product conclusion are redundant" - _ -> return ruvariant + _ -> return ruvariant -- | @normRule irule@ computes the normal form of @irule@ normRule' :: IntrRuleAC -> WithMaude IntrRuleAC normRule' (Rule i ps cs as) = reader $ \hnd -> let normFactTerms = map (fmap (\t -> norm' t `runReader` hnd)) in Rule i (normFactTerms ps) (normFactTerms cs) (normFactTerms as) + +------------------------------------------------------------------------------ +-- Multiset intruder rules +------------------------------------------------------------------------------ + +multisetIntruderRules :: [IntrRuleAC] +multisetIntruderRules = [mkDUnionRule [x_var, y_var] x_var] + where x_var = varTerm (LVar "x" LSortMsg 0) + y_var = varTerm (LVar "y" LSortMsg 0) + +mkDUnionRule :: [LNTerm] -> LNTerm -> IntrRuleAC +mkDUnionRule t_prems t_conc = + Rule (DestrRule unionSymString) + [kdFact $ fAppAC Union t_prems] + [kdFact t_conc] [] + +------------------------------------------------------------------------------ +-- Bilinear Pairing Intruder rules. +------------------------------------------------------------------------------ + +bpIntruderRules :: WithMaude [IntrRuleAC] +bpIntruderRules = reader $ \hnd -> minimizeIntruderRules $ + [ pmultRule ConstrRule kuFact return + , emapRule ConstrRule kuFact return + ] + ++ -- pmult is similar to exp + (variantsIntruder hnd id $ pmultRule DestrRule kdFact (const [])) + ++ -- emap is different + (bpVariantsIntruder hnd $ emapRule DestrRule kdFact (const []) ) + + where + + x_var_0 = varTerm (LVar "x" LSortMsg 0) + x_var_1 = varTerm (LVar "x" LSortMsg 1) + + pmultRule mkInfo kudFact mkAction = + Rule (mkInfo pmultSymString) [bfact, efact] [concfact] (mkAction concfact) + where + bfact = kudFact x_var_0 + efact = kuFact x_var_1 + conc = fAppPMult (x_var_1, x_var_0) + concfact = kudFact conc + + emapRule mkInfo kudFact mkAction = + Rule (mkInfo emapSymString) [bfact, efact] [concfact] (mkAction concfact) + where + bfact = kudFact x_var_0 + efact = kudFact x_var_1 + conc = fAppEMap (x_var_0, x_var_1) + concfact = kudFact conc + +bpVariantsIntruder :: MaudeHandle -> IntrRuleAC -> [IntrRuleAC] +bpVariantsIntruder hnd ru = do + ruvariant <- variantsIntruder hnd minimizeVariants ru + + -- For the rules "x, pmult(y,z) -> em(x,z)^y" and + -- "pmult(y,z),x -> em(z,x)^y", we + -- have to make x a KU premise. Here we rely on the + -- fact that all other variants are of the form + -- "pmult(..), pmult(..) -> em(..)" + case ruvariant of + Rule i [Fact KDFact args@[viewTerm -> Lit (Var _)], yfact] concs actions -> + return $ Rule i [Fact KUFact args, yfact] concs actions + Rule i [yfact, Fact KDFact args@[viewTerm -> Lit (Var _)]] concs actions -> + return $ Rule i [yfact, Fact KUFact args] concs actions + _ -> return ruvariant + + where + minimizeVariants = nub . map canonize + canonize subst = canonizeSubst . substFromListVFresh $ zip doms (sort rngs) + where + mappings = substToListVFresh subst + doms = map fst mappings + rngs = map snd mappings + +------------------------------------------------------------------------------ +-- Classification functions +------------------------------------------------------------------------------ + +isDRule :: ByteString -> Rule (RuleInfo t IntrRuleACInfo) -> Bool +isDRule ruString ru = case get rInfo ru of + IntrInfo (DestrRule n) | n == ruString -> True + _ -> False + +isDExpRule, isDPMultRule, isDEMapRule + :: Rule (RuleInfo t IntrRuleACInfo) -> Bool +isDExpRule = isDRule expSymString +isDPMultRule = isDRule pmultSymString +isDEMapRule = isDRule emapSymString diff --git a/src/Theory/Tools/RuleVariants.hs b/src/Theory/Tools/RuleVariants.hs --- a/src/Theory/Tools/RuleVariants.hs +++ b/src/Theory/Tools/RuleVariants.hs @@ -31,8 +31,21 @@ import qualified Data.Set as S import Data.Traversable (traverse) -import Debug.Trace.Ignore +-- import Utils.Misc (stringSHA256) + +-- import System.IO.Unsafe +-- import System.IO +-- import System.Directory +-- import qualified Data.Binary as B +-- import qualified Data.ByteString.Lazy as BS +import Debug.Trace.Ignore + + +tmpdir :: FilePath +tmpdir = "/tmp/tamarin/" + + -- Variants of protocol rules ---------------------------------------------------------------------- @@ -52,7 +65,7 @@ let eqsAbstr = map swap (M.toList bindings) abstractedTerms = map snd eqsAbstr abstractionSubst = substFromList eqsAbstr - variantSubsts = computeVariants (fAppList abstractedTerms) `runReader` hnd + variantSubsts = computeVariantsCached (fAppList abstractedTerms) hnd substs = [ restrictVFresh (frees abstrPsCsAs) $ removeRenamings $ ((`runReader` hnd) . normSubstVFresh') $ composeVFresh vsubst abstractionSubst @@ -62,7 +75,7 @@ [] -> error $ "variantsProtoRule: rule has no variants `"++show ru++"'" _ -> do -- x <- return (emptySubst, Just substs) -- - x <- simpDisjunction hnd (const False) (Disj substs) + x <- simpDisjunction hnd (const (const False)) (Disj substs) case trace (show ("SIMP",abstractedTerms, "abstr", abstrPsCsAs, "substs", substs, @@ -80,10 +93,10 @@ <*> mapM abstrFact concs0 <*> mapM abstrFact acts0 - irreducible = irreducibleFunctionSymbols (mhMaudeSig hnd) + irreducible = irreducibleFunSyms (mhMaudeSig hnd) abstrFact = traverse abstrTerm - abstrTerm (viewTerm -> FApp (NonAC o) args) | o `S.member` irreducible = - fAppNonAC o <$> mapM abstrTerm args + abstrTerm (viewTerm -> FApp o args) | o `S.member` irreducible = + fApp o <$> mapM abstrTerm args abstrTerm t = do at :: LNTerm <- varTerm <$> importBinding (`LVar` sortOfLNTerm t) t (getHint t) return at @@ -98,3 +111,19 @@ freshSubsts = map (restrictVFresh (frees (prems, concs, acts))) freshSubsts0 trueDisj = [ emptySubstVFresh ] + +computeVariantsCached :: LNTerm -> MaudeHandle -> [LNSubstVFresh] +computeVariantsCached inp hnd = computeVariants inp `runReader` hnd +{- + unsafePerformIO $ do + createDirectoryIfMissing True tmpdir + let hashInput = tmpdir ++ stringSHA256 (show inp) + fEx <- doesFileExist hashInput + if fEx + then B.decodeFile hashInput + else do let result = computeVariants inp `runReader` hnd + (tmpFile,tmpHnd) <- openBinaryTempFile tmpdir "variants.tmp" + BS.hPut tmpHnd $ B.encode result + renameFile tmpFile hashInput + return result +-} diff --git a/src/Theory/Tools/Wellformedness.hs b/src/Theory/Tools/Wellformedness.hs --- a/src/Theory/Tools/Wellformedness.hs +++ b/src/Theory/Tools/Wellformedness.hs @@ -399,10 +399,16 @@ \ have forgotten a #-prefix. Sort prefixes can only be dropped where\ \ this is unambiguous." where + irreducible = irreducibleFunSyms $ get (sigpMaudeSig . thySignature) thy + offenders = filter (not . allowed) $ formulaTerms fm allowed (viewTerm -> Lit (Var (Bound _))) = True allowed (viewTerm -> Lit (Con (Name PubName _))) = True - allowed _ = False + -- we allow multiset union + allowed (viewTerm2 -> FUnion args) = all allowed args + -- we allow reducible function symbols + allowed (viewTerm -> FApp o args) | o `S.member` irreducible = all allowed args + allowed _ = False -- check that the formula can be converted to a guarded formula checkGuarded header fm = case formulaToGuarded fm of @@ -447,8 +453,8 @@ <*> mapM (traverse replaceAbstracted) acts <*> mapM (traverse replaceAbstracted) rhs - abstractTerm (viewTerm -> FApp (NonAC o) args) | o `S.member` irreducible = - fAppNonAC o <$> mapM abstractTerm args + abstractTerm (viewTerm -> FApp o args) | o `S.member` irreducible = + fApp o <$> mapM abstractTerm args abstractTerm (viewTerm -> Lit l) = return $ lit l abstractTerm t = varTerm <$> importBinding (`LVar` sortOfLNTerm t) t "x" @@ -476,7 +482,7 @@ , lvarSort v /= LSortPub ] - irreducible = irreducibleFunctionSymbols $ get (sigpMaudeSig . thySignature) thy + irreducible = irreducibleFunSyms $ get (sigpMaudeSig . thySignature) thy diff --git a/tamarin-prover-theory.cabal b/tamarin-prover-theory.cabal --- a/tamarin-prover-theory.cabal +++ b/tamarin-prover-theory.cabal @@ -2,7 +2,7 @@ cabal-version: >= 1.8 build-type: Simple -version: 0.8.2.0 +version: 0.8.4.0 license: GPL license-file: LICENSE category: Theorem Provers @@ -44,7 +44,7 @@ , containers >= 0.4.2 && < 0.5 , dlist == 0.5.* , mtl == 2.0.* - , cmdargs == 0.9.* + , cmdargs == 0.10.* , filepath >= 1.1 && < 1.4 , directory >= 1.0 && < 1.2 , process == 1.1.* @@ -60,8 +60,8 @@ , parallel == 3.2.* , HUnit == 1.2.* - , tamarin-prover-utils >= 0.8.2 && < 0.9 - , tamarin-prover-term >= 0.8.2 && < 0.9 + , tamarin-prover-utils >= 0.8.4 && < 0.9 + , tamarin-prover-term >= 0.8.4 && < 0.9 hs-source-dirs: src