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

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




Theory datatype and transformations on it.



data Axiom Source

An axiom describes a property that must hold for all traces. Axioms are always used as lemmas in proofs.



axName :: forall arr. Arrow arr => Lens arr Axiom StringSource

axFormula :: forall arr. Arrow arr => Lens arr Axiom LNFormulaSource


data TraceQuantifier Source

A TraceQuantifier stating whether we check satisfiability of validity.



data Lemma p Source

A lemma describes a property that holds in the context of a theory together with a proof of its correctness.


Functor Lemma 
Foldable Lemma 
Traversable Lemma 
Eq p => Eq (Lemma p) 
Ord p => Ord (Lemma p) 
Show p => Show (Lemma p) 
Binary p_1628398076 => Binary (Lemma p_1628398076) 
NFData p_1628398076 => NFData (Lemma p_1628398076) 

lName :: forall arr p. Arrow arr => Lens arr (Lemma p) StringSource

lTraceQuantifier :: forall arr p. Arrow arr => Lens arr (Lemma p) TraceQuantifierSource

lFormula :: forall arr p. Arrow arr => Lens arr (Lemma p) LNFormulaSource

lAttributes :: forall arr p. Arrow arr => Lens arr (Lemma p) [LemmaAttribute]Source

lProof :: forall arr p. Arrow arr => Lens arr (Lemma p) pSource

unprovenLemma :: String -> [LemmaAttribute] -> TraceQuantifier -> LNFormula -> Lemma ProofSkeletonSource

Create a new unproven lemma from a formula modulo E.


data Theory sig c r p Source

A theory contains a single set of rewriting rules modeling a protocol and the lemmas that




_thyName :: String
_thySignature :: sig
_thyCache :: c
_thyItems :: [TheoryItem r p]


(Eq sig, Eq c, Eq r, Eq p) => Eq (Theory sig c r p) 
(Ord sig, Ord c, Ord r, Ord p) => Ord (Theory sig c r p) 
(Show sig, Show c, Show r, Show p) => Show (Theory sig c r p) 
(Binary sig_1628398556, Binary c_1628398557, Binary r_1628398558, Binary p_1628398559) => Binary (Theory sig_1628398556 c_1628398557 r_1628398558 p_1628398559) 
(NFData sig_1628398556, NFData c_1628398557, NFData r_1628398558, NFData p_1628398559) => NFData (Theory sig_1628398556 c_1628398557 r_1628398558 p_1628398559) 

data TheoryItem r p Source

A theory item built over the given rule type.


RuleItem r 
LemmaItem (Lemma p) 
AxiomItem Axiom 
TextItem FormalComment 


Functor (TheoryItem r) 
(Eq r, Eq p) => Eq (TheoryItem r p) 
(Ord r, Ord p) => Ord (TheoryItem r p) 
(Show r, Show p) => Show (TheoryItem r p) 
(Binary r_1628398560, Binary p_1628398561) => Binary (TheoryItem r_1628398560 p_1628398561) 
(NFData r_1628398560, NFData p_1628398561) => NFData (TheoryItem r_1628398560 p_1628398561) 

thyName :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) StringSource

thySignature :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) sigSource

thyCache :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) cSource

thyItems :: forall arr sig c r p. Arrow arr => Lens arr (Theory sig c r p) [TheoryItem r p]Source

theoryRules :: Theory sig c r p -> [r]Source

All rules of a theory.

theoryLemmas :: Theory sig c r p -> [Lemma p]Source

All lemmas of a theory.

theoryAxioms :: Theory sig c r p -> [Axiom]Source

All axioms of a theory.

addAxiom :: Axiom -> Theory sig c r p -> Maybe (Theory sig c r p)Source

Add a new axiom. Fails, if axiom with the same name exists.

addLemma :: Lemma p -> Theory sig c r p -> Maybe (Theory sig c r p)Source

Add a new lemma. Fails, if a lemma with the same name exists.

removeLemma :: String -> Theory sig c r p -> Maybe (Theory sig c r p)Source

Remove a lemma by name. Fails, if the lemma does not exist.

lookupLemma :: String -> Theory sig c r p -> Maybe (Lemma p)Source

Find the lemma with the given name.

