Verification of Information Flow Properties  under Rational Observation


Electronic Communications of the EASST
Volume 70 (2014)

Proceedings of the
14th International Workshop on

Automated Verification of Critical Systems (AVoCS 2014)

Verification of Information Flow Properties
under Rational Observation

Béatrice Bérard and John Mullins

15 pages

Guest Editors: Marieke Huisman, Jaco van de Pol
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

Verification of Information Flow Properties
under Rational Observation

Béatrice Bérard1∗ and John Mullins2†‡

1Beatrice.Berard@lip6.fr
Sorbonne Universités, UPMC Univ Paris 06, UMR 7606, LIP6, F-75005 Paris, France

CNRS, UMR 7606, LIP6, F-75005 Paris, France

2john.mullins@polymtl.ca
École Polytechnique de Montréal

Campus of the Université de Montréal, Montreal (Quebec), Canada.

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 mod-
eled 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.

Keywords: Information flow, Security predicates, Opacity, Declassification, Con-
ditional anonymity, Rational transducers, Formal verification.

1 Introduction

Motivations. Generic models for information flow properties aim at expressing, in a uniform
setting, the various capabilities of observers to infer information from partially observable sys-
tems. These models provide a description of the system behaviour, a parametric description
of the observation by the environment and the secret parts of the system, and a security cri-
terion. A security property is an instantiation of such a model, with the goal of avoiding a
particular information flow. Generic models have been thoroughly investigated, for instance
in [Man00, FG01, BKMR08]. They propose various classifications and comparisons of se-
curity properties, either for transition systems or directly for traces. In the case of transition
systems [FG01, BKMR08], the branching structure permits to express security properties as

∗ This author is supported by a grant from Coopération France-Québec, Service Coopération et Action Culturelle
2012/26/SCAC.
† This author is supported by the NSERC Discovery Individual grant No. 13321 (Government of Canada), the
FQRNT Team grant No. 167440 (Quebec’s Government) and the CFQCU France-Quebec Cooperative grant No.
167671 (Quebec’s Government).
‡ This work has been partially done while this author was visiting the LIP6, Université Pierre & Marie Curie.

1 / 15 Volume 70 (2014)

mailto:Beatrice.Berard@lip6.fr
mailto:john.mullins@polymtl.ca


Verification of Information Flow Properties under Rational Observation

equivalences like weak or strong (bi-)simulations. For trace-based models, properties are stated
as relations between languages, also called security predicates in [Man00].

In addition to classification, an important question about security properties concern their
verification: given a system S and a security property P, does S satisfy P ? Since [FG01], much
attention has been given to such questions for various classes of systems (or their sets of traces)
and security properties [BKMR08, DHRS11, CDM12, DFK+12, BD12, MY14, CFK+14]. This
is the problem we consider in this work, for a subclass of trace-based information flow properties.

Contributions. We first introduce the class of Rational Information Flow Properties (RIFP),
in a language-theoretic setting. In this class, observations are modeled by rational transducers,
called here rational observers. For a language L in some family of languages L , an RIFP is
then defined as an inclusion relation L1 ⊆ L2, where L1 and L2 are obtained from L by induc-
tively applying rational observers, unions and intersections. This mechanism produces the set of
properties RIF(L ), and a generic decidability result can be stated for the verification problem
of these properties. In the particular case of the family Reg of regular languages, generated by
finite automata (also called labelled transition systems), we obtain a PSPACE-complete verifica-
tion problem for the class RIF(Reg). We then proceed to show that this result subsumes most
existing decidability results for security properties on regular languages, thus establishing the
pertinency of our model. This involves expressing properties in our formalism by designing suit-
able rational observers. We first consider the particular case where observations are functions
and we show that opacity properties with regular secrets are RIFPs. To illustrate the expres-
siveness of RIFPs, we introduce a subclass of functional rational observers that we call rational
Orwellian observers and show that several properties including intransitive non-interference and
selective intransitive non-interference for a language L ∈ L are in RIF(L ). We also reduce their
verification to the verification of opacity w.r.t. Orwellian observers. These observers are more
powerful than those considered so far in literature as they model not only observers constrained
to a fixed a priori interpretation of unobservable events (static observers) or even to observers
able to base this interpretation on observation of previous events (dynamic observers), but also
able to re-interpret past unobservable events on the base of subsequent observation. We finally
consider general observers and we show that all Mantel’s Basic Security Predicates (BSPs) are
RIFPs. Finally, we illustrate the applicability of our framework by providing the first formal
specification for conditional anonymity guaranteeing anonymity of agents unless revocation (for
instance, the identity of an agent discovered to be dishonest can be revealed).

Outline. The rest of the paper is organized as follows. Rational Information flow proper-
ties are defined in Section 2, with the associated decidability results. RIFPs w.r.t. rational
observation functions are investigated in Section 3: rational opacity properties as RIFP are
presented in Subsection 3.1, Orwellian observers in Subsection 3.2 and their application to in-
transitive non-interference and selective intransitive non-interference in Subsection 3.3. RIFPs
w.r.t. general rational observation relations are investigated in Section 4: BSPs as RIFPs are
presented in Subsection 4.1 and an application of general rational observation relation to condi-
tional anonymity is presented in Subsection 4.2. In Section 5, we discuss related work and we
conclude in Section 6.

Proc. AVoCS 2014 2 / 15



ECEASST

