Semi-Persistent Facts
I would like to share some knowledge on how to model semi-persistent facts. Maybe they find their way into the manual at some point or (ideally) they are implemented directly in Tamarin.
Use Case
While persistent facts are read-only-and-never-change and linear facts are destroy/consume-on-read, we often need a thing inbetween. For example modeling a storage cell with an identifier ~id
where we sometimes want to read the value but sometimes also want to change it.
Implementation with Linear Facts (not recommended)
With that, the exact same Fact has to be inserted again in the Read
-rule such that it is not destroyed when reading it:
rule Init: [Fr(~id), In(val)] --> [Cell(~id, val)]
rule Read: [Cell(~id, val)] --> [Cell(~id, val), Out(val)]
rule Write: [Cell(~id, oldVal), In(val)] --> [Cell(~id, val)]
This has one big disadvantage: Often in proofs, we need to find the source of a value. For example "where did that secret key come from". If we have some Read
-rules between writing and the current point, Tamarin is easily trapped into a loop or has to unfold many Read
-steps before finding the source - the rule where the value was actually written.
Implementation with Persistent Facts and Restrictions
The other idea is to use persistent facts as follows:
rule Init:
[Fr(~id), In(val)]
--[WriteCell(~id, val)]->
[!Cell(~id, val)]
rule Read:
[!Cell(~id, val)]
--[ReadCell(~id, val)]->
[Out(val)]
rule Write:
[In(~id), In(val)]
--[WriteCell(~id, val)]->
[!Cell(~id, val)]
restriction StorageCell:
"∀ id c #i. ReadCell(id, c)@i
==> ∃ #j. WriteCell(id, c)@j ∧ j<i
∧ ¬∃ d #k. WriteCell(id, d)@k ∧ j<k ∧ k<i"
Note that we have to add action facts to the rules now such that the restriction can talk about them.
The restriction then ensures that when reading from a cell, there has to be a WriteCell
with the same value which was not overwritten.
That approach works but has some caveats. Notably, the restriction will spawn a WriteCell
goal for each ReadCell
. This can cause looping problems if ReadCell
and WriteCell
are in the same rule. But even without that, it creates additional goals which are not needed as there is already a goal that aims to satisfy the source of the persistent fact !Cell(...)
. A better way to write what we want in a restriction is actually:
restriction StorageCellBetter:
"∀ id c d #i #j #k. WriteCell(id, c)@i
∧ WriteCell(id, d)@j ∧ i<j
∧ ReadCell(id, c)@k ∧ j<k
==> ∃ #l. WriteCell(id, c)@l ∧ ¬l<j ∧ l<k"
Here we let the persistent fact goals for !Cell(...)
do their job until a "bad" situation occurs where we have a second WriteCell@j
inbetween a ReadCell@i
and a WriteCell@k
. In that case we require a third WriteCell@l
which is after the second WriteCell@j
(or equal to it in case of c=d
).
This way of writing the restriction is much less invasive as it triggers only if we have a "bad" situation to "heal" it. Thus, it does not pollute our goals.
Separating cells
Quite often, we want to store multiple values grouped together. For example on a device ~id
we store a long term key ltk
and an ephemeral key eph
which is changed each protocol iteration. Then we can model this as Cell(~id, ltk, eph)
. However, if we want to find the source of the ltk
, we would have to trace it back trough all changes of eph
which usually requires to write (possibly multiple) loop breaker lemmas.
Instead we can model the same behaviour with separate facts LtkCell(~id, ltk)
and EphCell(~id, eph)
- deciding upon need which one is persistent, semi-persistent or linear. That has the advantage that it is now irrelevant how often we change eph
between writing and reading ltk
because we directly jump to the source of ltk
. Note that you then need a restriction for each Cell name which would be StorageLtkCell
and StorageEphCell
in this case.
Be aware that this separation has disatvantages as well - especially when trying to prove connections between two separated values. And writing a fitting oracle might be harder because you have to deal with more goals. However, I found that it helps especially for more complex protocols where I had to write oracles anyways.
A Direct Implementation in Tamarin
There are multiple ways of dealing with the problems of semi-persistence and separation and I'm thinking about ways to implement them. Things that I thought about:
- Adding the action facts is quite nasty and a source of error if they become out of sync with the persistent facts when changing the model
- Letting the user write the restrictions is a source of error
- Thus, it would be nice to have a new type of fact (maybe called storage-fact) which does effectively what we do with persistent facts and restrictions.
- If we use a constraint rewriting rule for that (instead of a restriction) we can directly refer to the rule that satisfied the premise fact instead of using an existential quantification as a hack to refer to it
- We can automatically detect linear facts that should be rewritten as storage facts and hint the user
- Automatically (internally) splitting facts is harder because it is not always beneficial - though it is definitely worth looking into them. One thought was to write
Cell(~id, a, b, _, _, _)
if only a
and b
are read and the others are unimportant for that specific rule.