addComment :: Doc -> Theory sig c r p -> Theory sig c r pSource

Add a comment to the theory.

addStringComment :: String -> Theory sig c r p -> Theory sig c r pSource

Add a comment represented as a string to the theory.

addFormalComment :: FormalComment -> Theory sig c r p -> Theory sig c r pSource

Open theories

type OpenTheory = Theory SignaturePure [IntrRuleAC] OpenProtoRule ProofSkeletonSource

Open theories can be extended. Invariants: 1. Lemma names are unique.

addProtoRule :: ProtoRuleE -> OpenTheory -> Maybe OpenTheorySource

Add a new protocol rules. Fails, if a protocol rule with the same name exists.

addIntrRuleACs :: [IntrRuleAC] -> OpenTheory -> OpenTheorySource

Add intruder proof rules.

normalizeTheory :: OpenTheory -> OpenTheorySource

Normalize the theory representation such that they remain semantically equivalent. Use this function when you want to compare two theories (quite strictly) for semantic equality; e.g., when testing the parser.

Closed theories

type ClosedTheory = Theory SignatureWithMaude ClosedRuleCache ClosedProtoRule IncrementalProofSource

Closed theories can be proven. Invariants: 1. Lemma names are unique 2. All proof steps with annotated sequents are sound with respect to the closed rule set of the theory. 3. Maude is running under the given handle.



:: FilePath

Path to the Maude executable.

-> OpenTheory 
-> IO ClosedTheory 

Close a theory by closing its associated rule set and checking the proof skeletons and caching AC variants as well as precomputed case distinctions.

This function initializes the relation to the Maude process with the correct signature. This is the right place to do that because in a closed theory the signature may not change any longer.

openTheory :: ClosedTheory -> OpenTheorySource

Open a theory by dropping the closed world assumption and values whose soundness dependens on it.

data ClosedProtoRule Source

A closed proto rule lists its original rule modulo E, the corresponding variant modulo AC, and if required the assertion soundness proof.

getIntrVariants :: ClosedTheory -> [IntrRuleAC]Source

The variants of the intruder rules.

getProtoRuleEs :: ClosedTheory -> [ProtoRuleE]Source

All protocol rules modulo E.

getProofContext :: Lemma a -> ClosedTheory -> ProofContextSource

Get the proof context for a lemma of the closed theory.

getClassifiedRules :: ClosedTheory -> ClassifiedRulesSource

The classified set of rules modulo AC in this theory.

getInjectiveFactInsts :: ClosedTheory -> Set FactTagSource

The facts with injective instances in this theory

getCaseDistinction :: CaseDistKind -> ClosedTheory -> [CaseDistinction]Source

The precomputed case distinctions.


type ProofSkeleton = Proof ()Source

Proof skeletons are used to represent proofs in open theories.



:: (Lemma IncrementalProof -> Bool)

Lemma selector.

-> Prover 
-> ClosedTheory 
-> ClosedTheory 

Prove both the assertion soundness as well as all lemmas of the theory. If the prover fails on a lemma, then its proof remains unchanged.

Lemma references

lookupLemmaProof :: LemmaRef -> ClosedTheory -> Maybe IncrementalProofSource

Resolve a path in a theory.

modifyLemmaProof :: Prover -> LemmaRef -> ClosedTheory -> Maybe ClosedTheorySource

Modify the proof at the given lemma ref, if there is one. Fails if the path is not present or if the prover fails.

Pretty printing

prettyFormalComment :: HighlightDocument d => String -> String -> dSource

Pretty print a formal comment

prettyLemmaName :: HighlightDocument d => Lemma p -> dSource

Pretty print the lemma name together with its attributes.

prettyAxiom :: HighlightDocument d => Axiom -> dSource

Pretty print an axiom.

prettyLemma :: HighlightDocument d => (p -> d) -> Lemma p -> dSource

Pretty print a lemma.

prettyClosedTheory :: HighlightDocument d => ClosedTheory -> dSource

Pretty print a closed theory.

prettyOpenTheory :: HighlightDocument d => OpenTheory -> dSource

Pretty print an open theory.

prettyIntruderVariants :: HighlightDocument d => [IntrRuleAC] -> dSource

Pretty-print a non-empty bunch of intruder rules.

Convenience exports