Interpretating interactive mode for source lemma

[Yuheng Wen]

Hi Group! 

Does the green or red highlight on the left penal for source lemma, or lemma that uses induction in general, mean anything? I wrote my source lemma that should be easily proved and shows "SOLVED" with red highlights. In terms of how Tamarin prove property by induction, as explained in manual 9.1, if I see "SOLVED", I should expect that it means my source lemma is proven to be true, right? I did not find explanations in the manual regarding how to interpret the resulting highlights after running autoprove for source lemma, and the hightlights truly confuse me. 

Thank you in advanced for your help!

Yuheng

[Felix Linker]

Hi Yuheng,

Red means that the lemma is false. Tamarin constructed a counter example. The GUI shows "SOLVED" because Tamarin uses constraint solving to prove formulas. It first negates the property to be proven, and then creates a constraint system that describes a minimal counterexample. To prove a property, we must show that this constraint system is contradictory by applying constraint solving rules, which (in general) leads to case splits and the proof tree. If Tamarin, during constraint solving, finds a "SOLVED" constraint system, this shows that the constraint system is not contradictory (as it could be solved), and it shows you a counter example to your lemma.

Sidenote: I see the arrows in your picture are a bit messy. This was caused by a bug in GraphVIZ version 14.0.0. I suggest upgrading your GraphVIZ dependency to 14.0.1 or higher to have nicer rendered arrows!

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/f0fefcf2-a0ca-4444-a06a-b64741205bfen%40googlegroups.com.

[Yuheng Wen]

Hi Felix,

Thank you for the quick response! 

I understand that what you described is how things works to prove a regular lemma, but I am wondering to interpret the interactive proof for source lemma, or lemma using induction, does this same way of interpretation apply? Because it seems to me that for lemma uses induction, the once we found a solution to the constraint system for the last time point, it means this property is proven instead of a counter example is found. 

Thank you! 

Yuheng

[Felix Linker]

Hi Yuheng,

The output should not be interpreted differently when using induction. It means exactly the same. Your property is false.

Best,

Felix

To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/a40ed592-5efe-4cda-beea-f1a3be46a82an%40googlegroups.com.

[Yuheng Wen]

Thank you for the clarification! 

To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/CAPeSryrNQhGmytN5%2BaNCxzMdFNVMQw%3DfXW-0KnL3f8q%3DtFr11A%40mail.gmail.com.