tamarin-prover-theory 0.8.2.0 → 0.8.4.0
raw patch · 23 files changed
+822/−248 lines, 23 filesdep ~cmdargsdep ~tamarin-prover-termdep ~tamarin-prover-utilsnew-uploader
Dependency ranges changed: cmdargs, tamarin-prover-term, tamarin-prover-utils
Files
- src/Theory/Constraint/Solver/CaseDistinctions.hs +106/−38
- src/Theory/Constraint/Solver/Contradictions.hs +215/−44
- src/Theory/Constraint/Solver/Goals.hs +65/−30
- src/Theory/Constraint/Solver/ProofMethod.hs +44/−24
- src/Theory/Constraint/Solver/Reduction.hs +6/−2
- src/Theory/Constraint/Solver/Simplify.hs +29/−8
- src/Theory/Constraint/Solver/Types.hs +16/−0
- src/Theory/Constraint/System.hs +17/−4
- src/Theory/Constraint/System/Constraints.hs +6/−0
- src/Theory/Constraint/System/Guarded.hs +66/−23
- src/Theory/Model/Atom.hs +2/−1
- src/Theory/Model/Fact.hs +1/−0
- src/Theory/Model/Formula.hs +1/−0
- src/Theory/Model/Rule.hs +16/−4
- src/Theory/Proof.hs +1/−0
- src/Theory/Text/Parser.hs +35/−23
- src/Theory/Text/Parser/Token.hs +6/−2
- src/Theory/Tools/AbstractInterpretation.hs +2/−2
- src/Theory/Tools/EquationStore.hs +18/−7
- src/Theory/Tools/IntruderRules.hs +121/−22
- src/Theory/Tools/RuleVariants.hs +35/−6
- src/Theory/Tools/Wellformedness.hs +10/−4
- tamarin-prover-theory.cabal +4/−4
src/Theory/Constraint/Solver/CaseDistinctions.hs view
@@ -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 $
src/Theory/Constraint/Solver/Contradictions.hs view
@@ -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
src/Theory/Constraint/Solver/Goals.hs view
@@ -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.
src/Theory/Constraint/Solver/ProofMethod.hs view
@@ -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
src/Theory/Constraint/Solver/Reduction.hs view
@@ -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 ()
src/Theory/Constraint/Solver/Simplify.hs view
@@ -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
src/Theory/Constraint/Solver/Types.hs view
@@ -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
src/Theory/Constraint/System.hs view
@@ -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
src/Theory/Constraint/System/Constraints.hs view
@@ -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
src/Theory/Constraint/System/Guarded.hs view
@@ -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
src/Theory/Model/Atom.hs view
@@ -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
src/Theory/Model/Fact.hs view
@@ -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
src/Theory/Model/Formula.hs view
@@ -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
src/Theory/Model/Rule.hs view
@@ -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
src/Theory/Proof.hs view
@@ -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 ------------------------------------------------------------------------------
src/Theory/Text/Parser.hs view
@@ -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--
src/Theory/Text/Parser/Token.hs view
@@ -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 ()
src/Theory/Tools/AbstractInterpretation.hs view
@@ -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
src/Theory/Tools/EquationStore.hs view
@@ -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
src/Theory/Tools/IntruderRules.hs view
@@ -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
src/Theory/Tools/RuleVariants.hs view
@@ -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+-}
src/Theory/Tools/Wellformedness.hs view
@@ -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
tamarin-prover-theory.cabal view
@@ -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