tamarin-prover-theory- Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone




The public interface of the constraint solver, which implements all constraint reduction rules and together with a rule application heuristic.


Constraint systems

Proof contexts

The proof context captures all relevant information about the context in which we are using the constraint solver. These are things like the signature of the message theory, the multiset rewriting rules of the protocol, the available precomputed case distinctions, whether induction should be applied or not, whether typed or untyped case distinctions are used, and whether we are looking for the existence of a trace or proving the absence of any trace satisfying the constraint system.

data ProofContext Source

A proof context contains the globally fresh facts, classified rewrite rules and the corresponding precomputed premise case distinction theorems.

joinAllRules :: ClassifiedRules -> [RuleAC]Source

joinAllRules rules computes the union of all rules classified in rules.

crProtocol :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source

crConstruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source

crDestruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source

Constraint reduction rules


All rules that reduce a constraint system to the empty set of constraint systems. The Contradiction datatype stores the information about the contradiction for later display to the user.

contradictions :: ProofContext -> System -> [Contradiction]Source

All CR-rules reducing a constraint system to *⟂* represented as a list of trivial contradictions. Note that some constraint systems are also removed because they have no unifier. This is part of unification. Note also that *S_{¬,@}* is handled as part of *S_∀*.

Precomputed case distinctions

For better speed, we precompute case distinctions. This is especially important for getting rid of all chain constraints before actually starting to verify security properties.

cdGoal :: forall arr. Arrow arr => Lens arr CaseDistinction GoalSource

cdCases :: forall arr. Arrow arr => Lens arr CaseDistinction (Disj ([String], System))Source



:: ProofContext 
-> [LNGuarded]


-> [CaseDistinction] 

Precompute a saturated set of case distinctions.



:: [LNGuarded]

Typing assumptions to use.

-> ProofContext

Proof context to use.

-> [CaseDistinction]

Original, untyped case distinctions.

-> [CaseDistinction]

Refined, typed case distinctions.

Refine a set of case distinction by exploiting additional typing assumptions.

unsolvedChainConstraints :: CaseDistinction -> [Int]Source

The number of remaining chain constraints of each case.

Proof methods

Proof methods are the external to the constraint solver. They allow its small step execution. This module also provides the heuristics for selecting the best proof method to apply to a constraint system.

Convenience export