Observational Equivalence: attack based on the recognition of two terms

[Guillaume Nibert]

Dear Tamarin Team,

I am still exploring the Basin et al's paper. There is an example on pairs of elements (example 6, page 5/25, https://hal.science/hal-01337409v2/document) where the aim is to distinguish two systems. The first outputs a pair of equal values, and the second may output a pair of different values.

The two systems are defined as follows:

S_A = { A : --[]-> Out_Sys((x, x)) }
S_B = { B : --[]-> Out_Sys((x, y)) }

The environment defined makes it possible to distinguish between systems (which represents an attack):

Env' = { E_fst : In_Env((x, y)) --[]-> M(x)

, E_snd : In_Env((x, y)) --[]-> M(y)

, E_cmp : M(x), M(x) --[]-> Out_Env(true) }

I am looking to revisit this example where the distinction of systems is defined by certain terms that are equal to certain indexes. For example:
I define the distinguashibility of these pairs (x, x), (x, y) is possible because x is common to both messages at index 1.

The environment I would like to use would look like this:

Env' = { E_fst : In_Env((x, y)) --[]-> M(x)

, E_snd : In_Env((x, y)) --[]-> M(y)

, E_cmp : M(x), M(x) --[]-> Out_Env(false) }

or something like this:

Env' = { E_fst : In_Env((x, y)) --[]-> M(x)

, E_snd : In_Env((x, y)) --[]-> M(y)

, E_cmp : M(x), not(M(x)) --[]-> Out_Env(true) }

When modelling on Tamarin with the diff operator, I feel like that I do not have any control over the environment.

To put it more clearly, perhaps abusively, I am trying to do the opposite of what we are used to doing: rather than showing that two distinguishable systems constitute an attack by their differences in the messages they output to the environment, I would prefer show that two systems with some terms that are common at specific indexes constitute an attack. And I think it is at the level of the environment that I have to define the check of what constitutes an attack or not (i.e., the fact that the term in the first index of the first system is equal to the other or not).

For this revisited example, I want to reason with observational equivalence and not with the trace.

Is it possible to control the environment with Tamarin's diff? Are there any resources related to formal verification that I should take a closer look at?

Best regards,

Guillaume Nibert