Scyther.Facts

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

Documentation

module Scyther.Protocol

module Scyther.Typing

module Scyther.Message

module Scyther.Event

module Scyther.Formula

Facts

data Facts

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

protocol :: Facts -> Protocol

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

Construction

empty :: Protocol -> Facts

Empty set of facts; logically equivalent to true.

freshTID :: Facts -> (TID, Facts)

Get a fresh TID and the updated set of facts.

freshAgentId :: Facts -> (AgentId, Facts)

Get a fresh AgentId and the updated set of facts.

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

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 Facts

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)

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 Facts

Set the typing.

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

Uses fail for error reporting.

Queries

nullFacts :: Facts -> Bool

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.

freeVariableMappings :: Facts -> Facts -> [Mapping]

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.

proveFacts

Arguments

:: Facts

From these premises

-> Facts

Show the these conclusion

-> Mapping

Mapping the free variables of the conclusion to the premises.

-> Bool

proveFalse :: Facts -> 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.

proveAtom :: Facts -> Atom -> Bool

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.

proveFormula :: Facts -> Formula -> Bool

Try to prove that the formula holds under these facts.

toAtoms :: Facts -> [Atom]

Represent the facts as a set of atoms.

nextTID :: Facts -> TID

The next free thread identifier

nextAgentId :: Facts -> AgentId

The next free agent identifier

quantifiedTIDs :: Facts -> [TID]

The list of thread ids that are quantified.

Substitution under the equalities of the facts

substEv :: Facts -> Event -> Event

Substitute an event.

threadRole :: TID -> Facts -> Maybe Role

The role assigned to a thread.

eqsToMapping :: Facts -> Mapping

Create a mapping from the equalities of the facts.

applyMapping :: Mapping -> Facts -> 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

oldestOpenMessages :: Facts -> [Message]

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

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

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.

saturateFacts :: Facts -> Facts

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

exploitTypingFacts :: MonadPlus m => Facts -> m 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.

exploitLongTermKeySecrecy :: Facts -> Maybe Message

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.

splittableEqs :: Facts -> [MsgEq]

Equalities that can be splitted.

splitEqFacts :: MsgEq -> Facts -> [Maybe Facts]

Split an equality between bi-directional symmetric shared keys.

Output

isaFacts

Arguments

:: IsarConf

-> Facts

-> ([Doc], [Doc], [Doc])

Quantified variables, representable facts, and non-representable facts

Pretty print the facts in Isar format.

sptFacts

Arguments

:: Facts

-> ([Doc], [Doc], [Doc])

Quantified variables, representable facts, and non-representable facts

Pretty print the facts in security protocol theory format.