A General Language-Based Framework for Specifying and Verifying Notions of Opacity

TL;DR

This paper introduces a comprehensive framework for specifying and verifying various notions of opacity in dynamic systems, unifying existing concepts and improving verification efficiency through novel methods and transformations.

Contribution

It provides a unified language-based and state-based framework for opacity, introduces new notions of K-step opacity, and offers more efficient verification techniques.

Findings

Unified framework for opacity notions

New K-step opacity concepts and verification methods

Significant reductions in runtime and space complexity

Abstract

Opacity is an information flow property that captures the notion of plausible deniability in dynamic systems, that is whether an intruder can deduce that "secret" behavior has occurred. In this paper we provide a general framework of opacity to unify the many existing notions of opacity that exist for discrete event systems. We use this framework to discuss language-based and state-based notions of opacity over automata. We present several methods for language-based opacity verification, and a general approach to transform state-based notions into language-based ones. We demonstrate this approach for current-state and initial-state opacity, unifying existing results. We then investigate the notions of K-step opacity. We provide a language-based view of K-step opacity encompassing two existing notions and two new ones. We then analyze the corresponding language-based verification methods both formally and with numerical examples. In each case, the proposed methods offer significant reductions in runtime and space complexity.