Tamarin-prover server cannot load a theory

[Lucca Hirschi]

Hi,

I'm trying to verify some privacy-related properties for the PACE protocol (embeds in ePassport RFID chips) but
I encounter a problem when loading the theory in interactive mode. The command

tamarin-prover interactive ./pace.spthy

works well without any warning and I can browse http://127.0.0.1:3001 and see by theory
but when I want to open the theory (by clicking on it), nothing happen
neither from the wepage, nor from the tamarin-prover daemon.
Note that in non-interactive mode, tamarin seems to loop indefinitely without logging
anything.

I don't know if my theory is badly written or it is a bug.
I used the tool Sapic (http://sapic.gforge.inria.fr/) to automatically
translate my modelization in Applied Pi-calculus style into MSR. Both
files are attached.

Kind regards,
Lucca Hirschi

[Benedikt Schmidt]

Hi Lucca,

it seems tamarin gets stuck when computing the variants of your rules.
Roughly, whenever you have x ^ y in your rules, this gets expanded to
multiple rules that cover all the possibilities. For example the case
where x = u ^ (w1*w2) and y = w1^-1 * w3 (for some u,w1,w2,w3) yields
the reduced result u1^(w2*w3). The number of variants grows very quickly
if your exponentiations are unrestricted. To limit the number of cases,
it helps to have as much local sort information as possible. For
example, x^~y (~y means that y can only be instantiated with fresh
values) generates fewer cases than x^y.

On thing you could try out it is to annotate the sorts as follows:
1. Whenever you get a fresh value using Fr, use a fresh variable Fr(~s).
2. Propagate this information manually. For example, if you know the
first component of State_010 is always of sort fresh, you can pattern
match in the LHS using a fresh variable.

You can see this pattern in the rules Init1 and Init2:
https://github.com/tamarin-prover/tamarin-prover/blob/develop/examples/csf12/NAXOS_eCK.spthy

Maybe Robert and Steve can tell you if it's possible to modify the sapic
input to get such a refined model.

Best,
Benedikt

> --
> You received this message because you are subscribed to the Google
> Groups "tamarin-prover" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to tamarin-prove...@googlegroups.com
> <mailto:tamarin-prove...@googlegroups.com>.
> To post to this group, send email to tamarin...@googlegroups.com
> <mailto:tamarin...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tamarin-prover/62d312e9-e35a-4127-9d00-8d82c3f568ee%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/62d312e9-e35a-4127-9d00-8d82c3f568ee%40googlegroups.com?utm_medium=email&utm_source=footer>.
> For more options, visit https://groups.google.com/d/optout.

[Lucca Hirschi]

Hi Benedikt,

thanks for the very quick answer and help.

I did what you suggested and simplified MSR rules a lot.
Now, Tamarin loads correctly the theory and is able to prove all my sanity-checks
almost automatically.

I'll work more on this and try to prove Unlinkability (of the ePassport). If you are
interested, the new file is attached.

Thanks again,
Lucca