help lemma

[hua hua]

Through manual searching, I found that when solving `solve(!KU(~k)@#vk)`, it would derive from `reveal_Ltk_Sym` and `secureChannel_compromised_out`. Therefore, I wrote a help lemma to prove that if the attacker knows `k`, then `k` must have been leaked and the channel must have been compromised, and the help lemma was proven correct (first figure) and marked as reuse. However, during the proof of the lemma below, I found that `solve(!KU(~k)@#vk)` still needs to be solved again (second figure) and cannot be proven directly. I believe the help lemma did not work, but I don't know why. I look forward to your response.

[Felix Linker]

Hi,

I think the issue is that you use K in your auxiliary lemma and not KU. Intuitively, K means that the adversary can derive something, and KU means that they used some value in their derivation. K can be thought of as a possibilistic fact. Tamarin will not instantiate it on its own. When you write auxiliary lemmas for the adversary, it’s sometimes better to use KU.

Cheers,

Felix

On 25 Nov 2024, at 15:29, hua hua <hhua...@gmail.com> wrote:

<11.png><22.png>Through manual searching, I found that when solving `solve(!KU(~k)@#vk)`, it would derive from `reveal_Ltk_Sym` and `secureChannel_compromised_out`. Therefore, I wrote a help lemma to prove that if the attacker knows `k`, then `k` must have been leaked and the channel must have been compromised, and the help lemma was proven correct (first figure) and marked as reuse. However, during the proof of the lemma below, I found that `solve(!KU(~k)@#vk)` still needs to be solved again (second figure) and cannot be proven directly. I believe the help lemma did not work, but I don't know why. I look forward to your response.

--
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 visit https://groups.google.com/d/msgid/tamarin-prover/79bc19a2-2ff9-451c-931e-29d870f8986dn%40googlegroups.com.
<22.png><11.png>

[hua hua]

Dear Felix

Thank you for your response,I have already tried (first figure), but it still did not work (second figure). Another question I have is regarding the role of the help lemma. My understanding is that when proving other lemmas, if a help lemma is reused and the same proof process as the help lemma is encountered, it should skip that part to speed up the proof process. I'm not sure if my understanding is correct?

[hua hua]

Dear All,

I have noticed a phenomenon: if I replace `Ex X key #r. Rev(X, <'k',key>)@r & Honest(X)@i` in the lemma with `Ex X data #r. Rev(X, data)@r`, the help lemma works (first figure). Moreover, even if I replace it with `Ex X data #r. Rev(X, data)@r & Honest(X)@i`, it still does not work. Why is this?

[Felix Linker]

Hi Hua Hua,

It’s hard to comment on your lemmas beyond what I’ve written initially. An auxiliary can help you in many ways. If you expect to derive an immediate contradiction from the auxiliary lemma, it must be strong enough to let you derive that.

For example:

If you have a lemma of the form: „All … P1 ==> Q | not R1“, and an auxiliary lemma „All … P2 ==> R2“ and you expect this lemma to let you derive a contradiction, you must have „R2 ==> R1.“

Does that make sense?

Cheers,

Felix

On 26 Nov 2024, at 09:45, hua hua <hhua...@gmail.com> wrote:

Dear All,

I have noticed a phenomenon: if I replace `Ex X key #r. Rev(X, <'k',key>)@r & Honest(X)@i` in the lemma with `Ex X data #r. Rev(X, data)@r`, the help lemma works (first figure). Moreover, even if I replace it with `Ex X data #r. Rev(X, data)@r & Honest(X)@i`, it still does not work. Why is this?

<333.png>

在2024年11月26日星期二 UTC+8 09:16:31<hua hua> 写道：

Dear Felix

Thank you for your response,I have already tried (first figure), but it still did not work (second figure). Another question I have is regarding the role of the help lemma. My understanding is that when proving other lemmas, if a help lemma is reused and the same proof process as the help lemma is encountered, it should skip that part to speed up the proof process. I'm not sure if my understanding is correct?

在2024年11月25日星期一 UTC+8 22:36:17<linke...@gmail.com> 写道：

Hi,

I think the issue is that you use K in your auxiliary lemma and not KU. Intuitively, K means that the adversary can derive something, and KU means that they used some value in their derivation. K can be thought of as a possibilistic fact. Tamarin will not instantiate it on its own. When you write auxiliary lemmas for the adversary, it’s sometimes better to use KU.

Cheers,

Felix

On 25 Nov 2024, at 15:29, hua hua <hhua...@gmail.com> wrote:

<11.png><22.png>Through manual searching, I found that when solving `solve(!KU(~k)@#vk)`, it would derive from `reveal_Ltk_Sym` and `secureChannel_compromised_out`. Therefore, I wrote a help lemma to prove that if the attacker knows `k`, then `k` must have been leaked and the channel must have been compromised, and the help lemma was proven correct (first figure) and marked as reuse. However, during the proof of the lemma below, I found that `solve(!KU(~k)@#vk)` still needs to be solved again (second figure) and cannot be proven directly. I believe the help lemma did not work, but I don't know why. I look forward to your response.

-- 
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 visit https://groups.google.com/d/msgid/tamarin-prover/79bc19a2-2ff9-451c-931e-29d870f8986dn%40googlegroups.com.
<22.png><11.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 visit https://groups.google.com/d/msgid/tamarin-prover/cd59ecb8-bf8f-460c-98e7-dc1bd9bed643n%40googlegroups.com.
<333.png>

[hua hua]

Dear Felix

Thank you for your response,I think in my model R2 =\=> R1,so the help lemma not work.