tamarin GUI Red Background color
57 views
Skip to first unread message
Alsita Putri
Jun 9, 2021, 4:19:10 AM6/9/21
to tamarin-prover
Hello all,
in tamarin GUI output, the red background color means that tamarin found counterexample to the lemma. But here I can't find the counterexample in the form of attack from the graph, and it is said that the theory is included into the "solved formulas". Also it is said that "constraint system is solved" . So is there something wrong with the theory? And what does it means?
Really looking forward for your help, thank you
in tamarin GUI output, the red background color means that tamarin found counterexample to the lemma. But here I can't find the counterexample in the form of attack from the graph, and it is said that the theory is included into the "solved formulas". Also it is said that "constraint system is solved" . So is there something wrong with the theory? And what does it means?
Really looking forward for your help, thank you
Jan
Jun 9, 2021, 4:43:10 AM6/9/21
to Alsita Putri, tamarin-prover
Hi Alsita,
The Commit action fact emitted at the bottom has $U and $CS as the first two parameters, but the running fact has $U and $U. I think this does not satisfy the requirement that if there is a Commit(A, B, ...) then there also exists a Running(B, A, ...) fact, because (I believe) $U ≠ $CS. I couldn't find in the trace what $CS actually is, so maybe it happens to coincide with $U, in which case I would be wrong.
I hope that helps!
Jan
The Commit action fact emitted at the bottom has $U and $CS as the first two parameters, but the running fact has $U and $U. I think this does not satisfy the requirement that if there is a Commit(A, B, ...) then there also exists a Running(B, A, ...) fact, because (I believe) $U ≠ $CS. I couldn't find in the trace what $CS actually is, so maybe it happens to coincide with $U, in which case I would be wrong.
I hope that helps!
Jan
--
Sent from my Android device with K-9 Mail. Please excuse my brevity.
Sent from my Android device with K-9 Mail. Please excuse my brevity.
Ralf Sasse
Jun 9, 2021, 5:30:17 AM6/9/21
to tamarin...@googlegroups.com, Jan, Alsita Putri
Hi Alsita,
Indeed, as Jan says, the screenshot shows a violation of your formula, that is, there is a Commit but no Running with the right parameters. The red shows an attack as expected, and the "Solved" is with respect to the negation of the property, meaning such a solution is an attack trace.
Best regards,
Ralf
Sent from my Android device with K-9 Mail. Please excuse my brevity. --
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 on the web visit https://groups.google.com/d/msgid/tamarin-prover/3A7421D2-398E-4AC1-BC90-7BA03CC87F12%40tuhh.de.
Alsita Putri
Jun 17, 2021, 10:39:49 PM6/17/21
to tamarin-prover
thankyou so much for al off your helps,
I have another question, what's the meaning of the dotted line in the GUI output?
I have another question, what's the meaning of the dotted line in the GUI output?
Ralf Sasse
Jun 18, 2021, 4:50:52 AM6/18/21
to tamarin...@googlegroups.com, Alsita Putri
Dotted lines in the GUI are time point relations, meaning that somehow (probably from a lemma, where #i < #j) the tool knows that the one rule instance must happen before the other, with the dotted line going from the earlier to the later event.
Cheers,
Ralf
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/3546c947-6e6b-4bf1-b20c-c6cc5612df1dn%40googlegroups.com.
Alsita Putri
Jul 5, 2021, 4:13:48 AM7/5/21
to tamarin-prover
thank you so much for your help ^^
Reply all
Reply to author
Forward
0 new messages