Precomputation halts when introducing a custom XOR

[Denis D'Ambrosi]

Good evening everyone,

I'm currently working on a protocol that requires the combined use of message splitting and XOR operations. Unfortunately, when I try to ran Tamarin on an incomplete draft of the theory's file, the computation simply does not seem to start: in the terminal, I can only read

maude tool: 'maude'
 checking version: 2.7.1. OK.
 checking installation: OK.

and then nothing happens. Trying to trace back the issue, I discovered that it was caused by importing of the builtin xor. So, since I will need a "custom" XOR to use in my splitting equations later on anyway (since it is not possible to use builtin symbols in custom equations as far as I can tell from this Google Group), I defined my own XOR and ZERO symbols and equations, following the ones described in Tamarin's manual.

The prover now works, but only if I exclude the associative property. If not, it halts again. Trying to give a minimal example of this problem, I wrote the following theory:

theory PROVA

begin

functions : f/2, z/0

equations : f(a,b) = f(b,a),

f(f(a,b),c) = f(a,f(b,c)),

f(a,z()) = a,

f(a,a) = z()

rule GenericRule :

[ Fr(~x) ] --[ MyX(~x) ]-> [ X(~x) ]

lemma Test :

exists-trace

"Ex #t x . MyX(x) @ #t"

end

When run from the terminal, it shows the same problem as before. On the other hand, an analogous theory that imports the builtin xor instead of defining custom equations clearly works flawlessly.

I'm currently lacking ideas to go forward, as I do not even have a clear idea of what the error actually is. It must clearly have something to do with Finite Variant properties, but I do not understand how I could overcome it.

Thank you in advance.

Denis

[Jannik Dreier]

Hi,

The user defined equations need to be convergent, however associativity
and commutativity are not convergent. This seems to make Maude run into
a loop here when loading your equations. This is also why there is a
builtin for XOR, as it is not possible to define XOR using "normal"
equations.

Note that Tamarin does not check whether your equations are convergent,
as this is not easy in general.

See also
https://tamarin-prover.github.io/manual/master/book/004_cryptographic-messages.html#sec:equational-theories

Best,
Jannik

> --
> 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/35f17e33-722d-413a-adc8-3db1300fd6a0n%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/35f17e33-722d-413a-adc8-3db1300fd6a0n%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

[Denis D'Ambrosi]

Dear prof. Dreier

Thank you for you answer and excuse me for such a late reply.

I have just read your article about introducing XOR into Tamarin and now it makes much more sense. Unfortunately, even when using the built-in XOR, I run in the issue of precomputation halting.

In particular, my protocol requires to derive a shared secret through multiple splitting, concatenation and XOR operations and everything works fine until I introduce the last rule for deriving the key on "Bob"'s side. At that point, the pre-computation simply does not seem to start. If I substitute the pattern for the key with a dummy constant, everything "works fine" (in the sense of actually reaching the end of pre-computation phase). Otherwise, I just get (now that I have updated Tamarin to 1.8.0):

[Open Chains] Too many chain goals, stopping precomputation. Open Chains limits (can be changed with -c=): 10
[Saturating Sources] Step 1/5

And nothing else.

Furthermore, by including XOR I am inherently not capturing some properties of the splitting and concatenation, as I cannot define a set of equations like

conc(split1(x), split2(x)) = x

conc(a,c) XOR conc(b,d) = conc(a XOR b, c XOR d)

Clearly the second equation is non-convergent, but excluding it from the theory would invalidate it. Any suggestions on how to continue?

By the way, on my previous toy example, I found it amusing that introducing commutativity as

f(f(a,b),z) = f(b,a)

did not halt the precomputation, while the same trick did not work with associativity.

Best regards,

Denis

[Jannik Dreier]

Dear Denis,

> I have just read your article about introducing XOR into Tamarin and now
> it makes much more sense. Unfortunately, even when using the built-in
> XOR, I run in the issue of precomputation halting.
> In particular, my protocol requires to derive a shared secret through
> multiple splitting, concatenation and XOR operations and everything
> works fine until I introduce the last rule for deriving the key on
> "Bob"'s side. At that point, the pre-computation simply does not seem to
> start. If I substitute the pattern for the key with a dummy constant,
> everything "works fine" (in the sense of actually reaching the end of
> pre-computation phase). Otherwise, I just get (now that I have updated
> Tamarin to 1.8.0):
>
> [Open Chains] Too many chain goals, stopping precomputation. Open Chains
> limits (can be changed with -c=): 10
> [Saturating Sources] Step 1/5

You can set a small bound on saturation, e.g., -s=1 or even -s=0, to be
able to load the file and see why there so many goals.

> And nothing else.
> Furthermore, by including XOR I am inherently not capturing some
> properties of the splitting and concatenation, as I cannot define a set
> of equations like
>
> conc(split1(x), split2(x)) = x
> conc(a,c) XOR conc(b,d) = conc(a XOR b, c XOR d)
>
> Clearly the second equation is non-convergent, but excluding it from the
> theory would invalidate it. Any suggestions on how to continue?

Try to find more restricted equations. In some sense, try to extract
what exactly you need for your model to work, without using the general
equations.

For example, if you only need this property to be applied once, one can
use two different conc symbols:

conc1(a,c) XOR conc1(b,d) = conc2(a XOR b, c XOR d)

I don't know if that makes sense for your case, but maybe this can serve
as inspiration.

Best,
Jannik

> By the way, on my previous toy example, I found it amusing that
> introducing commutativity as
>
> f(f(a,b),z) = f(b,a)
>
> did not halt the precomputation, while the same trick did not work with
> associativity.
>
> Best regards,
> Denis
>
>
>
> Il giorno giovedì 19 ottobre 2023 alle 10:18:04 UTC+2
> rese...@jannikdreier.net ha scritto:
>
> Hi,
>
> The user defined equations need to be convergent, however associativity
> and commutativity are not convergent. This seems to make Maude run into
> a loop here when loading your equations. This is also why there is a
> builtin for XOR, as it is not possible to define XOR using "normal"
> equations.
>
> Note that Tamarin does not check whether your equations are convergent,
> as this is not easy in general.
>
> See also

> https://tamarin-prover.github.io/manual/master/book/004_cryptographic-messages.html#sec:equational-theories <https://tamarin-prover.github.io/manual/master/book/004_cryptographic-messages.html#sec:equational-theories>

> https://groups.google.com/d/msgid/tamarin-prover/35f17e33-722d-413a-adc8-3db1300fd6a0n%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/35f17e33-722d-413a-adc8-3db1300fd6a0n%40googlegroups.com> <https://groups.google.com/d/msgid/tamarin-prover/35f17e33-722d-413a-adc8-3db1300fd6a0n%40googlegroups.com?utm_medium=email&utm_source=footer <https://groups.google.com/d/msgid/tamarin-prover/35f17e33-722d-413a-adc8-3db1300fd6a0n%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

> <tel:+33%203%2054%2095%2084%2046>

>
> --
> 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/7c80649d-fcd9-4b7a-a7b0-cb5084b77b33n%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/7c80649d-fcd9-4b7a-a7b0-cb5084b77b33n%40googlegroups.com?utm_medium=email&utm_source=footer>.