计算可靠且高效的群组密钥协商协议符号化分析方法

摘要

The computational soundness of symbolic analysis is always argued, because the cryp-tographic primitives are viewed as black boxes, and the specific security properties of those cryp-tographic primitives have not been considered yet. Moreover, this kind of approaches is ineffec-tive , when it is used to analyze group key exchange protocols with a large number of participants. This paper considers those problems above, and proposes computationally sound and effective symbolic analysis of group key exchange protocols. More specifically, we design a pattern func-tion for symbolic expression, so as to define the concrete security properties that modular expo-nentiation operation needs satisfy. Based on that, we prove the symbolic analysis of Burmester-Desmedt protocol is computationally sound in universally composable security framework. Fur-thermore, we use mathematical inductive method to prove the security of Burmester-Desmedt protocol is unrelated to the number of participants. The number of the participants does not affect symbolic analysis. As a result, the efficiency of symbolic analysis is improved.%符号化分析方法将密码原语视为黑盒,且未研究其需要满足的具体安全属性,因而计算可靠性一直备受质疑.而且,这类方法在分析参与者数目较多的群组密钥协商协议时不具有高效性.针对上述两个问题,文中提出了一种计算可靠且高效的群组密钥协商协议符号化分析方法.该方法通过为符号化表达式设计一个Pattern函数,定义了模幂运算需要满足的具体安全属性,并基于此证明了符号化分析Burmester-Desmedt协议在通用可组合安全框架下是计算可靠的.进而通过数学归纳法,证明了Burmester-Desmedt协议的安全性与参与者数目无关,避免了参与者数目对符号化分析造成的影响,提高了符号化分析方法的效率.