Portability	portable
Maintainer	Simon Meier <iridcode@gmail.com>
Safe Haskell	None

Theory.Model.Rule

Contents

General Rules
- Accessors
- Genereal protocol and intruder rules
Protocol Rule Information
Intruder Rule Information
Concrete Rules
Pretty-Printing

Description

Rewriting rules representing protocol execution and intruder deduction. Once modulo the full Diffie-Hellman equational theory and once modulo AC.

Synopsis

General Rules

data Rule i Source

Rewriting rules with arbitrary additional information and facts with names and logical variables.

Constructors

Rule
Fields _rInfo :: i _rPrems :: [LNFact] _rConcs :: [LNFact] _rActs :: [LNFact]

Instances

Functor Rule
Typeable1 Rule
HasRuleName RuleACInst
HasRuleName RuleAC
HasRuleName ProtoRuleAC
HasRuleName ProtoRuleE
HasRuleName IntrRuleAC
Eq i => Eq (Rule i)
Data i => Data (Rule i)
Ord i => Ord (Rule i)
Show i => Show (Rule i)
Binary i_1627482811 => Binary (Rule i_1627482811)
NFData i_1627482811 => NFData (Rule i_1627482811)
Apply i => Apply (Rule i)
(Show i, HasFrees i) => HasFrees (Rule i)
Sized (Rule i)

newtype PremIdx Source

An index of a premise. The first premise has index '0'.

Constructors

PremIdx
Fields getPremIdx :: Int

Instances

Enum PremIdx
Eq PremIdx
Data PremIdx
Ord PremIdx
Show PremIdx
Typeable PremIdx
Binary PremIdx
NFData PremIdx
Apply PremIdx
HasFrees PremIdx

newtype ConcIdx Source

An index of a conclusion. The first conclusion has index '0'.

Constructors

ConcIdx
Fields getConcIdx :: Int

Instances

Enum ConcIdx
Eq ConcIdx
Data ConcIdx
Ord ConcIdx
Show ConcIdx
Typeable ConcIdx
Binary ConcIdx
NFData ConcIdx
Apply ConcIdx
HasFrees ConcIdx

Accessors

rInfo :: forall arr i. Arrow arr => Lens arr (Rule i) iSource

rPrems :: forall arr i. Arrow arr => Lens arr (Rule i) [LNFact]Source

rConcs :: forall arr i. Arrow arr => Lens arr (Rule i) [LNFact]Source

rActs :: forall arr i. Arrow arr => Lens arr (Rule i) [LNFact]Source

rPrem :: PremIdx -> Rule i :-> LNFact Source

rPrem i is a lens for the i-th premise of a rule.

rConc :: ConcIdx -> Rule i :-> LNFact Source

rConc i is a lens for the i-th conclusion of a rule.

lookupPrem :: PremIdx -> Rule i -> Maybe LNFact Source

lookupPrem i ru returns the i-th premise of rule ru, if possible.

lookupConc :: ConcIdx -> Rule i -> Maybe LNFact Source

lookupConc i ru returns the i-th conclusion of rule ru, if possible.

enumPrems :: Rule i -> [(PremIdx, LNFact)]Source

Enumerate all premises of a rule.

enumConcs :: Rule i -> [(ConcIdx, LNFact)]Source

Enumerate all conclusions of a rule.

Genereal protocol and intruder rules

data RuleInfo p i Source

Rule information for protocol and intruder rules.

Constructors

ProtoInfo p
IntrInfo i

Instances

HasRuleName RuleACInst
HasRuleName RuleAC
(Eq p, Eq i) => Eq (RuleInfo p i)
(Ord p, Ord i) => Ord (RuleInfo p i)
(Show p, Show i) => Show (RuleInfo p i)
(Binary p_1627483252, Binary i_1627483253) => Binary (RuleInfo p_1627483252 i_1627483253)
(NFData p_1627483252, NFData i_1627483253) => NFData (RuleInfo p_1627483252 i_1627483253)
(Apply p, Apply i) => Apply (RuleInfo p i)
(HasFrees p, HasFrees i) => HasFrees (RuleInfo p i)

ruleInfo :: (p -> c) -> (i -> c) -> RuleInfo p i -> cSource

ruleInfo proto intr maps the protocol information with proto and the intruder information with intr.

Protocol Rule Information

data ProtoRuleName Source

A name of a protocol rule is either one of the special reserved rules or some standard rule.

Constructors

FreshRule
StandRule String	Some standard protocol rule

data ProtoRuleACInfo Source

Information for protocol rules modulo AC. The variants list the possible instantiations of the free variables of the rule. The typing is interpreted modulo AC; i.e., its variants were also built.

Constructors

ProtoRuleACInfo
Fields _pracName :: ProtoRuleName _pracVariants :: Disj LNSubstVFresh _pracLoopBreakers :: [PremIdx]

Instances

Eq ProtoRuleACInfo
Ord ProtoRuleACInfo
Show ProtoRuleACInfo
Binary ProtoRuleACInfo
NFData ProtoRuleACInfo
HasFrees ProtoRuleACInfo
HasRuleName RuleAC
HasRuleName ProtoRuleAC

pracName :: forall arr. Arrow arr => Lens arr ProtoRuleACInfo ProtoRuleName Source

pracVariants :: forall arr. Arrow arr => Lens arr ProtoRuleACInfo (Disj LNSubstVFresh)Source

pracLoopBreakers :: forall arr. Arrow arr => Lens arr ProtoRuleACInfo [PremIdx]Source

data ProtoRuleACInstInfo Source

Information for instances of protocol rules modulo AC.

Constructors

ProtoRuleACInstInfo
Fields _praciName :: ProtoRuleName _praciLoopBreakers :: [PremIdx]

Instances

