Verification Of K-step Opacity And Infinite-step Opacity Based On Deterministic Finite State Automata

With the growing development of shared network technology,the importance of network security has become increasingly prominent.In discrete event systems,a set of states of the system is usually used as the secret information possessed by the system.Suppose that there is a potential intruder in the system,who has mastered the complete structure and secret states of the system,but has only partial observations on the events that drive the state transitions of the system.Opacity characterizes the ability of the system to keep a secret.If any se-cret state cannot be determined by an intruder within K steps（including K steps）during the whole running period of the system,the system is said to satisfy K-step opacity.Similarly,a system is said to satisfy infinite-step opacity if any secret state cannot be determined by an intruder within infinite steps.As a mathematical model in discrete event systems,automata can represent language according to well-defined rules and can clearly characterize systems whose state transitions are driven by the occurrence of events.In this thesis,K-step opacity and infinite-step opacity of systems modeled as deterministic finite-state automata are inves-tigated in depth.Based on the analysis of K-step opacity of the system,this thesis defines the dangerous state set of the system.Each element of the set is a dangerous state of the system,and dangerous states are states that may reveal secret information about the system.First,by studying the relationship between the dangerous states and the current states,this thesis provides two suf-ficient conditions for verifying K-step opacity of the system.For some systems with good characteristics,this sufficient condition can be used to quickly determine whether K-step opacity is satisfied.Secondly,this thesis also defines the step size dangerous state set and the i-step dangerous state set.The former can clearly describe the step size between the secret states and the corresponding dangerous states?the latter represents all the dangerous states in the system that are at i-step away from the secret state at a particular moment.Finally,inspired by the way to verify current-state opacity,this thesis constructs a new information structure:a verifier（V）.With the occurrence of observable events in the system,the veri-fier can capture the current state set and the step size dangerous state set of the system.By comparing the relationship between the current states and the i-step dangerous states in each node of the verifier,it can determine whether the system has K-step opacity.This method is universal.Infinite-step opacity can be viewed as K-step opacity when K is infinite.Based on the re-search idea of K-step opacity,this thesis studies the infinite-step opacity of the system.First,use the upper bound of the K step opacity to transform infinite-step opacity into(2^|X|-2)-step opacity.Then use the verifier to verify the(2^|X|-2)-step opacity of the system.Sec-ondly,this thesis extends the sufficient condition for verifying K-step opacity to verify the infinite-step opacity of the system.Based on this sufficient condition,this thesis finally con-structs another information structure:an improved-verifier（V_I）.Using V_Ito verify whether the system is infinite-step opacity is similar to the principle when using V,except that the former is more efficient in most application cases.V_Iis also suitable for verifying K-step opacity of the system.