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)

  • 1
    $\begingroup$ Did you take a look at Verifpal? $\endgroup$ Jul 10 at 6:04
  • 1
    $\begingroup$ Arxiv 1805.12482 "..Towards Formal Proof for Secure Multi-Party Computation" $\endgroup$ Jul 10 at 10:29
  • $\begingroup$ @VadymFedyukovych Thank you for sharing this paper, I am reading it now. $\endgroup$
    – Mona
    Jul 11 at 16:44
  • $\begingroup$ @AaqibBashir Is Verifpal any different from AVISPA? $\endgroup$
    – Mona
    Jul 11 at 16:45
  • 1
    $\begingroup$ Verifpal is one of the state-of-the-art tools for verification of cryptographic protocols. For more understanding you can read eprint.iacr.org/2019/971.pdf $\endgroup$ Jul 12 at 4:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.