Journal
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
Volume 59, Issue 1, Pages 120-133Publisher
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2013.2279914
Keywords
Automata; discrete event systems (DES); Markov processes; opacity; verification complexity
Funding
- 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
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available