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

Scyther.Sequent

Contents

Synopsis

# Datatype

data Sequent Source

A sequent with a conjunction of a set of facts as the premise and a single formula as the conclusion denoting a statement about a reachable state of a protocol.

Constructors

 Sequent FieldssePrem :: Facts seConcl :: Formula

Instances

 Eq Sequent Data Sequent Ord Sequent Show Sequent Typeable Sequent

The protocol of a sequent.

## Logically safe construction

wellTypedCases :: MonadPlus m => Sequent -> m [(String, Sequent)]Source

The named list of sequents which need to be proven in order to prove that the given protocol is well typed or weakly-atomic

PRE: The conclusion of the sequent must be typing atom.

Uses `fail` for error reporting.

saturate :: MonadPlus m => Sequent -> m SequentSource

Try to saturate a sequent, if possible and leading to new facts.

Arguments

 :: MonadPlus m => Sequent rule -> Sequent proof state -> m (Mapping, Maybe Sequent) some result if resolution worked. Nothing denotes that False was derived. Just means that premises of proof state were extended. mzero if rule could not be applied

Like `fruleInst` but tries all mappings.

Arguments

 :: MonadPlus m => Sequent rule -> Mapping mapping of free variables of rule to proof state -> Sequent proof state -> m (Maybe Sequent) some result if resolution worked. Nothing denotes that False was derived. Just means that premises of proof state were extended. mzero if rule could not be applied

Emulate a variant Isabelle's `frule` tactic. It works only if the given maping of free variables of the rule makes the premise of the rule provable under the given proof state. Then, the conclusion of the rule with free variables mapped accordingly is added to premises of the proof state. The last step works currently only for conclusions being false of pure conclusions.

NOTE that `frule` works only for rules that contain no existential quantifiers in the conclusion.

chainRule :: MonadPlus m => Sequent -> Message -> m [((String, [Either TID AgentId]), Sequent)]Source

Try to use the chain rule.

MonadPlus is used to report a failure to apply the rule.

Split a splittable equality. splitting can be done.

Try to exploit the typing. Fails if no new facts could be derived.

Make all thread identifiers occurring in the sequent unique by consistently relabeling the thread identifiers in the conclusion.