Observational Equivalence proofs

[mohit jangid]

Tamarin manual explains observational equivalence (https://tamarin-prover.github.io/manual/book/007_property-specification.html).  I have the following questions for observational equivalence proofs:

1. A secrecy lemma is presented in the explanation. However, I believe it is used to show that the protocol satisfies secrecy but not privacy. Also, proving the secrecy lemma is not necessary to prove observations equivalence. Please correct me if I am wrong.   

2. Do Restrictions and reuse lemmas influence the observational equivalence proof run-times and steps (similar to trace properties)? 

3. If I try to prove the model using the command.

 
tamarin-prover --diff ObservationalEquivalenceExample.spthy --prove=Observational_equivalence

It gives the error that

WARNING: ignoring the following wellformedness errors

Check presence of the --prove/--lemma arguments in theory:
--> 'Observational_equivalence' from arguments do(es) not correspond to a specified lemma in the theory

To my understanding, it is still valid proof. The warning merely cautions about the absence of an observational equivalence lemma generated automatically. Please correct me if I am wrong.

4. Observational equivalence mode supports only heuristics: C O c s o. I wonder why does it not support the other heuristics. 

---

Regards
Mohit Kumar Jangid 

[Ralf Sasse]

Dear Mohit,

I am responding inline.

On 07.02.23 18:44, mohit jangid wrote:

Tamarin manual explains observational equivalence (https://tamarin-prover.github.io/manual/book/007_property-specification.html).  I have the following questions for observational equivalence proofs:

1. A secrecy lemma is presented in the explanation. However, I believe it is used to show that the protocol satisfies secrecy but not privacy. Also, proving the secrecy lemma is not necessary to prove observations equivalence. Please correct me if I am wrong.  

Correct, the secrecy lemma is here to show the difference between being able to derive the encrypted content (~b) [secrecy property] and distinguishing whether the known value (~a) was encrypted or not [privacy property].

The secrecy lemma here has no impact on the equivalence property, it is just for comparison.

2. Do Restrictions and reuse lemmas influence the observational equivalence proof run-times and steps (similar to trace properties)?

Yes, they do influence proofs.

3. If I try to prove the model using the command.

 
tamarin-prover --diff ObservationalEquivalenceExample.spthy --prove=Observational_equivalence

It gives the error that

WARNING: ignoring the following wellformedness errors

Check presence of the --prove/--lemma arguments in theory:
--> 'Observational_equivalence' from arguments do(es) not correspond to a specified lemma in the theory

To my understanding, it is still valid proof. The warning merely cautions about the absence of an observational equivalence lemma generated automatically. Please correct me if I am wrong.

This will not work. As the automatically generated lemma Observational_equivalence does not exist on loading, the --prove command will not actually prove anything. The summary at the end of Tamarin's run will show:

DiffLemma:  Observational_equivalence : analysis incomplete (1 steps)

In that case, nothing(!) is proven. You can simply start the proof with the --prove (without parameter), but note all lemmas will be proven. You can comment the others out, if you don't want that.

4. Observational equivalence mode supports only heuristics: C O c s o. I wonder why does it not support the other heuristics. 

Not entirely sure anymore, but we probably did not have a use for those heuristics and thus did not enable them for Observational Equivalence. The 'missing' heuristics include those for SAPIC (which does not support translation to diff theories, I believe) which would thus not be useful anyway, and injective rankings.

Cheers,
Ralf

---

Regards
Mohit Kumar Jangid 

--
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/037378c3-7cb6-437a-9093-c01a7e76e533n%40googlegroups.com.

[Jannik Dreier]

Hi Mohit,

let me add three things:

>> Tamarin manual explains observational equivalence
>> (https://tamarin-prover.github.io/manual/book/007_property-specification.html). I have the following questions for observational equivalence proofs:
>>
>> 1. A secrecy lemma is presented in the explanation. However, I believe
>> it is used to show that the protocol satisfies secrecy but not
>> privacy. Also, proving the secrecy lemma is not necessary to prove
>> observations equivalence. Please correct me if I am wrong.
>
> Correct, the secrecy lemma is here to show the difference between being
> able to derive the encrypted content (~b) [secrecy property] and
> distinguishing whether the known value (~a) was encrypted or not
> [privacy property].
>
> The secrecy lemma here has no impact on the equivalence property, it is
> just for comparison.
>
>>

>> 2. Do /Restrictions/ and /reuse lemmas /influence the observational

>> equivalence proof run-times and steps (similar to trace properties)?
> Yes, they do influence proofs.

They behave exactly as in trace mode, they will be applied when proving
the observational equivalence lemma. Note however that restrictions are
currently not very well handled in equivalence mode, and often lead to
non-termination.

>>
>> 3. If I try to prove the model using the command.
>>
>> tamarin-prover --diff ObservationalEquivalenceExample.spthy
>> --prove=Observational_equivalence
>>
>> It gives the error that
>>
>> WARNING: ignoring the following wellformedness errors
>>
>> Check presence of the --prove/--lemma arguments in theory:
>> --> 'Observational_equivalence' from arguments do(es) not correspond
>> to a specified lemma in the theory
>>
>> To my understanding, it is still valid proof. The warning merely
>> cautions about the absence of an observational equivalence lemma
>> generated automatically. Please correct me if I am wrong.
>
> This will not work. As the automatically generated lemma
> Observational_equivalence does not exist on loading, the --prove command
> will not actually prove anything. The summary at the end of Tamarin's
> run will show:
>
> DiffLemma:  Observational_equivalence : analysis incomplete (1 steps)
>
> In that case, nothing(!) is proven. You can simply start the proof with
> the --prove (without parameter), but note all lemmas will be proven. You
> can comment the others out, if you don't want that.

I agree with Ralf's explanation, but this is not very nice from a user
point of view. Feel free to open an issue for this.

>
>>
>> 4. Observational equivalence mode supports only heuristics: C O c s o.
>> I wonder why does it not support the other heuristics.
>>
> Not entirely sure anymore, but we probably did not have a use for those
> heuristics and thus did not enable them for Observational Equivalence.
> The 'missing' heuristics include those for SAPIC (which does not support
> translation to diff theories, I believe) which would thus not be useful
> anyway, and injective rankings.

I agree, there was no use for the other ones. But fundamentally, there
is nothing that would prevent us from enabling them. (Anyway oracles
allow to have different rankings.)

Cheers,
Jannik

>
> Cheers,
> Ralf
>
>
>> ---
>> Regards
>> Mohit Kumar Jangid
>> --
>> 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/037378c3-7cb6-437a-9093-c01a7e76e533n%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/037378c3-7cb6-437a-9093-c01a7e76e533n%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-prove...@googlegroups.com>.

> To view this discussion on the web visit

> https://groups.google.com/d/msgid/tamarin-prover/e27759d1-2f96-8440-5c04-ec3db70029b5%40inf.ethz.ch <https://groups.google.com/d/msgid/tamarin-prover/e27759d1-2f96-8440-5c04-ec3db70029b5%40inf.ethz.ch?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

[mohit jangid]

Thank you Dr. Ralf and Dr. Jannik for clarification. It is very useful.

A minor nitpick for Q# 3: The command 
tamarin-prover --diff ObservationalEquivalenceExample.spthy --prove=Observational_equivalence

provides an attack trace (a complete execution output), instead of showing incomplete analysis, for my case (Ubuntu 22.04) as shown below:

/*
Generated from:
Tamarin version 1.7.1
Maude version 3.1
Git revision: 7c980321158ebf7c7c03c53cee93248507584065, branch: develop
Compiled at: 2023-02-06 16:08:09.443373763 UTC
*/

end

==============================================================================
summary of summaries:

analyzed: ObservationalEquivalenceExample.spthy

  processing time: 1.02s
 
  WARNING: 1 wellformedness check failed!
           The analysis results might be wrong!
 
  RHS :  B_is_secret (all-traces): analysis incomplete (1 steps)
  LHS :  B_is_secret (all-traces): analysis incomplete (1 steps)
  DiffLemma:  Observational_equivalence : falsified - found trace (9 steps)

==============================================================================

  
So then, Should I assume that the proof is valid regardless of the warning? Also, as Dr. Jannik said, I can create an issue for this.