Can Shamir secret sharing scheme (SSS) be verified using automated verification tools such as AVISPA? I read in the HLPSL manual that we cannot use arithmetic or relative operations such +,-,< ...etc in the HLPSL description of the protocol. Thus, we cannot implement LaGrange's interpolation formula?!! Do all protocol verification have this limitation?
(There are other protocol verification tools, but recently, I got familiar with AVISPA)