Scyther.Proof

Contents

Datatypes
- Proof construction
- Queries
  - Proof sizes
Special Proofs

Description

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

Synopsis

Datatypes

data Proof Source

A proof of a sequent.

Constructors

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.

Instances

Eq Proof
Data Proof
Show Proof
Typeable Proof

data TrivReason Source

Triviality reasons.

Constructors

TrivContradictoryPremises
TrivPremisesImplyConclusion
TrivLongTermKeySecrecy Message

Instances

Eq TrivReason
Data TrivReason
Show TrivReason
Typeable TrivReason

data Rule Source

Supported rules.

Constructors

Saturate
ForwardResolution (Named Sequent) Mapping
ChainRule Message [(String, [Either TID AgentId])]
SplitEq MsgEq [Bool]
TypingCases [String]

Instances

Eq Rule
Data Rule
Show Rule
Typeable Rule

Proof construction

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

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 Proof Source

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

minimizeProof :: Proof -> Proof Source

Minimize a proof by removing all unnecesary forward resolutions.

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

Map the sequents of the proof.

Queries

prfSequent :: Proof -> Sequent Source

Extract the proven sequent from a proof.

prfProto :: Proof -> Protocol Source

Extract the protocol concerned by a proof.

isAxiomProof :: Proof -> Bool Source

True iff the proof is an axiom definition.

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

isTrivialProof :: Proof -> Bool Source

True iff the proof is trivial.

complete :: Proof -> Bool Source

A proof is complete iff no Missing proof or PossibleAttack is part of it.

sound :: Proof -> Bool Source

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.

Instances

Eq ProofSize
Ord ProofSize
Show ProofSize
Monoid ProofSize

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

Extract the raw proof size information.

missingProofSize :: ProofSize Source

The size of a missing proof.

proofSize :: Proof -> ProofSize Source

Compute the size of a proof.

Special Proofs

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

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

displayChainRule :: Protocol -> Maybe Typing -> Proof Source