Petri Net-based Security Protocol Analysis And Detection Methods

With the Internet technique Developing quickly, the safety problem of information on the network is increasingly serious. Especially in the new businesses such as electronic commerce, numerical currency and the network bank etc., the confidentiality, integrity and usability etc.of the information become the key problems.The security protocols are based on the cryptology, it provides various safe services for each kind of the networks and the distributed systems.The targets of the Security protocols all have something to do with safety, for example, the identity of the attestation for the individuals;the allotment of the conversation keys between the individuals ;Currently security protocols are extensively applied in the network of computers and the distributed systems, one of the key point concerning the safety problems is the formal description and analysis.Currently, the formal analysis methods of the security protocols include the logistic methods,the model checking methods, theorem probative method etc. Each method have its own advantages and disadvantages.This paper mainly studied the checking of security protocols useing Petri nets model as foundation combining other methods. The paper proposed a new kind method applying the new method to analyse and check the security protocols and verify its usefulness.The main innovation points and productions of this paper are as follows:1 .Proposed a new security protocols modelling method. This method based on the three states of individuals to construct the model of the security protocols. The model constructed by the new method have clear meaning and can is easily to analyse.2.Usually many scholars using Petri Nets to analysis security protocols estimate the insecurity states would appear or not to judge the security of the protocols. But the new method proposed by this paper check an existent attack of possibility from the original state of the protocols.3.During the period of checking a security protocols, this method integrate other analysis methods and construct the analytic gathers of each individuals.4.This paper proposed the rules of updating the analytic gathers and the rules of checking attacks.5.In this paperts applied the new method to analyse and check the classic security protocols and find out the potential attacks.