Common restrictions section in Manual

[claudiacauli]

This is more of a clarification (and support) thread, rather than an actual issue, apologies for that.

In the Common Restrictions section of the manual, two of the common restrictions explained are Unique and OnlyOnceV.
However, these two seem identical to me (modulo renaming). Q1: Am I correct?

Q2: Is it also correct to say that both these restriction could be called AtMostOnce? (given that the rules carrying these facts may appear either 0 or 1 time within a trace).

Also (here comes the support request), to enforce a given rule X to be instantiated ExactlyOnce within every trace, I'm using the following restriction:

restriction exactlyOnceX:
" Ex #i . ExactlyOnceX()@i 
  & All #i #j . ExactlyOnceX()@i & ExactlyOnceX()@j ==> #i=#j "

However, I was unable to write a more general version that is parameterized by a specific instantiation of a variable, as that seems to introduce an invalid formula (universal quantifier without toplevel implication).

// Not allowed
restriction exactlyOnce: 
" All v . ( Ex #i . ExactlyOnce(v)@i ) & ( All #i #j . ExactlyOnce(v)@i & ExactlyOnce(v)@j ==> #i=#j ) "

Q3: Would you confirm that the only way to enforce a rule to appear exactly once in a trace is by my first restriction?
(And there is no way to have a more general version like my second restriction?)

Thanks!

[rsasse]

Your Q1 raises a good observation, you are correct. The two restrictions are indeed renamings of each other. The idea behind their (duplicate) explanation in the manual was that the first one is intended for values as parameters, while the second one was intended for rule names as parameters. These are of course both usable in both ways.

@ Tamarin team: we should fix this, by at least adding a comment that these are the same, but the proposed use case is different. Alternatively drop one, and put one explanation for values and rule names.

For Q2, the naming of the restrictions or facts used by them are not important anyway, and indeed their semantics is that the fact may appear 0 or 1 times, but no more than that.

"ExactlyOnceX", without parameter (as described by you), or with a fixed (constant) parameter (like a rule name as 'string') is possible, as you observe. But note that it means that the empty trace is NOT a valid trace for the system any more. So, when trying to prove any lemma, the initial states Tamarin considers will already each contain an instance of a rule with that fact (plural because there might be multiple rules with this).

You can actually extend this to a fixed number of instances (either as maximum, or requiring exactly that many), which is a bit cumbersome to write for larger numbers, and will result in the initial states containing many instances.

Having the lemma you call "exactlyOnce" with a value all-quantified is simply not possible. What would it mean for the initial state? Well, it would have to contain a rule with an instance of that fact FOR EVERY POSSIBLE VALUE. Observe that the quantification here is NOT over a given set of values already appearing in your trace, or over some arbitrary chosen small set. It is rather over the infinite set of all possible values (including all fresh and public variables, etc.). So, the initial state for Tamarin must be infinitely large already, which is not useful to analyze. Thus, the requirement of the formula having to be guarded (shown by the "universal quantifier without toplevel implication" error) saves you from this situation that could not possibly terminate or be useful.

For Q3 it is not quite that clear to me what you are asking, so I cannot say yes/no. As mentioned, we can write it for many fixed constants, or have one restriction that requires multiple such with fixed constants. Note that maybe what you seem to want is some notion of "progress", i.e., that something must have happened for you to consider the trace relevant? There is already work in that direction:

"A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange" by Michael Backes, Jannik Dreier, Steve Kremer, Robert Künneman. See https://hal.inria.fr/hal-01396282/file/fairexchange-long.pdf