Portability | GHC only |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
Facts used to formulate and reason about protocol execution.
- data Fact t = Fact {}
- data Multiplicity
- = Persistent
- | Linear
- data FactTag
- matchFact :: Fact t -> Fact t -> Match t
- isLinearFact :: Fact t -> Bool
- isPersistentFact :: Fact t -> Bool
- isProtoFact :: Fact t -> Bool
- factTagName :: FactTag -> String
- showFactTag :: FactTag -> String
- showFactTagArity :: FactTag -> String
- factTagArity :: FactTag -> Int
- factTagMultiplicity :: FactTag -> Multiplicity
- factArity :: Fact t -> Int
- factMultiplicity :: Fact t -> Multiplicity
- data DirTag
- kuFact :: t -> Fact t
- kdFact :: t -> Fact t
- kFactView :: LNFact -> Maybe (DirTag, LNTerm)
- dedFactView :: LNFact -> Maybe LNTerm
- isKFact :: LNFact -> Bool
- isKUFact :: LNFact -> Bool
- isKDFact :: LNFact -> Bool
- freshFact :: t -> Fact t
- outFact :: t -> Fact t
- inFact :: t -> Fact t
- kLogFact :: t -> Fact t
- dedLogFact :: t -> Fact t
- protoFact :: Multiplicity -> String -> [t] -> Fact t
- type NFact v = Fact (NTerm v)
- type LFact c = Fact (LTerm c)
- type LNFact = Fact LNTerm
- unifyLNFactEqs :: [Equal LNFact] -> WithMaude [LNSubstVFresh]
- unifiableLNFacts :: LNFact -> LNFact -> WithMaude Bool
- prettyFact :: Document d => (t -> d) -> Fact t -> d
- prettyNFact :: Document d => LNFact -> d
- prettyLNFact :: Document d => LNFact -> d
Fact
Facts.
Functor Fact | |
Typeable1 Fact | |
Foldable Fact | |
Traversable Fact | |
Eq t => Eq (Fact t) | |
Data t => Data (Fact t) | |
Ord t => Ord (Fact t) | |
Show t => Show (Fact t) | |
Binary t_1627410334 => Binary (Fact t_1627410334) | |
NFData t_1627410334 => NFData (Fact t_1627410334) | |
Apply t => Apply (Fact t) | |
HasFrees t => HasFrees (Fact t) | |
Sized t => Sized (Fact t) |
data Multiplicity Source
Fact tags/symbols
ProtoFact Multiplicity String Int | A protocol fact together with its arity and multiplicity. |
FreshFact | Freshly generated value. |
OutFact | Sent by the protocol |
InFact | Officially known by the intruder/network. |
KUFact | Up-knowledge fact in messsage deduction. |
KDFact | Down-knowledge fact in message deduction. |
DedFact | Log-fact denoting that the intruder deduced a message using a construction rule. |
matchLFact t p
is a complete set of AC matchers for the term fact t
and the pattern fact p
.
Queries
isLinearFact :: Fact t -> BoolSource
True if the fact is a linear fact.
isPersistentFact :: Fact t -> BoolSource
True if the fact is a persistent fact.
isProtoFact :: Fact t -> BoolSource
True iff the fact is a non-special protocol fact.
factTagName :: FactTag -> StringSource
The name of a fact tag, e.g., factTagName KUFact = KU
.
showFactTag :: FactTag -> StringSource
Show a fact tag as a String
. This is the factTagName
prefixed with
the multiplicity.
showFactTagArity :: FactTag -> StringSource
Show a fact tag together with its aritiy.
factTagArity :: FactTag -> IntSource
The arity of a FactTag
.
factTagMultiplicity :: FactTag -> MultiplicitySource
The multiplicity of a FactTag
.
factMultiplicity :: Fact t -> MultiplicitySource
The multiplicity of a Fact
.
dedFactView :: LNFact -> Maybe LNTermSource
View a deduction logging fact.
Construction
dedLogFact :: t -> Fact tSource
A fact logging that the intruder deduced a message using a construction rule. We use this to formulate invariants over normal dependency graphs.
protoFact :: Multiplicity -> String -> [t] -> Fact tSource
A protocol fact denotes a fact generated by a protocol rule.
NFact
LFact
type LNFact = Fact LNTermSource
Facts used for proving; i.e. variables fixed to logical variables and constant fixed to names.
unifyLNFactEqs :: [Equal LNFact] -> WithMaude [LNSubstVFresh]Source
Unify a list of LFact
equalities.
Pretty-Printing
prettyFact :: Document d => (t -> d) -> Fact t -> dSource
Pretty print a fact.
prettyNFact :: Document d => LNFact -> dSource
Pretty print a NFact
.
prettyLNFact :: Document d => LNFact -> dSource
Pretty print a LFact
.