信息安全若干关键技术的研究与应用
|
摘要
信息安全在银行、电信、政府机关大型软件系统中的重要性愈来愈显突出，这些领域的软件系统对安全性要求极高。由于信息安全对国民经济的影响日益加深，研究信息安全的关键技术，尤其是基础理论及其实际应用尤其显得重要和紧迫。本文拟研究信息安全的两大基础理论，其一是密码学，现代信息安全的基石是密码学，包括传统密码学，对称密码学，非对称密码学，消息摘要，数字签名，公开密钥基础设施PKI，SSL：其二是密码协议，它是应用密码学，使用密码协议可以对保证网络通信协议的认证性、秘密性、完整性和非否认性，这对于大型软件系统十分重要。本文对密码协议采用形式化方法进行分析和验证，这是一种严格而有效的方法。在此基础上，将给出一个基于J2EE大型电子银行应用系统的安全体系结构模型，为银行、电信、政府机关大型软件系统的安全提供保障。
针对上述研究目标，本文主要进行了以下工作：
(1)研究密码学和信息安全的基本理论和关键技术
(2)针对安全协议分析和设计的困难性，对现有的安全协议形式化分析和验证方法进行了分析比较
(3)使用形式化方法BAN逻辑分析验证NSSK协议，针对NSSK协议的一个缺陷提出了改进方法，并对该协议进行了优化
(4)使用形式化方法Kailar逻辑分析CMP协议，并指出了Kailar逻辑的特点及局限性
(5)研究核心Java安全模块及其类库
(6)针对“没有整体安全设计和安全部署，即无计算机信息安全可言”这一论断，使用面向对象语言Java，提出一个基于J2EE的四层电子银行应用程序的安全体系结构模型
Information security's significance is more and more prominent in the software system of bank, telecom and government, it requires very high security. Because information security increasingly affect economy deeply. research to its key technolgies, especially its basic theory and application is of importance and pressure. This thesis focus on its two basic theory, one is cryptography , it is a foundation of modern information security; the other is security protocol, its aim is ensure authentication security integrity and non-repudiation of network communication protocol , and it is very important to software system. What's more, this thesis use formal method to analyze and verify security protocol , formal method is regraded as a strict and valid method. Then we will present a security architecture model of e-bank application system based on J2EE, it provides guarantee to software system of bank, telecom and government.
According to these research aims, this paper mainly conduct following works: (1)Research basic theory and key technologies of cryptography and information security
(2)According to the difficulty of security protocol analysis and design, we discuss formal methods of security protocol at present
(3)Using BAN logic analyze NSSK protocol, according to a deficiency of NSSK protocol we pose a improving method , and optimize it
(4)Using Kailar logic analyze CMP protocol and point to its characteristic and limitation
(5) Research core Java security module and its class libraries
(6)According to the judgment that "if no overall security design and deploy there is no computer information security", we pose a security architecture model founding on four layers e-bank application system
针对上述研究目标，本文主要进行了以下工作：
(1)研究密码学和信息安全的基本理论和关键技术
(2)针对安全协议分析和设计的困难性，对现有的安全协议形式化分析和验证方法进行了分析比较
(3)使用形式化方法BAN逻辑分析验证NSSK协议，针对NSSK协议的一个缺陷提出了改进方法，并对该协议进行了优化
(4)使用形式化方法Kailar逻辑分析CMP协议，并指出了Kailar逻辑的特点及局限性
(5)研究核心Java安全模块及其类库
(6)针对“没有整体安全设计和安全部署，即无计算机信息安全可言”这一论断，使用面向对象语言Java，提出一个基于J2EE的四层电子银行应用程序的安全体系结构模型
Information security's significance is more and more prominent in the software system of bank, telecom and government, it requires very high security. Because information security increasingly affect economy deeply. research to its key technolgies, especially its basic theory and application is of importance and pressure. This thesis focus on its two basic theory, one is cryptography , it is a foundation of modern information security; the other is security protocol, its aim is ensure authentication security integrity and non-repudiation of network communication protocol , and it is very important to software system. What's more, this thesis use formal method to analyze and verify security protocol , formal method is regraded as a strict and valid method. Then we will present a security architecture model of e-bank application system based on J2EE, it provides guarantee to software system of bank, telecom and government.
According to these research aims, this paper mainly conduct following works: (1)Research basic theory and key technologies of cryptography and information security
(2)According to the difficulty of security protocol analysis and design, we discuss formal methods of security protocol at present
(3)Using BAN logic analyze NSSK protocol, according to a deficiency of NSSK protocol we pose a improving method , and optimize it
(4)Using Kailar logic analyze CMP protocol and point to its characteristic and limitation
(5) Research core Java security module and its class libraries
(6)According to the judgment that "if no overall security design and deploy there is no computer information security", we pose a security architecture model founding on four layers e-bank application system
引文
1. Qing, SH. Cryptography and Computer Network Security. Beijing: Tsinghua University Press, 2001.
2. Meadows C. Formal verification of cryptographic protocols: A survey. In: Advances in Cryptology, Asiacrypt'96 Proceedings. LNCS 1163, Berlin: Springer-Verlag, 1996
3. ] Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press
4. Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security, 1999
5. Abadi M, Tuttle MR. A semantics for a logic of authentication. In: Proceedings of the 10th ACM Symposium on Principles of Distributed Computing. ACM Press, 1991
6. van Oorschot PC. Extending cryptographic logics or belief to key agreement protocols. In: Proceedings of the 1st ACM Conference on Computer and Communications Security. ACM Press, 1993
7. Dolev D, Yao A. On the sccurity of puhlic key protocols. IEEE Transactions on Information Theory, 1983
8. Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978
9. Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, 1996
10. Syverson P. Formal semantics for logics of cryptographic protocols. In: Proceedings of the Computer Security Foundations Workshop Ⅲ. Los Alamitos: IEEE Computer Society Press
11. ] Burrows M, Abadi M, Needbam R. Rejoinder to Nessett. Operating Systems Review, 1990
12. Diffie W, Hellman ME. New directions in cryptography. IEEE Transactions on Information Theory, 1976
13. Lowe G. A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1997
14. Guttman JD, Thayer FJ. Authentication tests. In: Proceedings of the 2000 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 2000
15. Schneider SA. Security properties and CSP. In: Proceedings of the 1996 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1996
16. Schneider S, Sidiropoutos A. CSP and anonymity. In: Proceedings of the
Computer Security-ES-ORICS'96. LNCS 950, Berlin: Springer-Verlag, 1996
17. Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software-Concepts and Tools, 1996
18．卢开澄．计算机密码学(第3版)，清华大学出版社
19．卿斯汉．密码学与计算机网络安全，清华大学出版社
20．Bruce Schneier著．吴世忠、祝世雄、张文政等译，机械工业出版社
21．Java安全性编程指南．Jess Garmas、Daniel Somerfield著，庞南、管和吕、陈立志等译，电子工业出版社
22．卿斯汉．安全协议20年研究进展，软件学报，2003，14
23．卿斯汉．认证协议的形式化分析．软件学报，1996，7
24．卿斯汉．一种新型的非否认协议．软件学报，2000，11
25．王贵林，卿斯汉，周展飞．认证协议的一些新攻击方法，软件学报，2001，12
26．周典萃，卿斯汉，周展飞．Kailar逻辑的缺陷，软件学报，1999，10
27．周典萃，卿斯汉，周展飞．一种分析电子商务协议的新工具，软件学报，2001，12
28．卿斯汉．安全协议的设计与逻辑分析，软件学报，2003，14
29．冯登国，吴文玲．分组密码的设计与分析，清华大学出版社，2000．
30．刘怡文，李伟琴．密码协议的分层安全需求及验证，北京航空航天大学学报 2002，28
2. Meadows C. Formal verification of cryptographic protocols: A survey. In: Advances in Cryptology, Asiacrypt'96 Proceedings. LNCS 1163, Berlin: Springer-Verlag, 1996
3. ] Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press
4. Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security, 1999
5. Abadi M, Tuttle MR. A semantics for a logic of authentication. In: Proceedings of the 10th ACM Symposium on Principles of Distributed Computing. ACM Press, 1991
6. van Oorschot PC. Extending cryptographic logics or belief to key agreement protocols. In: Proceedings of the 1st ACM Conference on Computer and Communications Security. ACM Press, 1993
7. Dolev D, Yao A. On the sccurity of puhlic key protocols. IEEE Transactions on Information Theory, 1983
8. Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978
9. Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, 1996
10. Syverson P. Formal semantics for logics of cryptographic protocols. In: Proceedings of the Computer Security Foundations Workshop Ⅲ. Los Alamitos: IEEE Computer Society Press
11. ] Burrows M, Abadi M, Needbam R. Rejoinder to Nessett. Operating Systems Review, 1990
12. Diffie W, Hellman ME. New directions in cryptography. IEEE Transactions on Information Theory, 1976
13. Lowe G. A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1997
14. Guttman JD, Thayer FJ. Authentication tests. In: Proceedings of the 2000 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 2000
15. Schneider SA. Security properties and CSP. In: Proceedings of the 1996 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1996
16. Schneider S, Sidiropoutos A. CSP and anonymity. In: Proceedings of the
Computer Security-ES-ORICS'96. LNCS 950, Berlin: Springer-Verlag, 1996
17. Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software-Concepts and Tools, 1996
18．卢开澄．计算机密码学(第3版)，清华大学出版社
19．卿斯汉．密码学与计算机网络安全，清华大学出版社
20．Bruce Schneier著．吴世忠、祝世雄、张文政等译，机械工业出版社
21．Java安全性编程指南．Jess Garmas、Daniel Somerfield著，庞南、管和吕、陈立志等译，电子工业出版社
22．卿斯汉．安全协议20年研究进展，软件学报，2003，14
23．卿斯汉．认证协议的形式化分析．软件学报，1996，7
24．卿斯汉．一种新型的非否认协议．软件学报，2000，11
25．王贵林，卿斯汉，周展飞．认证协议的一些新攻击方法，软件学报，2001，12
26．周典萃，卿斯汉，周展飞．Kailar逻辑的缺陷，软件学报，1999，10
27．周典萃，卿斯汉，周展飞．一种分析电子商务协议的新工具，软件学报，2001，12
28．卿斯汉．安全协议的设计与逻辑分析，软件学报，2003，14
29．冯登国，吴文玲．分组密码的设计与分析，清华大学出版社，2000．
30．刘怡文，李伟琴．密码协议的分层安全需求及验证，北京航空航天大学学报 2002，28