2 Rational Information flow properties

We briefly recall the notions of finite automata and finite transducers before defining rational
information flow properties.

2.1 Automata and transducers

The set of natural numbers is denoted by N and the set of words over a finite alphabet A is denoted
by A∗, with ε for the empty word and A+ = A∗ \{ε}. The length of a word w is written |w| and
for any a ∈ A, |w|a is the number of occurrences of a in w. A language is a subset of A

∗.

Finite Labelled Transition Systems. A finite labelled transition system (LTS or automaton for
short), over a finite set Lab of labels, is a tuple A = 〈Q,I,∆,F〉, where Q is a finite set of states,
I ⊆ Q is the subset of initial states, ∆ ⊆ Q × Lab × Q is a finite transition relation and F ⊆ Q is a
set of final states. Note that Lab can be an alphabet but also a (subset of a) monoid.

Given two states q,q′ ∈ Q, a path from q to q′ with label u, written as q
u

−→q′, is a sequence of
transitions q

a1
−→q1, q1

a2
−→q2,··· , qn−1

an
−→q′, with ai ∈ Lab and qi ∈ Q, for 1 ≤ i ≤ n − 1, such

that u = a1 ···an. The path is accepting if q ∈ I and q
′ ∈ F , and the language of A , denoted by

L(A ), is the set of labels of accepting paths. A regular language over an alphabet A is a subset
of A∗ accepted by a finite LTS over the set of labels A.

Finite Transducers. A finite transducer (or transducer for short) is a finite LTS T with set of
labels Lab ⊆ A∗ × B∗ for two alphabets A and B. A label (u,v) ∈ A∗ × B∗ is also written as u|v.
The subset L(T ) of A∗ × B∗ is a rational relation [Sak09] from A∗ to B∗. The transducer T is
said to realize the relation L(T ) (see Figure 1 for basic examples of transducers).

Given a rational relation R, we write R(u) = {v ∈ B∗ | (u,v) ∈ R} for the image of u ∈ A∗,
R−1(v) = {u ∈ A∗ | (u,v) ∈ R} for the inverse image of v ∈ B∗, possibly extended to subsets of
A∗ or B∗ respectively, and dom(R) = {u ∈ A∗ | ∃v ∈ B∗,(u,v) ∈ R} for the domain of R. The
relation R is complete if dom(R) = A∗, it is a function if for each u ∈ dom(R), R(u) contains a
single element v ∈ B∗.

For a subset P of A∗, the identity relation {(u,u) | u ∈ P} on A∗ × A∗ is denoted by IdP. The
composition of rational relations R1 on A

∗ × B∗ and R2 on B
∗ × C∗, denoted by R1R2 (from

left to right) or by R2 ◦ R1 (from right to left), is the rational relation on A
∗ × C∗ defined by

{(u,w) | ∃v (u,v) ∈ R1 ∧(v,w) ∈ R2} ([EM65]). The family of regular languages is closed under
rational relations [Ber79].

2.2 Rational observers

Information flow properties are related to what an agent can learn from a given system. In
a language-based setting, the behavior of the system is described by a language L over some
alphabet A, and some function O associates with each w ∈ L its observation O(w) visible by the
agent. We generalize the notion of observation by defining O as a relation on A∗ × B∗ for some
alphabet B, but we restrict O to be a rational relation.

3 / 15 Volume 70 (2014)



Verification of Information Flow Properties under Rational Observation

Definition 1 (Rational observer) A rational observer is a rational relation O on A∗ ×B∗, for two
alphabets A and B. The observation of a word w ∈ A∗ is the set O(w) = {w′ ∈ B∗ | (w,w′) ∈ O}
and for any language L ⊆ dom(O), the observation of L is O(L) = ∪w∈LO(w).

As pointed out in [DHRS11], a large amount of information flow properties of a language L are
expressed as relations of the form op1(L) ⊆ op2(L), for some language theoretic operations op1
and op2. Actually, we show below that op1 and op2 are often rational relations corresponding to
some specific observations of L. Also, we define the class of rational information flow properties
as those using rational observers, and positive boolean operations:

Definition 2 (Rational information flow property) A rational information flow property (RIFP)
for a language L is any relation of the form L1 ⊆ L2, where L1 and L2 are languages given by the
grammar:

L1,L2 ::= L | O(L1) | L1 ∪ L2 | L1 ∩ L2

where O is a rational observer.

Hence, from Def. 1, we recover information flow properties of L of the form O1(L) ⊆ O2(L)
for two rational observers, as a particular case. However it has to be noted that Def. 1 does
not reduce to these inclusions since rational relations are not closed under intersection [Ber79].
Given a family of languages L , we define RIF(L ) as the set of RIFPs for languages in L . We
immediately have the following general result:

Proposition 1 Let L be a family of languages closed under union, intersection, and rational
transductions, such that the relation ⊆ is decidable in L . Then any property in RIF(L ) is
decidable.

In particular, the class Reg of regular languages satisfies the conditions above and it has a
PSPACE-complete inclusion problem. We then have:

Corollary 1 The problem of deciding a property in RIF(Reg) is PSPACE-complete.

Proof. It follows from the remark above that the problem is in PSPACE. For PSPACE-hardness,
recall that for a language K, the relation OK defined by OK(w) = {w}∩ K is a rational observer
if (and only if) K is a regular language [Sak09]. Let L1 and L2 be two regular languages, and
let OL1 , OL2 be the two corresponding relations, then for L = A

