Embedded Insertion Functions for Opacity Enforcement

We investigate the enforcement of opacity, an information-flow privacy property, using insertion sequences that modify the output of the system by event insertions. Previous work considered the problem of enforcing the opacity under the assumption that the insertion functions were based on the observed system strings. Now, we investigate the more powerful method of insertion sequences based on the...