Theory.Model.Fact

Facts used to formulate and reason about protocol execution.

Fact

data Fact t

Facts.

Constructors

Fact

Fields

factTag :: FactTag

factTerms :: [t]

Instances

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_1627412214 => Binary (Fact t_1627412214)

NFData t_1627412214 => NFData (Fact t_1627412214)

Apply t => Apply (Fact t)

HasFrees t => HasFrees (Fact t)

Sized t => Sized (Fact t)

data Multiplicity

Constructors

Persistent

Linear

Instances

Eq Multiplicity

Data Multiplicity

Ord Multiplicity

Show Multiplicity

Typeable Multiplicity

Binary Multiplicity

NFData Multiplicity

data FactTag

Fact tags/symbols

Constructors

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.

Instances

Eq FactTag

Data FactTag

Ord FactTag

Show FactTag

Typeable FactTag

Binary FactTag

NFData FactTag

matchFact

Arguments

:: Fact t

Term

-> Fact t

Pattern

-> Match t

matchLFact t p is a complete set of AC matchers for the term fact t and the pattern fact p.

Queries

isLinearFact :: Fact t -> Bool

True if the fact is a linear fact.

isPersistentFact :: Fact t -> Bool

True if the fact is a persistent fact.

isProtoFact :: Fact t -> Bool

True iff the fact is a non-special protocol fact.

factTagName :: FactTag -> String

The name of a fact tag, e.g., factTagName KUFact = KU.

showFactTag :: FactTag -> String

Show a fact tag as a String. This is the factTagName prefixed with the multiplicity.

showFactTagArity :: FactTag -> String

Show a fact tag together with its aritiy.

factTagArity :: FactTag -> Int

The arity of a FactTag.

factTagMultiplicity :: FactTag -> Multiplicity

The multiplicity of a FactTag.

factArity :: Fact t -> Int

The arity of a Fact.

factMultiplicity :: Fact t -> Multiplicity

The multiplicity of a Fact.

data DirTag

A direction tag

Constructors

UpK

DnK

Instances

Eq DirTag

Ord DirTag

Show DirTag

kuFact :: t -> Fact t

kdFact :: t -> Fact t

kFactView :: LNFact -> Maybe (DirTag, LNTerm)

View a message-deduction fact.

dedFactView :: LNFact -> Maybe LNTerm

View a deduction logging fact.

isKFact :: LNFact -> Bool

True if the fact is a message-deduction fact.

isKUFact :: LNFact -> Bool

True if the fact is a KU-fact.

isKDFact :: LNFact -> Bool

True if the fact is a KD-fact.

Construction

freshFact :: t -> Fact t

A fresh fact denotes a fresh unguessable name.

outFact :: t -> Fact t

A fact denoting a message sent by the protocol to the intruder.

inFact :: t -> Fact t

A fact denoting that the intruder sent a message to the protocol.

kLogFact :: t -> Fact t

A fact logging that the intruder knows a message.

dedLogFact :: t -> Fact t

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 t

A protocol fact denotes a fact generated by a protocol rule.

NFact

type NFact v = Fact (NTerm v)

Facts with literals containing names and arbitrary variables.

LFact

type LFact c = Fact (LTerm c)

Facts with literals arbitrary constants and logical variables.

type LNFact = Fact LNTerm

Facts used for proving; i.e. variables fixed to logical variables and constant fixed to names.

unifyLNFactEqs :: [Equal LNFact] -> WithMaude [LNSubstVFresh]

Unify a list of LFact equalities.

unifiableLNFacts :: LNFact -> LNFact -> WithMaude Bool

True iff the two facts are unifiable.

Pretty-Printing

prettyFact :: Document d => (t -> d) -> Fact t -> d

Pretty print a fact.

prettyNFact :: Document d => LNFact -> d

Pretty print a NFact.

prettyLNFact :: Document d => LNFact -> d

Pretty print a LFact.