A representation for proofs constructed using our security protocol verification theory.
- data Proof
- data TrivReason
- data Rule
- dfsProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof
- shortestProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof
- minimizeProof :: Proof -> Proof
- mapProofSequents :: (Sequent -> Sequent) -> Proof -> Proof
- prfSequent :: Proof -> Sequent
- prfProto :: Proof -> Protocol
- isAxiomProof :: Proof -> Bool
- isTrivialProof :: Proof -> Bool
- complete :: Proof -> Bool
- sound :: Proof -> Bool
- depends :: Proof -> Set (String, Protocol)
- extractTypeInvariant :: Proof -> Maybe (Named Typing)
- data ProofSize
- getProofSize :: ProofSize -> (Int, Int, Int)
- missingProofSize :: ProofSize
- proofSize :: Proof -> ProofSize
- existsPossibleAttack :: (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof
- displayChainRule :: Protocol -> Maybe Typing -> Proof
A proof of a sequent.
Assumed as an axiom.
|PossibleAttack Sequent Sequent|
A possible attack on the given sequent.
|Missing Sequent String Bool|
A missing proof and the reason why it is missing plus a flag for displaying the sequent.
|Trivial Sequent TrivReason|
A trivial proof for the sequent and the reason why it is trivial.
|RuleApp Sequent Rule [Proof]|
An application of a rule/theorem and the proofs for all the resulting sequents.
|ForwardResolution (Named Sequent) Mapping|
|ChainRule Message [(String, [Either TID AgentId])]|
|SplitEq MsgEq [Bool]|
Use a (possibly bounded) depth-first search for finding the proof. TODO: Make error handling explicit.
Use branch-and-bound search to find the shortest proof. TODO: Make error handling explicit.
Minimize a proof by removing all unnecesary forward resolutions.
True iff the proof is an axiom definition.
NOTE: This checks only if the proof is directly by axiom.
Extracts the first type invariant occurring in a forward resolution. This is required because in Isabelle type invariants are handled using locales, while we are handling them using forward resolution.
Note that our system here is more general, but for the current setup, we do not see this generality.
Proof size datatype counting number of chain rule applications and the
number of forward resolutions. The
Monoid instance corresponds to adding
Check if there exists a case where the prover gets stuck using unbounded DFS and the given heuristic and theorems to reuse.