EngineeringInformation SecurityInformation LeakageVerificationCommunicationFormal VerificationControl ProtocolHardware SecurityJoint Opacity PropertiesSpecified Secret InformationConfidentiality PropertyInformation Theoretic SecuritySystems EngineeringSecure CommunicationPrivacy-preserving CommunicationOpacity-enforcement ApproachesSecure ProtocolMechanism DesignInsertion FunctionsData PrivacySupervisory ControlComputer ScienceFinite-state SystemData SecurityCryptographyReachability AnalysisDiscrete Event SystemFormal MethodsEnforce Decentralized
Opacity is a confidentiality property that characterizes the non-disclosure of specified secret information of a system to an outside observer. In this paper, we consider the enforcement of opacity within the discrete-event system formalism in the presence of multiple intruders. We study two cases, one without coordination among the intruders and the other with coordination. We propose appropriate notions of opacity corresponding to the two cases, respectively, and propose enforcement mechanisms based on the implementation of insertion functions, which manipulates the output of the system by inserting fictitious observable events whenever necessary. The effectiveness of the proposed opacity-enforcement approaches is validated through illustrative examples.
17
Opacity of discrete event systems and its applications
Feng Lin · Automatica · 2011 · 282 citations
Verification of State-Based Opacity Using Petri Nets
Yin Tong, Zhiwu Li, Carla Seatzu et al. · IEEE Transactions on Automatic Control · 2016 · 269 citations · Full text