Verification of Archive System Opacity With Bounded Labeled Petri Nets

Opacity is an essential security indicator in archive systems. There exists a set of secret states and an external intruder who can observe the behavior of the system in the archive system. The intruder can steal private information by observing the behavior of the system. The system is said to be ${K}$ -step opaque when the intruder cannot confirm whether the system has been in a secret state at any time, within the observation of ${K}$ events. In the case where an intruder can never be sure whether the system has ever been in a secret state, the system is referred to be infinite-step opaque. To be realistic, we consider an archive system modeled as a bounded labeled Petri net, and propose an algorithm for constructing a modified state estimator to increase the security of the archive system. Our aim is to verify the two types of opacity of the system by the observer and the modified state estimator. Our new algorithm improves the security of the system so that an intruder cannot easily know whether the system is in a secret state or not, which also improves the previously-known results.