| dc.contributor.author | Saboori, A. | en |
| dc.contributor.author | Hadjicostis, Christoforos N. | en |
| dc.creator | Saboori, A. | en |
| dc.creator | Hadjicostis, Christoforos N. | en |
| dc.date.accessioned | 2019-04-08T07:48:14Z | |
| dc.date.available | 2019-04-08T07:48:14Z | |
| dc.date.issued | 2012 | |
| dc.identifier.uri | http://gnosis.library.ucy.ac.cy/handle/7/44824 | |
| dc.description.abstract | 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. © 2012 IEEE. | en |
| dc.source | IEEE Transactions on Automatic Control | en |
| dc.source.uri | https://www.scopus.com/inward/record.uri?eid=2-s2.0-84860430528&doi=10.1109%2fTAC.2011.2173774&partnerID=40&md5=41716b33735428cfb8c7ae6cc4cfee7e | |
| dc.subject | Discrete event simulation | en |
| dc.subject | Sensor networks | en |
| dc.subject | Internet protocols | en |
| dc.subject | Initial state | en |
| dc.subject | Nondeterministic finite automaton | en |
| dc.subject | Opacity | en |
| dc.subject | Illustrative examples | en |
| dc.subject | Partial observation | en |
| dc.subject | System state | en |
| dc.subject | Discrete event systems (des) | en |
| dc.subject | Pseudorandom generators | en |
| dc.subject | Security requirements | en |
| dc.subject | System operation | en |
| dc.subject | Web transactions | en |
| dc.title | Verification of infinite-step opacity and complexity considerations | en |
| dc.type | info:eu-repo/semantics/article | |
| dc.identifier.doi | 10.1109/TAC.2011.2173774 | |
| dc.description.volume | 57 | |
| dc.description.issue | 5 | |
| dc.description.startingpage | 1265 | |
| dc.description.endingpage | 1269 | |
| dc.author.faculty | Πολυτεχνική Σχολή / Faculty of Engineering | |
| dc.author.department | Τμήμα Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών / Department of Electrical and Computer Engineering | |
| dc.type.uhtype | Article | en |
| dc.source.abbreviation | IEEE Trans Autom Control | en |
| dc.contributor.orcid | Hadjicostis, Christoforos N. [0000-0002-1706-708X] | |
| dc.gnosis.orcid | 0000-0002-1706-708X | |
