期刊
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
卷 59, 期 1, 页码 120-133出版社
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2013.2279914
关键词
Automata; discrete event systems (DES); Markov processes; opacity; verification complexity
资金
- National Science Foundation (NSF), under NSF CNS Award [0834409]
- European Commission (EC) [INFSO-ICT-223844, PIRG02-GA-2007-224877]
- Direct For Computer & Info Scie & Enginr
- Division Of Computer and Network Systems [0834409] Funding Source: National Science Foundation
A system is said to be current-state opaque if the entrance of the system state to a set of secret states remains opaque (uncertain) to an intruder-at least until the system leaves the set of secret states. This notion of opacity has been studied in nondeterministic finite automata settings (where the intruder observes a subset of events, for example, via some natural projection mapping) and has been shown to be useful in characterizing security requirements in many applications (including encryption using pseudorandom generators and coverage properties in sensor networks). One limitation of the majority of existing analysis is that it fails to provide a quantifiable measure of opacity for a given system; instead, it simply provides a binary characterization of the system (being opaque or not opaque). In this paper, we address this limitation by extending current-state opacity formulations to systems that can be modeled as probabilistic finite automata under partial observation. We introduce three notions of opacity, namely: 1) step-based almost current-state opacity; 2) almost current-state opacity; and 3) probabilistic current-state opacity, all of which can be used to provide a measure of a given system's opacity. We also propose verification methods for these probabilistic notions of opacity and characterize their corresponding computational complexities.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据