what does "/* from formulas */" mean

[mmhuang]

Hi everyone:

I am a novice of tamarin prover. I did practice according to tamarin_toy_protocol (https://github.com/benjaminkiesl/tamarin_toy_protocol/tree/master). 

In toy_protocol_3_mac.spthy, I tried to prove lemma if_b_finishes_a_has_finished_too, the output showed "by contradiction /* from formulas */". I can understand the result is in contradiction, so the trace is not exist and lemma is true. However, what does "from formulas" mean? Is there a trace showed in the output GUI image.

Thanks very much.

Huang

[Felix Linker]

Hi Huang,

„From formulas“ means that either (a) parts of your initial lemma, (b) an auxiliary lemma, or (c) a restriction lead to the contradiction.

Let me give an example. Presume, you would like to prove secrecy but it is part of your threat model that you do not consider compromised public keys. Your lemma could look something like this:

lemma Secrecy:

  „All m #x. Sent(m) @ #x ==> (not Ex #t. K(m) @ #t) | (Ex #x. PublicKeyReveal() @ #x)“

When you start proving this formula, it will be negated yielding:

  Ex m #x. Sent(m) @ #x & (Ex #t. K(m) @ #t) & (All #x. PublicKeyReveal() @ #x ==> \bot)

Tamarin will next instantiate the Sent and K facts on the trace, leaving you with the formula (All #x. PublicKeyReveal() @ #x ==> \bot). Should it now happen that the fact PublicKeyReveal appears in your dependency graph, Tamarin will apply a constraint reduction rule that introduces the formula \bot into the constraint set, which is a direct contradiction. This contradiction is marked as „from formulas,“ because Tamarin applied formula reduction rules to derive it.

I hope this is clear!

Best,

Felix

On 1 Aug 2024, at 03:11, mmhuang <mmhua...@gmail.com> wrote:

Hi everyone:

I am a novice of tamarin prover. I did practice according to tamarin_toy_protocol (https://github.com/benjaminkiesl/tamarin_toy_protocol/tree/master). 

In toy_protocol_3_mac.spthy, I tried to prove lemma if_b_finishes_a_has_finished_too, the output showed "by contradiction /* from formulas */". I can understand the result is in contradiction, so the trace is not exist and lemma is true. However, what does "from formulas" mean? Is there a trace showed in the output GUI image.

Thanks very much.

Huang

<Snipaste_2024-08-01_09-10-06.png>

<AReceiveNonceInstallKey.png>

--
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/f341fa0e-6d02-45b4-aba3-e24da3337ac0n%40googlegroups.com.
<toy_protocol_3_mac.spthy><AReceiveNonceInstallKey.png><Snipaste_2024-08-01_09-10-06.png>