|Maintainer||Simon Meier <firstname.lastname@example.org>|
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.
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.