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.

Key words: Pi-calculus, secret sharing, formal analysis, protocol verification

摘要： 针对秘密共享方案的自动化验证问题，提出一种基于等值理论的秘密共享方案自动化验证方法。首先通过等值理论在应用Pi演算中对可验证的多秘密共享方案的密码学语义进行了形式化定义。在此基础上，进一步提出了一种用于将所提出等值理论转化为自动化协议验证器ProVerif中重写机制的编码方法，在ProVerif中实现了关于可验证的多秘密共享方案的自动化验证。通过证明给出了关于可验证的多秘密共享方案形式化分析结果的健壮性结论：如果自动化协议验证器ProVerif中可验证的多秘密共享方案的形式化分析结果满足特定安全属性，则其能够归约证明应用Pi演算模型中针对可验证的多秘密共享方案所建立的现实敌手可以“模拟”ProVerif验证器中的理想敌手，其意味着现实敌手与理想敌手是不可区分的。

关键词: Pi演算, 秘密共享, 形式化分析, 协议验证