Revocation and refresh modelling

[Daniel S]

Dear All,

Is there a recommended way to handle protocol actions such as key revocation or key refreshing using tamarin? I'd like to have facts that I can use multiple times, but that I can also modify using other rules. I could use linear facts and duplicate them in input and output, but that feels very likely to run into termination problems.

I presume that there is no way to force consumption of a persistent fact nor any way to change its terms (which would be solutions to my question).

With thanks in advance,

Daniel

[Cas Cremers]

Hi Daniel,

While this is a typical case that we want to make better in the future, I think in this case I would recommend:

 - Model the keys using persistent facts
 - Ensure revocation of a key has a corresponding action fact "Revoke(k)"
 - At the point in your model where a user supposedly checks if a key k is revoked, add an action "IsNotRevoked(k)"
 - Add a restriction that forces that for all IsNotRevoked(k)@i, there cannot be a Revoke(k)@j with j < i .

You can do something similar for refreshing keys.

Hope this helps,

Cas