scyther-proof-0.3.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.




A representation for proofs constructed using our security protocol verification theory.



data Proof Source

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.

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.

mapProofSequents :: (Sequent -> Sequent) -> Proof -> ProofSource

Map the sequents of the proof.


prfSequent :: Proof -> SequentSource

Extract the proven sequent from a proof.

prfProto :: Proof -> ProtocolSource

Extract the protocol concerned by 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.

sound :: Proof -> BoolSource

A proof is sound iff it is complete and each inference step is sound.

depends :: Proof -> Set (String, Protocol)Source

Output the set of theorems a proof depends on.

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

data ProofSize Source

Proof size datatype counting number of chain rule applications and the number of forward resolutions. The Monoid instance corresponds to adding proof sizes.

getProofSize :: ProofSize -> (Int, Int, Int)Source

Extract the raw proof size information.

missingProofSize :: ProofSizeSource

The size of a missing proof.

proofSize :: Proof -> ProofSizeSource

Compute the size of a proof.

Special Proofs

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

Check if there exists a case where the prover gets stuck using unbounded DFS and the given heuristic and theorems to reuse.