Restrictions in diff-mode

[Prashant Agrawal]

Dear all,

I have a diff protocol where I require the adversary to supply an input that follows a certain restriction. However, Tamarin reports a diff-equivalence violation by finding a trace where the left process satisfies the restriction and the right process does not. That is, Tamarin considers the restriction violation itself as a distinguishing attack. Is there a way to avoid it?

Here is a minimal example:

theory Test

begin

functions: enc/3, m0/0, m1/0

rule R1: [Fr(~k), Fr(~r), In(<mL, mR>)] --> [ Out( diff(enc(mL, ~k, ~r), enc(mR, ~k, ~r)) )]

rule R2 [no_derivcheck]: [In(enc(m, k, r))] --[ Handle(m) ]-> []

restriction X:

"All m #i. Handle(m) @ i ==> (m = m0 | m = m1)"

end

Here, in rule R2, the adversary is required to produce an encryption of either m0 or m1. However, Tamarin produces an attack where the adversary sends mL=m0 and mR=m* to rule R1, where m* is some adversary-generated message. In this way, in the left process, the adversary satisfies the restriction and in the right process, it does not. Tamarin claims this to be a violation of diff-equivalence. How do I exclude such attacks? That is, how do I make Tamarin respect the restriction on both sides and not treat its violation as a distinguishing capability itself?

Thanks for any pointers.

Best regards,

Prashant

[Felix Linker]

Hi Prashant,

Did you try applying the restriction to R1 instead of R2? I think Tamarin is right in distinguishing the two traces as the adversary can send something other than m1 and m2 in R1, but the protocol execution will not continue. This is what the adversary can distinguish. When you apply the restriction earlier, the protocol won't even start.

Best,

Felix

--
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/544f72c0-350d-4950-a6ee-19fc085a4fben%40googlegroups.com.

[Prashant Agrawal]

Hi Felix,

Thanks for your quick reply. Actually, the protocol I am modeling is such that rules R1 and R2 represent two different honest processes and the security guarantees hold under the assumption that R2 receives an encryption of either m0 or m1. Putting the restriction at R1 would not model the assumption accurately.

For comparison, the same protocol modeled in Proverif gives me the desired output: Proverif respects restrictions on both sides and says that diff-equivalence is true.

free ch : channel.

type nonce.

type msg.

free m0: msg.

free m1: msg.

fun pair(msg, msg) : msg [data].

fun enc(msg, nonce, nonce) : msg.

let R1 =

new k : nonce;

in(ch, pair(mL: msg, mR: msg));

new r : nonce;

out(ch, diff[ enc(mL, k, r), enc(mR, k, r) ]).

event Handle(msg).

restriction yL: msg, yR: msg, k: nonce, r: nonce;

event(Handle(diff[yL,yR])) ==>

(yL = enc(m0, k, r) && yR = enc(m1, k, r)).

let R2 =

in(ch, y: msg);

event Handle(y).

process

R1 | R2

Is there a way to make Tamarin behave similarly? If not for this issue, Tamarin is more attractive to me than Proverif because of its wider equational theory support.

Thanks,

Prashant

[Felix Linker]

Hi Prashant,

I think my point is that you do require m1/m2 to be sent for the model to be observational equivalent. If you think that assuming that is not realistic, then maybe your protocol does not provide observational equivalence.

I cannot tell you why the model written using process syntax is observational equivalence. I don't know that syntax well enough. Maybe it's because R1 definitely needs to be applied before R2 as the participants communicate over the channel ch (not the insecure network)? You could try using a secure channel in your Tamarin model too. Not sure, though, whether channel ch is a secure channel.

Best,

Felix

To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/e5594143-bd9e-45c0-9101-2375816c5021n%40googlegroups.com.