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




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




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.

protocol :: Facts -> ProtocolSource

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


empty :: Protocol -> FactsSource

Empty set of facts; logically equivalent to true.

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

Get a fresh TID and the updated set of facts.

freshAgentId :: Facts -> (AgentId, Facts)Source

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.


nullFacts :: Facts -> BoolSource

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]Source

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.



:: Facts

From these premises

-> Facts

Show the these conclusion

-> Mapping

Mapping the free variables of the conclusion to the premises.

-> Bool 

proveFalse :: Facts -> BoolSource

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 -> BoolSource

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 -> BoolSource

Try to prove that the formula holds under these facts.

toAtoms :: Facts -> [Atom]Source

Represent the facts as a set of atoms.

nextTID :: Facts -> TIDSource

The next free thread identifier

nextAgentId :: Facts -> AgentIdSource

The next free agent identifier

quantifiedTIDs :: Facts -> [TID]Source

The list of thread ids that are quantified.

Substitution under the equalities of the facts

substEv :: Facts -> Event -> EventSource

Substitute an event.

threadRole :: TID -> Facts -> Maybe RoleSource

The role assigned to a thread.

eqsToMapping :: Facts -> MappingSource

Create a mapping from the equalities of the facts.

applyMapping :: Mapping -> Facts -> FactsSource

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]Source

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.

saturateFacts :: Facts -> FactsSource

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 FactsSource

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 MessageSource

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]Source

Equalities that can be splitted.

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

Split an equality between bi-directional symmetric shared keys.




:: IsarConf 
-> Facts 
-> ([Doc], [Doc], [Doc])

Quantified variables, representable facts, and non-representable facts

Pretty print the facts in Isar format.



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

Quantified variables, representable facts, and non-representable facts

Pretty print the facts in security protocol theory format.