Theory.Tools.InjectiveFactInstances

Computate an under-approximation to the set of all facts with unique instances, i.e., fact whose instances never occur more than once in a state. We use this information to reason about protocols that exploit exclusivity of linear facts.

Computing injective fact instances.

simpleInjectiveFactInstances :: [ProtoRuleE] -> Set FactTag

Compute a simple under-approximation to the set of facts with injective instances. A fact-tag is has injective instances, if there is no state of the protocol with more than one instance with the same term as a first argument of the fact-tag.

We compute the under-approximation by checking that (1) the fact-tag is linear, (2) every introduction of such a fact-tag is protected by a Fr-fact of the first term, and (3) every rule has at most one copy of this fact-tag in the conlcusion and the first term arguments agree.

We exclude facts that are not copied in a rule, as they are already handled properly by the naive backwards reasoning.