Enforcement of K-Step Opacity with Edit Functions
Andrew Wintenberg, Matthew Blischke, Stéphane Lafortune, Necmiye Özay · 2021 60th IEEE Conference on Decision and Control (CDC) · 2021
Opacity is an information flow property for dynamic systems describing plausible deniability, that is whether an eavesdropper can deduce that "secret" behavior has occurred. In particular, K-step opacity considers secret actions that have occurred within the last K-steps in the past. We consider the problem of K-step opacity enforcement over automata using obfuscation. We present a general framework for K-step opacity enforcement and transform the problem of enforcing K-step opacity to enforcing current-state opacity. We can then apply existing obfuscation synthesis methods for current-state opacity to K-step opacity. We demonstrate this approach by enforcing privacy in the context of a novel contact tracing model.