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

Scyther.Theory

Synopsis

# Theorems

A theorem is just a named proof.

The protocol of a theorem.

The name of a theorem.

The sequent of a theorem.

The proof of a theorem.

Check if a theorem is an axiom.

# Theory items

data ThyItem Source

A theory item is a (meta-)logical fact representable by our security protocol theory.

Constructors

 ThyProtocol Protocol ThySequent (Named Sequent) ThyTheorem (Named Proof) ThyText String

Instances

 Eq ThyItem Data ThyItem Show ThyItem Typeable ThyItem

# Theory Datatypes

data Theory Source

Constructors

 Theory FieldsthyName :: String thyItems :: [ThyItem]

Instances

 Eq Theory Data Theory Show Theory Typeable Theory

## Construction

Adapt the theory name to the base name of the given file.

Insert a theory item into a theory.

shrinkTheory :: (String -> Bool) -> Theory -> TheorySource

Only keep theorems for which the given predicate is true or which are referenced by some kept theorem.

Arguments

 :: (Sequent -> Theorem -> Bool) Predicate determining theorems for reuse for proving the given sequent. -> ([Named Sequent] -> Sequent -> Maybe Proof) Proof construction function. -> Theory -> Theory

Prove all claims with the given heuristic optionally using the given bound.

Map the sequents of a theory.

Most proofs require a typing invariant to be present for the protocol under investigation. We try to derive one from the protcol specification for every protocol that has none.

Ensures that all roles are globally uniquely named by prefixing all role names with their corresponding protocol name, if two roles have equal names.

Compose all protocol in the theory in parallel. Assumes that both protocol names as well as role names are globally unique.

## Queries

Find a protocol in the theory according to its name.

Find all unsound theorems of the theory.

Total proof size.

classifyProperties :: (String -> Bool) -> Theory -> (Int, Int, Int)Source

Count and classify the properties selected by the given predicate into secrecy properties, authentication properties, and other properties.