Verification of initial-state opacity in security applications of discrete event systems

DOI10.1016/j.ins.2013.05.033zbMath1320.68119OpenAlexW2004398490MaRDI QIDQ497279

Anooshiravan Saboori, Christoforos N. Hadjicostis

Publication date: 23 September 2015

Published in: Information Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ins.2013.05.033

zbMATH Keywords

discrete event systemformal methods in security analysisinitial state estimationinitial state estimatortracking in sensor network

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Discrete event control/observation systems (93C65) Observability (93B07) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

A framework for current-state opacity under dynamic information release mechanism, \(k\)-memory-embedded insertion mechanism for opacity enforcement, Current-state opacity and initial-state opacity of modular discrete event systems, Decidability of opacity verification problems in labeled Petri net systems, Initial-state detectability of stochastic discrete-event systems with probabilistic sensor failures, A new approach for the verification of infinite-step and \(K\)-step opacity using two-way observers, Initial-state detectability and initial-state opacity of unambiguous weighted automata, Compositional synthesis of opacity-preserving finite abstractions for interconnected systems, Networked opacity for finite state machine with bounded communication delays, Verification and enforcement of current-state opacity based on a state space approach, Enforcement and validation (at runtime) of various notions of opacity, Strong current-state and initial-state opacity of discrete-event systems, State-based opacity of labeled real-time automata, Game current-state opacity formulation in probabilistic resource automata, Active opacity of discrete-event systems, Matrix approach for verification of opacity of partially observed discrete event systems, Dynamics based privacy preservation in decentralized optimization, Privacy and safety analysis of timed stochastic discrete event systems using Markovian trajectory-observers, Enforcing opacity by insertion functions under multiple energy constraints, Infinite-step opacity and \(K\)-step opacity of stochastic discrete-event systems, Verification of initial-state opacity in security applications of discrete event systems, State Estimation and Fault Detection Using Petri Nets, Current-state opacity modelling and verification in partially observed Petri nets, Probabilistic system opacity in discrete event systems, Detectability of networked discrete event systems, Enforcement of opacity by public and private insertion functions, Supervisor synthesis to thwart cyber attack with bounded sensor reading alterations, On-line verification of current-state opacity by Petri nets and integer linear programming, Relative predictability of failure event occurrences and its opacity-based test algorithm, Opacity of networked discrete event systems, Verification of approximate opacity for switched systems: a compositional approach, Analysis of strong and strong periodic detectability of bounded labeled Petri nets, Online verification of \(K\)-step opacity by Petri nets in centralized and decentralized structures, Enforcing opacity of regular predicates on modal transition systems

Uses Software

• UMDES

Cites Work

• Verification of initial-state opacity in security applications of discrete event systems
• \(k\)-anonymous data collection
• On NFAs where all states are final, initial, or both
• On observability of discrete-event systems
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Decentralized supervisory control of discrete-event systems
• Applicability of fair simulation
• Concurrent secrets
• Classical and Logic-Based Dynamic Observers for Finite Automata
• Introduction to Discrete Event Systems
• Supervisory Control of a Class of Discrete Event Processes
• Testing finite-state machines: state identification and verification
• Unnamed Item
• Unnamed Item