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

关于秘密共享方案在应用Pi演算中实现 　　摘要： 针对秘密共享方案的自动化验证问题，提出一种基于等值理论的秘密共享方案自动化验证方法。首先通过等值理论在应用Pi演算中对可验证的多秘密共享方案的密码学语义进行了形式化定义。在此基础上，进一步提出了一种用于将所提出等值理论转化为自动化协议验证器ProVerif中重写机制的编码方法，在ProVerif中实现了关于可验证的多秘密共享方案的自动化验证。通过证明给出了关于可验证的多秘密共享方案形式化分析结果的健壮性结论：如果自动化协议验证器ProVerif中可验证的多秘密共享方案的形式化分析结果满足特定安全属性，则其能够归约证明应用Pi演算模型中针对可验证的多秘密共享方案所建立的现实敌手可以“模拟”ProVerif验证器中的理想敌手，其意味着现实敌手与理想敌手是不可区分的。 关键词： Pi演算；秘密共享；形式化分析；协议验证 0引言 安全协议是保证信息系统安全的重要手段之一。而分析安全协议中存在的缺陷却是一个非常困难的问题。目前，安全协议的安全性证明主要包括基于逻辑的形式化证明方法、基于随机预言机模型的证明方法、基于标准模型的证明方法以及基于零知识证明理论的证明方法。与其他方法相比，安全协议的形式化分析技术具有以下优点： 1）能够更准确地界定安全协议的边界，即安全协议与其运行环境的界面； 2）能够更准确地定义安全协议参与者的行为； 3）能够更准确地定义安全协议的安全属性； 4）能够证明安全协议满足其安全属性，以及证明安全协议在什么条件下才能满足其安全属性。 当前安全协议形式分析技术面对的主要挑战之一是如何对复杂密码操作进行形式化定义。传统的安全协议分析技术只对包括加密和数字签名在内的基本密码操作进行了形式化定义，此类基本密码操作仅仅具备认证性与秘密性的安全属性。而现代安全协议中出现了许多新的密码操作，此类密码操作具备了比基本密码操作更为复杂的安全属性。秘密共享就属于这样一类密码操作。 1994年，Dawson等[1]提出了一种多秘密共享（MultiSecret Sharing， MSS） 方案，在这个方案中，多个秘密可以在同一秘密共享方案执行过程中被共享。2004年，Yang等[2]提出了一种新的多秘密共享方案（YangChangHwang， YCH），此方案通过采用单向映射函数实现了多秘密的并行构建。2005年，Shao等[3]基于YCH提出了一种可验证的多秘密共享（Verifiable MultiSecret Sharing， VMSS）方案。2006年，Zhao等[4]基于YCH提出了一种实用的可验证多秘密共享方案。秘密共享方案的上述这些独特的安全属性及其有效实现使得其在现代安全协议中被广泛应用。 对于门限值为（l，t）的秘密共享方案，其参与者包括秘密委托者1，2，…，l与一个可信任的秘密分发者。秘密共享方案包括关于秘密份额的分割算法、验证算法与合并算法。在秘密分发阶段，秘密分发者通过输入秘密分发者参数产生秘密份额密钥SK1，SK2，…，SKl与秘密份额验证公钥VK1，VK2，…，VKl。之后，秘密分发者或者秘密委托者i可以通过输入秘密委托者参数以及由秘密分发者分配的秘密份额密钥SKi，生成秘密份额Di。秘密份额的验证算法则通过输入秘密份额Di和秘密份额验证公钥VKi来验证秘密份额Di是否有效。秘密份额的合并算法则通过输入t个有效的秘密份额生成秘密D。其中秘密D是通过对秘密分发者参数与秘密委托者参数进行基本密码操作而得到的信息项序列。秘密共享方案的基本安全属性表现为： 1）通过t个或者更多个秘密份额Di可以计算得到秘密D（正确性）； 2）通过t-1个或者更少个秘密份额Di计算得到秘密D是不可行的（健壮性）。 由于可验证的多秘密共享方案本身的复杂性，对其所有安全属性进行形式化定义非常困难，Yew等[5]在Coq工具中提出过关于一般秘密共享方案的形式化定义，但其仍然无法实现对可验证的多秘密共享方案进行形式化建模。 因此，本文在应用Pi演算中实现了关于可验证的多秘密共享方案相关密码操作的形式化定义，同时，利用等值理论对可验证的多秘密共享方案的密码学语义进行了描述。在此基础上，本文提出了一种用于将上述等值理论转化为自动化验证器ProVerif中重写机制的编码方法，并且，最终在ProVerif中实现了可验证的多秘密共享方案的形式化验证。 1应用Pi演算与等值理论 应用Pi演算[6-9]是当前主要的安全协议形式化分析技术，其成功地实现了关于安全协议抗拒绝服务性、秘密性、认证性、不可否认性等安全属性的验证。基于应用Pi演算的ProVerif安全协议自动化验证器是当前主要的安全协议自