Hadjicostis C N (2020) Introduction to Estimation and Inference in Discrete Event Systems. In: Montanari U, Rolim J D P, Welzl E (eds) Automata, Languages and Programming, Lecture Notes in Computer Science. įocardi R, Gorrieri R, Martinelli F (2000) Non Interference for the Analysis of Cryptographic Protocols. įalcone Y, Marchand H (2015) Enforcement and validation (at runtime) of various notions of opacity. , IEEE Transactions on Automatic Controlįalcone Y, Marchand H (2013) Runtime Enforcement of K-step Opacity, pp 7271–7278. (1:5)2009, arXiv: 0902.3958ĭubreil J, Darondeau P, Marchand H (2010) Supervisory Control for Opacity. Springer, Berlin, pp 265–284ĭoyen L, Raskin J-F (2009) Antichains for the Automata-Based Approach to Model-Checking. In: Abadi M, Kremer S (eds) Principles of Security and Trust, Lecture Notes in Computer Science. Springer, Berlin, pp 352–367Ĭlarkson M R, Finkbeiner B, Koleini M, Micinski K K, Rabe M N, Sãnchez C (2014) Temporal Logics for Hyperproperties. In: Liu Z, Ravn A P (eds) Automated Technology for Verification and Analysis, Lecture Notes in Computer Science. Springer, Berlin, pp 21–30Ĭassez F, Dubreil J, Marchand H (2009) Dynamic Observers for the Synthesis of Opaque Systems. In: Park J H, Chen H-H, Atiquzzaman M, Lee C, Kim T-, Yeo S-S (eds) Advances in Information Security and Assurance, Lecture Notes in Computer Science. Springer, New YorkĬassez F (2009) The Dark Side of Timed Opacity. Ĭassandras C G, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. īryans J W, Koutny M, Mazaré L, Ryan P Y A (2008) Opacity generalised to transition systems. Electr Notes Theor Comput Sci 121:101–115. īryans J, Koutny M, Ryan P (2005) Modelling Opacity Using Petri Nets. In Application and Theory of Petri Nets and Concurrency (pp. , arXiv: 1301.6799īérard B, Haar S, Schmitz S, Schwoon S (2017) The Complexity of Diagnosability and Opacity Verification for Petri Nets. In each case, the proposed methods offer significant reductions in runtime and space complexity.īérard B, Mullins J, Sassolas M (2015) Quantifying Opacity. We then analyze the corresponding language-based verification methods both formally and with numerical examples. We provide a language-based view of K-step opacity encompassing two existing notions and two new ones. We then investigate the notions of K-step opacity. We demonstrate this approach for current-state and initial-state opacity, unifying existing results. We present several methods for language-based opacity verification, and a general approach to transform state-based notions into language-based ones. We use this framework to discuss language-based and state-based notions of opacity over automata. In this paper we provide a general framework of opacity to unify the many existing notions of opacity that exist for discrete event systems. Opacity is an information flow property that captures the notion of plausible deniability in dynamic systems, that is whether an intruder can deduce that “secret” behavior has occurred.
0 Comments
Leave a Reply. |