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