Verification of Information Flow Properties under Rational Observation

Beatrice Berard, John Mullins

Abstract


Information flow properties express the capability for an agent to infer information about secret behaviours of a partially observable system. In a language-theoretic setting, where the system behaviour is described by a language, we define the class of rational information flow properties (RIFP), where observers are modeled by finite transducers, acting on languages in a given family L. This leads to a general decidability criterion for the verification problem of RIFPs on L, implying PSPACE-completeness for this problem on regular languages. We show that most trace-based information flow properties studied up to now are RIFPs, including those related to selective declassification and conditional anonymity. As a consequence, we retrieve several existing decidability results that were obtained by ad-hoc proofs.


Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.70.979

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.70.979.965

Hosted By Universit├Ątsbibliothek TU Berlin.