[question] builtin xor equational theory and partial deconstructions

[gilcu3]

Dear all:

I have tried using the builtin xor to model several protocols using Tamarin, and quite frequently it leads to non-termination, probably generated by the so called partial deconstructions. Attached there is a very simple example (not even a protocol, it's just two rules). While running it with Tamarin using interactive mode, I get the aforementioned issue of partial deconstructions. While checking the web interface, I noticed that in Multiset Rewriting Rules, there is this rule:

rule (modulo AC) r2:
   [ Fr( ~b ), In( a ) ] --> [ Out( <z, h(~b)> ) ]
  variants (modulo AC)
  1. ~b = ~b.4
     a = a.4
     z = (~b.4⊕a.4)
  
  2. ~b = ~b.4
     a = zero
     z = ~b.4
  
  3. ~b = ~x.4
     a = ~x.4
     z = zero
  
  4. ~b = ~x.4
     a = (~x.4⊕x.5)
     z = x.5

The 4th variant doesn't make sense to me, in the sense that if 'a' is received in an In fact, it is impossible that it contains the fresh ~b as a subterm. I think this specific variant is what leads to the partial deconstructions.

Can someone clarify me on this? Is there any particular or general strategy to use the builtin xor and avoid partial deconstructions?

Cheers

[Ralf Sasse]

This issue seems highly related to

https://github.com/tamarin-prover/tamarin-prover/issues/362

and particularly the linked short example

https://gist.github.com/maurozenoni/e52f36faf7e4c0495ca15b2a2600a5d0

where even though a value is created freshly in the rule, Tamarin does not automatically rule out the equality with inputs received.

In your example here that basic problem of not understanding that input and local fresh are different, is obfuscated behind an XOR operator, but as above seems to have a more fundamental source. If you want to add your example to that issue, it would give us more information for later.

Unfortunately, at this time, I do not see an easy workaround. Making such a change inside Tamarin has to be done carefully, as a mistake would impact soundness immediately.

Cheers,
Ralf

--
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/da93265f-a59d-42fa-880c-f562fabadf48%40googlegroups.com.

[gilcu3]

Thank you Ralf for your answer, I agree the issue you mention seems highly related, so I will add this example there ASAP.

On the other hand, I couldn't generate this behavior with other builtin, for example using the diffie-hellman builtin. I have attached two examples (the xor one very similar to the one above), one using xor and the other using diffie-hellman, Both are equivalent except one uses xor and the other one uses diffie-hellman (which in the exponent has AC properties, as xor).

In the theory xor_problem, when running in interactive mode, tamarin gets partial deconstructions as mentioned above.

In the theory dh_problem, when running in interactive mode, tamarin doesn't get partial deconstructions.

In the case of rule r2, it shows:

rule (modulo AC) r2:
   [ Fr( ~b ), In( z ) ] --> [ Out( z.1 ) ]
  variants (modulo AC)
  1. ~b = ~b.5
     z = 'g'
     z.1 = 'g'^~b.5
  
  2. ~b = ~b.5
     z = 'g'^a.5
     z.1 = 'g'^(~b.5*a.5)
  
  3. ~b = ~x.5
     z = 'g'^inv(~x.5)
     z.1 = 'g'
  
  4. ~b = ~x.5
     z = 'g'^inv((~x.5*x.6))
     z.1 = 'g'^inv(x.6)
  
  5. ~b = ~x.5
     z = 'g'^(x.6*inv(~x.5))
     z.1 = 'g'^x.6
  
  6. ~b = ~x.5
     z = 'g'^(x.6*inv((~x.5*x.7)))
     z.1 = 'g'^(x.6*inv(x.7))

The 5th variant corresponds to the 4th variant in the xor case, but surprisingly this doesn't lead to partial deconstructions. Why is this different?

Cheers

To unsubscribe from this group and stop receiving emails from it, send an email to tamarin...@googlegroups.com.

[Ralf Sasse]

The short answer to what is different is "extractability". From a DH exponent the element can never be extracted directly. From the XOR it can be extracted, by XORing whatever else is in the term, i.e., BAD XOR otherstuff XOR otherstuff simplifies to BAD which may now be known to the attacker. That's *probably* the reason why the resulting behavior is different regarding partial deconstructions in XOR.

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 on the web visit https://groups.google.com/d/msgid/tamarin-prover/966c322e-2e7e-4b5d-9de7-9f7cccd40310%40googlegroups.com.

[gilcu3]

Just to check if my intuition is correct.

To apply that 5th variant, the adversary would need to generate a term like g^(x6*inv(~b)), which (forgetting about the freshness of ~b issue) depends on the adversary already knowing x6. So as the rule outputs g^x6 and not x6, there is no partial deconstruction.

Now, if tamarin had a way to generate a random element of the group <g>  g^x, but without knowing x, then a partial deconstruction should appear, as in the xor case. Is this correct?

Cheers

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/966c322e-2e7e-4b5d-9de7-9f7cccd40310%40googlegroups.com.

[Guillaume Nibert]

Dear all,

I am very interested in this topic, especially the XOR problem. I have seen that it is possible to manually specify variants for a rule (https://tamarin-prover.com/manual/master/book/016_syntax_description.html). Removing the 4th variant removes 3 partial deconstructions.

When Dr. Sasse explains this "Unfortunately, at this time, I do not see an easy workaround. Making such a change inside Tamarin has to be done carefully, as a mistake would impact soundness immediately." Does this also mean that an easy workaround is not possible for this particular theory?

By defining rule 2 as follows...

--

rule r2:

[Fr(~b), In(a)]

--[R1_IN(a)]->

[Out(a XOR ~b)]

variants

rule (modulo AC) r2___VARIANT_1:

[Fr(~b.1), In( a.2 )]

--[R1_IN(a.2)]->

[Out(~b.1 XOR a.2)],

rule (modulo AC) r2___VARIANT_2:

[Fr(~b.1), In( zero )]

--[R1_IN(zero)]->

[Out(~b.1)],

rule (modulo AC) r2___VARIANT_3:

[Fr(~b.1), In( ~b.1 )]

--[R1_IN(~b.1)]->

[Out( zero )]

--

...there are only 3 deconstructions left to solve. I am thinking that by adding a source lemma it might be possible.

This one is true according to Tamarin, but does not solve the problems of deconstruction:

--

lemma src [sources]:

"(All a #i. R1_IN(a) @ i

==>

((Ex #j. (!KU(a) @ j) & (j < i))

|

(Ex #j. (R1_OUT( a ) @ j) & (j < i))))"

--

This one is wrong, but solves the deconstructions:

--

lemma src [sources]:

"(All a #i. R1_IN(a) @ i

==>

((Ex #j. (R1_OUT( a ) @ j) & (j < i))))"

--

Is my approach naive? Because there are other problems to deal with? How can I come up with a good source lemma for this problem, if it is easy to do?

Is variant 3 also related to this problem? https://github.com/tamarin-prover/tamarin-prover/issues/362

I have attached a modified version of the original problem written by gilcu3.

Thank you in advance,

Best regards,
Guillaume Nibert

[Ralf Sasse]

Dear Guillaume,

Yes, changing variants is a possibility and it is nice to see that this helps with some of the partial deconstructions. Note though that you are modifying the possible search space, which means you could possibly lose attacks with this. So, i would be very careful when removing variants.

Your (false but helpful) sources lemma by the way would force that all input accepted in rule r2 is something that was previously output by rule r1. So, the input to r2 is thus both a fresh value, and only from that rule r1.

If you are happy only to accept fresh values you could replace the r2 rule with:

rule r2:
    [Fr(~b), In(~a)]
    --[R1_IN(~a)]->
    [Out(~a XOR ~b)]

where I have added a ~ to the a, to get ~a. But note that this implies that the receiver here can check if something is a fresh value, and that any x XOR y would not be accepted as the value of ~a. Which is probably what you must allow, as otherwise you again lose attacks possibly.

In summary, I am very worried about soundness, and one would have to look at the resulting theory and try to prove it represents what is appropriate. Also, I doubt that a sources lemma will be enough to do the trick here.

For the question about comparison to issue #362 it seems possible that there is a connection. Indeed a fresh ~x (that we know is fresh in the rule) certainly cannot cancel with anything that is in an incoming In(y). This seems a bigger underlying issue that would benefit from optimization in Tamarin in general as that issue points out. However, I don't see how to generalize this and put it in the implementation easily.

Best regards,
Ralf

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/71974386-e1b7-4015-bc8c-30efe04be808n%40googlegroups.com.

[Jannik Dreier]

Dear Guillaume,

I suspect that simply removing a variant will cause the verification to
be incorrect. If you specify variants you have to manually check that
they are correct - Tamarin does not check this for you.

Best regards,
Jannik

>> rule(moduloAC) r2___VARIANT_2:

>> [Fr(~b.1), In( zero )]
>> --[R1_IN(zero)]->
>> [Out(~b.1)],
>> rule(moduloAC) r2___VARIANT_3:
>> [Fr(~b.1), In( ~b.1)]
>> --[R1_IN(~b.1)]->
>> [Out( zero )]
>> --
>> ...there are only 3 deconstructions left to solve. I am thinking that
>> by adding a source lemma it might be possible.
>>
>> This one is true according to Tamarin, but does not solve the problems
>> of deconstruction:
>> --
>> lemmasrc[sources]:
>> "(Alla #i.R1_IN(a) @i
>> ==>
>> ((Ex#j.(!KU(a) @j) &(j <i))
>> |

>> (Ex#j.(R1_OUT( a ) @j) &(j <i))))"

>> --
>>
>> This one is wrong, but solves the deconstructions:
>> --
>> lemmasrc[sources]:
>> "(Alla #i.R1_IN(a) @i
>> ==>

>> ((Ex#j.(R1_OUT( a ) @j) &(j <i))))"

>>>> https://groups.google.com/d/msgid/tamarin-prover/da93265f-a59d-42fa-880c-f562fabadf48%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/da93265f-a59d-42fa-880c-f562fabadf48%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...@googlegroups.com.
>>
>>> To view this discussion on the web visit

>>> https://groups.google.com/d/msgid/tamarin-prover/966c322e-2e7e-4b5d-9de7-9f7cccd40310%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/966c322e-2e7e-4b5d-9de7-9f7cccd40310%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.
>> To view this discussion on the web visit

>> https://groups.google.com/d/msgid/tamarin-prover/71974386-e1b7-4015-bc8c-30efe04be808n%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/71974386-e1b7-4015-bc8c-30efe04be808n%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/2071fff4-417a-4403-b09c-e945fed880be%40inf.ethz.ch <https://groups.google.com/d/msgid/tamarin-prover/2071fff4-417a-4403-b09c-e945fed880be%40inf.ethz.ch?utm_medium=email&utm_source=footer>.