期刊
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
卷 57, 期 5, 页码 1265-1269出版社
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2011.2173774
关键词
Discrete event systems (DES)
资金
- U.S. National Science Foundation [0426831, 0834409]
- European Commission [INFSO-ICT-223844, PIRG02-GA-2007-224877]
- Division Of Computer and Network Systems
- Direct For Computer & Info Scie & Enginr [0834409] Funding Source: National Science Foundation
We describe and analyze the complexity of verifying the notion of infinite-step opacity in systems that are modeled as non-deterministic finite automata with partial observation on their transitions. Specifically, a system is infinite-step opaque if the entrance of the system state, at any particular instant, to a set of secret states remains opaque (uncertain), for the length of the system operation, to an intruder who observes system activity through some projection map. Infinite-step opacity can be used to characterize the security requirements in many applications, including encryption using pseudo-random generators, coverage properties in sensor networks, and anonymity requirements in protocols for web transactions. We show that infinite-step opacity can be verified via the construction of a set of appropriate initial state estimators and provide illustrative examples. We also establish that the verification of infinite-step opacity is a PSPACE-hard problem.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据