point addition and multiplication wellformed failed

[zidni hakam]

Dear all,

I am using Tamarin for my current research, but there is some problem that I don't know the solution yet. In the protocol that I  pick, there is so much function such as point addition, point multiplication, and billinear-pairing on ECC. I cannot found the ECC point addition in tamarin and my model still have multiplication wellformed failed like this :

can someone tell me how to fix it?

Another question, how to modelling ECC point addition in tamarin?

Thank you

[Jannik Dreier]

Dear Zidni Hakam,

Short answer: Tamarin does not support point addition nor group element
multiplication (see
https://infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/tamarin_group_sp.pdf
for details), so I don't think you will be able to model your protocol
without abstracting some of the cryptographic operations.

Best regards,
Jannik

On 15/03/2021 03:58, zidni hakam wrote:
>
> Dear all,
> I am using Tamarin for my current research, but there is some problem
> that I don't know the solution yet. In the protocol that I  pick, there
> is so much function such as point addition, point multiplication, and
> billinear-pairing on ECC. I cannot found the ECC point addition in
> tamarin and my model still have multiplication wellformed failed like this :

> Screenshot from 2021-03-15 09-38-24.png
> can someone tell me how to fix it?
> Another question, how to modelling ECC point addition in tamarin?
>
> Thank you
>

> --
> 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/889f4222-87f0-444d-83f0-d6c3b0f1aea8n%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/889f4222-87f0-444d-83f0-d6c3b0f1aea8n%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

[zidni hakam]

Thank you for your explanation.

For the multiplication problem in my model, I finally can solve it.

Best regard,

Zidni