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

Scyther.Facts

Description

Conjunctions of the logical facts needed during a proof using decryption chain reasoning.

Synopsis

# Facts

data Facts Source

A conjunction of logical facts.

Invariants that hold for a value `facts = Facts _ evs evord co uc eqs`:

1. All facts are invariant under their corresponding substitution. This excludes the quantifiers, as they are no facts.
2. All trivial learn events are removed (or split in case of a pair).

We assume that all thread identifiers that are assigned to a role are locally quantified. The kind of quantification depends on the context. If the set of facts models the premises of a proof state then this would be universal quantification. If the set of facts models an authentication conclusion this would be existential quantification.

Instances

 Eq Facts Data Facts Ord Facts Show Facts Typeable Facts

The protocol that the current state is a reachable state of.

## Construction

Empty set of facts; logically equivalent to true.

freshTID :: Facts -> (TID, Facts)Source

Get a fresh TID and the updated set of facts.

Get a fresh AgentId and the updated set of facts.

quantifyTID :: Monad m => TID -> Facts -> m FactsSource

Tries to quantify the given thread identifier. If it is already quantified `fail` is called in the given monad.

quantifyAgentId :: Monad m => AgentId -> Facts -> m FactsSource

Tries to quantify the given agent identifier. If it is already quantified `fail` is called in the given monad.

conjoinAtoms :: Monad m => [Atom] -> Facts -> m (Maybe Facts)Source

Build the conjunction of the atoms and the facts; a result of `Nothing` means that the conjunction is logically equivalent to False. This will occur in case `AFalse` is conjoined or an equality that cannot be unified.

PRE: The atom must pass certification under the given facts.

PRE: The atom must not be a `AHasTyp` or a `ATyping` atom, as they are not representable by `Facts`

setTyping :: Monad m => Typing -> Facts -> m FactsSource

Set the typing.

PRE: There mustn't be a different existing typing.

Uses `fail` for error reporting.

## Queries

True if no premises apart from state reachability and the optional well-typedness claim are present. Note that there may be quantifiers and covered goals.

Possible unifiers making the first set of facts provable under the second set of facts. resulting equalities describe the mapping from all logical variables of the first set of facts logical variables of the second set of facts.

NOTE: You may want to use `trimQuantifiers` before using this function to avoid getting superfluous unifiers.

Arguments

 :: Facts From these premises -> Facts Show the these conclusion -> Mapping Mapping the free variables of the conclusion to the premises. -> Bool

Check if a set of facts is trivially contradictory.

NOTE: This is not the same as trying to prove the atom AFalse under these premises. The checks are separated due to efficiency reasons.

True iff the facts imply the validity of the given atom. Note that this check is incomplete; i.e. there may be atoms that would be true under these facts, but are not detected as such.

PRE: Trivial learn events must be split. You may achieve this using `removeTrivialFacts`.

Try to prove that the formula holds under these facts.

toAtoms :: Facts -> [Atom]Source

Represent the facts as a set of atoms.

The next free agent identifier

quantifiedTIDs :: Facts -> [TID]Source

The list of thread ids that are quantified.

## Substitution under the equalities of the facts

Substitute an event.

The role assigned to a thread.

Create a mapping from the equalities of the facts.

Apply the mapping of agent and thread equalities to the facts.

TODO: Improve error handling. Currently, `error` is called if the facts are contradictory after the substitution.

## Rule applications

Sort open messages ascending with respect to the maximal thread id.

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

Apply the chain rule to a message in the context of a protocol and a set of established facts. Returns the list of facts corresponding to the disjunctions in the conclusion of the chain rule, which are not trivially false due to syntactic inequality.

Saturate facts modulo removal of trivial facts; i.e. apply all rules except the chain rule eagerly and remove trivial facts.

Make use of the typing assumption by checking for instantiated message variables if their instantiation does not agree with the structural type and hence they must be known before the given step.

Is equal to `mzero` in case the facts don't contain a typing.

Try to find a long-term-key that must be secret due to the uncompromisedness assumptions, but is claimed to be known to the intruder; i.e. if this method returns a message, then the premises are contradictory.

Equalities that can be splitted.

Split an equality between bi-directional symmetric shared keys.

# Output

Arguments

 :: IsarConf -> Facts -> ([Doc], [Doc], [Doc]) Quantified variables, representable facts, and non-representable facts

Pretty print the facts in Isar format.

Arguments

 :: Facts -> ([Doc], [Doc], [Doc]) Quantified variables, representable facts, and non-representable facts

Pretty print the facts in security protocol theory format.