A Finite Equivalence of Verifiable Multi-secret Sharing
We give an abstraction of verifiable multi-secret sharing schemes that is accessible to a fully mechanized analysis. This abstraction is formalized within the applied pi-calculus by using an equational theory which characterizes the cryptographic semantics of secret share. We also present an encoding from the equational theory into a convergent rewriting system, which is suitable for the automated protocol verifier ProVerif. Based on that, we verify the threshold certificate protocol in ProVerif.
International Journal of Communication Systems
Sun, J. Z.,
(2012). A Finite Equivalence of Verifiable Multi-secret Sharing. International Journal of Communication Systems, 5(1), 1-12.
Available at: http://aquila.usm.edu/fac_pubs/140