Reuse Behavior

[Hugo Mqt]

Hi, I hope it is not redundant wih the previous question on "Reuse Behavior".

I am a newbie on Tamarin and I am trying to code the basic TLS Handshake on it.

So I had a lemma for session key secrecy that was proven as false with an autoprove (without aridity of 5).

Then I wrote some other lemma (inspired by the implementation of C.Cramers) and used some lemma labelled as [reuse].
Then it worked (I used one autoprove with aridity of 5 because my PC crashed otherwise). 

It worked because I did not do a whole autoprove and thus missed the couter example or is it due to the behavior of Reuse ? 

If it is due to the behavior of Reuse, why is this changing the verification. Because as I understood : lemma are just things that need to be verified by the deconstruction of the rules and thus does not induce any changes. 

Thanks for the answer :) 

Have a good day,

Tamarin Newbie

[Ralf Sasse]

Hello,

I am not entirely sure what you did, but can clarify the behavior of reuse lemmas. Tamarin assumes all reuse-marked lemmas are correct, and it is the obligation of the user to check that they do verify. To make an extreme example, not using actual tamarin syntax:

lemma prop1: "False"

lemma fake [reuse]: "False"

lemma prop2: "False"

Tamarin will correctly falsify lemma prop1, as expected. Tamarin will also falsify lemma fake. After that, lemma prop2 is proven correct. This is due to the fact that Tamarin uses lemma fake as a reuse lemma, independently of whether it has already been verified/falsified and whether it's correct or not. This is the user's responsibility.

Thus, any Tamarin theory which contains reuse lemmas require that those are correct, otherwise verification results following that reuse lemma are invalid.

Independent of that, if you only do a partial proof up to a certain depth, and there is no counter-example until that depth, it is unknown whether the statement holds or not. If there is any "sorry" proof goal left the result is unknown. If no "sorry" are left, the bounded verification can suffice.

Cheers,
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/302a6c3f-71f8-445c-b97f-7bfe1ffa9b11n%40googlegroups.com.