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

Scyther.Formula

Contents

Data Types
- Construction
- Queries
Pretty Printing

Synopsis

Data Types

data Atom Source

A representable logical atom.

Constructors

AFalse	`False` in Isabelle.
AEq AnyEq	An equality
AEv Event	An event must have happened.
AEvOrd (Event, Event)	An event order.
ACompr Message	A compromised agent variable.
AUncompr Message	An uncompromised agent variable.
AHasType MVar (Maybe Type)	A claim that a variable is of the given type; Nothing stands for weakly-atomic.
ATyping Typing	A claim that the current state of a protocol is approximated by the given typing.
AReachable Protocol	A claim that the current state is reachable.

Instances

Eq Atom
Data Atom
Ord Atom
Show Atom
Typeable Atom

data Formula Source

A representable logical formula. Currently these are monotonic formula.

Constructors

FAtom Atom
FConj Formula Formula
FExists (Either TID AgentId) Formula

Instances

Eq Formula
Data Formula
Ord Formula
Show Formula
Typeable Formula

Construction

substAtom :: Equalities -> Atom -> Atom Source

Substitute all variables in an atom.

NOTE: A HasType atom will only have its thread identifier substituted, but not the whole message variable.

relabelTIDs :: [TID] -> Formula -> Formula Source

Relabel quantified TIDs according to the given list of labels.

Queries

hasQuantifiers :: Formula -> Bool Source

True iff the formula does contain an existential quantifier.

conjuncts :: Formula -> [Formula]Source

Split all toplevel conjunctions.

conjunctionToAtoms :: MonadPlus m => Formula -> m [Atom]Source

Convert a formula consisting of conjunctions only to a list of atoms. Uses fail for error reporting.

isTypingFormula :: Formula -> Bool Source

A formula is a single atom claiming well-typedness.

destTypingFormula :: Formula -> Maybe Typing Source

Extract the typing from a singleton well-typedness formula.

atomTIDs :: Atom -> [TID]Source

Compute the threads associated to the given atom.

findRole :: TID -> Formula -> Maybe Role Source

Find the first conjoined thread to role equality for this thread, if there is any.

Pretty Printing

isaCompr :: IsarConf -> Message -> Doc Source

A compromised agent variable in Isar format.

isaUncompr :: IsarConf -> Message -> Doc Source

An uncompromised agent variable in Isar format.

sptAtom :: Mapping -> Atom -> Doc Source

Pretty print an atom in security protocol theory format.

isaAtom :: IsarConf -> Mapping -> Atom -> Doc Source

Pretty print an atom in Isar format.

isaFormula :: IsarConf -> Mapping -> Formula -> Doc Source

A formula in Isar format.

sptFormula :: Mapping -> Formula -> Doc Source

A formula in security protocol theory format.