Tamarin looking for sources posted May 2017

Tamarin will sometimes be unable to find the real source of a premise ([premise]-->[conclusion]) and will end up spinning until the scary words "partial deconstructions" will be flashed at the screen.

Raw sources is Tamarin trying to find the source of each of your rules. That's a bunch of pre-computation to help him prove things afterwards, because Tamarin works like that under the hood (or so I've heard): it searches for things backward.

(This might be a good reason to start designing your protocol from the end!)

Partial deconstructions can happen when for example you happen to have used a linear fact both in the premise and the conclusion of a rule:

rule creation:
  [Fr(~a)]-->[Something(~a)]

rule loop:
  [Something(a)]-->[Something(a), Out(a)]

This is bad, because when looking for the source of the loop rule, Tamarin will find the loop rule as a possible origin. This over and over and over.

Source lemmas are special lemmas that can be used during this pre-computation to get rid of such loops. They basically prove that for such loop rules, there is a beginning: a creation rule. Source lemmas are automatically proven using induction which is the relevant strategy to use when trying to prove such things.

Refined sources are the raw sources helped by the source lemmas. If your wrote the right source lemmas, you will get rid of the partial deconstructions in the refined sources and Tamarin will use the refined sources for its proofs instead of the raw sources.

Persistent Facts is the answer. Anytime we have a linear fact persisting across a rule, there is little reason (I believe) not to use a persistent fact (which also allows to model replays in the protocol). We can now rewrite our previous rules with a bang:

rule creation:
  [Fr(~a)]-->[!Something(~a)]

rule loop:
  [!Something(a)]-->[Out(a)]

This way Tamarin will always correlate this Fact to its very creation.