Conjunctions of the logical facts needed during a proof using decryption chain reasoning.
- module Scyther.Protocol
- module Scyther.Typing
- module Scyther.Message
- module Scyther.Event
- module Scyther.Formula
- data Facts
- protocol :: Facts -> Protocol
- empty :: Protocol -> Facts
- freshTID :: Facts -> (TID, Facts)
- freshAgentId :: Facts -> (AgentId, Facts)
- quantifyTID :: Monad m => TID -> Facts -> m Facts
- quantifyAgentId :: Monad m => AgentId -> Facts -> m Facts
- conjoinAtoms :: Monad m => [Atom] -> Facts -> m (Maybe Facts)
- setTyping :: Monad m => Typing -> Facts -> m Facts
- nullFacts :: Facts -> Bool
- freeVariableMappings :: Facts -> Facts -> [Mapping]
- proveFacts :: Facts -> Facts -> Mapping -> Bool
- proveFalse :: Facts -> Bool
- proveAtom :: Facts -> Atom -> Bool
- proveFormula :: Facts -> Formula -> Bool
- toAtoms :: Facts -> [Atom]
- nextTID :: Facts -> TID
- nextAgentId :: Facts -> AgentId
- quantifiedTIDs :: Facts -> [TID]
- substEv :: Facts -> Event -> Event
- threadRole :: TID -> Facts -> Maybe Role
- eqsToMapping :: Facts -> Mapping
- applyMapping :: Mapping -> Facts -> Facts
- oldestOpenMessages :: Facts -> [Message]
- chainRuleFacts :: MonadPlus m => Message -> Facts -> m [((String, [Either TID AgentId]), Facts)]
- saturateFacts :: Facts -> Facts
- exploitTypingFacts :: MonadPlus m => Facts -> m Facts
- exploitLongTermKeySecrecy :: Facts -> Maybe Message
- splittableEqs :: Facts -> [MsgEq]
- splitEqFacts :: MsgEq -> Facts -> [Maybe Facts]
- isaFacts :: IsarConf -> Facts -> ([Doc], [Doc], [Doc])
- sptFacts :: Facts -> ([Doc], [Doc], [Doc])
A conjunction of logical facts.
Invariants that hold for a value
facts = Facts _ evs evord co uc eqs:
- All facts are invariant under their corresponding substitution. This excludes the quantifiers, as they are no facts.
- 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.
Tries to quantify the given thread identifier. If it is already quantified
fail is called in the given monad.
Tries to quantify the given agent identifier. If it is already quantified
fail is called in the given monad.
Build the conjunction of the atoms and the facts; a result of
means that the conjunction is logically equivalent to False. This will occur
AFalse is conjoined or an equality that cannot be unified.
PRE: The atom must pass certification under the given facts.
Set the typing.
PRE: There mustn't be a different existing typing.
fail for error reporting.
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.
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
Try to prove that the formula holds under these facts.
Substitution under 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.
Sort open messages ascending with respect to the maximal thread id.
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.
Split an equality between bi-directional symmetric shared keys.
|-> ([Doc], [Doc], [Doc])|
Quantified variables, representable facts, and non-representable facts
Pretty print the facts in Isar format.