Limitations of Observational Equivalence Mode

[Henning Arvid Ladewig]

Dear all,

I am a bachelor's student and recently started familiarising myself with Tamarin.
Especially observational equivalence raised my interest.

A simple theory for exploring the limitations of this mode I came up with is the following:

theory DiffIndMin begin

rule Start:
    [ Fr(~id), Fr(~a), Fr(~b) ]
  --[ OnlyOnce(), Start(~id, ~a, ~b) ]->
    [ L(~id, ~a, ~b) ]

rule Step:
    [ L(~id, a, b) ]
  --[ Step(~id, a, b) ]->
    [ L(~id, a, b) ]

rule Stop:
    [ L(~id, a, b) ]
  --[ Stop(~id, a, b) ]->
    [ Out(diff(a, b)) ]

restriction OnlyOnce:
  "All #i #j. OnlyOnce() @ i & OnlyOnce() @ j ==> #i = #j"

end

I have also attached the file.

Obviously, observational equivalence should hold for this theory, but I surmise this is only provable using induction.
This seems obvious when looking at the following screenshot from interactive mode trying to prove the observational equivalence lemma:


I have looked into the paper introducing observational equivalence a bit, and in section "6. Related Work and Conclusion", it is mentioned that "We will also tackle protocols with loops, where proofs will likely require induction."

From this I conclude that indeed, induction is currently not at all supported for the observational equivalence mode.
And it is also not possible to use helper lemmas, right?

Therefore, this is impossible to prove, or am I mistaken?

Kind regards,
Henning

[Jannik Dreier]

Dear Henning,

Tamarin's equivalence mode uses approximations, in particular when it
comes to restrictions. This means that it is incomplete and sometimes
returns spurious attacks, as is the case for your example.

You are also right that there is no induction for equivalence.

Best regards,
Jannik

> diffind-problem.png
>
> I have looked into the paper introducing observational equivalence a
> bit, and in section "6. Related Work and Conclusion", it is mentioned
> that "We will also tackle protocols with loops, where proofs will likely
> require induction."
>
> From this I conclude that indeed, induction is currently not at all
> supported for the observational equivalence mode.
> And it is also not possible to use helper lemmas, right?
>
> Therefore, this is impossible to prove, or am I mistaken?
>
> Kind regards,
> Henning
>

> --
> 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-
> prover+un...@googlegroups.com>.
> To view this discussion visit https://groups.google.com/d/msgid/tamarin-
> prover/7b80e8ff-1de4-4d52-9a90-ff824304da25n%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-
> prover/7b80e8ff-1de4-4d52-9a90-ff824304da25n%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

[Henning Arvid Ladewig]

Dear Jannik,

thank you very much for your answer.

I now removed the OnlyOnce-restriction; I had only added preemptively to obtain nice dependency graphs.

However, may I ask what exactly you mean by a spurious attack in this specific case?

Neither in the original version nor in the one without the restriction I can find an attack in Tamarin.

Kind regards,
Henning

[Yuheng Wen]

Hi Jannik,

Just to double check, resource lemma (using induction techniques) can still be used in --diff mode, yes? 

[Ralf Sasse]

Yes, sources lemmas can be used to reduce the pre-computed state space as usual, and induction is applied for them, also in diff mode.

Cheers,
Ralf

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/37df64cb-b16e-4307-a333-5de6a45d6c9an%40googlegroups.com.

[Jannik Dreier]

This is because source lemmas reason only about traces, hence the normal
induction can be applied.

Jannik

>> <http://40googlegroups.com>
>> > <https://groups.google.com/d/msgid/tamarin-
>> > prover/7b80e8ff-1de4-4d52-9a90-ff824304da25n%40googlegroups.com
>> <http://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 <tel:
>> +33%203%2054%2095%2084%2046>

>>
>> --
>> 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/37df64cb-b16e-4307-

>> a333-5de6a45d6c9an%40googlegroups.com <https://groups.google.com/d/
>> msgid/tamarin-prover/37df64cb-b16e-4307-
>> a333-5de6a45d6c9an%40googlegroups.com?utm_medium=email&utm_source=footer>.

>
> --
> 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-
> prover+un...@googlegroups.com>.
> To view this discussion visit https://groups.google.com/d/msgid/tamarin-

> prover/021aa932-ca19-4a0e-9a58-50f45651e6b4%40inf.ethz.ch <https://
> groups.google.com/d/msgid/tamarin-prover/021aa932-
> ca19-4a0e-9a58-50f45651e6b4%40inf.ethz.ch?
> utm_medium=email&utm_source=footer>.

[Jannik Dreier]

Dear Henning,

You are right, the OnlyOnce restriction in your example does not lead to
spurious attacks - I jumped to a conclusion too quickly.

One can use helper (reuse) lemmas in equivalence mode, however they can
only reason on traces on each side seperately, but not on both at the
same time. One could for example prove that there is necessary an
instance of the start rule if there is a stop or step rule, but this
does not help for the equivalence proof.

Best regards,
Jannik

> tamarin- <https://groups.google.com/d/msgid/tamarin->
> > prover/7b80e8ff-1de4-4d52-9a90-ff824304da25n%40googlegroups.com
> <http://40googlegroups.com>
> > <https://groups.google.com/d/msgid/tamarin- <https://
> groups.google.com/d/msgid/tamarin->
> > prover/7b80e8ff-1de4-4d52-9a90-ff824304da25n%40googlegroups.com
> <http://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 <tel:
> +33%203%2054%2095%2084%2046>

>
> --
> 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-
> prover+un...@googlegroups.com>.
> To view this discussion visit https://groups.google.com/d/msgid/tamarin-

> prover/c9dd8ac3-175e-4fcf-9a37-0901ef1f4669n%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/
> c9dd8ac3-175e-4fcf-9a37-0901ef1f4669n%40googlegroups.com?
> utm_medium=email&utm_source=footer>.