Research On Opacity In Discrete Event Systems

With the rapid development of network devices and network technologies,safety and privacy in online services and network communications have received considerable attention.Over the last decade,opacity of Discrete Event Systems(DESs)has become a very fertile field of research.A system is opaque if an outside intruder is unable to infer important information(namely "secret")of system.In DESs,depending on the definition of secret,opacity is usually categorized as current-state opacity,initial-state opacity,initial-and-final-state opacity,language-based opacity,K-step opacity and infinite step opacity,etc.In this thesis,we discuss the verification of opacity of DESs by using semi-tensor product(STP)of matrices,and study the enforcement of opacity of DESs by using a new insertion mechanism.The main works of this dissertation are listed as follows:In Chapter 1,there is a brief introduction for the research state of opacity in DESs.Some interesting results about opacity in DESs are also introduced in this chapter.In Chapter 2,we present some preliminaries including notions and knowledges about the automata model,the definition and properties of STP of matrices,and so on.In Chapter 3,we study the verification of opacity of DESs based on STP of matrices.Using the STP of matrices,the algebraic expression of the observable dynamic of the transition of system is given,then some necessary and sufficient conditions are obtained.Thus,opacity of the nondeterministic finite-state automaton can be verified.In addition,an illustrative example is presented to verify the effectiveness of our method.The proposed matrix-based characterization can make the DESs problems intuitively,and it may provide a helpful angel in contributing to the comprehension of the structure of opacity.Moreover,it provides a new aspect for the verification of opacity of DESs by using the algebraic expression.In Chapter 4,we investigate the enforcement of opacity based on k-memory-embedded insertion mechanism.The enforcement of opacity becomes an important research topic when the given system is not opaque.Based on the embedded insertion mechanism and the k-memory insertion mechanism,we introduce a new mechanism named k-memory-embedded insertion mechanism.Specially,in our k-memory-embedded insertion mechanism,the insertion decision is determined based on the knowledge of system's exact states and the stored next sequence of events with length k.We construct a verifier of this insertion mechanism,then give a necessary and sufficient condition for the enforcement of a given opacity notion of the system.In addition,an example is presented to illustrate the effectiveness of our method.Our proposed mechanism improves the embedded insertion mechanism,can be applied to a broader class of systems,and improves the k-memory insertion mechanism by reducing the number of consecutive events needing to be stored.In Chapter 5,a brief conclusion is presented to end this work,also the prospect for the work is made.