Model-checking bisimulation-based information flow properties for pushdown systems
Deepak D'Souza, K.R.Raghavendra
Abstract: Bisimulation-based information flow properties were intro-
duced by Focardi and Gorrieri in 2005 as a way of specifying security
properties for transition system models. These properties were shown to be
decidable for finite-state systems. In this paper, we study the problem
of verifying these properties for some well-known classes of infinite state
systems. We show that all the properties are undecidable for each of
these classes of systems.
pdf