Name
Abstract | ||
|---|---|---|
We consider the problem of model-checking some of the well-known trace-based information flow properties from the literature for classes of infinite-state system models. We first define some language-theoretic operations that help to characterize language inclusion in terms of these properties. This gives us a reduction of the language inclusion problem for a class of system models, say F, to the model checking problem for F, whenever F is effectively closed under these language-theoretic operations. We apply this result to show that the problem of model-checking any of these properties for One Counter Nets, One-Counter Automata, Basic Parallel Processes, and some properties for deterministic One Counter Automata, is undecidable. We also consider the class of Visibly Pushdown Systems and show that their model-checking problem is undecidable for a couple of properties. For the special case when all confidential events are internal we show that model-checking each of these properties for Visibly Pushdown Systems becomes decidable. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.3233/JCS-160549 | JOURNAL OF COMPUTER SECURITY |
Keywords | Field | DocType |
Model-checking,Petri net,information flow,security,pushdown,visibly pushdown,deterministic pushdown,one-counter | Language inclusion,Information flow (information theory),Model checking,Computer science,Automaton,Decidability,Theoretical computer science,Special case,Undecidable problem | Journal |
Volume | Issue | ISSN |
24 | 5 | 0926-227X |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Deepak D'souza | 1 | 239 | 17.90 |
| Raghavendra K. Ramesh | 2 | 6 | 0.81 |