非否认协议的UC可靠的形式化验证
|
摘要
在网络时代,人们对安全协议的安全性要求越来越高,而借助形式化方法对安全协议进行安全分析是检验安全协议安全性的重要手段。但是形式化的验证方式是建立在密码学完备的基础上的,也就是说被形式化验证证明为安全的协议,在现实中不一定是安全的。所以,Canetti提出了相对于UC框架是可靠的UCSA框架,而后人们对UCSA框架做出了扩展,把UCSA框架转变为基于PAPi演算,并且加入了更多的通信信道假设和密码学抽象。在本文中,我们一方面对前人的工作做出了进一步的扩充和改进,另外一方面我们也用UCSA框架对某一个具体的协议进行了安全分析。本文的主要贡献如下:
首先,本文在前人的基础上添加了可恢复的认证通信这一种新的通信假设,使之可以分析更多种类的安全协议。为此,我们定义了可恢复的认证通信的辅助进程,定义了可恢复的认证通信的理想功能并且证明了在扩展后的UCSA框架下,形式化安全与UC安全的等价性。我们对UCSA框架下的简单协议进行了扩充,使之能够使用新加入的可恢复的认证通信假设。我们还定义了新的简单协议翻译规则和新的攻击者策略和新的协议事件来反映所添加的可恢复的认证通信假设。
其次,我们在本文中用扩展后的UCSA框架对Zhou-Gollmann协议(以下简称ZG协议)进行了安全分析,分析它在无可恢复的认证通信假设和在有可恢复的认证通信假设的情况下是否符合非否认性的形式化定义。本文用UCSA框架及其变体对某一个具体的安全协议做出从头到尾的分析。本文根据ZG协议的定义对协议的参与者用简单协议进行建模,然后用简单协议到形式化协议的翻译规则把它们翻译成相对应的形式化进程。最后分析整个协议的进程是否满足非否认性的形式化定义。
最后,本文证明了在无可恢复信道假设下,ZG协议不符合非否认性的标准,但是在有可恢复信道的假设下,ZG协议符合非否认性的标准。
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.
首先,本文在前人的基础上添加了可恢复的认证通信这一种新的通信假设,使之可以分析更多种类的安全协议。为此,我们定义了可恢复的认证通信的辅助进程,定义了可恢复的认证通信的理想功能并且证明了在扩展后的UCSA框架下,形式化安全与UC安全的等价性。我们对UCSA框架下的简单协议进行了扩充,使之能够使用新加入的可恢复的认证通信假设。我们还定义了新的简单协议翻译规则和新的攻击者策略和新的协议事件来反映所添加的可恢复的认证通信假设。
其次,我们在本文中用扩展后的UCSA框架对Zhou-Gollmann协议(以下简称ZG协议)进行了安全分析,分析它在无可恢复的认证通信假设和在有可恢复的认证通信假设的情况下是否符合非否认性的形式化定义。本文用UCSA框架及其变体对某一个具体的安全协议做出从头到尾的分析。本文根据ZG协议的定义对协议的参与者用简单协议进行建模,然后用简单协议到形式化协议的翻译规则把它们翻译成相对应的形式化进程。最后分析整个协议的进程是否满足非否认性的形式化定义。
最后,本文证明了在无可恢复信道假设下,ZG协议不符合非否认性的标准,但是在有可恢复信道的假设下,ZG协议符合非否认性的标准。
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.
引文
[1] Qing SH. Twenty years development of security protocols research. Journal of Software, 2003, 14(10): 1740~1752.
[2] M Burrows, M Abadi, R Needham. A logic of Authentication.ACM SIGOPS Symposium on Operating Systems Principles, December 1989.
[3] F. Javier, J. Herzog, J. Guttman. Strand spaces: why is a security protocol correct? In IEEE Symposium on Security and Privacy, Washington-Brussels-Tokyo, 1998:24-34
[4] C.A.R. Hoare. Communicating Sequential Processes. Communications of the ACM, 21(8):666-677, 1978.
[5] Martin Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Inf. Comput., 148(1):1-70, 1999.
[6] Martin Abadi and Phillip Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). In IFIP TCS, pages 3-22, 2000.
[7] Martin Abadi and Jan Jurjens. Formal eavesdropping and its computational interpretation. In TACS, pages 82-94, 2001.
[8] Daniele Micciancio and Bogdan Warinschi. Soundness of formal encryption in the presence of active adversaries. In TCC, pages 133-151, 2004.
[9] Ran Canetti and Jonathan Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). In TCC, 2006. 10 kshay Patil On Symbolic nalysis of Cryptographic Protocols Master’s thesis,MASSCHUSETTS INSTITUTE OF TECHNOLOGY, 2005.
[11]罗正钦.基于UC框架的安全协议形式化分析.硕士论文,上海交通大学, 2007
[12] Jianying Zhou, Dieter Gollmann. A Fair Non-repudiation Protocol. IEEE Symposium on Security and Privacy 1996: 55-61.
[13] Ran Canetti. Universally Composable Security: A new Paradigm for cryptographic Protocols. In FOCS, Pages136-145, 2001.
[14] Shimon Even, Oded Goldreich, Abraham Lempel: A Randomized Protocol for Signing Contracts. Commun. ACM 28(6): 637-647, 1985
[15] Ernest F. Brickell, David Chaum, Ivan Damg?rd, Jeroen van de Graaf: Gradual and Verifiable Release of a Secret. CRYPTO 1987: 156-166
[16] Bruce Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. New York: Wiley, 1996.
[17] Shafi Goldwasser, Silvio Micali, Charles Rackoff: The Knowledge Complexity of Interactive Proof Systems. SIAM J. Comput. 18(1): 186-208, 1989
[18] Jean Goubault-Larrecq, Catuscia Palamidessi, Angelo Troina: A Probabilistic Applied Pi-Calculus. APLAS 2007: 175-190.
[19] Shimon Even, Oded Goldreich, Abraham Lempel: A Randomized Protocol for Signing Contracts. Commun. ACM 28(6): 637-647, 1985
[20] ISO/IEC JTC1/SC27 N993. 6th working draft on Non-repudiation, Part 3: Mechanisms using asymmetric techniques. ISO/IEC WD 13888-3, April 1995.
[21] S. Schneider. Formal analysis of a non-repudiation protocol. In Proceedings of 11th IEEE Computer Security Foundations Workshop, pages 54-65, 2001
[22] KIM K, PARK S, BAEK J. Improving fairness and privacy of Zhou Gollmann’s fair non-repudiation protocol. In Proc of ICPP Work-shops on Security. pages 140-145, 1999.
[23] Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: International Refinement Workshop and Formal Methods Pacific 1998. pages 370-380, 1998
[24] Kremer S, Markowitch O. Fair multi-party non-repudiation protocols. International Journal of Information Security, 2003, 1(4): 223-235.
[25] Schneider S. Formal analysis of a non-repudiation protocol. In: Proceedings of the 11th IEEE Computer Security Foundations Workshop, pages 54-65, 1998
[26] KimK, Park S, Baek J. Improving fairness and privacy of Zhou-Gollmann’s fairnon-repudiation protocol. In: Proceedings of the 1999 ICPP Workshops on Security, pages 140-145, 1999
[27]黎波涛,罗军舟. Zhou-Gollmann不可否认协议的一种新的改进.计算机学报, 2005, 28(1):35-46
[28] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Pro-ceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 104-115, 2001.
[29] Jesus F. Almansa, The Full Abstraction of the UC Framework, Cryptology ePrint Archive, 2005
[2] M Burrows, M Abadi, R Needham. A logic of Authentication.ACM SIGOPS Symposium on Operating Systems Principles, December 1989.
[3] F. Javier, J. Herzog, J. Guttman. Strand spaces: why is a security protocol correct? In IEEE Symposium on Security and Privacy, Washington-Brussels-Tokyo, 1998:24-34
[4] C.A.R. Hoare. Communicating Sequential Processes. Communications of the ACM, 21(8):666-677, 1978.
[5] Martin Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Inf. Comput., 148(1):1-70, 1999.
[6] Martin Abadi and Phillip Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). In IFIP TCS, pages 3-22, 2000.
[7] Martin Abadi and Jan Jurjens. Formal eavesdropping and its computational interpretation. In TACS, pages 82-94, 2001.
[8] Daniele Micciancio and Bogdan Warinschi. Soundness of formal encryption in the presence of active adversaries. In TCC, pages 133-151, 2004.
[9] Ran Canetti and Jonathan Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). In TCC, 2006. 10 kshay Patil On Symbolic nalysis of Cryptographic Protocols Master’s thesis,MASSCHUSETTS INSTITUTE OF TECHNOLOGY, 2005.
[11]罗正钦.基于UC框架的安全协议形式化分析.硕士论文,上海交通大学, 2007
[12] Jianying Zhou, Dieter Gollmann. A Fair Non-repudiation Protocol. IEEE Symposium on Security and Privacy 1996: 55-61.
[13] Ran Canetti. Universally Composable Security: A new Paradigm for cryptographic Protocols. In FOCS, Pages136-145, 2001.
[14] Shimon Even, Oded Goldreich, Abraham Lempel: A Randomized Protocol for Signing Contracts. Commun. ACM 28(6): 637-647, 1985
[15] Ernest F. Brickell, David Chaum, Ivan Damg?rd, Jeroen van de Graaf: Gradual and Verifiable Release of a Secret. CRYPTO 1987: 156-166
[16] Bruce Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. New York: Wiley, 1996.
[17] Shafi Goldwasser, Silvio Micali, Charles Rackoff: The Knowledge Complexity of Interactive Proof Systems. SIAM J. Comput. 18(1): 186-208, 1989
[18] Jean Goubault-Larrecq, Catuscia Palamidessi, Angelo Troina: A Probabilistic Applied Pi-Calculus. APLAS 2007: 175-190.
[19] Shimon Even, Oded Goldreich, Abraham Lempel: A Randomized Protocol for Signing Contracts. Commun. ACM 28(6): 637-647, 1985
[20] ISO/IEC JTC1/SC27 N993. 6th working draft on Non-repudiation, Part 3: Mechanisms using asymmetric techniques. ISO/IEC WD 13888-3, April 1995.
[21] S. Schneider. Formal analysis of a non-repudiation protocol. In Proceedings of 11th IEEE Computer Security Foundations Workshop, pages 54-65, 2001
[22] KIM K, PARK S, BAEK J. Improving fairness and privacy of Zhou Gollmann’s fair non-repudiation protocol. In Proc of ICPP Work-shops on Security. pages 140-145, 1999.
[23] Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: International Refinement Workshop and Formal Methods Pacific 1998. pages 370-380, 1998
[24] Kremer S, Markowitch O. Fair multi-party non-repudiation protocols. International Journal of Information Security, 2003, 1(4): 223-235.
[25] Schneider S. Formal analysis of a non-repudiation protocol. In: Proceedings of the 11th IEEE Computer Security Foundations Workshop, pages 54-65, 1998
[26] KimK, Park S, Baek J. Improving fairness and privacy of Zhou-Gollmann’s fairnon-repudiation protocol. In: Proceedings of the 1999 ICPP Workshops on Security, pages 140-145, 1999
[27]黎波涛,罗军舟. Zhou-Gollmann不可否认协议的一种新的改进.计算机学报, 2005, 28(1):35-46
[28] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Pro-ceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 104-115, 2001.
[29] Jesus F. Almansa, The Full Abstraction of the UC Framework, Cryptology ePrint Archive, 2005