The Research Of Security Protocols In Special Environment

With the development of Internet technology, security protocols play more and more important in e-business and e-government application. People pay more attention on the security of protocols, especially in how to model and analyze security protocols in special environment.We first research and analyze on the existing modeling and analyzing methods on security protocols and find the advantages and disadvantages of them. Considering the speciality of the environment, we choose event-based GSPML language to set up visual models for general challenge-response protocol and the simplified version of TLS handshake protocol, which meet all out standards.Then we give a detail analysis on the security conditions for general challenge-response protocol, and we list the necessary conditions for challenge-response protocol in both symmetry and asymmetry cryptographic forms, as well as the attack to them if the conditions are not met. The point we should pay attention to is the difference between the minimum forms of both cryptographic forms. After that, we analyze the traditional three rounds authentication protocols and find that the pure authentication protocol cannot achieve its goal in the environment with active intruders.Besides that, four automation tools of formal methods are analyzed in this paper. These tools contain the logic, model checking and proving methods. We compare these tools from user interface and usability, number of running stats and time, the support of data independence and discrete time modeling, ability of error checking, and draw a result on the comprehensive abilities of them.