module Scyther.Proof (
Proof(..)
, TrivReason(..)
, Rule(..)
, dfsProof
, shortestProof
, minimizeProof
, mapProofSequents
, prfSequent
, prfProto
, isAxiomProof
, isTrivialProof
, complete
, sound
, depends
, extractTypeInvariant
, ProofSize
, getProofSize
, missingProofSize
, proofSize
, existsPossibleAttack
, displayChainRule
) where
import Data.Function
import Data.Maybe
import Data.List
import Data.Monoid
import qualified Data.Set as S
import Data.Data
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Control.Monad.BoundedDFS
import Extension.Prelude
import Scyther.Facts
import qualified Scyther.Equalities as E
import Scyther.Sequent
data Proof =
Axiom Sequent
| PossibleAttack Sequent Sequent
| Missing Sequent String Bool
| Trivial Sequent TrivReason
| RuleApp Sequent Rule [Proof]
deriving( Eq, Show, Data, Typeable )
data TrivReason =
TrivContradictoryPremises
| TrivPremisesImplyConclusion
| TrivLongTermKeySecrecy Message
deriving( Eq, Show, Data, Typeable )
data Rule =
Saturate
| ForwardResolution (Named Sequent) E.Mapping
| ChainRule Message [(String, [Either TID AgentId])]
| SplitEq E.MsgEq [Bool]
| TypingCases [String]
deriving( Eq, Show, Data, Typeable )
isTrivialProof :: Proof -> Bool
isTrivialProof (Trivial _ _) = True
isTrivialProof _ = False
isAxiomProof :: Proof -> Bool
isAxiomProof (Axiom _) = True
isAxiomProof _ = False
prfSequent :: Proof -> Sequent
prfSequent (Axiom se) = se
prfSequent (PossibleAttack se _) = se
prfSequent (Missing se _ _) = se
prfSequent (Trivial se _) = se
prfSequent (RuleApp se _ _) = se
prfProto :: Proof -> Protocol
prfProto = seProto . prfSequent
byAssumption :: Monad m => Sequent -> m Proof
byAssumption se@(Sequent prem concl)
| proveFalse prem = return $ Trivial se TrivContradictoryPremises
| proveFormula prem concl = return $ Trivial se TrivPremisesImplyConclusion
| otherwise = case exploitLongTermKeySecrecy prem of
Just key -> return $ Trivial se (TrivLongTermKeySecrecy key)
Nothing -> fail $ "byAssumption: cannot prove conclusion from premises"
reuseOrder :: Formula -> Formula -> Ordering
reuseOrder (FAtom (ATyping typ1)) (FAtom (ATyping typ2)) = compare typ1 typ2
reuseOrder (FAtom (ATyping _)) _ = LT
reuseOrder _ (FAtom (ATyping _)) = GT
reuseOrder (FAtom AFalse) (FAtom AFalse) = EQ
reuseOrder (FAtom AFalse) _ = LT
reuseOrder _ (FAtom AFalse) = GT
reuseOrder f1 f2 = compare f1 f2
genericProof :: MonadPlus m
=> m ()
-> (Facts -> [Message])
-> [Named Sequent]
-> Sequent
-> m Proof
genericProof chainRuleMarker goals rawRules se0 =
case saturate se0 of
Just se1 -> (RuleApp se0 Saturate . return) `liftM` prove se1
Nothing -> prove se0
where
reusableRules :: [Named Sequent]
reusableRules = sortBy (reuseOrder `on` (seConcl . snd)) rawRules
reuseRule se rule = do
(mapping, optSequent) <- frule (snd rule) se
let mkProof = RuleApp se (ForwardResolution rule mapping)
case optSequent of
Nothing -> return $ return $ mkProof []
Just sequent -> return $ (mkProof . return) `liftM` prove sequent
useChainRule se m = do
chainRuleMarker
case chainRule se m of
Just cases -> do
let (info, sequents) = unzip cases
(RuleApp se (ChainRule m info)) `liftM` mapM prove sequents
Nothing -> return $ Missing se "prover stuck => no type invariant available" True
prove se =
case byAssumption se of
Just prf -> return prf
Nothing ->
case wellTypedCases se of
Just cases -> do
let (names, sequents) = unzip cases
RuleApp se (TypingCases names) `liftM` mapM prove sequents
Nothing ->
case msum (map (reuseRule se) reusableRules) of
Just mkPrf -> mkPrf
Nothing ->
case splittableEqs (sePrem se) of
eq:_ -> do
let sequents = splitEq eq se
RuleApp se (SplitEq eq (map isJust sequents)) `liftM`
mapM prove (catMaybes sequents)
[] ->
case goals (sePrem se) of
[] -> return $ PossibleAttack se se
ms -> msum $ map (useChainRule se) ms
dfsProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof
dfsProof Nothing heuristic rules se =
runUnboundedDFS $ genericProof (return ()) heuristic rules se
dfsProof (Just bound) heuristic rules se =
evalBoundedDFS (genericProof (updateCost succ) heuristic rules se) (<= bound) 0
shortestProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof
shortestProof optBound heuristic rules se =
evalBranchAndBound
(genericProof (updateCost (fmap succ)) heuristic rules se)
optBound
existsPossibleAttack :: (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof
existsPossibleAttack heuristic rules se =
findAttack =<< (runUnboundedDFS $ genericProof (return ()) heuristic rules se)
checkProof :: Sequent -> Proof -> Maybe Proof
checkProof se0 prf0 = evalStateT (go prf0) se0
where
mkSubproof se prf = put se >> go prf
go :: Proof -> StateT Sequent Maybe Proof
go (Missing _ reason showSequent) =
Missing <$> get <*> pure reason <*> pure showSequent
go prf@(Axiom seAxiom) = do
se <- get
guard (se == seAxiom)
return prf
go prf@(PossibleAttack seAttacked _) = do
se <- get
guard (se == seAttacked)
return prf
go (Trivial _ reason@TrivContradictoryPremises) = do
prem <- gets sePrem
guard (proveFalse prem)
Trivial <$> get <*> pure reason
go (Trivial _ reason@TrivPremisesImplyConclusion) = do
se <- get
guard (proveFormula (sePrem se) (seConcl se))
Trivial <$> get <*> pure reason
go (Trivial _ reason@(TrivLongTermKeySecrecy key)) = do
se <- get
case exploitLongTermKeySecrecy (sePrem se) of
Just key' -> do guard (key == key')
Trivial <$> get <*> pure reason
Nothing -> mzero
go (RuleApp _ Saturate [prf]) = do
se <- get
case saturate se of
Just se' -> (RuleApp se Saturate . return) <$> (put se' >> go prf)
Nothing -> go prf
go (RuleApp _ rule@(ForwardResolution thm mapping) prfs) = do
se <- get
let statePrem = sePrem se
guard (proveFacts statePrem (sePrem $ snd thm) mapping)
optSequent <- fruleInst (snd thm) mapping se
case optSequent of
Nothing -> do guard (null prfs)
return $ RuleApp se rule prfs
Just sequent -> case prfs of
[prf] -> (RuleApp se rule . return) `liftM` mkSubproof sequent prf
_ -> mzero
go (RuleApp _ rule@(ChainRule m info) prfs) = do
se <- get
guard (proveAtom (sePrem se) (AEv (Learn m)))
(info', sequents') <- unzip `liftM` chainRule se m
guard (info == info')
RuleApp <$> get <*> pure rule <*> zipWithM mkSubproof sequents' prfs
go (RuleApp _ rule@(SplitEq eq info) prfs) = do
se <- get
guard (eq `elem` splittableEqs (sePrem se))
let optSequents' = splitEq eq se
info' = map isJust optSequents'
sequents' = catMaybes optSequents'
guard (info == info')
RuleApp <$> get <*> pure rule <*> zipWithM mkSubproof sequents' prfs
go (RuleApp _ rule@(TypingCases info) prfs) = do
se <- get
(info', sequents') <- unzip `liftM` wellTypedCases se
guard (info == info')
RuleApp <$> get <*> pure rule <*> zipWithM mkSubproof sequents' prfs
go _ = mzero
findAttack :: Proof -> Maybe Proof
findAttack = fmap head . go . return
where
unvisited prf = Missing (prfSequent prf) "not yet investigated" False
go :: [Proof] -> Maybe [Proof]
go [] = Nothing
go (prf : prfs) = case prf of
RuleApp se rule subprfs ->
(do subprfs' <- go subprfs
return $ RuleApp se rule subprfs' : map unvisited prfs
) `mplus`
((unvisited prf :) `liftM` go prfs)
PossibleAttack _ _ -> return $ prf : map unvisited prfs
_ -> (unvisited prf :) `liftM` go prfs
complete :: Proof -> Bool
complete (Missing _ _ _) = False
complete (PossibleAttack _ _) = False
complete (RuleApp _ _ prfs) = all complete prfs
complete _ = True
sound :: Proof -> Bool
sound prf = complete prf && isJust (checkProof (prfSequent prf) prf)
minimizeProof :: Proof -> Proof
minimizeProof prf0 = fromMaybe prf0 $ do
prf <- go prf0
checkProof (prfSequent prf) prf
where
go (RuleApp se rule@(ForwardResolution _ _) [prf]) = do
prf' <- go prf
(checkProof se prf' <|> pure (RuleApp se rule [prf']))
go (RuleApp se rule prfs) =
RuleApp se rule <$> mapM go prfs
go prf = return prf
depends :: Proof -> S.Set (String, Protocol)
depends (RuleApp _ (ForwardResolution (name, se) _) prfs) =
S.insert (name, seProto se) $ S.unions $ map depends prfs
depends (RuleApp _ _ prfs) = S.unions $ map depends prfs
depends _ = S.empty
extractTypeInvariant :: Proof -> Maybe (Named Typing)
extractTypeInvariant (RuleApp _ (ForwardResolution (name, se) _) prfs) =
case destTypingFormula (seConcl se) of
Just typ -> return (name, typ)
Nothing -> msum $ map extractTypeInvariant prfs
extractTypeInvariant (RuleApp _ _ prfs) = msum $ map extractTypeInvariant prfs
extractTypeInvariant _ = mzero
newtype ProofSize = ProofSize (Sum Int, Sum Int, Sum Int)
deriving( Eq, Ord, Monoid )
instance Show ProofSize where
show s =
concat ["C:", show nChain, " F:", show nForward, " M:", show nMissing]
where
(nChain, nForward, nMissing) = getProofSize s
getProofSize :: ProofSize -> (Int, Int, Int)
getProofSize (ProofSize (nChain, nForward, nMissing)) =
(getSum nChain, getSum nForward, getSum nMissing)
missingProofSize :: ProofSize
missingProofSize = ProofSize (mempty, mempty, Sum 1)
proofSize :: Proof -> ProofSize
proofSize (Axiom _) = mempty
proofSize (PossibleAttack _ _) = mempty
proofSize (Trivial _ _) = mempty
proofSize (Missing _ _ _) = missingProofSize
proofSize (RuleApp _ rule prfs) = mconcat $
(case rule of
ChainRule _ _ -> pure $ ProofSize (Sum 1, mempty, mempty)
ForwardResolution _ _ -> pure $ ProofSize (mempty, Sum 1, mempty)
_ -> mempty
) ++ map proofSize prfs
mapProofSequents :: (Sequent -> Sequent) -> Proof -> Proof
mapProofSequents f = go
where
go (Axiom se) = Axiom (f se)
go (PossibleAttack se se') = PossibleAttack (f se) (f se')
go (Trivial se reason) = Trivial (f se) reason
go (Missing se reason hide) = Missing (f se) reason hide
go (RuleApp se rule prfs) = RuleApp (f se) rule (map go prfs)
displayChainRule :: Protocol -> Maybe Typing -> Proof
displayChainRule _ _ = error "displayChainRule: not yet upgraded"