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

# Datatypes

A proof of a sequent.

Axiom 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. |

data TrivReason Source

Triviality reasons.

Supported rules.

## Proof construction

dfsProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe ProofSource

Use a (possibly bounded) depth-first search for finding the proof. TODO: Make error handling explicit.

shortestProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe ProofSource

Use branch-and-bound search to find the shortest proof. TODO: Make error handling explicit.

minimizeProof :: Proof -> ProofSource

Minimize a proof by removing all unnecesary forward resolutions.

## Queries

prfSequent :: Proof -> SequentSource

Extract the proven sequent from a proof.

isAxiomProof :: Proof -> BoolSource

True iff the proof is an axiom definition.

NOTE: This checks only if the proof is directly by axiom.

isTrivialProof :: Proof -> BoolSource

True iff the proof is trivial.

complete :: Proof -> BoolSource

A proof is complete iff no `Missing`

proof or `PossibleAttack`

is part of it.

extractTypeInvariant :: Proof -> Maybe (Named Typing)Source

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 sizes

Proof size datatype counting number of chain rule applications and the
number of forward resolutions. The `Monoid`

instance corresponds to adding
proof sizes.

missingProofSize :: ProofSizeSource

The size of a missing proof.