Based On Uml Security Protocol Modeling And Automatic Detection

The network security is a focus which people pay close attention to at present, and the safety of security protocol is the key to the network security.The security protocol applies to conveying the file,carrying on various kinds of trade in the network and visiting to computer system etc. people have already proved that some security protocols are not as safe as they have been declared through different methods. So verifying safe of security protocol becomes the hotspot.The main task of the thesis is to investigate the visual modeling and automatically verifying of security protocol.The paper introduces the security protocol at first,and introduces the formalized methode and automatically verifying of security protocol, It also introduces the principles,characteristics of model checking tool SPIN and its modeling language PROMELA emphatically.Then the paper proposes the rule and course of UML modeling of security protocol,and the process of transforming UML model of security procotol to PROMELA programs and how to produce attacker model automatically are presented. In order to combine the visual design of security protocol with its automatically verifying,the automatic verification tool for UML model of security procotol has been designed and developed.