Multiplication restriction rule

[zidni hakam]

Dear all,

I still have a problem with my multiplication function in my protocol model. When i try to run the model, the program tell me that my model wellformedness check failed.  The problem is the following rule is not multiplication restricted:

rule Registered:
  let
    PbX = padd(PX, PN)
    m = H1(PbX, IdX)
    PrX = dX + (m * ~rX)
  in
    [ !Point_init($X, IdX, PX, ~rX), In(<$NM, $X, PN>), In(<$NM, $X, dX>) ]
  --[ Honest($NM), Honest($X), Secret(PrX) ]->
    [ !Pb($X, PbX), !Pr($X, PrX) ]

Best Regard,
Zidni

[Jannik Dreier]

Dear Zigni,

Tamarin forbids the use of multiplication in protocol rules, that is why
you get the warning. If you nevertheless use multiplication, Tamarin's
results might be wrong. One solution is to use a higher level
abstraction, where you do not need to model multiplication explicitly.

Best regards,
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/3725ceee-bdbb-47b9-b54a-e7845f67c644n%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/3725ceee-bdbb-47b9-b54a-e7845f67c644n%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]

Dear Jannik,

Thank you for the explanation. If I still use the multiplication instead of using another abstraction, is it okay to just ignore the warning? And where we can use the multiplication function if it is not in the protocol rule?

Best Regards,

Zidni