Analysis And Verification Of The SSL Handshake Protocol Model Based On Event-B

With the development and popularization of Intrnet technology,network environment is becoming increasingly complex.In the open network,how to ensure the security of the communication is an important issue nowadays.On the basis of the password techniques,network security protocol realizes the communication security in the open network environment,and it is the foundation of the network information security.Due to the importance of network security protocol,its correctness and rationality of the design has become an important part of the study of network security.This paper attempted to use formal methods Event-B to analyze and verify the model of the handshake protocol of Secure Sockets Layer on Rodin platform.This paper first introduces the concept of formal methods and safety related contents of network protocol.Then the formal method Event-B and its tool Rodin was introduced in brief.Secondly,Secure Sockets Layer protocol stack architecture,working principle and security mechanism are preliminary researched in this paper,and the handshake protocol is explored.Then,we tried to extract the protocol's specifications,and formulated the elaboration strategy of model at the same time.Based on these,we built and analyzed the handshake protocol model tentatively.After this,we tried to analyze the process of public key authentication and the situation of attacker involved.Finally,we attempted to verify the validity of the model with the help of automatic and interactive proving mechanism in Rodin platform.The result of this paper shows that the analysis and verification of handshake protocol model based on Event-B is relatively effective,elaboration of model is helpful to thorough comprehension of the protocol.Under certain condition,protocol has been proved with authentication and confidentiality,the mechanism of protocol itself can detect attacks on message tampering or such behaviors.We focused on the model of SSL handshake protocol in this paper,the modeling analysis of the protocol stack can be done on the basis of this paper in the future.