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