Can I reuse a wrong result to prove another lemma?

[Marco Calipari]

Hi everyone,

I ran into something interesting while working with Tamarin for my project on Monday. I set up three lemmas: I expected one to fail and the other two to pass. However, one of the lemmas that was supposed to pass didn't because it looks like the attacker was able to pretend to be a CA.

Here's the twist: when I reuse (with the [reuse] command) the result from the lemma I expected to fail as part of my analysis, the lemma that didn't pass before now passes.

I'm not an expert, but I'm wondering if it's possible to use a failed result to make another lemma work, especially if the now verified lemma failed for a reason that doesn't make sense. I'm guessing this might happen because Tamarin might ignore some traces, but I'm not totally sure.

What do you all think?

Cheers!

[Jannik Dreier]

Hi,

Reuse lemmas are reused no matter if they are proven or not (to be able
to reuse them without being obliged to reprove these lemmas every time
one loads a theory).

This means in particular that also "wrong" lemmas can be reused, i.e.,
Tamarin will use the "wrong" statement as an assumption when proving the
following lemmas.

This implies that if one of the reuse lemmas is wrong, all following
results become essentially meaningless. So always make sure your reuse
lemmas are true and can be proven!

Best,
Jannik

> --
> 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
> <mailto:tamarin-prove...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tamarin-prover/4c76f4d6-11b3-41c8-bb8f-fb03f9208a42n%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/4c76f4d6-11b3-41c8-bb8f-fb03f9208a42n%40googlegroups.com?utm_medium=email&utm_source=footer>.

--
Jannik Dreier
Maître de Conférences | Associate Professor
Université de Lorraine | TELECOM Nancy | LORIA
rese...@jannikdreier.net | +33 3 54 95 84 46

[Ralf Sasse]

Hi Marco,

To clarify [reuse] lemma behavior: these lemmas are reused in all other later lemmas, even if they are not proved, and even if they are actually wrong(!).

So, if you set up lemmas like

lemma A [reuse]

lemma B

Then the content of lemma A may be used in the proof attempt of B. So, if A were to just say 'false', B is now easily provable.

Separately from that, if Tamarin finds an attack that looks weird to you, then you should carefully inspect the attack to ensure it really is not possible. If you are convinced, then you have to adjust the model to make sure the attacker cannot do what it should not (say, impersonate a CA). You can do this using extra action facts and restrictions, or encoding this in the security property lemmas.

Cheers,
Ralf

Cheers! --
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/4c76f4d6-11b3-41c8-bb8f-fb03f9208a42n%40googlegroups.com.

[Marco Calipari]

Dear all,

Thank you for your prompt response.

I believe I may have used incorrect terminology previously. To clarify, my setup is as follows:

Lemma A [reuse]
Lemma B
In this setup, Lemma A is falsified, which was expected and thus is considered "correct". However, if I do not reuse Lemma A, Lemma B is also falsified due to the implausible scenario in which the protocol operates with the CA acting as an agent rather than strictly as a CA. Conversely, by reusing Lemma A (despite its falsification), Lemma B is verified, aligning with my expectations for the protocol.

Given this, I am pondering whether the results can be deemed meaningful, or if the mere fact that one of the lemmas is falsified and then reused could lead to incorrect conclusions.

Thank you for your time and patience.
Cheers

[Marco Calipari]

What I mean by "correct" is that I expect it to become red, simply speaking. If it were not to be red that would mean that there is a problem in the model.

[Ralf Sasse]

To reiterate what Jannik said:

It does not matter if the reuse lemma is true or false. It also does not matter what the user thinks it should be. The reuse lemma can indeed be used in any other later lemma.

Essentially, if you have a reuse lemma that is not provable (or falsified), then ALL PROOFS OF LEMMAS SYNTACTICALLY LATER must be considered POTENTIALLY WRONG.

If I write

lemma A [reuse]: "false"

and then have a lemma B, then Tamarin will first falsify lemma A. Nevertheless, it will still use lemma A to "prove" lemma B. Now, I have not learned anything about whether B is true or not.

Overall, this is the responsibility of the user. Only mark a lemma as reuse if you are sure that it will correctly verify.

Cheers,
Ralf

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/669e60d9-292d-4940-8da4-ada93390e08dn%40googlegroups.com.