How to suppress constraint graph using lemmas

[Prashant Agrawal]

Hi,

I am just starting up with Tamarin, and I was wondering if it is possible to suppress part of the constraint graph using sources lemmas/reuse lemmas, etc. 

Consider the following example:

1. A rule R has Recv(m,S) in its premise.

2. I have proved in a separate lemma L the following property: All m,S #i1. Recv(m,S)@i1 => (Ex i2. Sent(m,S)@i2 & i2<i1).

3. Can I make the Tamarin constraint graph in the GUI connect source Sent(m,S) directly to R (i.e., using lemma L) and not show me the full derivation of Received(m,S)? Since authenticated channels are part of a much larger system I am modelling, seeing all these derivations clutters the view very much and makes debugging very difficult. 

Thanks for any help.

Prashant  

[Ralf Sasse]

Dear Prashant,

Unfortunately, it is not possible to hide parts of the displayed graphs at the moment. This feature may be added in the future in an overhaul of the graph presentation.

The lemmas are still useful to improve search performance when marked [reuse] as you do.

Best regards,
Ralf

--
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/7fec8104-b5ec-4a59-bfe6-2a143a5a52afn%40googlegroups.com.

[Prashant Agrawal]

Thank you for the response. Is it at least possible to see somewhere which goals were discharged using one of the source/reusable lemmas, so that I can manually skim over parts of the proof tree that were derived using already proven lemmas?

Thanks,

Prashant 

[Ralf Sasse]

The only thing I could think of is to watch in the interactive mode which proof step applies a lemma and the resulting graph addition could be skimmed. But after further steps you have to re-identify this yourself each time, so it's not practical, I feel.

If anyone else has another, actually useful, idea for this problem, do let us know!

Cheers,
Ralf

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/ade0494d-3c13-4e06-809a-d9122e7d36bcn%40googlegroups.com.

[Prashant Agrawal]

Okay. Thank you for that tip. I'll keep an eye out on this thread to see if someone has another idea.