A finite equivalence of multisecret sharing based on Lagrange interpolating polynomial. Issue 9 (24th January 2013) - Zhao, Hui; Sun, Jonathan Z.; Wang, Fengying; Zhao, Lei
ABSTRACT: We give an abstraction of multisecret sharing based on Lagrange interpolating polynomial that is accessible to a fully mechanized analysis. This abstraction is formalized in the applied pi‐calculus by using an equational theory that characterizes the cryptographic semantics of multisecret sharing based on Lagrange interpolating polynomial. We also present an encoding from the equational theory into a convergent rewriting system, which is suitable for the automated protocol verifier ProVerif. Finally, we verify the Yang–Chang–Hwang (YCH) protocol in ProVerif. Copyright © 2013 John Wiley & Sons, Ltd. Abstract : In this paper, we give an abstraction of multi‐secret sharing based on Lagrange interpolating polynomial that is accessible to a fully mechanized analysis. We also present an encoding from the equational theory into a convergent rewriting system, which is suitable for the automated protocol verifier ProVerif. Finally, we verify a practical verifiable multi‐secret sharing scheme based on YCH in ProVerif.