关于秘密共享方案在应用Pi演算中的实现

摘要：

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

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

所属期刊栏目：33

分类号：TN95

在线出版日期：2013-12-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：3247-3251