Theorems

type Theorem = Named Proof Source

A theorem is just a named proof.

thmProto :: Theorem -> Protocol Source

The protocol of a theorem.

thmName :: Theorem -> String Source

The name of a theorem.

thmSequent :: Theorem -> Sequent Source

The sequent of a theorem.

thmProof :: Theorem -> Proof Source

The proof of a theorem.

isAxiom :: Theorem -> Bool Source

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
Fields thyName :: String thyItems :: [ThyItem]

Instances

Eq Theory
Data Theory
Show Theory
Typeable Theory

Construction

adaptTheoryName :: FilePath -> Theory -> Theory Source

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

insertItem :: ThyItem -> Theory -> Theory Source

Insert a theory item into a theory.

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

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

proveSequents Source

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.

mapTheorySequents :: (Sequent -> Sequent) -> Theory -> Theory Source

Map the sequents of a theory.

addMissingTypingInvariants :: Theory -> Theory Source

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.

ensureUniqueRoleNames :: Theory -> Theory Source

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

composeParallel :: Theory -> Theory Source

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

Queries

lookupProtocol :: String -> Theory -> Maybe Protocol Source

Find a protocol in the theory according to its name.

unsoundTheorems :: Theory -> [(Protocol, String)]Source

Find all unsound theorems of the theory.

theoryProofSize :: Theory -> ProofSize Source

Total proof size.

theoryOverview :: Theory -> Theory Source

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.