Journal of University of Chinese Academy of Sciences >
The Running-Mode Analysis of SSL310 Basic Handshake Protocol
Received date: 2004-05-09
Revised date: 2004-07-26
Online published: 2005-07-15
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
MO Yan , ZHANG Yu-Qing , LI Xue-Gan . The Running-Mode Analysis of SSL310 Basic Handshake Protocol[J]. Journal of University of Chinese Academy of Sciences, 2005 , 22(4) : 511 -517 . DOI: 10.7523/j.issn.2095-6134.2005.4.018
[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
/
| 〈 |
|
〉 |