收稿日期: 2004-05-09
修回日期: 2004-07-26
网络出版日期: 2005-07-15
基金资助
国家自然科学基金项目 (60102004,60273027,60025205)资助
The Running-Mode Analysis of SSL310 Basic Handshake Protocol
Received date: 2004-05-09
Revised date: 2004-07-26
Online published: 2005-07-15
莫燕 , 张玉清 , 李学干 . SSL3.0基本握手协议的运行模式分析[J]. 中国科学院大学学报, 2005 , 22(4) : 511 -517 . DOI: 10.7523/j.issn.2095-6134.2005.4.018
The simplified SSL310 basic handshake protocol is analyzed by using a formal analysis method called the approach of the running-mode analysis. By analyzing the protocol, we find three different types of attack. Through an in-depth research,we also find that although these three attacks seem to result from the leak of allowing different versions to coexist, they are different. The major difference is the different role imitation, which probably leads to potential attacks. Finally, some improvement is made to avoid these three attacks effectively, which improves the security of the protocol.
Key words： SSL protocol; formal analysis; running-mode analysis
[1] Alan Ofreier, Philip Karlton, Paul CKocher. The SSL version 31 0, interne-t draft, netscape communications. 1996. http:PPwp. netscape. comPengP ssl3Pss-l toc. html
[2] DWagner, BSchneiner. Analysis of the SSL 31 0 protocol. In: 2nd USENIX Workshop on Elecctronic Commerce. 1996. http:PPwww. schneier. comPpaper-ssl. pdf
[3] JCMitchell, VShmat ikov, USt ern. Finite-state analysis of SSL 31 0. In: 7th USENIX Security Symposium, San Ant onio. 1998. 201～216
[4] SDietrich. A formal analysis of the secure socket s layer protocol : [Ph. D. thesis]. Dept Mathematics and Comput er Science. Adelphi University, 1997
[5] Zhang YQ. Study on analysis of security protocol of computer communicat ion network: [Ph. D. thesis]. Xidian University, 2000(in Chinese with English abstract)
[6] Will Marrero, Edmund Clarke, Somesh Jha. A model checker for authent ication protocols. In: Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Prot ocols. 1997. dimacs. rutgers. eduPWorkshopsPSecurityPprogram2Pmarrero. ps
[7] Zhang YQ,Li JH, Xiao GZ. An approach to the formal verificat ion of the two-party cryptographic protocols. ACM Operating Systems Review, 1999,33(4) : 48～51
/
| 〈 |
|
〉 |