Eq ProtoRuleACInstInfo
Ord ProtoRuleACInstInfo
Show ProtoRuleACInstInfo
Binary ProtoRuleACInstInfo
NFData ProtoRuleACInstInfo
Apply ProtoRuleACInstInfo
HasFrees ProtoRuleACInstInfo
HasRuleName RuleACInst

praciName :: forall arr. Arrow arr => Lens arr ProtoRuleACInstInfo ProtoRuleName Source

praciLoopBreakers :: forall arr. Arrow arr => Lens arr ProtoRuleACInstInfo [PremIdx]Source

type RuleACConstrs = Disj LNSubstVFresh Source

Intruder Rule Information

data IntrRuleACInfo Source

An intruder rule modulo AC is described by its name.

Constructors

ConstrRule ByteString
DestrRule ByteString
CoerceRule
IRecvRule
ISendRule
PubConstrRule
FreshConstrRule

Concrete Rules

type ProtoRuleE = Rule ProtoRuleName Source

A rule modulo E is always a protocol rule. Intruder rules are specified abstractly by their operations generating them and are only available once their variants are built.

type ProtoRuleAC = Rule ProtoRuleACInfo Source

A protocol rule modulo AC.

type IntrRuleAC = Rule IntrRuleACInfo Source

An intruder rule modulo AC.

type RuleAC = Rule (RuleInfo ProtoRuleACInfo IntrRuleACInfo)Source

A rule modulo AC is either a protocol rule or an intruder rule

type RuleACInst = Rule (RuleInfo ProtoRuleACInstInfo IntrRuleACInfo)Source

A rule instance module AC is either a protocol rule or an intruder rule. The info identifies the corresponding rule modulo AC that the instance was derived from.

Queries

class HasRuleName t whereSource

Types that have an associated name.

Methods

ruleName :: t -> RuleInfo ProtoRuleName IntrRuleACInfo Source

Instances

HasRuleName RuleACInst
HasRuleName RuleAC
HasRuleName ProtoRuleAC
HasRuleName ProtoRuleE
HasRuleName IntrRuleAC
HasRuleName ClosedProtoRule

isIntruderRule :: HasRuleName r => r -> Bool Source

True iff the rule is an intruder rule

isDestrRule :: HasRuleName r => r -> Bool Source

True iff the rule is a destruction rule.

isConstrRule :: HasRuleName r => r -> Bool Source

True iff the rule is a construction rule.

isFreshRule :: HasRuleName r => r -> Bool Source

True iff the rule is the special fresh rule.

isIRecvRule :: HasRuleName r => r -> Bool Source

True iff the rule is the special learn rule.

isISendRule :: HasRuleName r => r -> Bool Source

True iff the rule is the special knows rule.

isCoerceRule :: HasRuleName r => r -> Bool Source

True iff the rule is the special coerce rule.

nfRule :: Rule i -> WithMaude Bool Source

True if the messages in premises and conclusions are in normal form

isTrivialProtoVariantAC :: ProtoRuleAC -> ProtoRuleE -> Bool Source

True if the protocol rule has only the trivial variant.

Conversion

ruleACToIntrRuleAC :: RuleAC -> Maybe IntrRuleAC Source

Converts between these two types of rules, if possible.

ruleACIntrToRuleAC :: IntrRuleAC -> RuleAC Source

Converts between these two types of rules.

ruleACIntrToRuleACInst :: IntrRuleAC -> RuleACInst Source

Converts between these two types of rules.

Construction

someRuleACInst :: MonadFresh m => RuleAC -> m (RuleACInst, Maybe RuleACConstrs)Source

Compute some rule instance of a rule modulo AC. If the rule is a protocol rule, then the given typing and variants also need to be handled.

Unification

unifyRuleACInstEqs :: [Equal RuleACInst] -> WithMaude [LNSubstVFresh]Source

Unify a list of RuleACInst equalities.

unifiableRuleACInsts :: RuleACInst -> RuleACInst -> WithMaude Bool Source

Are these two rule instances unifiable.

Pretty-Printing

reservedRuleNames :: [String]Source

List of all reserved rule names.

showRuleCaseName :: HasRuleName (Rule i) => Rule i -> String Source

Pretty print the rule name such that it can be used as a case name

prettyProtoRuleName :: Document d => ProtoRuleName -> dSource

prettyRuleName :: (HighlightDocument d, HasRuleName (Rule i)) => Rule i -> dSource

prettyProtoRuleE :: HighlightDocument d => ProtoRuleE -> dSource

prettyProtoRuleAC :: HighlightDocument d => ProtoRuleAC -> dSource

prettyIntrRuleAC :: HighlightDocument d => IntrRuleAC -> dSource

prettyIntrRuleACInfo :: Document d => IntrRuleACInfo -> dSource

prettyRuleAC :: HighlightDocument d => RuleAC -> dSource

prettyLoopBreakers :: HighlightDocument d => ProtoRuleACInfo -> dSource

prettyRuleACInst :: HighlightDocument d => RuleACInst -> dSource

Eq ProtoRuleName
Data ProtoRuleName
Ord ProtoRuleName
Show ProtoRuleName
Typeable ProtoRuleName
Binary ProtoRuleName
NFData ProtoRuleName
Apply ProtoRuleName
HasFrees ProtoRuleName
HasRuleName ProtoRuleE

Eq IntrRuleACInfo
Data IntrRuleACInfo
Ord IntrRuleACInfo
Show IntrRuleACInfo
Typeable IntrRuleACInfo
Binary IntrRuleACInfo
NFData IntrRuleACInfo
Apply IntrRuleACInfo
HasFrees IntrRuleACInfo
HasRuleName RuleACInst
HasRuleName RuleAC
HasRuleName IntrRuleAC