节点文献

非否认协议的UC可靠的形式化验证

Universally Composable Symbolic Analysis of Non-repudiation Protocols

【作者】 杨杰

【导师】 傅育熙;

【作者基本信息】 上海交通大学 , 计算机科学, 2009, 硕士

【摘要】 在网络时代,人们对安全协议的安全性要求越来越高,而借助形式化方法对安全协议进行安全分析是检验安全协议安全性的重要手段。但是形式化的验证方式是建立在密码学完备的基础上的,也就是说被形式化验证证明为安全的协议,在现实中不一定是安全的。所以,Canetti提出了相对于UC框架是可靠的UCSA框架,而后人们对UCSA框架做出了扩展,把UCSA框架转变为基于PAPi演算,并且加入了更多的通信信道假设和密码学抽象。在本文中,我们一方面对前人的工作做出了进一步的扩充和改进,另外一方面我们也用UCSA框架对某一个具体的协议进行了安全分析。本文的主要贡献如下:首先,本文在前人的基础上添加了可恢复的认证通信这一种新的通信假设,使之可以分析更多种类的安全协议。为此,我们定义了可恢复的认证通信的辅助进程,定义了可恢复的认证通信的理想功能并且证明了在扩展后的UCSA框架下,形式化安全与UC安全的等价性。我们对UCSA框架下的简单协议进行了扩充,使之能够使用新加入的可恢复的认证通信假设。我们还定义了新的简单协议翻译规则和新的攻击者策略和新的协议事件来反映所添加的可恢复的认证通信假设。其次,我们在本文中用扩展后的UCSA框架对Zhou-Gollmann协议(以下简称ZG协议)进行了安全分析,分析它在无可恢复的认证通信假设和在有可恢复的认证通信假设的情况下是否符合非否认性的形式化定义。本文用UCSA框架及其变体对某一个具体的安全协议做出从头到尾的分析。本文根据ZG协议的定义对协议的参与者用简单协议进行建模,然后用简单协议到形式化协议的翻译规则把它们翻译成相对应的形式化进程。最后分析整个协议的进程是否满足非否认性的形式化定义。最后,本文证明了在无可恢复信道假设下,ZG协议不符合非否认性的标准,但是在有可恢复信道的假设下,ZG协议符合非否认性的标准。

【Abstract】 Formal methods become tremendously important in the analysis of security protocols in order to meet nowadays’increasing demand of internet security requirement. However, most existing formal methods abstract away symbolic operations from concrete cryptographic primitives. Thus, it cannot guarantee that the protocol which has been proved to be secure in a formal method remains its security in the real world. The framework UCSA (Universally Composable Symbolic Analysis), proposed by Canetti, constructing general computationally sound proofs of security protocols. After that, Luo extended UCSA into a framework based on PAPi calculus which can handle new communication channel assumptions and new cryptographic primitives. This thesis extends Luo’s framework to deal with new security requirements– non-repudiation. The main contributions are threefold:Firstly, we add resilient authentication communication channel assumption to the UCSA framework so that it can handle the non-repudiation requirement. In order to achieve this, we define a respective assistant process and the ideal functionality for the resilient communication channels and prove the soundness and completeness between them. We extend the simple protocol, adversary strategy and protocol event defined in UCSA to model the new assumption.Secondly, we use the framework to analyze Zhou-Gollmann protocol to check whether it satisfies the non-repudiation requirement with and without resilient communication assumption. It applies UCSA to analyze a concrete protocol ever since it was devised. This thesis models every participant in the ZG protocol and translates the simple protocol into respective symbolic protocol.Finally, we prove that ZG protocol without resilient communication assumption does not meet the security requirement of non-repudiation protocols while ZG protocol with resilient communication assumption does.

节点文献中: 

本文链接的文献网络图示:

本文的引文网络