Opacity For Discrete Event Systems Based On Structural Analysis

With the development of modern network technology,information has spread to every corner of people's lives.Information security has become an important issue.In terms of information security,researchers have proposed the concept of opacity.If an intruder cannot deduce sensitive information(called secret)by observing a system,then the system is opaque.In a discrete event system,opacity is usually categorized as current-state opacity,initial-state opacity,and language opacity.Existing methods for verifying current-state opacity require calculate reachable markings or basic markings of labeled Petri nets.For large systems,the problem of state explosion is inevitable.For reducing the computational complexity of determining opacity of a system,this thesis discusses opacity based on structure analysis.Labeled Petri nets are analyzed,and the concepts of equivalent places,equivalent markings and subnets of labeled Petri net are proposed.A theorem for determining current-state opacity is proposed according to the concepts of reachable markings of subnets and equivalent markings.By simplifying labeled Petri nets,the burden of calculation to verify current-state opacity is reduced.The main tasks completed in this thesis are:1.For current-state opacity,labeled Petri nets are analyzed,and the concepts of pre-equivalent places,post-equivalent places,pre-equivalent markings and post-equivalent markings are proposed.A theorem of sets of markings consistent with observation sequence is proposed by the definitions of subnets consistent with observation sequence and post-equivalent markings.2.A sufficient condition for determining current-state opacity of a system is proposed by solving post-equivalent markings of secret.The calculations of reachable markings of labeled Petri net and markings consistent with observation sequence can be avoided.Therefore,the proposed approach is better than other methods.3.By computing post-equivalent markings of subnets consistent with observation sequence,a necessary and sufficient condition for determining current-state opacity of a system is proposed.The method reduces the number of states.The definition of semi-concealed markings is proposed.A theorem for determining current-state opacity is proposed according to the definitions of markings of subnets consistent with observation sequence and semi-concealed markings.The theorem avoids solving the post-equivalent markings of subnets consistent with observation sequence.Therefore,the efficiency of the algorithm is further improved.