Subterm restriction causes unexpected lemma contradictions

[Nikodem Witkiewicz]

Hi Tamarin group,

I want to use the subterm operator "<<". I found some Tamarin behavior with this operator that I don't understand. I provide the model in the attachment and its description below, with questions at the end of the email.

*Model Description*
We have one rule that generates a fresh value a and evaluates the function g(a). It separately saves a and g(a) in actions, and also creates, separately, A(a) and G(g(a)) facts in the conclusions. Then we have a second rule that simply takes A and G in the premises and saves an AG(a,g) action. Finally, I add the restriction "All A G #i. AG(A,G)@i ==> A << G". Generally, I want to ensure that every rule with an AG(a,g) action is constructed with an a such that it is a subterm of g (i.e., a was used to evaluate g).

I wrote some experimental lemmas and got unexpected results. I will focus specifically on the four of them: the 4th, 5th, 6th, and 7th lemmas, but in the attachment I sent a file with all of them.

Namely, the 4th lemma states that there exists a trace with an AG(A,G) action, and because of the restriction, it is false. But why exactly it is false, I don't know. Tamarin ends the proof with "contradiction /* cyclic */", where it points to a constraint system with a rule with action AG(a,g(a)). That's exactly what I wanted to prove is possible, but we have a false statement.

Moreover, the 6th lemma is the same but with added pattern matching such that we are sure that the terms a and g are created in the same rule: "Ex a g #i #j. Aa(a)@i & G(g)@i & AG(a,g)@j". This lemma is true. This lemma is more restrictive than the 4th one and is true.

Lemmas 5th and 7th are equivalents of the 4th and 6th, but they require that a is a subterm of g. Their proofs are exact copies of the 4th and 6th.

Questions:
1. What exactly does it mean that Tamarin found a "contradiction /* cyclic */"?
2. Why are the 4th and 5th lemmas false, but when we enforce that a and g are created in the same rule, then these statements are true?

Bests, 
Nikodem 

[Felix Linker]

Hi Nikodem,

Thank you for reaching out with your theory! The behavior you see is certainly a bug and I was able to reproduce the behavior in a smaller theory. I created an issue with a hypothesis on where the bug comes from: https://github.com/tamarin-prover/tamarin-prover/issues/809

But to your questions:

1. Tamarin supports constraints on time, i.e., that one event needs to happen after another. When there are two events that have a circular time dependency, Tamarin derives the contradiction "cylic." One place where this comes up often is when the adversary needs to use a fresh term before it was introduced.
2. The issue seems to come from Tamarin deriving wrongly that one event must have happened before the other. When you solve for the subterm formula, the two events are unified (made the same), but now Tamarin believes that the event must have happened "before itself." I don't know why Tamarin derives this, but the issue seems less to come from subterm reasoning, and more from Tamarin deriving when events need to happen before one another.

I hope we can investigate and fix this soon. Thank you very much for reporting!

Best,

Felix

--
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.
To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/9135a162-a624-4a0e-9afb-0c3d6f97d9a5n%40googlegroups.com.

[Nikodem Witkiewicz]

Hi Felix,
Thank you very much for your answers. It's quite funny to find a bug in a tool to find "bugs". I'm glad I could help.

Best,
Nikodem 

To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/CAPeSryrQg4rFf6uF0dnLEnUgAkYoZ4vYn5E0gaxpb14DbH5TXQ%40mail.gmail.com.