∗, we have L1 ⊆ L2 if and only if
OL1(L) ⊆ OL2 (L).

This corollary subsumes many existing decidability results for IF properties. The rest of the
paper is devoted to establish reductions of some of these to the RIF(Reg) verification problem.

3 RIF properties with rational functions

In this section, we consider the generic model of opacity introduced in [BKMR08] for transition
systems. Opacity is parametrized with observation functions, that are classified in [BKMR08]

Proc. AVoCS 2014 4 / 15



ECEASST

as static, dynamic or Orwellian to reflect the computational power of the observer. In a static
observation, actions are always interpreted in the same way. It is defined as a morphism and
hence, it is a rational function. A particular case of static observer is the projection πB from
A∗ into B∗ for a subalphabet B of A, so that πB(a) = a if a ∈ B and πB(a) = ε otherwise. In a
dynamic observation function, interpretation of the current action depends on the sequence of
actions observed so far and hence, it is also a rational function.

Example 1 In Figure 1 (where all states are final states), the left hand side depicts a transducer
realizing the projection from {a,b}∗ onto {b}∗ while the right hand side depicts a transducer
realizing the following dynamic observation function (translated from [CDM12]): The first oc-
currence of the first action is observed, then nothing is observed until the first occurrence of
the second action (b if the trace begins with a and a otherwise) and everything is observed in
clear as soon as this second action occurs that is, O(aa∗bu) = abu and O(bb∗au) = bau for any
u ∈ {a,b}∗.

0

a|ε,b|b
0 1 3

2

a|a

b|b

b|ε

a|a

a|ε

b|b

a|a,b|b

Figure 1: Examples of transducers realizing basic observation functions

In Orwellian observation functions, the current observation depends not only on the prefix of
actions observed so far but also on the complete trace. It reflects the capability of the observer
to use subsequent knowledge to re-interpret past actions. In the rest of this section we will study
opacity w.r.t. rational Orwellian observers.

3.1 Opacity w.r.t. rational functions

In its original setting, opacity is related to a language L ⊆ A∗ modelling the behaviour of a system,
a function O from A∗ to B∗ and in addition, a predicate ϕ given as a subset of L, describing a
secret. Two words w and w′ of L are observationally equivalent for O if O(w) = O(w′). The
observation class of w in L is the set [w]L

O
= {w′ ∈ L | O(w) = O(w′)} = L ∩ O−1(O(w)).

The secret ϕ is opaque in L for O if for any word in ϕ , there is another word in L \ ϕ such that
w and w′ are observationally equivalent. Hence, ϕ is opaque if and only if O(ϕ) ⊆ O(L \ ϕ),
which we take as definition when O is a rational function:

Definition 3 (Rational Opacity) Given a language L ⊆ A∗, a language ϕ ⊆ L and a rational
function O, ϕ is rationally opaque in L for O if O(ϕ) ⊆ O(L \ ϕ).

The information flow deduced by an observer when the system is not opaque is captured by

5 / 15 Volume 70 (2014)



Verification of Information Flow Properties under Rational Observation

the notion of secret disclosure: A word w ∈ L discloses the secret S w.r.t. O if [w]L
O
⊆ ϕ . We

have:

Proposition 2 Rational opacity properties on languages in some family L for regular secrets
belong to RIF(L ).

Proof. As already seen in the proof of Corollary 1, intersection with a regular set K is a ra-
tional observation OK . Since the secret ϕ is regular, opacity of ϕ in L for O is equivalent to
O(Oϕ (L)) ⊆ O(O¬ϕ (L)).

Non-interference and weak and strong anonymity have been shown to reduce to opacity w.r.t.
suitable observers (see [BKMR08]). In [CDM12], PSPACE-hardness is established for opacity
of regular secrets for regular languages w.r.t. static and dynamic observers.

3.2 Rational Orwellian observers

In the sequel, we denote the disjoint union by ⊎. In our context, Orwellian observation functions
from [BKMR08] are realized by rational Orwellian observers:

Definition 4 (Rational Orwellian Observer) A rational Orwellian observer is a rational func-
tion, given as a disjoint union of functions: O = ⊎1≤i≤nOi, where the domains {dom(Oi),1 ≤
i ≤ n} form a partition of A∗. The partial functions Oi are called views.

Note that O is a function because the domains of the views are disjoint. We simply call
these functions Orwellian observers for short, since there is no ambiguity in our context. The
terminology Orwellian comes from the ability of the observer to somehow see in the future, as
illustrated in the following example.

Example 2 (A simple example) The function O = Oa ⊎ Ob ⊎ Oε is an Orwellian observer on
{a,b} realized by the transducer depicted in Figure 2. The function is defined by O(ε) = ε and:

O(w) =

