Secrecy Analysis For Security Protocol Based On Logic Of Events

The security protocol is the foundation of modern network communication,and the issue of proving the security of protocols is one of the current research hotspots.Authentication and secrecy are the two basic security properties of security protocols.In the complex network environment,if the security properties of the security protocol have not been rigorously proven,the risks in network communication cannot be estimated.At present,the most powerful method for analyzing and verifying security protocols is the Formal Methods.The Logic of Events Theory(LoET)is a formal method for proving security properties of security protocols by defining event structures,which includes an event system,an axiom system,predicate formulas,and a formal description of the protocol.Using the Logic of Events Theory to analyze security protocols,it is only necessary to infer events defined on the honest principle of the protocol,and events of intruder will not affect the inference results.Based on the Logic of Events Theory,we define a lot of predicate formulas,combined with the definition,a set of inference rules is given,and the secrecy proof system is constructed,the improved Logic of Events Theory is used to prove the security properties of two different protocols,so that the application scope of the Logic of Events Theory is expanded,and the secrecy of the security protocol can be verified.The main work and innovations of this paper are as follows:1.The predicate formulas are extended for the Logic of Events Theory.Based on the existing Logic of Events Theory,the predicate formulas are extended to characterize the state of the protocol principles.The extended contents include predicate Has to describe the principle having atomic terms,and the corresponding definition is given,laying the foundation for the secrecy specification;The predicates Fresh and FirstSend are expanded to characterize the freshness of data items and the initiation of sending events,and the corresponding inference rules are given,which enhances the events ordering ability of Logic of Events Theory and reduces the complexity in the protocol analysis process,making the proof of protocol security properties more concise.2.The concept of trace is introduced into the Logic of Events Theory,and definition is given.Based on the trace,the intruder characterization is introduced,and the mathematical induction method is used to prove that proving the secrecy of the protocol in the logic of events secrecy proof system only needs to prove that the message sent by the honest initiator and responder in the protocol is safe without need to show reasoning about the possible attack behavior of the intruder。3.The secrecy proof system of logic of events is built.Based on the Logic of Events Theory,the secrecy proof system is expanded,and the expansion includes the definition of GoodMsg to characterize the security of messages;Defining GoodSend to characterize the security of sending events,and GoodNet is given when the principles satisfy GoodSend in the entire network;Introduce the concepts of KeyHonest and SecHonest to characterize the properties of honest principles;And from the above definitions,a series of inference rules are constructed;Based on the Logic of Events Theory,the general secrecy specification formula is given,which makes the goal more clear,the versatility of the Logic of Events Theory is more stronger,and expands the application scope of the Logic of Events Theory.