A Verification Approach Of K-step Opacity And Infinite-step Opacity Using Labeled Petri Nets

As an effective mathematical modeling tool in discrete event systems,Petri nets are powerful to solve practical problems.Therefore,Petri nets are applied to network security.Opacity is an urgent problem from the aspect of network security.For a discrete event system,the system is opaque when the secret states that the system needs to hide can not be known by an external intruder,who is generally regarded as an external observer.At present,the main models for discrete event systems of the research on K-step opacity and infinite-step opacity are automata.However,this thesis addresses the verification problem of infinite-step opacity and K-step opacity for discrete event systems modeled with bounded labeled Petri nets.The notions of K-step opacity and infinite-step opacity follow the state-based setting.Opacity is a kind of confidential attribute of a system characterized by a “secret”.A system is said to be K-step opaque if the “secret” cannot be determined within K steps,from step 0 to step K,by an external observer called an “intruder” for all the strings that can be generated by the system,where K is a non-negative integer.Infinite-step opacity can be viewed as K-step opacity,where K is infinite.Based on a basis reachability graph(BRG)that is a compact representation of the reachability graph of a Petri net,a new information structure called a K-delayed observer of the basis reachability graph is proposed in this thesis which based on a basis reachability graph.The K-delayed observer of the basis reachability graph can capture all the k-delayed estimates of the states of the basis reachability graph,where k is a non-negative integer less than or equals to K.The verification of K-step opacity calls for the notion of the k-step unobservable reach.The k-step unobservable reach of a marking is a subset of the unobservable reach of the marking.At this time,by deciding whether all the k-step unobservable reach of the basis markings that the system needs to verify(all the k-step unobservable reach from step 0 to step K)is “secret”,we can confirm whether the system is K-step opaque.The aforementioned method with some changes can be applied to verify whether the system is infinite-step opaque as well.To verify infinite-step opacity for a system,this work proposes a new method based on a basis reachability graph.First,a basis reachability graph and a reversed basis reachability graph(RBRG)of a system are constructed.Then,based on the observers of the basis reachability graph and reversed basis reachability graph,the state intersection of the two observers,called state-intersections,can be found.Finally,a system is verified to be infinite-step opaque if each state-intersection has at least one marking whose infinite-step unobservable reach is not a subset of the secret.The infinite-step unobservable reach of a marking is a subset of the unobservable reach of the marking.This algorithm with some modifications can also be applied to confirm whether the system is K-step opaque.