{

π{b}(w) if the last letter of w is a
π{a}(w) if the last letter of w is b.

Hence, the observer interpretation of the current event depends on the last event of the trace. If it
is a then O interprets the trace as its projection over {b} and the other way around, if it is b then
it interprets the trace as its projection over {a}.

p0Oa : p1 q0Ob : q1 r0Oε :
a|ε

a|ε, b|b a|a, b|ε

b|ε

Figure 2: The Orwellian observer O = Oa ⊎ Ob ⊎ Oε .

Proc. AVoCS 2014 6 / 15



ECEASST

Despite its observational power, this observer is not able to deduce whether the first event in
the trace in L = (a + b)(a∗ + b∗)(a + b) is an a. Indeed, let ϕ = a(a∗ + b∗)(a + b) be the secret,
corresponding to the set of traces in L with a as the first event. Then ϕ is opaque w.r.t. O in L.
To see this, if a secret trace w is observed, examine what O can deduce from this observation.

• If w ends with an a then O(w) = bn for some n ≥ 0 but bna 6∈ ϕ is also observed by bn.

• If w ends with a b then O(w) = an for some n ≥ 0 but banb 6∈ ϕ is also observed by an.

Example 3 (Static and dynamic observers) Static and dynamic observations are of course spe-
cial cases of Orwellian observers, where O consists of a single complete view. Note that static
and dynamic observations preserve prefixes while it is not necessarily the case for Orwellian
observations (see examples 2 and 4).

Example 4 (Intransitive non-interference) Let A = V ⊎ C ⊎ D be a partition of the alphabet
into visible actions in V , confidential actions in C and declassification actions in D. When a
declassification action occurs in a word, the prefix is observed in clear. The corresponding ob-
servation function is called in [MY14] the projection on V unless D, and defined as a mapping
πV,D : A∗ → A∗ such that πV,D(ε) = ε and

πV,D(ua) =







ua if a ∈ D,
πV,D(u)a if a ∈ V,
πV,D(u) otherwise.

A language L satisfies intransitive non-interference (INI) if πV,D(L) ⊆ L. Again:

Proposition 3 The function πV,D is an Orwellian observer, hence INI for languages in L be-
longs to RIF(L ).

Proof. The function πV,D is a sum of two views: πV,D = Oε ⊎ OD, realized by the transducers
depicted in Figure 3.

p0Oε : q0OD : q1

v|v, v ∈ V
c|ε, c ∈ C a|a, a ∈ A

v|v, v ∈ V
c|ε, c ∈ C

d|d, d ∈ D

Figure 3: The Orwellian observer πV,D = Oε ⊎ OD.

It has been shown in [MY14] that a language L satisfies intransitive non-interference (INI) if
and only if ϕINI = {w ∈ L | πV,D(w) 6= w} is opaque in L w.r.t. the observer πV,D.

This can be generalized as follows, showing that many non-interference like properties reduce
to opacity w.r.t. Orwellian observers.

7 / 15 Volume 70 (2014)



Verification of Information Flow Properties under Rational Observation

Proposition 4 Let O be a rational idempotent function (i.e. O2 = O). Then O(L) ⊆ L if and
only if ϕO = {w ∈ L | O(w) 6= w} is opaque in L for O.

Proof. First assume that O(L) ⊆ L and let w ∈ ϕO . Then O(w) 6= w. For w′ = O(w), we have:
w′ ∈ L and O(w′) = O2(w) = O(w) = w′, hence w′ /∈ ϕO . Opacity of ϕO follows.
Conversely, assume that ϕO is opaque and let w be an element of L. If w ∈ ϕO , then there
exists w′ ∈ L \ ϕO such that O(w) = O(w′). Since w′ /∈ ϕO , O(w′) = w′, hence w′ = O(w) ∈ L.
Otherwise, w /∈ ϕO implies O(w) = w ∈ L. In all cases, O(w) ∈ L and O(L) ⊆ L.

Finally, we can state the following:

Proposition 5 Given an Orwellian observer O, deciding opacity of regular secrets w.r.t. O for
regular languages is PSPACE-complete.

Proof. Corollary 1 implies that the problem is in PSPACE. For the PSPACE-hardness, it suffices
to observe that dynamic or static observers are particular Orwellian observers for which the
problem is already PSPACE-hard.

In the next paragraph, we show that the observation function defined for selective declassifi-
cation is an Orwellian observer.

3.3 Selective declassification

Intransitive non-interference with selective declassification (INISD) generalizes INI by allowing
to each downgrading action to declassify only a subset of confidential actions. It has recently
been proposed in [BD12] for a class of Petri net languages (that does not include rational lan-
guages). To formalize INISD, the alphabet is partitioned into A = V ⊎ C ⊎ D as in example 4.
In addition, with each declassification action d ∈ D is associated a specific set C(d) ⊆ C of
confidential events, with the following meaning: An occurrence of d in a word w declassifies
all previous occurrences of actions from C(d), hence these actions are observable while other
confidential events in C are not.

Let Σ(D) = {σ ∈ D∗ | |w|d ≤ 1 for all d ∈ D} be the set of repetition-free sequences of down-
grading actions in D. With any σ = d1d2 ...dn ∈ Σ(D), we associate the sets:

Aσ = V ⊎C ⊎{d1,...,dn}

Wσ = A
∗
σ · d1 ·(Aσ \{d1})

∗ · d2 · ... · dn ·(Aσ \{d1,...,dn})
∗

Vσ,i = V ∪{d j, i + 1 ≤ j ≤ n}∪
n
⋃

j=i+1

C(d j), for every i ∈ {0,...,n}

with the convention Vσ,n = V , and the projections πσ,i : A∗ → V ∗σ,i for every i ∈ {0,...,n}.
For a given σ = d1 ... dn ∈ Σ(D), the set Wσ contains the words w in A∗ where the set of all

downgrading actions is precisely {d1,...,dn} and such that the last occurrence of di precedes the
last occurrence of di+1 for any 1 ≤ i ≤ n − 1. Note that the family of all these sets {Wσ , σ ∈ Σ}
form a partition of A∗. Besides, the projection πσ,i observes in clear any confidential event in
∪nj=i+1C(d j), in addition to the visible events in V and the declassifying events from σ .

Proc. AVoCS 2014 8 / 15



ECEASST

Now the property called INISD in [BD12] can be stated in our general context for a language
L as follows: For any σ ∈ Σ(D) and for any word w = w0d1w1 ... dnwn in L ∩Wσ , there exists a
word w′ = w′0d1w

′
1 ...dnw

′
n in L ∩Wσ such that for every i ∈ {0,...,n}, w

′
i ∈ V

∗
σ,i and πσ,i(wi) =

πσ,i(w′i). We have:

Proposition 6 The INISD property for languages in L belongs to RIF(L ).

Proof. We build an (idempotent) Orwellian observer OSD such that a language L satisfies INISD
if and only if OSD(L) ⊆ L. Let OSD =

⊎

σ∈Σ(D) Oσ , where the view Oε and a generic view Oσ for
some non empty σ = d1 ... dn ∈ Σ(D) are depicted in Figure 4.

p0Oε :

v|v, v ∈ V
c|ε, c ∈ C

q0Oσ : q1
d1

··· qn

v|v, v ∈ Vσ ,0
c|ε, c ∈ Aσ \Vσ ,0

v|v, v ∈ Vσ ,1
c|ε, c ∈ Aσ \Vσ ,1

v|v, v ∈ Vσ ,n
c|ε, c ∈ Aσ \Vσ ,n

d2 dn

Figure 4: Views of the observation OSD

Let w = w0d1w1 ... dnwn be a word in L ∩Wσ , the observation of w is

Oσ (w) = πσ,0(w0)d1πσ,1(w1)... dnπσ,1(wn).

Then L satisfies INISD if and only if Oσ (L ∩Wσ ) ⊆ L ∩Wσ for any σ ∈ Σ(D). Since the fam-
ily {Wσ , σ ∈ Σ} is a partition of A∗, the family {L ∩ Wσ , σ ∈ Σ} is a partition of L and the
result follows. Each view Oσ is idempotent and the partitionning also ensures that OSD itself is
idempotent. As a consequence, proposition 4 applies here.

Remark 1 Also note that a secret ϕ is opaque for a language L w.r.t. OSD if and only if for all
σ ∈ Σ(D), ϕ ∩ Wσ is opaque for L ∩ Wσ w.r.t. Oσ . Indeed, the result again holds because the
family {L ∩Wσ , σ ∈ Σ} is a partition of L: for all σ ∈ Σ(D), Oσ (Wσ ) ⊆ Wσ , we have that ϕ is
opaque for L w.r.t. OSD if and only if for all σ ∈ Σ(D),

Oσ (ϕ ∩Wσ ) ⊆ Oσ ((L \ ϕ)∩Wσ ) = Oσ ((L ∩Wσ )\(ϕ ∩Wσ )).

Like before, for regular languages, decidability of INISD as well as opacity under OSD, are
consequences of corollary 1 and proposition 6 above. This property is studied in [BD12] for the
prefix languages of (unbounded) labelled Petri nets. This family is closed under intersection,
inverse morphisms and alphabetical morphisms, hence it is also closed under rational transduc-
tions (by Nivat’s theorem [Ber79]), but it has an undecidable inclusion problem. A very nice
proof is given in [BD12] for the decidability of the INISD property: it relies on the decidability
of the inclusion problem for the particular case of free nets (where all transitions have distinct
labels, different from ε ).

The following example (inspired from [BD12]) tries to explain the essence of selective declas-
sification.

9 / 15 Volume 70 (2014)



Verification of Information Flow Properties under Rational Observation

pi3

pi2Goat(i) : pi4

pi1

d3

d1l2
d2

l3

l1

q j1

q j0Raptor( j) :

q j3

q j2

h1

d1 h2

d2

h3d3

r10

r11Gate(1) :

r20

r21

Gate(2) : r30

r31Gate(3) :

h1h3

l1,h1

h2h1

l2,h2

h3h2

l3,h3

Figure 5: The dining Raptors

Example 5 (The Dining Raptors) A circuit followed by a herd of goats is divided in three
sections. Each section is guarded by a gate. When gate i is open, goats can move clockwise
from section i to section i + 1 (mod 3). The center of the circuit is occupied by a den of raptors.
When gate i + 1 (mod 3) is open, a raptor can leave the den and hide around gate i after opening
it and closing gate i + 1 (mod 3) to increase chance of success. When a raptor is embushed near
a section and there is a goat in this section, the raptor can catch prey and come back to the den.

This scenario is modelled with the transition system

DR(n,m) =
n

∏
i=1

Goat(i)×
m

∏
j=1

Raptor( j)×
3

∏
k=1

Gate(k)

obtained by synchronizing the components depicted in Figure 5 on the complementary actions.
Goats’ move from gate i to gate i+1 (mod 3) is modelled with visible action l1, raptors’ embush
action at section i, with the confidential action hi and the raptors’ catch action in section i, by the
declassification action di. Opacity of ϕDR w.r.t. OSD in L(DR(m,n)) where

ϕDR = {u ∈ L(DR(m,n)) | OSD(u) 6= u}

comes down to absence of information the goats can get from environment about the moment
they will be caught until this happens. Hence there is no strategy that they can oppose to the
raptors. In the case where initially goats are in section 2 and gates 1 and 3 are opened, as shown
in Figure 5, L(DR(n,m)) is not opaque w.r.t. ϕDR since l3l1h2l2 reveals the secret (h2l3l1l2,
l3h2l1l2 and l3l1h2l2 are the only traces observed as l3l1l2) and this, for any number of raptors
and goats. This example may be of course modified in various ways as follows. If all three gates
are open, goat 1 never realizes she dies since l3l1h1d1 does not reveals the secret but following
this, as gate 2 is now close, goat 2 after l3l1l2 will know that a raptor is embushed at gate 2
since l3l1h1d1l3l1h2l2 reveals the secret. If only gate 3 is open, l3h2d2h1l1 reveals to the herd,

Proc. AVoCS 2014 10 / 15



ECEASST

that one of them is now trapped in section 2. Finally, if we dismantle all three gates, the only
synchronizing actions are now the declassification ones and ϕDR becomes opaque w.r.t. OSD.

4 RIF properties with full rational relations

In this section, we first revisit Basic Security Predicates (BSP) presented in [Man00, Man01] and
used as building blocks of the Mantel’s generic security model. In the second part, we investigate
anonymity properties.

4.1 Basic Security Predicates

For BSPs, the alphabet A is partitioned into A = V ⊎C ⊎ N, where V is the set of visible events,
C is the set of confidential events and N is a set of internal events. Informally, a BSP for a given
language L over A, is an implication stating that for any word w in L satisfying some restriction
condition, there exists a word w′ also in L which is observationnally equivalent to w and which
fulfills some closure condition describing the way w′ is obtained from w by adding or removing
some confidential events. The conditions are sometimes parametrized by an additional set X ⊆ A
of so-called admissible events. We prove:

Proposition 7 Any BSP over languages in some family L belongs to RIF(L ).

Due to lack of space, the proof is omitted (but will be found in a long version). It mainly
consists in exhibiting rational observers together with an inclusion relation such that a language
L satisfies a given BSP if and only if this relation holds.

In [DHRS11], the decidability results for all 14 BSPs on regular languages are obtained by
ad-hoc proofs establishing that regularity is preserved by the various op1, op2 operations. These
include auxiliary functions on languages (like mark, unmark, etc.) that are unnecessary in our
setting. Actually, we show how decidability of BSPs is an immediate consequence of corollary 1
and proposition 7 above. The more difficult case of pushdown systems (generating prefix-closed
context-free languages) is also investigated in [DHRS11]: Although context-free languages are
closed under rational transductions, they are not closed under intersection and the inclusion prob-
lem is undecidable for context-free languages [Ber79]. Finally, several undecidability results are
presented in [DHRS11]. In particular, they exhibit an information flow property called Weak
Non Inference (WNI) shown to be undecidable even for regular languages. Hence, WNI cannot
be expressed neither as a conjunction of BSPs, and as matter of fact, neither as an RIFP. Also, in
order to get decidable cases, authors had to restrict the languages and/or the class of properties
like reducing the size of the alphabet (card(V ) ≤ 1 and card(C) ≤ 1).

4.2 Conditional anonymity

Conditional or escrowed anonymity is concerned with the revocation of the guarantee, under
well-defined conditions, to which an agent agrees, that his identification w.r.t. a particular (non-
secret) action will remain secret and in such case, conditional anonymity guarantees the un-
linkability of revoked users in order to guarantee anonymity to “legitimate” agents [DS08]. As

11 / 15 Volume 70 (2014)



Verification of Information Flow Properties under Rational Observation

suggested in [BKMR08], Orwellian observation can be used to model conditional anonymity
but [BKMR08] contains neither a definition of such a property, nor any investigation of its de-
cidability. We close the gap in this paper.

The alphabet is partitioned into A = V ⊎ P ⊎ R where P is the set of actions performed by
anonymous participants, V is the set of visible actions and R is the set of anonymity revocation
actions, such that for each participant corresponds a dedicated revocation action r allowing to
reveal the subset P(r) of all its anonymous actions. Hence the sets P(r) are mutually disjoint.

In [SS96], definitions of weak and strong anonymity are given in the setting of the process
algebra CSP. A language is strongly anonymous (SA) if it is stable under any “perturbation” of
anonymous actions where an anonymous action in P can be replaced by any other element of
P. It is weakly anonymous (WA) if it is stable under any permutation on the set of anonymous
actions. For a finite set Z, we denote by SZ the set of all permutations on Z. We first have:

Proposition 8 Weak and strong anonymity on languages in L belong to RIF(L ).

Proof. For these two properties, the subalphabet R of revocation actions is empty. We express
the properties in our language-based setting, similarly as in [BKMR08].

A language L is strongly anonymous w.r.t. P if OPSA(L) ⊆ L where O
P
SA is the mapping defined

on A = V ⊎ P by: OPSA(a) = P if a ∈ P and O
P
SA(a) = {a} otherwise. Such mappings (called

rational substitutions in [Ber79]) are well known to be rational relations, hence the result follows.

A language L is weakly anonymous w.r.t. P if OPWA(L) ⊆ L where O
P
WA =

⊎

α∈SP Oα and Oα is
the morphism which applies the permutation α on letters of P:

Oα(a) = α(a) if a ∈ P and Oα (a) = a otherwise.

With any σ ⊆ R, we associate:

• Wσ = {w ∈ A
∗ | πR(w) ∈ σ ∗}, the set of words w in A∗ where the set of revocation actions

appearing in w is σ ,

• Pσ = P \
⊎

r∈σ P(r), the set of actions of legitimate agents.

We denote by 2R the powerset of R and remark that here also, the sets Wσ for σ ∈ 2R form
a partition of A∗. In order to provide at any moment strong (weak) anonymization to legitimate
agents, we define conditional anonymity as follows:

Definition 5 With the notations above, a language L on V ⊎ P ⊎ R is:

• conditionally weakly anonymous (CWA) if for any σ ⊆ R, L ∩Wσ is WA w.r.t. Pσ ,

• conditionally strongly anonymous (CSA) if for any σ ⊆ R, L ∩Wσ is SA w.r.t. Pσ .

Now we have:

Proposition 9 Weak and strong conditional anonymity on languages in L belong to RIF(L ).

Proof. We build rational observers, with a view-like component for each possible subset σ of re-
voked users, corresponding to OSA (resp. OWA) localized to Wσ , i.e. revocation actions are those
in σ , anonymous actions are restricted to Pσ and visible actions are extended to V ⊎

⊎

r∈σ P(r):

Proc. AVoCS 2014 12 / 15



ECEASST

OCSA =
⊎

σ∈2R
O

Pσ
SA and OCWA =

⊎

σ∈2R
O

Pσ
WA

Then L is conditionally strongly anonymous (CSA) if and only if OCSA(L) ⊆ L and L is condi-
tionally weakly anonymous (CWA) if and only if OCWA(L) ⊆ L, which yields the result.

5 Related works.

Along the lines, important connections between RIFPs and information flow properties have
been established, hence in this section, we will focus on extending the picture.

Algorithms for verifying opacity in Discrete Event Systems w.r.t. projections are presented
together with applications in [BBB+07, TK09, SH11, Lin11]. In [BBB+07], the authors consider
a concurrent version of opacity and show that it is decidable for regular systems and secrets.
In [TK09], the authors define what they called secrecy and provide algorithms for verifying
this property. A system property satisfies secrecy if the property and its negation are state-based
opaque. In [Lin11] the author provides an algorithm for verifying state-based opacity (called
strong opacity) and shows how opacity can be instantiated to important security properties in
computer systems and communication protocols, namely anonymity and secrecy. In [SH11], the
authors define the notion of K-step opacity where the system remains state-based opaque in any
step up to depth-k observations that is, any observation disclosing the secret has a length greater
than k. Two methods are proposed for verifying K-step opacity. All these verification problems
can be uniformly reduced to the RIFP verification problem.

In [FG01], the authors provide decision procedures for a large class of trace-based secu-
rity properties that can all be reduced to the RIFP verification problem for regular languages.
In [MZ07], decision procedures are given for trace-based properties like non-deducibility, gener-
alized non-interference and forward correctability. The PSPACE-completeness results for these
procedures can be reduced to our results.

Concerning intransitive information flow (IIF), non-interference (NI) and intransitive non-
interference (INI) for deterministic Mealy machines have been defined in [Rus92]. In [Pin95],
an algorithm is provided for INI. A formulation of INI in the context of non-deterministic LTSs is
given in [Mul00], in the form of a property called admissible interference (AI), which is verified
by reduction to a stronger version of NI. This property, called strong non-deterministic non-
interference (SNNI) in [FG01], is applied to N finite transition systems where N is the number
of downgrading transitions of the original system. This problem was also reduced to the opacity
verification problem w.r.t. Orwellian projections in [MY14]. In [BPR04], various notions of
trace-based INI declassification properties are considered and compared. In contrast, our generic
model is instantiable to a much larger class of IIF properties.

In [vdM07], the author has argued that Rushby’s definition of security for intransitive policies
suffers from some flaw, and proposed some stronger variations. The considered flaw relies to the
fact that, if u ∈ Wd1 and v ∈ Wd2 , that is u (resp. v) declassifies only h1 ∈ H(d1) (resp. h2 ∈ H(d2)),
then the shuffle of u and v resulting of their concurrent interaction will reveal the order in which
h1 and h2 have been executed. The proof techniques used in this paper for deciding the RIFP

13 / 15 Volume 70 (2014)



Verification of Information Flow Properties under Rational Observation

verification problem relies on their end-to-end execution semantics and hence does not address
this problem.

6 Conclusion

We introduce a language-theoretic model for trace-based information flow properties, the RIFPs
where observers are modelled by rational transducers. Given a family L of languages, our
model provides a generic decidability result to the RIF(L ) verification problem: Given L ∈ L
and a security property P in RIF(L ), does L satisfy P? When L is the class Reg of regular
languages, the problem is shown PSPACE-complete. This result subsumes most decidability
results for finite systems. In order to prove that, we have shown that opacity properties and
Mantel’s BSPs, two major generic models for trace-based IF properties, are RIFPs. We illustrated
the expressiveness of our model by showing that the verification problem of INI and INISD
can be reduced to the verification problem of opacity w.r.t. a subclass of rational observers
called rational Orwellian observers. Finally we illustrated the applicability of our framework by
providing the first formal specification of conditional anonymity.

Bibliography

[BBB+07] E. Badouel, M. A. Bednarczyk, A. M. Borzyszkowski, B. Caillaud, P. Darondeau.
Concurrent Secrets. Discrete Event Dynamic Systems 17(4):425–446, 2007.

[BD12] E. Best, P. Darondeau. Deciding Selective Declassification of Petri Nets. In Proc. of
1st Conf. on Princples of Security and Trust (POST 2012), LNCS 7215, pp. 290–
308. Springer, 2012.

[Ber79] J. Berstel. Transductions and context-free languages. Teubner, 1979.

[BKMR08] J. Bryans, M. Koutny, L. Mazaré, P. Y. A. Ryan. Opacity generalised to transition
systems. Int. J. Inf. Sec. 7(6):421–435, 2008.

[BPR04] A. Bossi, C. Piazza, S. Rossi. Modelling Downgrading in Information Flow Secu-
rity. In Proc. of CSFW’04, pp. 187–201. IEEE Computer Society Press, 2004.

[CDM12] F. Cassez, J. Dubreil, H. Marchand. Synthesis of opaque systems with static and
dynamic masks. Formal Methods in System Design 40(1):88–115, 2012.

[CFK+14] M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, C. Sánchez.
Temporal Logics for Hyperproperties. In Proc. of POST 2014. pp. 265–284. 2014.

[DFK+12] R. Dimitrova, B. Finkbeiner, M. Kovács, M. N. Rabe, H. Seidl. Model Checking
Information Flow in Reactive Systems. In Proc. of VMCAI 2012, pp. 169–185.
Springer, 2012.

[DHRS11] D. D’Souza, R. Holla, K. R. Raghavendra, B. Sprick. Model-checking trace-based
information flow properties. Journal of Computer Security 19(1):101–138, 2011.

Proc. AVoCS 2014 14 / 15



ECEASST

[DS08] G. Danezis, L. Sassaman. How to Bypass Two Anonymity Revocation Schemes.
In Borisov and Goldberg (eds.), Privacy Enhancing Technologies. Lecture Notes in
Computer Science 5134, pp. 187–201. Springer, 2008.

[EM65] C. C. Elgot, J. E. Mezei. On relations defined by generalized finite automata. IBM
Journal Res. Develop. 9:47–68, 1965.

[FG01] R. Focardi, R. Gorrieri. Classification of Security Properties (Part I: Information
Flow). In Foundations of Security Analysis and Design. LNCS 2171, pp. 331–396.
Springer, 2001.

[Lin11] F. Lin. Opacity of discrete event systems and its applications. Automatica
47(3):496–503, 2011.

[Man00] H. Mantel. Possibilistic Definitions of Security - An Assembly Kit. In Proceedings
of CSFW’00, pp. 185–199. IEEE Computer Society, 2000.

[Man01] H. Mantel. Information Flow Control and Applications - Bridging a Gap. In Oliveira
and Zave (eds.), Proc. of FME 2001. LNCS 2021, pp. 153–172. Springer, 2001.

[vdM07] R. van der Meyden. What, Indeed, Is Intransitive Noninterference? In Biskup and
Lopez (eds.), ESORICS. LNCS 4734, pp. 235–250. Springer, 2007.

[Mul00] J. Mullins. Non-Deterministic Admissible Interference. Journal of Universal Com-
puter Science 6(11):1054–1070, 2000.

[MY14] J. Mullins, M. Yeddes. Opacity with Orwellian Observers and Intransitive Non-
interference. In 12th IFAC - IEEE International Workshop on Discrete Event Sys-
tems (WODES’14). Pp. 344–349. 2014.

[MZ07] R. van der Meyden, C. Zhang. Algorithmic Verification of Noninterference Proper-
ties. Electr. Notes Theor. Comput. Sci. 168:61–75, 2007.

[Pin95] S. Pinsky. Absorbing covers and intransitive non-interference. In Proceedings of
the 1995 IEEE Symposium on Security and Privacy. SP ’95, pp. 102–113. IEEE
Computer Society, Washington, DC, USA, 1995.

[Rus92] J. Rushby. Noninterference, transitivity and channel-control security policies. Tech-
nical report CSL-92-02, SRI International, Menlo Park CA, USA, Dec. 1992.

[Sak09] J. Sakarovitch. Elements of automata theory. Cambridge University Press, 2009.

[SH11] A. Saboori, C. N. Hadjicostis. Verification of K-Step Opacity and Analysis of Its
Complexity. IEEE T. Automation Science and Engineering 8(3):549–559, 2011.

[SS96] S. Schneider, A. Sidiropoulos. CSP and anonymity. In In European Symposium on
Research in Computer Security. Pp. 198–218. Springer-Verlag, 1996.

[TK09] S. Takai, R. Kumar. Verification and synthesis for secrecy in discrete-event systems.
In Proceedings of ACC’09, pp. 4741–4746. IEEE Press, Piscataway, NJ, USA, 2009.

15 / 15 Volume 70 (2014)


	Introduction
	Rational Information flow properties
	Automata and transducers
	Rational observers

	RIF properties with rational functions
	Opacity w.r.t. rational functions
	Rational Orwellian observers
	Selective declassification

	RIF properties with full rational relations
	Basic Security Predicates
	Conditional anonymity

	Related works.
	Conclusion