A finite equivalence of multisecret sharing based on Lagrange interpolating polynomial
Hui Zhao, Jonathan Z. Sun, Fengying Wang, Lei Zhao · Security and Communication Networks · 2013
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.