Verification of Strong K-Step Opacity for Discrete-Event Systems

Autor:	Han, Xiaoguang, Zhang, Kuize, Li, Zhiwu
Rok vydání:	2022
Předmět:	Computer Science - Cryptography and Security Computer Science - Formal Languages and Automata Theory
Druh dokumentu:	Working Paper
Popis:	In this paper, we revisit the verification of strong K-step opacity (K-SSO) for partially-observed discrete-event systems modeled as nondeterministic finite-state automata. As a stronger version of the standard K-step opacity, K-SSO requires that an intruder cannot make sure whether or not a secret state has been visited within the last K observable steps. To efficiently verify K-SSO, we propose a new concurrent-composition structure, which is a variant of our previously- proposed one. Based on this new structure, we design an algorithm for deciding K-SSO and prove that the proposed algorithm not only reduces the time complexity of the existing algorithms, but also does not depend on the value of K. Furthermore, a new upper bound on the value of K in K-SSO is derived, which also reduces the existing upper bound on K in the literature. Finally, we illustrate the proposed algorithm by a simple example. Comment: 6 pages, 2 figures, submitted to IEEE CDC on March 28, 2022
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2204.04698 Zobrazit plný text záznamu View this record from Arxiv