Abstract：In this paper, an abstraction of secret-sharing schemes that is accessible to a fully mechanized analysis was given. This abstraction was formalized within the applied Pi-calculus by using an equational theory that characterized the cryptographic semantics of secret share. Based on that, an encoding method from the equational theory into a convergent rewriting system was presented, which was suitable for the automated protocol verifier ProVerif. Finally, the first general soundness result for verifiable multi-secret sharing schemes was concluded: for the multi-secret sharing schemes satisfying the specified security criterion in ProVerif, the realistic adversaries modeled on multi-secret sharing schemes in Pi-calculus can simulate the ideal adversaries in verifier ProVerif, which means that realistic adversaries and ideal adversaries are indistinguishable.
徐军. 关于秘密共享方案在应用Pi演算中的实现[J]. 计算机应用, 2013, 33(11): 3247-3251.
XU Jun. About the secret sharing scheme applied in the Pi calculus. Journal of Computer Applications, 2013, 33(11): 3247-3251.
2013, Vol. 33 
