Leakage and Protocol Composition in a Game-Theoretic Perspective
Mário S. Alvim Konstantinos Chatzikokolakis Yusuke Kawamoto Catuscia Palamidessi


Plasma ramps caused by outflow in gas-filled capillaries
    [
    December 30, 2023
========================================================




In the inference attacks studied in Quantitative Information Flow (QIF),
the adversary typically tries 
to interfere with the system in the attempt 
to increase its leakage of secret information. 
The defender, on the other hand, 
typically tries 
to decrease leakage by introducing some controlled noise.
This noise introduction can be modeled as a type of protocol composition, i.e., 
a probabilistic choice among different protocols, and its effect on
the amount of leakage depends heavily on whether or not this choice is 
visible to the adversary.
In this work we consider operators for modeling visible and
invisible choice in protocol composition, and we study 
their algebraic properties.
We then formalize the interplay between defender and adversary in a 
game-theoretic framework adapted to the specific issues of QIF, 
where the payoff is information leakage. 
We consider various kinds of leakage games, depending on whether players 
act simultaneously or sequentially, and on whether or not the choices of the 
defender are visible to the adversary.
Finally, we establish a hierarchy of these games in terms
of their information leakage, and provide methods for finding 
optimal strategies (at the points of equilibrium) for both attacker and
defender in the various cases.
The full version of this paper can be found in <https://arxiv.org/abs/1803.10042>




§ INTRODUCTION


A fundamental problem in computer security is the leakage of sensitive information due to  
correlation of secret values with 
observables—i.e., any information accessible to the attacker, 
such as, for instance, the system's outputs or execution time.
The typical defense consists in reducing this correlation, 
which can be done in, essentially, two ways.
The first, applicable when the correspondence secret-observable is deterministic, 
consists in coarsening the equivalence classes of 
secrets that give rise to the same observables. 
This can be 
achieved with post-processing, i.e., sequentially composing the original system 
with a program that removes information from observables.
For example, a typical attack on encrypted web traffic consists on the analysis of the packets' 
length, and a typical defense consists in padding extra bits so to diminish the length variety 
<cit.>. 

The second kind of defense, on which we focus in this work, 
consists in adding controlled noise to the observables produced by
the system. 
This can be usually seen as a composition of different protocols via 
probabilistic choice.
[Differential privacy]
Consider a counting query f, namely a function that, applied to a dataset x, returns the number of individuals in x that satisfy a given property. A way to implement differential privacy <cit.> is to add geometrical noise to the result of f, so to obtain a probability distribution P on integers of the form P(z) = c   e^|z-f(x)|, where c is a normalization factor. The resulting mechanism can  be interpreted as a probabilistic choice on protocols of the form f(x), f(x) + 1, f(x) + 2, … , f(x) - 1, f(x)-2, …, where the probability assigned to 
 f(x) + n and to f(x)-n decreases exponentially with n.

[Dining cryptographers]
Consider two agents running the dining cryptographers protocol <cit.>, which consists in tossing a fair binary coin and then declaring 
the exclusive or ⊕ of their secret value x and the result of the coin.  The protocol can be thought as the fair probabilistic choice  of two protocols, one consisting simply of declaring x, and the other declaring x⊕ 1. 


Most of the work in the literature of quantitative information flow (QIF) considers passive attacks,
in which the adversary only observes the system. 
Notable exceptions are the works <cit.>, 
which consider attackers 
who interact with and influence the system, possibly in an adaptive way, with
the purpose of maximizing the leakage of information. 

[CRIME attack]
Compression Ratio Info-leak Made Easy (CRIME) <cit.> is a
security exploit against secret web cookies over connections using the HTTPS and SPDY protocols and  data compression. 
The idea is that the attacker can inject some content a in the communication of the secret x from the target site to the server. The server then compresses and  encrypts the data, including both a and x, and sends back the result. By observing the length of the result, the attacker can then infer information about x. 
To mitigate the leakage, one possible defense would consist in transmitting, along with x, also an encryption method f selected randomly from a set F. Again, the resulting protocol can be seen as a composition, using probabilistic choice, of the protocols in the set F.  


In all examples above the main use of the probabilistic choice is to  
obfuscate the relation between secrets and observables, 
thus reducing their correlation—and, hence, the information leakage. 
To achieve this goal, it is essential that the attacker never comes to 
know the result of the choice. 
In the CRIME example, however, if 
f and  a are chosen independently, then (in general) it is still better 
to choose f probabilistically, even if the adversary will come to know, afterwards, 
the choice of f. 
In fact, this is true also for the attacker: his best strategies (in general) are to chose a
according to some probability distribution. 
Indeed, suppose that F={f_1,f_2} are the defender's choices and 
A={a_1,a_2} are the attacker's, and that 
f_1(·,a_1) leaks more than f_1(·,a_2), while f_2(·,a_1) 
leaks less than f_2(·,a_2). 
This is a scenario like the matching pennies in game theory: 
if one player selects an action deterministically, the other player 
may exploit this choice and  get an advantage. 
For each player the optimal strategy is to play probabilistically, 
using a distribution that maximizes his own gain for all possible actions 
of the adversary. 
In zero-sum games, in which the gain of one player coincides 
with the loss of the other, the optimal pair of distributions always exists, 
and it is called saddle point. 
It also coincides with the Nash equilibrium, which is defined as the 
point in which neither of the two players gets any advantage in changing 
unilaterally his strategy. 

Motivated by these examples, this paper investigates the two kinds of choice, visible 
and hidden (to the attacker), in a game-theoretic setting. 
Looking at them as language operators, we study their algebraic properties, which will
help reason about their behavior in games. 
We consider zero-sum games, in which the gain (for the attacker) is represented by the leakage. 
While for visible choice it is appropriate to use the “classic” game-theoretic
framework, for hidden  choice we need to adopt the more general framework of the
information leakage games proposed in <cit.>. 
This happens because, in contrast with standard game theory, 
in games with hidden choice the utility of a mixed strategy is 
a convex function of the distribution on the defender's pure actions, 
rather than simply the expected value of their utilities.
We will consider both simultaneous games—in which each player chooses independently—and sequential games— in which one player chooses his action first. We aim at comparing all these situations, and at identifying the precise advantage of the hidden choice over the visible one. 

To measure leakage we use the well-known information-theoretic model. 
A central notion in this model is that of entropy, but here
we  use its converse, vulnerability, which 
represents  the magnitude of the threat. 
In order to derive results as general as possible, we  adopt 
the very comprehensive notion of vulnerability as any convex and continuous 
function, as  used in <cit.> and 
<cit.>. 
This notion has been shown <cit.> to subsume most 
 information measures, including 
Bayes vulnerability (aka min-vulnerability, aka (the converse of) 
Bayes risk) <cit.>, 
Shannon entropy <cit.>, 
guessing entropy <cit.>, and 
g-vulnerability <cit.>.



The main contributions of this paper are:


  * We present a general framework for reasoning about information leakage
in a game-theoretic setting, extending the notion of information leakage games proposed 
in <cit.> to both simultaneous and sequential games,
with either hidden or visible choice.



  * We present a rigorous compositional way, using visible and hidden choice operators, for representing adversary and defender's actions in information leakage games.
In particular, we study the algebraic properties of visible and hidden choice on channels,
and compare the two kinds of choice with respect to the capability of reducing 
leakage, in  presence of an adaptive attacker.


  * We provide a taxonomy of the various scenarios (simultaneous and sequential) 
showing when randomization is necessary, for either attacker or defender, 
to achieve optimality.
Although it is well-known in information flow that the defender's best strategy 
is usually randomized, only recently it has been shown that
when defender and adversary act simultaneously, the adversary's optimal strategy 
also requires randomization <cit.>.


  * We use our framework in a detailed case study of a password-checking protocol. 
The naive program, which checks the password bit by bit and stops when it finds a 
mismatch, is clearly very insecure, because it reveals at each attempt the maximum 
correct prefix. 
On the other hand,  if we continue checking until the end of the string (time padding), 
the program becomes very inefficient. 
We show that, by using probabilistic choice instead, 
we can obtain a good trade-off between security and efficiency.




  
*Plan of the paper.
The remaining of the paper is organized as follows.
In Section <ref> we review some basic notions of game theory and 
quantitative information flow. 
In Section <ref> we introduce our running example. 
In Section <ref> we define the visible and hidden choice operators 
and demonstrate their algebraic properties. 
In Section <ref>, the core of the paper, we examine
various scenarios for leakage games. 
In Section <ref> we show an application of our framework 
to a password checker. 
In Section <ref> we discuss related work and,
finally, in Section <ref> we conclude.   




§ PRELIMINARIES


In this section we review some basic notions from game theory
and quantitative information flow.
We use the following notation:
Given a set , we denote by  the 
set of all probability distributions over .
Given μ∈, its support
μ{ i ∈ : μ(i)>0 } 
is the set of its elements with positive probability.
We use iμ to indicate that a value 
i∈ is sampled from a distribution μ on .



 §.§ Basic concepts from game theory





  §.§.§ Two-player games



Two-player games are a model for reasoning about 
the behavior of two players.

In a game, each player has at its disposal a set of actions 
that he can perform, and he obtains some gain or loss depending on
the actions chosen by both  players.
Gains and  losses are defined using a real-valued payoff
function.
Each player is assumed to be rational, i.e.,  
his choice is driven by the attempt to maximize his own expected payoff.
We also assume that 
the set of possible actions and the payoff functions of both players 
are common knowledge.

In this paper we only consider finite games, in which the 
set of actions available to the players are finite.   
Next we introduce an important distinction between simultaneous 
and sequential games. 
In the following, we will call the two players defender 
and attacker.



  §.§.§ Simultaneous games



In a  simultaneous game, each player chooses his action without knowing 
the action chosen by the other.
The term “simultaneous” here does  not  mean that the players' actions 
are chosen at the same time, but only that they are chosen independently.
Formally, such a game  is defined as a tuple[Following the convention of security games, we set the first player to be the defender.] 
(, , , ), where
 is a nonempty set of defender's actions, 
 is a nonempty set of attacker's actions,
: ×→ is the defender's payoff function, and
: ×→ is the attacker's payoff function.

Each player may choose an action deterministically or probabilistically.
A pure strategy of the defender (resp. attacker) is a deterministic 
choice of an action, i.e., an element d∈ (resp. a∈). 
A pair (d, a) is called pure strategy profile, and 
(d, a), (d, a) represent the defender's and the attacker's 
payoffs, respectively. 

A mixed strategy of the defender (resp. attacker) is a probabilistic 
choice of an action, defined as a probability distribution 
δ∈ (resp. α∈).
A pair  (δ, α) is called  mixed strategy profile.
The defender's and the attacker's expected payoff functions for
mixed strategies are defined, respectively, as:
(δ,α)
d←δa←α(d, a)
=∑_d∈
 a∈δ(d) α(a) (d, a)
and 
(δ,α) 
d←δa←α(d, a)
= ∑_d∈
 a∈δ(d) α(a) (d, a).

A defender's mixed strategy δ∈ is a best response to 
an attacker's mixed strategy α∈ if 
(δ, α) = max_δ'∈(δ', α).
Symmetrically, α∈ is a best response to 
δ∈ if 
(δ, α) = max_α'∈(δ, α').
A mixed-strategy Nash equilibrium is a  profile (δ^*, α^*) such 
that δ^* is the best response to α^* and vice versa. 
This means that in a Nash equilibrium, no unilateral deviation by any single 
player provides better payoff to that player.
If δ^* and α^* are point distributions 
concentrated on some d^*∈ and a^*∈ respectively, 
then (δ^*, α^*) is a pure-strategy Nash equilibrium, 
and will be denoted by (d^*, a^*). 

While not all games have a pure strategy Nash equilibrium, every finite game 
has a mixed strategy Nash equilibrium.



  §.§.§ Sequential games


In a sequential game players may take turns in choosing their
actions.
In this paper, we only consider the case in which each player 
moves only once, in such a way that one of the players (the leader) 
chooses his action first, and commits to it, before the other player 
(the follower) makes his choice. 
The follower may have total knowledge of the choice made by the leader, or only partial. 
We refer to the two scenarios by the terms perfect and imperfect information, 
respectively.


We now give the precise definitions assuming that the leader is the defender.  
The case in which the leader is the attacker is similar. 

A defender-first sequential game with perfect information is a 
tuple (, , , ) where , ,  and  are
defined as in simultaneous games. 
Also the strategies of the defender (the leader) are defined as in simultaneous games:  
an  action d∈ for the pure case, and a  distribution δ∈  for the mixed one. 
On the other hand, a  pure strategy for the attacker is a function :, which represents the fact that 
his choice of an action  in  depends on the 
defender's choice d.
An attacker's mixed strategy is a probability distribution  ∈() over his pure strategies.[The definition of the mixed strategies as (→) means that the attacker 
draws a function : before he knows the choice of the defender. In contrast, the so-called  behavioral strategies   are defined as functions →, and formalize the idea that the draw is made  after the attacker knows such choice. In our setting,  these two definitions are equivalent, in the sense that they yield the same payoff.
]
The defender's and the attacker's expected payoff functions for mixed strategies are defined, respectively, as
(δ,) 
d←δ←(d, (d))
= ∑_d∈
:δ(d) () (d, (d))
and
(δ,)
d←δ←(d, (d))
= ∑_d∈
:δ(d) () (d, (d)).

The case of imperfect information 
is typically formalized by assuming an indistinguishability (equivalence) relation over the actions chosen 
by the leader, representing a scenario in which the follower cannot distinguish between the actions belonging to the same equivalence class. 
The pure strategies of the followers, therefore,  are functions from the set of the equivalence classes on the actions of the leader to his own actions. Formally,  a defender-first  sequential game with imperfect information  is a
tuple (, →, , ) where , ,  and  are
defined as in simultaneous games, and  is a partition of .  
The expected payoff functions are defined as before, except that now the argument of 
 is the equivalence class of d. 
Note that in the case in which all defender's actions are indistinguishable from each other at the eyes of the attacker  (totally imperfect information), we have  = {} and the expected payoff
functions coincide with those of the simultaneous games. 

 


  §.§.§ Zero-sum games and Minimax Theorem



A game (, , , ) is zero-sum if for any d∈ and any a∈, the defender's loss is equivalent to the attacker's gain, i.e., (d, a) = -(d, a).
For brevity, in zero-sum games we denote by u the attacker's payoff function , and by U the attacker's expected payoff .[Conventionally in game theory  the payoff u is  set to 
be that of the first player, but we prefer to look at the payoff from the point of view of the attacker to be in line with the definition of payoff as vulnerability.]
Consequently,  the goal of the defender is to minimize U, and the goal of the attacker is to maximize it. 

In simultaneous zero-sum games the Nash equilibrium corresponds to the solution of the minimax problem (or equivalently,  the maximin problem), namely, the strategy profile (δ^*, α^*) such that 
U(δ^*, α^*)=min_δmax_α U(δ, α). 
The  von Neumann's minimax theorem, in fact, ensures that such solution (which always exists) is stable.

[von Neumann's minimax theorem]Theoremres:vonneumann

Let ⊂^m and ⊂^n be compact convex sets,
and : ×→ be a continuous function such that
(x, y) is a convex function in x∈ and a concave function in y∈.
Then

min_x∈max_y∈(x, y) = max_y∈min_x∈(x, y).



A related property is that, under the conditions of Theorem <ref>, there exists a saddle point (x^*, y^*) s.t., for all x∈  and y∈: 


(x^*, y)≤(x^*, y^*)≤(x, y^*).


The solution of the minimax problem can be obtained by using convex optimization techniques. 
In case (x, y) is affine in x and in y, we can also use linear optimization. 

In case  and  contain two elements each, there is a closed form for the solution.  
Let  ={d_0,d_1} and ={a_0,a_1} respectively. 
Let u_ij be the utility of the defender on d_i, a_j.           
Then the Nash equilibrium (δ^*,α^*) is given by:
δ^*(d_0)=(u_11 - u_10)/(u_00 - u_01 - u_10 +u_11)
and
α^*(a_0)=(u_11 - u_01)/(u_00 - u_01 - u_10 +u_11)
if these values are in [0,1].  
Note that, since there are only two elements, the strategy δ^* is completely specified by its value in d_0, and analogously for α^*.


 §.§ Quantitative information flow



Finally, we briefly review the standard framework of
quantitative information flow, which is concerned with
measuring the amount of information leakage in a 
(computational) system.
  


  
Secrets and vulnerability
A secret is some piece of sensitive information the 
defender wants to protect, such as a user's password, social 
security number, or current location. 
The attacker usually only has some partial knowledge 
about the value of a secret, represented as a probability
distribution on secrets called a prior.
We denote by  the set of possible secrets,
and we typically use π to denote a prior belonging to 
the set  of probability distributions over 
. 

The  vulnerability of a secret is a measure of the utility that it represents for the attacker. 
In this paper we consider a very general notion of  vulnerability, following <cit.>, and we define 
a vulnerability  to be any continuous and convex function of type →.

It has been shown in <cit.> 
that these functions coincide
with the set of g-vulnerabilities, 
and are, in a precise sense, the most general 
information measures w.r.t. a set of basic 
axioms. [More precisely, if posterior vulnerability 
is defined as the expectation of the vulnerability of posterior
distributions, 
the measure respects the data-processing inequality 
and always yields non-negative leakage iff
vulnerability is convex.]



  
Channels, posterior vulnerability, and leakage
Computational systems can be modeled as information
theoretic channels.
A 
channel
C : ×→ is a function
in which  is a set of input values,  is a set 
of output values, and C(x,y) represents the conditional 
probability of the channel producing output y ∈ when 
input x ∈ is provided. 
Every channel C satisfies 0 ≤ C(x,y) ≤ 1 for all 
x∈ and y∈, and ∑_y∈ C(x,y) = 1 for all x∈.

A distribution π∈ and a channel C 
with inputs  and outputs  induce a joint distribution
p(x,y) = π(x)C(x,y) on ×,
producing joint random variables X, Y with marginal 
probabilities p(x) = ∑_y p(x,y) and 
p(y) = ∑_x p(x,y), and conditional probabilities 
p(x|y) = p(x,y)/p(y) if p(y)≠ 0. 
For a given y (s.t. p(y)≠ 0), the conditional 
probabilities p(x|y) for each x ∈ form the 
posterior distribution p_X | y.

A channel C in which  is a set of secret values 
and  is a set of observable values produced
by a system can be used to model computations on secrets.
Assuming the attacker has prior knowledge π about
the secret value, knows how a channel C works, and
can observe the channel's outputs, the effect of the channel 
is to update the attacker's knowledge from π to a 
collection of posteriors p_X | y, each occurring 
with probability p(y).


Given a vulnerability , a prior π, and a channel C, 
the posterior vulnerability πC is the vulnerability 
of the secret after the attacker has observed the output of the channel C.
Formally:
πC∑_y ∈ p(y) p_X | y.

It is known from the literature <cit.> 
that  the posterior vulnerability is a convex function of π. 
Namely, for any channel C, any family of distributions {π_i}, and any set of convex coefficients {c_i}, we have: 
∑_i c_i π_iC≤∑_i c_i π_iC.

The (information) leakage of 
channel C under prior π is a comparison between 
the vulnerability of the secret before the system
was run—called prior vulnerability—and the 
posterior vulnerability of the secret.
Leakage reflects by how much the observation of 
the system's outputs increases the attacker's 
information about the secret. 
It can be defined either 
additively (πC-π), or
multiplicatively (πC/π).





§ AN ILLUSTRATIVE EXAMPLE


r0.31





 x ∈{0,1}

 a ∈{0,1}

 y∈{0,1}

y= x · a

return y



 x ∈{0,1}

 a ∈{0,1}

 y∈{0,1}

c flip coin with bias a/3

if c = ℎ𝑒𝑎𝑑𝑠 {y = x} 

else {y = x̅}

return y



Running example.





We introduce an example which will serve as running example through the paper. 
Although admittedly contrived, this example is simple and yet produces
different leakage measures for all different combinations of visible/invisible choice and simultaneous/sequential games, 
thus providing a way to compare all different scenarios we are interested in. 

Consider that a binary secret must be processed by a program.
As usual, a defender wants to protect the secret value, 
whereas an attacker wants to infer it by observing the 
system's output.
Assume the defender can choose which among two
alternative versions of the program to run.
Both programs take the secret value x as high input,  
and a binary low input a whose value is chosen by the attacker. 
They both return the output in a low variable y. [We adopt the usual 
convention in QIF of referring to secret variables, inputs and outputs in programs 
as high, and to their observable counterparts as low.]
 returns the binary product of x and a,
whereas  flips a coin with bias a/3
(i.e., a coin which returns heads with probability a/3)
and returns x if the  result is
heads, and the complement x̅ of x otherwise.
The two programs are represented in Figure <ref>.

The combined choices of the defender's and of the
attacker's determine how the system behaves.
Let ={0,1} represent the set of the defender's
choices—i.e., the index of the program to use—, and
= {0,1} represent the set of the attacker's
choices—i.e., the value of the low input a. 
We shall refer to the elements of  and  as actions.
For each possible combination of actions 
d ∈ and a ∈, we can construct a channel 
C_da modeling how the resulting system behaves.
Each channel C_da is a function of type 
×→, where 
= {0,1} is the set of possible high input values 
for the system, and = {0,1} is the set of possible 
output values from the system.
Intuitively, each channel provides the probability that the
system (which was fixed by the defender) produces output 
y∈ given that the high input is x ∈
(and that the low input was fixed by the attacker). 
The four possible channels are depicted as matrices below.


    [ C_00  y=0  y=1;  x=0    1    0;  x=1    1    0;      ]  [ C_01  y=0  y=1;  x=0    1    0;  x=1    0    1;      ]  [ C_10  y=0  y=1;  x=0    0    1;  x=1    1    0;      ]  [ C_11  y=0  y=1;  x=0  1/3  2/3;  x=1  2/3  1/3;      ]



Note that channel C_00 does not leak any 
information about the input x (i.e., it is 
non-interferent), whereas channels C_01 and 
C_10 completely reveal x.
Channel C_11 is an intermediate case: it leaks some 
information about x, but not all.

We want to investigate how the defender's and the attacker's choices
influence the leakage of the system. 
For that we can just consider the (simpler) notion of posterior vulnerability, 
since in order to make the comparison fair we need to assume that the prior is 
always the same in the various scenarios, and this implies that the 
leakage is in a one-to-one correspondence with the posterior vulnerability 
(this happens for both additive and multiplicative leakage). 

r0.42





    [     a=0 a=1; d=0 1/2   1; d=1   1 2/3;     ]





Vulnerability of each channel C_da in the running example. 




For this example, assume we are interested in 
Bayes vulnerability <cit.>, defined as
(π) = max_xπ(x) for every π∈.
Assume for simplicity that 
the prior is the uniform prior π_u.
In this case we know from <cit.> that the posterior 
Bayes vulnerability of a channel is the sum of the greatest elements 
of each column, divided by the total number of inputs. 
Table <ref> provides the
Bayes vulnerability _daπ_uC_da
of each channel considered above.

Naturally, the attacker aims at maximizing the vulnerability of the system, 
while the defender tries to minimize it. 
The resulting vulnerability will depend on various factors, in particular on
whether the two players make their choice simultaneously 
(i.e. without knowing the choice of the opponent) or sequentially. 
Clearly, if the choice of a player who moves first is known by an opponent who moves second, 
the opponent will be in advantage. 
In the above example, for instance, if the defender knows the choice a of the attacker, the most convenient choice for him is to set  d=a, and 
the vulnerability will be at most 2/3 . 
Vice versa, if the attacker knows the choice d  of the defender, the most convenient choice for him is to set  a≠ d. The vulnerability in this case will be 1.

Things become more complicated when players make choices simultaneously. 
None of the pure choices of d and a are the best for the corresponding player, 
because the vulnerability of the system depends also on the (unknown) choice of the other player. 
Yet there is a strategy leading to the best possible situation for both players (the Nash equilibrium), but it is mixed (i.e., probabilistic), in that the players randomize their choices according to some precise distribution. 

Another factor that affects vulnerability is whether or not the defender's choice is known to the attacker at the moment in which he observes the output of the channel. 
Obviously, this corresponds to whether or not the attacker knows what channel he is observing. 
Both cases are plausible: naturally the defender has all the interest in keeping his choice 
(and, hence, the channel used) secret, since then the attack will be less effective 
(i.e., leakage will be smaller). 
On the other hand, the attacker may be able to identify the channel used anyway, for instance 
because the two programs have different running times. 
We will call these two cases hidden and visible choice, respectively. 

It is possible to model players' strategies, as well as hidden and visible choices, 
as operations on channels. 
This means that we can look at the whole system as if it were a single channel, 
which will turn out to be useful for some proofs of our technical results.
Next section is dedicated to the definition of these operators. 
We will calculate the exact values for our example in Section <ref>. 






§ VISIBLE AND HIDDEN CHOICE OPERATORS ON CHANNELS


In this section we define matrices and 
some basic operations on them.
Since channels are a particular kind of 
matrix, we use these matrix operations to define
the operations of visible and hidden choice among
channels, and to prove important properties of 
these channel operations.



 §.§ Matrices, and their basic operators



Given two  sets  and , a matrix 
is a total function of type ×→.

Two matrices 
M_1: _1×_1→ and 
M_2: _2×_2→ 
are said to be compatible if _1 = _2.
If it is also the case that _1 = _2, we say 
that the matrices have the same type.
The scalar multiplication r·M between a scalar r and
a matrix M is defined as usual, and so is the summation
(∑_i ∈ M_i)(x,y) = M_i_1(x,y) … M_i_n(x,y)
of a family {M_i}_i ∈ of matrices all of a same type.

Given a family {M_i}_i ∈ of
compatible matrices s.t. each M_i has type 
×_i→, their concatenation _i ∈ 
is the matrix having all columns of every matrix in the family,
in such a way that every column is tagged with the matrix it
came from.
Formally, 
( _i ∈ M_i)(x,(y,j)) =  M_j(x,y), 
if y ∈_j,
and the resulting matrix has type
×( _i ∈_i) →. [
_i ∈_i = _i_1⊔_i_2⊔…⊔_i_n denotes the disjoint union 
{ (y,i) | y ∈_i, i ∈}
of the sets _i_1, _i_2, …, _i_n.
]
When the family {M_i} has only two elements
we may use the binary version  of the
concatenation operator.
The following 
depicts the concatenation of two matrices M_1 and M_2 in tabular form.

    [ M_1 y_1 y_2; x_1   1   2; x_2   3   4;     ][ M_2 y_1 y_2 y_3; x_1   5   6   7; x_2   8   9  10;     ] = [ M_1 M_2 (y_1,1) (y_2,1) (y_1,2) (y_2,2) (y_3,2);     x_1       1       2       5       6       7;     x_2       3       4       8       9      10;         ]




 §.§ Channels, and their hidden and visible choice operators



A channel 
is a stochastic matrix, i.e., 
all elements are non-negative, and all rows sum up to 1.
Here we will define two operators specific for channels.
In the following, for any real value 0 ≤ p ≤ 1, 
we denote by p̅ the value 1 - p.




  §.§.§ Hidden choice

The first operator models a hidden probabilistic 
choice among channels.
Consider a family { C_i}_i ∈ 
of channels of a same type.
Let μ∈ be a probability
distribution on the elements of the index set .
Consider an input x is fed to one of
the channels in { C_i}_i ∈,
where the channel is randomly picked according to μ.
More precisely, an index i ∈ is sampled with 
probability μ(i),  then the input
x is fed to channel C_i,
and the output y produced by the channel is then made visible, 
but not the index i of the channel that was used.
Note that we consider hidden choice only among
channels of a same type:  if the sets of outputs
were not identical, the produced output 
might implicitly reveal which channel was used.

Formally, given a family {C_i}_i ∈ of 
channels s.t. each C_i has same type 
×→, the 
hidden choice operator iμ 
is defined as 


iμ C_i = ∑_i ∈μ(i)  C_i.


Propositionrestypehiddenchoice

Given a family {C_i}_i ∈ of 
channels of  type ×→, 
and a distribution μ on , 
the hidden choice 
iμ C_i is 
a channel of type
×→.


In the particular case in which the family {C_i} 
has only two elements C_i_1 and C_i_2, the
distribution μ on indexes is completely determined 
by a real value 0 ≤ p ≤ 1 s.t. 
μ(i_1) = p and μ(i_2) = p̅.
In this case we may use the binary version p
of the hidden choice operator:

C_i_1pC_i_2 = p C_i_1+p̅ C_i_2.


The example 

below depicts the hidden choice
between channels C_1 and C_2, with probability
p=1/3.

    [ C_1 y_1 y_2; x_1 1/2 1/2; x_2 1/3 2/3;     ]1/3[ C_2 y_1 y_2; x_1 1/3 2/3; x_2 1/2 1/2;     ]  =  [ C_11/3 C_2        y_1        y_2;        x_1       7/18      11/18;        x_2        4/9        5/9;            ]






  §.§.§ Visible choice

The second operator models a visible probabilistic 
choice among channels.
Consider a family { C_i}_i ∈ 
of compatible channels.
Let μ∈ be a probability
distribution on the elements of the index set .
Consider an input x is fed to one of
the channels in { C_i}_i ∈,
where the channel is randomly picked according to μ.
More precisely, an index i ∈ is sampled with 
probability μ(i),  then the input
x is fed to channel C_i, and the output y produced by the channel is then made visible, 
along with the index i of the channel that was used.
Note that visible choice makes sense only 
between compatible channels,
but it is not required that the output set of each channel 
be the same.

Formally, given  {C_i}_i ∈ of
compatible channels s.t. each C_i has type 
×_i→, 
and a distribution μ on , the 
visible choice operator iμ 
is defined as 

iμ C_i = _i ∈ μ(i)  C_i.


Propositionrestypevisiblechoice

Given a family {C_i}_i ∈ of 
compatible channels s.t. each C_i has type 
×_i→,
and a distribution μ on , 
the result of the visible choice 
iμ C_i is a channel
of type 
×( _i ∈_i) →.


In the particular case the family {C_i} 
has only two elements C_i_1 and C_i_2, the
distribution μ on indexes is completely determined 
by a real value 0 ≤ p ≤ 1 s.t. 
μ(i_1) = p and μ(i_2) = p̅.
In this case we may use the binary version p
of the visible choice operator:

C_i_1p C_i_2 = p  C_i_1p̅  C_i_2.


The following 
depicts the visible choice 
betwee channels C_1 and C_3, with probability
p=1/3.

    [ C_1 y_1 y_2; x_1 1/2 1/2; x_2 1/3 2/3;     ]1/3[ C_3 y_1 y_3; x_1 1/3 2/3; x_2 1/2 1/2;     ]  =  [ C_11/3 C_3    (y_1,1)    (y_2,1)    (y_1,3)    (y_3,3);        x_1        1/6        1/6        2/9        4/9;        x_2        1/9        2/9        1/3        1/3;            ]




 §.§ Properties of hidden and visible choice operators



We now prove algebraic properties of channel operators.
These properties will be useful when we model a (more complex) 
protocol as the composition of smaller channels via hidden or visible 
choice.

Whereas the properties of hidden choice 
hold generally with equality, those of 
visible choice are subtler.
For instance, visible choice is not idempotent,
since in general CpC ≠ C.
(In fact if C has type ×→,
CpC has type × (⊔) →.)
However, idempotency and other properties involving visible
choice hold if we replace the notion of 
equality with the more relaxed notion of equivalence 
between channels.
Intuitively, two channels are equivalent if they
have the same input space and yield 
the same value of vulnerability for every 
prior and every vulnerability function.

[Equivalence of channels]

Two compatible channels C_1 and C_2
with domain 
are equivalent, denoted by C_1≡ C_2,
if for every prior π∈ and every 
posterior vulnerability  we have

πC_1 = πC_2.



Two equivalent channels are indistinguishable from the point of view of information leakage, and in most cases we can just identify them. 
Indeed, nowadays there is a tendency to use abstract channels <cit.>, which capture exactly 
the important behavior with respect to any  form of leakage. 
In this paper, however, we cannot use abstract channels because the hidden choice operator needs a concrete representation in order to be defined
unambiguously. 

The first properties we prove regard idempotency of operators, which
can be used do simplify the representation of some protocols.


[Idempotency]Propositionresidempotency

Given a family {C_i}_i ∈ of 
channels s.t. C_i = C for all i ∈,
and a distribution μ on , then:



(a) iμC_i = C; and

(b) iμC_i≡ C.




The following properties regard the reorganization of operators, 
and they will be essential in some technical results in which we invert 
the order in which hidden and visible choice are applied in a protocol.


[Reorganization of operators]Propositionresreorganizationoperators

Given a family {C_i j}_i ∈, j ∈ of 
channels indexed by sets  and ,
a distribution μ on , and
a distribution η on :



  * iμ jη C_i j = iμjη C_i j, if all C_i's have the same type;



  * iμ jη C_i j≡iμjη C_i j, if all C_i's are compatible; and



  * iμ jη C_i j≡jη iμ C_i j, 
if, for each i, all C_i j's have same type ×_j→.






 §.§ Properties of vulnerability w.r.t. channel operators



We now derive some relevant properties of vulnerability w.r.t. our 
channel operators, which will be later used to obtain the Nash equilibria 
in information leakage games with different choice operations.

The first result states that posterior vulnerability is 
convex w.r.t. hidden choice (this result was already presented in <cit.>), and 
linear w.r.t. to visible choice.

TheoremresconvexVq

Let {C_i}_i ∈ be a family of channels,
and μ be a distribution on .
Then, for every distribution π on , and every
vulnerability :



  * 
posterior vulnerability is convex w.r.t. to hidden choice:

πiμ C_i≤∑_i ∈μ(i)  πC_i

if all C_i's have the same type.


  * 
posterior vulnerability is linear w.r.t. to visible choice:

πiμ C_i = ∑_i ∈μ(i)  πC_i

if all C_i's are compatible.



The next result is concerned with posterior vulnerability 
under the composition of channels using both operators.

CorollaryresconcaveconvexV

Let {C_i j}_i ∈, j ∈ be a family of channels,
all with domain  and with the same type, and let π∈, and  be any vulnerability. 
Define
: ×→ as follows:

(μ, η) πiμ jη  C_i j.

Then  is convex on μ and linear on η.






§ INFORMATION LEAKAGE GAMES


In this section we present our framework for  reasoning about information leakage, 
extending the notion of information leakage games proposed in <cit.> from only simultaneous games with hidden choice to 
both simultaneous and sequential games, with either hidden or visible choice.

In an information leakage game the defender tries to minimize the leakage of information 
from the system, while the attacker tries to maximize it.
In  this basic scenario, their goals are just opposite (zero-sum). 
Both of them can influence the execution and the observable behavior of the system via a 
specific set of actions.
We assume players to be rational (i.e., they are able to figure out what is 
the best strategy to 
maximize their expected payoff), and that the set of actions and the
payoff function are common knowledge. 

Players choose their own strategy, which in general may be mixed 
(i.e. probabilistic), and choose their action by a random draw 
according to that strategy. 
After both players have performed their actions, the system runs 
and produces some output value which is visible to the attacker and
may leak some information about the secret.
The amount of leakage constitutes the attacker's gain, and the defender's loss. 

To quantify the  leakage we model the system as an information-theoretic channel  
(cf. Section <ref>). We recall that leakage is defined as the difference (additive leakage) 
or the ratio (multiplicative leakage) between posterior and prior vulnerability. 
Since we are only interested in comparing the leakage of different channels
for a given prior, 
we will define the payoff just as the posterior vulnerability,
as the value of prior vulnerability will be the same for every channel.



 §.§ Defining information leakage games



An (information) leakage game

consists of:


(1) two nonempty sets ,  of defender's and attacker's actions  
respectively,


(2) a function C: ×→ (×→) 
that associates to each pair of actions  (d,a)∈× a channel 
C_da: ×→, 

(3) a prior π∈ on secrets, and 

(4) a vulnerability measure .  


The payoff function u: ×→ for pure strategies 
is defined as
u(d,a) πC_da.
We have only one payoff function because the game is zero-sum. 

Like in traditional game theory, the order of actions and the extent by which a player knows the move performed by the opponent play a critical role in deciding strategies and determining the payoff. 
In security, however, knowledge of the opponent's move affects the game in yet another way:
the effectiveness of the attack, i.e., the amount of leakage, depends crucially on whether or not
the attacker knows what channel is being used. 
It is therefore convenient to distinguish two phases in the leakage game: 










  Phase 1: Each player determines the most convenient strategy (which in general is mixed) for himself, and draws his action accordingly. One of the players may commit first to his action, and his choice may or may not be revealed to the follower. In general, knowledge of the leader's action may help the follower choose a more advantageous strategy. 


  Phase 2:  The attacker observes the output of the selected channel C_da and performs his attack on the secret. In case he knows the defender's action, he is able to determine the exact channel C_da being used (since, of course, the attacker knows his own action), 
and his payoff will be the posterior vulnerability πC_da.
However, if the attacker does not know exactly which channel has been used, then his payoff will be smaller.  


Note that the issues raised in Phase 2 are typical of leakage games; 
they do not have a correspondence (to the best of our knowledge) 
in traditional game theory. 
On the other hand, these issues are central to security, as they 
reflect the principle of preventing the attacker from inferring 
the secret by obfuscating the link between secret and observables. 



Following the above discussion, we consider various possible 
scenarios for games, along two lines of classification.
First, there are three possible orders for the two players' actions.



  Simultaneous:
The players choose (draw) their actions in parallel, each without knowing the choice of the other.

  Sequential, defender-first:
The defender draws an action, and commits to it,  before the attacker does.

  Sequential, attacker-first:
The attacker draws an action, and commits to it,  before the defender does.

Note that these sequential games may present imperfect information
(i.e., the follower may not know the leader's action).

Second, the visibility of the defender's action during the attack may vary:


  Visible choice: 
The attacker knows the defender's action when he observes the output of the channel, and therefore 
he knows which channel is being used.
Visible choice is modeled by the operator .  

  Hidden choice:
The attacker does not know the defender's action when he observes the output of the channel, and therefore in general he does not exactly know which channel is used (although in some special cases he may infer it from the output).  
Hidden choice is modeled by the operator . 


Note that the distinction between sequential and simultaneous games
is orthogonal to that between visible and hidden choice.
Sequential and simultaneous games model whether or not, respectively,
the follower's choice can be affected by knowledge of the leader's action.
This dichotomy captures how knowledge about the other player's actions 
can help a player choose his own action.
On the other hand, visible and hidden choice capture whether or not, respectively, the 
attacker is able to fully determine the channel representing the system, 
once defender and attacker's actions have already been fixed.
This dichotomy reflects the different amounts of information leaked by 
the system as viewed by the adversary.
For instance, in a simultaneous game neither player can choose his action based on 
the choice of the other.
However, depending on whether or not the defender's choice is visible, 
the adversary will or will not, respectively, be able to completely recover 
the channel used, which will affect the amount of leakage.


If we consider also the subdivision of sequential games into perfect and imperfect information, 
there are 10 possible different combinations. 
Some, however, make little sense. 
For instance,  defender-first sequential game with perfect information 
(by the attacker) 
does not combine naturally with hidden choice
, 
since that would mean that the attacker knows the action of the defender 
and choses his strategy accordingly, but forgets it at the moment of the attack. 
(We assume perfect recall, i.e., the players never forget what they have learned.)
Yet other combinations are not interesting, such as the attacker-first sequential game with 
(totally) imperfect information (by the defender), since it coincides with the simultaneous-game case. 
Note that attacker and defender are not symmetric with respect to hiding/revealing their actions a and d, since the knowledge of a affects the game only in the usual sense of game theory, while the knowledge of d also affects the computation of the payoff (cf.  Phase 2 above). 

Table <ref> lists the meaningful and interesting combinations. 
In Game V we assume imperfect information: the attacker does not 
know the action chosen by the defender. 
In all the other sequential games we assume that the follower has perfect 
information.
In the remaining of this section, we discuss each game individually, using the example of Section <ref> as running example. 





  §.§.§ Game I (simultaneous with visible choice)


This simultaneous game can be represented by a tuple (, , ). 
As in all games with visible choice , 
the expected payoff  of a mixed strategy profile (δ,α) 
is defined to be the expected value of u, as in traditional game theory: 

(δ,α) 
d←δa←α(d, a)
=∑_d∈
 a∈δ(d)  α(a) (d, a),

where we recall that (d,a) = πC_da. 

From Theorem <ref>(<ref>) we derive:

(δ,α) 
= πdδaα C_da.

hence the whole system can be equivalently regarded as 
the channel dδaα C_da. 

Still from Theorem <ref>(<ref>) we 
can derive that (δ,α) is linear in δ and α. 
Therefore the Nash equilibrium can be computed using the minimax method 
(cf. Section <ref>). 

Consider the example of Section <ref> in the setting of Game I.
The Nash equilibrium (δ^*,α^*) can be obtained using the closed formula 
from Section <ref>,
and it is given by
δ^*(0) =α^*(0) =(2/3-1)/(1/2-1-1+2/3)=2/5.
The corresponding payoff is
(δ^*,α^*)= 2/5 2/5 1/2+2/5 3/5 + 3/5 2/5 + 3/5 3/5 2/3= 4/5.




  §.§.§ Game II (defender 1st with visible choice)


This defender-first sequential game can be represented by a tuple (, , ). 
A mixed strategy profile is of the form (δ, ), with δ∈ and ∈(), and the corresponding payoff is

(δ,) 
d←δ←(d, (d))
= ∑_d∈
:δ(d) () (d, (d)),

where  (d, (d)) = πC_d(d). 


Again, from Theorem <ref>(<ref>) we derive:

(δ,) 
= πdδ  C_d (d)

and hence the system can be expressed as channel 
dδ C_d (d).
From the same Theorem we also derive that (δ,) is 
linear in δ and , so the mutually optimal strategies can 
be obtained again by solving the minimax problem.
In this case, however, the solution is particularly simple, because it 
is  known that there are optimal strategies which are deterministic.
Hence it is sufficient for the defender to find  the action d which 
minimizes max_a (d,a). 


Consider  the example of Section <ref> in the setting of Game II.
If the defender chooses 0 then the attacker chooses 1. 
If the defender chooses 1 then the attacker chooses 0.
In both cases, the payoff is 1. The game has therefore two solutions, (0,1) and (1,0).




  §.§.§ Game III (attacker 1st with visible choice)


This game is also a sequential game, but with the attacker as the leader. 
Therefore it can be represented as tuple of the form (, , ). 
It is the same as Game II, except that the roles of the attacker and the 
defender are inverted. 
In particular, the payoff of a mixed strategy profile 
(, α)∈()× is given by



(,α)  
←a←α((a),a) = ∑_:
 a∈() 
   α(a) ((a), a)  
= πaα  C_(a) a,



and  the whole system can be equivalently regarded as channel 
aα  C_(a) a. 

Obviously, also  in this case the minimax problem has  a deterministic solution. 

In summary, in the sequential case, whether the leader is the defender or the attacker
(Games II and III, respectively), the minimax problem has always a deterministic 
solution <cit.>.



In a defender-first sequential game with visible choice, there exist 
d∈ and a∈ such that, 
for every δ∈ and ∈() we have:
(d,)≤(d,a)≤(δ,a).
Similarly, in an attacker-first sequential game with visible choice, there exist 
d∈ and a∈ such that, 
for every ∈() and α∈ we have:
(d,α)≤(d,a)≤(,a).



Consider now the example of Section <ref> in the setting of Game III.
If the attacker chooses 0 then the defender chooses 0 and the payoff is 1/2.  
If the attacker chooses 1 then the defender  chooses 1 and the payoff is 2/3.
The latter case is more convenient for the attacker, hence the solution of the game is the strategy profile (1,1). 




  §.§.§ Game IV (simultaneous with hidden choice)


This game is a tuple (,,).
However, it is not an ordinary game in the sense that 
the payoff a mixed strategy profile cannot be defined by averaging
the payoff of the corresponding pure strategies. 
More precisely, the payoff of a mixed profile is defined by
averaging on the strategy of the attacker, but not on that 
of the defender. 
In fact, when hidden choice is used, there is an additional level 
of uncertainty in the relation between the observables and the secret 
from the point of view of the attacker, since he is not sure about which 
channel is producing those observables. 
A mixed strategy δ for the defender produces a convex combination 
of  channels  (the channels associated to the pure strategies) with the 
same coefficients, and we know from previous sections that  the vulnerability 
is a convex function of the channel, and in general is not linear. 

In order to define the payoff of a mixed strategy  profile  (δ,α), 
we need therefore to consider the channel that the attacker perceives given his 
limited knowledge. Let us assume that the action that the attacker draws from 
α  is a. 
He does not know the action of the defender, but we can assume 
that he knows his strategy (each player can derive the optimal strategy of the 
opponent, under the assumption of common knowledge and rational players).

The channel the attacker will see is 
dδ C_d a, obtaining a corresponding payoff of 
πdδC_d a.
By averaging on the strategy of the attacker we obtain 
(δ,α) 
a←α πdδC_d a
= ∑_a∈ α(a) πdδC_d a.

From Theorem <ref>(<ref>) we derive:

(δ,α) 
= πaα dδC_d a

and hence the whole system can be equivalently regarded as channel 
aα dδC_d a.

Note that, by Proposition <ref>(<ref>), 
the order of the operators is interchangeable, and the system can be 
equivalently regarded as dδ aαC_d a.
This shows the robustness of this model. 

From Corollary <ref> we  derive that (δ,α) is convex in δ and linear in η, hence we can compute the Nash equilibrium by the minimax method.


Consider now the example of Section <ref> in the setting of Game IV.
For δ∈ and α∈, let p=δ(0) and q=α(0). 
The system can be represented by the channel 
(C_00p C_10)q(C_01p C_11)
represented below.

    [ C_00p C_10        y=0        y=1;        x=0          p         p̅;        x=1          1          0;            ]  q  [ C_01p C_11        y=0        y=1;        x=0 1/3+ 2/3 p 2/3- 2/3 p;        x=1 2/3- 2/3 p 1/3+ 2/3 p;            ]

For uniform π, we have
π C_00p C_10=1-1/2;
and 
π C_10p C_11 is equal to
2/3- 2/3 p if p≤1/4,
and equal to 
1/3+ 2/3 p 
if p> 1/4.

Hence the payoff, expressed in terms of p and q, is
(p,q) = q(1-1/2) + q̅ (2/3 - 2/3 p)
if p≤1/4, and 
(p,q) = q(1-1/2) + q̅ (1/3 + 2/3 p) 
if p> 1/4.
The Nash equilibrium (p^*,q^*) is given by
p^* = _pmax_q 	(p,q)
and 
q^* = _qmin_p 	(p,q), and by solving the above, we obtain
p^* = q^*= 4/7.





  §.§.§ Game V (defender 1st with hidden choice)


This is a defender-first sequential game with imperfect information, hence it can be represented as a tuple of the form  (, →, , ), where  is a partition of . 
Since we are assuming perfect recall, and the attacker does not know anything about the 
action chosen by the defender in Phase 2, i.e., at the moment of the attack (except the probability distribution determined by his strategy), we must assume that the attacker does not know anything in Phase 1 either. Hence the indistinguishability relation must be total, i.e.,  ={}. But {}→ is equivalent to , hence this kind of game is equivalent to Game IV.

It is also a well known fact in Game theory that when in a sequential game 
the follower does not know the leader's move before making his choice, 
the game is equivalent to a simultaneous game.[However, one could
argue that, since the defender has already committed, the attacker does not
need to perform the action corresponding to the Nash equilibrium, any 
payoff-maximizing solution would be equally good for him.]



  §.§.§ Game VI (attacker 1st with hidden choice)


This game is also a sequential game with the attacker as the leader, hence it is a tuple of the form
(, , ). 
It is  similar to Game III, except that the payoff is convex on the strategy of the defender, instead of linear. 
The payoff of the mixed strategy profile  (, α)∈()×  is



(,α)  
a←α πC_(a) a 
= πaα   C_(a) a,


so the whole system can be equivalently regarded as channel 
aα   C_(a) a.

Also in this case the minimax problem has  a deterministic solution, but only for the attacker.

In an attacker-first sequential game with hidden choice, 
there exist  a∈ and δ∈ such that, for every α∈ and ∈() we have that
(δ,α)≤(δ,a)≤(,a).



Consider again the example of Section <ref>, this time in the setting of Game VI.
Consider also the calculations made in Example <ref>, we will use the same results and notation here. 

In this setting, the attacker is obliged to make its choice first. 
If he chooses 0, which corresponds to committing to the system C_00p C_10, 
then the defender will choose p=1/4, which minimizes its vulnerability. 
If he chooses 1, which corresponds to committing to the system C_01p C_11, 
the defender will choose p=1, which minimizes its vulnerability of the above channel. 
In both cases, the leakage is p=1/2, hence both these strategies are solutions to the minimax. 
Note that in the first case the strategy of the defender is mixed, while that of the attacker is always pure. 





 §.§ Comparing the games



If we look at the various payoffs obtained for the running example in the various games, we obtain the following values (listed in decreasing order):
II:  1;  I: 4/5;  III: 2/3;  IV: 4/7;  V: 4/7;  VI: 1/2.
Convert this into a theorem. 
Then probably Theorem <ref> will become a lemma.
And we have to check the relation of all this with Theorem <ref>.
Let's do it in the journal version of this POST paper.

r0.3


    < g r a p h i c s >



Order of games w.r.t. payoff. 
Games higher in the lattice have larger payoff.




This order is not accidental:
for any vulnerability function, and for any prior, the various games are
ordered, with respect to the payoff, as shown in Figure <ref>.
The relations between II, I, and III, and between IV-V and VI come from the fact that, in any zero-sum sequential game the leader's payoff  will
be less or equal to his payoff in the corresponding simultaneous game.
We think this result is well-known in  game theory, but we give the hint of the proof nevertheless, for the sake of clarity.
Theoremorder

It is the case that:


  * 
[ min_δmax_πdδ  C_d (d)                     ≥  min_δmax_απdδaα C_da;                                           ≥ max_αmin_πaα  C_(a) a ]

 


  * min_δmax_απaα dδC_d a≥max_αmin_πaα   C_(a) a



We prove the first inequality in (<ref>). 
Independently of δ, consider the attacker strategy τ_a that assigns probability 1 to the function  defined as
(d) = _a πC_d a.
Then we have that

    min_δmax_πdδ  C_d (d)≥     min_δπdδτ_a  C_d (d)
    ≥     min_δmax_απdδaα C_da

Note that the strategy τ_a is optimal  for the adversary, so the first of the above inequalities is actually an equality. 

All other cases can be proved with an analogous reasoning. 

 
 
 
Concerning III and IV-V: these are not related. In the running example the payoff for III is higher than for IV-V, but it is easy to find other cases in which the situation is reversed. For instance, if in the running example we set C_11 to be the same as C_00, the payoff for  III  will be 1/2, and that for IV-V will be 2/3.

Finally, the relation between III  and VI comes from the fact that they are both attacker-first sequential games, and 
the only difference is the way in which the payoff is defined. 
Then, just observe that in general we have, for every a∈ and every δ∈:
πdδC_d a≤πdδC_d a.
 
The relations in Figure <ref> can be used by the defender as guidelines to better protect the system, if he has some control over the rules of the game. Obviously, for the defender the games lower in the ordering are to be preferred. 
 





§ CASE STUDY: A SAFER, FASTER PASSWORD-CHECKER


[14]r0.44





 x ∈{000, 001, …, 111}

 a ∈{000, 001, …, 111}

 y∈{,}
 
accept := 

for i = 1, 2, 3 do

 if a_i≠ x_i then

  accept :=

  break

 end if

end for

return accept



Password-checker algorithm.


In this section we apply our game-theoretic, compositional
approach to show how a defender can mitigate an attacker's typical timing 
side-channel attack while avoiding the usual burden imposed on the 
password-checker's efficiency.

Consider the password-checker 123 of 
Figure <ref>, which performs a bitwise-check of
a 3-bit low-input a=a_1a_2a_3, provided by the attacker,
against a 3-bit secret password x=x_1x_2x_3.
The low-input is rejected as soon as it mismatches the secret, 
and is accepted otherwise.

The attacker can choose low-inputs to try to gain information about 
the password. 
Obviously, in case 123 accepts the low-input,
the attacker learns the password value is a=x.
Yet, even when the low-input is rejected,
there is some leakage of information:
from the duration of the execution the attacker can estimate how 
many iterations have been performed before the low-input was rejected, 
thus inferring a prefix of the secret password. 

To model this scenario, let = {000,001,…,111} be the set of all possible 3-bit 
passwords, and = {(,1), (,2),  (,3), (,3)} be 
the set of observables produced by the system.
Each observable is an ordered pair whose first element indicates whether the password 
was accepted ( or ), and the second element indicates the duration of 
the computation (1, 2, or 3 iterations).
For instance, channel C_123,101 in Figure <ref>
models 123's behavior when the 
attacker provides low-input a=101.

We will adopt as a measure of information Bayes vulnerability <cit.>.
The prior Bayes vulnerability of a distribution π∈ is 
defined as
π=max_x ∈π_x,
and represents the probability that the attacker guesses correctly
the password in one try.
For instance, if the distribution on all possible 3-bit passwords is 
π̂=(0.0137, 0.0548, 0.2191,  0.4382,  0.0002,  0.0002,  0.0548,  0.2191), 
its prior Bayes vulnerability is π̂=0.4382.

The posterior Bayes vulnerability of a prior π and a channel 
C:×→ is defined as
πC=∑_y ∈max_x ∈π_x C(x,y),
and it represents the probability that the attacker guesses correctly
the password in one try, after he observes the output of the channel (i.e.,
after he has measured the time needed for the checker to accept or reject 
the low-input).
For prior π̂ above, the posterior 
Bayes 
vulnerability of channel C_123,101 is π̂C_123,101=0.6577
(which represents an 
increase in Bayes vulnerability 
of about 50%), and the expected running time for this checker is of 1.2747 iterations.

A way to mitigate this timing side-channel is to make the checker's
execution time independent of the secret. 
Channel C_cons,101 from Figure <ref> models
a checker that does that (by eliminating the  command within 
the loop in 123) when the attacker's low-input 
is a=101.
This channel's posterior 
Bayes vulnerability is π̂C_123,101=0.4384, 
which brings the multiplicative
Bayes leakage down to an increase of only about 0.05%.
However, the expected running time goes up to 3 iterations 
(an increase of about 135% w.r.t. that of C_123,101).

r0.61



[ 2*C_123,101          y=          y=          y=          y=;                    (,1)        (,2)        (,3)        (,3);       x=000           1           0           0           0;       x=001           1           0           0           0;       x=010           1           0           0           0;       x=011           1           0           0           0;       x=100           0           0           1           0;       x=101           0           0           0           1;       x=110           0           1           0           0;       x=111           0           1           0           0;             ]
  
[ 2*C_cons,101           y=           y=;                      (,3)         (,3);        x=000            1            0;        x=001            1            0;        x=010            1            0;        x=011            1            0;        x=100            1            0;        x=101            0            1;        x=110            1            0;        x=111            1            0;              ]

Channels C_da modeling the password
checker for defender's action d and attacker's action a.




Seeking some compromise between security and efficiency, assume that 
the defender can employ password-checkers that perform the bitwise 
comparison among low-input a and secret password x in 
different orders.
More precisely, there is one version of the checker for every 
possible order in which the index i 
ranges in the control of the loop.
For instance, while 123 checks the bits in the order 
1,2,3, the alternative algorithm 231 uses the order 
2,3,1.

To determine a defender's best choice of which versions of the checker to run,
we model this problem as game.
The attacker's actions = {000, 001, …, 111} are all possible low-inputs
to the checker, 
and the defender's = {123,   132,   213,   231,   312,  321} are all orders
to perform the comparison.
Hence, there is a total of 48 possible channels 
C_ad:×→, one for
each combination of d∈, a∈.

In our framework, the utility of a mixed strategy profile
(δ, α) is given by
(δ,α)  = a←α πdδC_d a.
For each pure strategy profile (d,a), the payoff of the game will be the posterior 
Bayes vulnerability
of the resulting channel C_da
(since, if we measuring leakage, the prior vulnerability is the same
for every channel once the prior is fixed).
Table <ref> depicts such payoffs.
Note that the attacker's and defender's actions substantially affect
the effectiveness of the attack:
vulnerability ranges between 0.4934 and 0.9311 
(and so multiplicative leakage is in the range
between an increase of 12% and one of 112%).
Using techniques from <cit.>, we can compute
the best (mixed) strategy for the defender in this game, which turns out 
to be
δ^*  = (0.1667, 0.1667, 0.1667, 0.1667, 0.1667, 0.1667).
This strategy is part of an equilibrium and guarantees that for any choice
of the attacker the posterior Bayes vulnerability is at most 0.6573
(so the multiplicative leakage is bounded by 50%, an intermediate value
between the minimum of about 12% and the maximum of about 112%).
It is interesting to note that the
expected running time, for any action
of the attacker, is bounded by at most
r0.71



[                                       2c                    8cAttacker's action a;                                     2-10                                   U(d,a)                                      000                                      001                                      010                                      011                                      100                                      101                                      110                                      111; 2-102-106*[origin=c]90Defender'saction d                                      123                                   0.7257                                   0.7257                                   0.9311                                   0.9311                                   0.6577                                   0.6577                                   0.7122                                   0.7122;                                     2-10                                      132                                   0.8900                                   0.9311                                   0.8900                                   0.9311                                   0.7122                                   0.7122                                   0.7122                                   0.7122;                                     2-10                                      213                                   0.5068                                   0.5068                                   0.9311                                   0.9311                                   0.4934                                   0.4934                                   0.7668                                   0.7668;                                     2-10                                      231                                   0.5068                                   0.5068                                   0.7668                                   0.9311                                   0.5068                                   0.5068                                   0.7668                                   0.9311;                                     2-10                                      312                                   0.7257                                   0.9311                                   0.7257                                   0.9311                                   0.7122                                   0.8766                                   0.7122                                   0.8766;                                     2-10                                      321                                   0.6712                                   0.7122                                   0.7257                                   0.9311                                   0.6712                                   0.7122                                   0.7257                                   0.9311;                                     2-10 ]



Utility for each pure strategy profile.




2.3922 iterations
(an increase of only 87% w.r.t. the channel _123),
which is below 
the worst possible expected 3 iterations of 
the constant-time password checker.





§ RELATED WORK


Many studies have applied game theory to analyses of security 
and privacy in networks <cit.>,
cryptography <cit.>,
anonymity <cit.>, 
location privacy <cit.>, and
intrusion detection <cit.>,
to cite a few.
See <cit.> for a survey. 

In the context of quantitative information flow, 
most works consider only passive attackers.
Boreale and Pampaloni <cit.> consider adaptive
attackers, but not adaptive defenders, and show that 
in this case the adversary's optimal strategy can 
be always deterministic.
Mardziel et al. <cit.> propose a model for both adaptive 
attackers and defenders, but in none of their extensive case-studies 
the attacker needs a probabilistic strategy to maximize leakage.
In this paper we characterize when randomization is necessary, 
for either attacker or defender, to achieve optimality in our general 
information leakage games.

Security games have been employed to model and analyze payoffs between 
interacting agents, especially between a defender and an attacker.
Korzhyk et al. <cit.> theoretically analyze security 
games and study the relationships between Stackelberg and Nash Equilibria 
under various forms of imperfect information.

Khouzani and Malacaria <cit.> study leakage properties when perfect
secrecy is not achievable due to constraints on the allowable size of the conflating
sets, and provide universally optimal strategies for a wide class of entropy measures,
and for g-entropies.
These works, contrarily to ours, do not consider games with hidden 
choice, in which optimal strategies differ from traditional game-theory.

Several security games have modeled leakage when the sensitive
information are the defender's choices themselves, rather than a system's 
high input.
For instance, Alon et al. <cit.> propose 
zero-sum games in which a defender chooses probabilities of secrets and an attacker chooses and learns some of the defender's secrets.
Then they present how the leakage on the defender's secrets gives influences on the defender's optimal strategy.

More recently, Xu et al. <cit.> show zero-sum games in which the attacker 
obtains partial knowledge on the security resources that the defender protects, and provide 
the defender's optimal strategy under the attacker's such knowledge.

Regarding channel operators, sequential and parallel composition of channels
have been studied (e.g., <cit.>), but we are unaware of any
explicit definition and investigation of hidden and visible choice operators.
Although Kawamoto et al. <cit.> implicitly use the hidden choice to model 
a probabilistic system as the weighted sum of systems, they do not derive the set 
of algebraic properties we do for this operator, and for its interaction with the 
visible choice operator.







§ CONCLUSION AND FUTURE WORK


In this paper we used protocol composition to model the introduction of noise 
performed by the defender to prevent leakage of sensitive information.
More precisely, we formalized visible and hidden probabilistic choices of different protocols.
We then formalized the interplay between defender and adversary in a game-theoretic framework adapted to the specific issues of QIF, where the payoff is information leakage. 
We considered various kinds of leakage games, depending on whether players act simultaneously or sequentially, and whether the choices of the defender are visible or not to the adversary.
We established a hierarchy of these games, and provided methods for finding the optimal strategies (at the points of equilibrium) in the various cases.

As future research, we would like to extend leakage games to the 
case of repeated observations, i.e., when the attacker can 
observe  the outcomes of the system in successive runs,  under the 
assumption that both attacker and defender may change the 
channel in each run. 
We would also like to extend our framework to non zero-sum games, in which
the costs of attack and defense are not equivalent, and to analyze differentially-private mechanisms.



  
*Acknowledgments

The authors are thankful to anonymous reviewers for helpful comments.
This work was supported by JSPS and Inria under the project LOGIS of the Japan-France AYAME Program,
and by the project Epistemic Interactive Concurrency (EPIC) from the STIC 
AmSud Program.
Mário S. Alvim was supported by CNPq, CAPES, and FAPEMIG.
Yusuke Kawamoto was supported by JSPS KAKENHI Grant Number JP17K12667.


plain










§ PROOFS OF TECHNICAL RESULTS



In this section we provide proofs for our technical results.






 §.§ Preliminaries for proofs


We start by providing some necessary background for
the subsequent technical proofs.

Definition <ref> states that
two compatible channels (i.e., with the same input space)
are equivalent if yield the same value of vulnerability 
for every prior and every vulnerability function.
The result below, from the literature, provides 
necessary and sufficient conditions for two channels being 
equivalent.
The result employs the extension of channels with an all-zero 
column as follows.
For any channel C of type ×→, 
its zero-column extension C^0 is the channel of type 
×(∪{y_0}) →,
with y_0∉, s.t. C^0(x,y) = C(x,y) for all 
x∈, y∈, and C^0(x,y_0) = 0 for all x ∈.

[Characterization of channel equivalence <cit.>]Lemmaresequivalentchannelsconditions

Two channels C_1 and C_2 are equivalent iff
every column of C_1 is a convex combination of 
columns of C_2^0, and every column of C_2 is a 
convex combination of columns of C_1^0.


Note that the result above implies that for being equivalent,
any two channels must be compatible.






 §.§ Proofs of Section <ref>


*


Since hidden choice is defined as a summation
of matrices, the type of iμ C_i is 
the same as the type of every C_i in the family.

To see that iμ C_i is a channel
(i.e., all of its entries are non-negative, and all
of its rows sum up to 1),
first note that, since each C_i in the family is a 
channel matrix, C_i(x,y) lies in the interval 
[0,1] for all x ∈, y∈.
Since μ is a set of convex coefficients, from 

the definition of hidden choice
it follows that
also ∑_i ∈μ(i)C_i(x,y) must lie 
in the interval [0,1] for every x,y.

Second, note that for all x ∈:

    ∑_y∈(iμ C_i)(x,y)
    =    ∑_y∈∑_i ∈μ(i)C_i(x,y)    (def. of hidden choice)
    
    =    ∑_i ∈μ(i) ∑_y∈ C_i(x,y) 
    
    =    ∑_i ∈μ(i) · 1    (C_i:×→ are channels)
    
    =     1    (μ is a prob. dist.)



*


Visible choice applied to a family {C_i} of channels 
scales each matrix C_i by a factor μ(i), which
preserves the type ×_i→ 
of each matrix, and then concatenates all the matrices so produced,
yielding a result of type
×( _i ∈_i) →.

To see that iμ C_i is a channel
(i.e., that all of its entries are non-negative, and that
all rows sum-up to 1), note that each element of the 
visible choice on the family {C_i} can be denoted by 
(iμ C_i)(x,(y,j)),
where x ∈, j ∈, and y ∈_j.
Then, note that for all x ∈, j ∈, and y ∈_j:

    (iμ C_i)(x,(y,j))  
    =    (_i ∈μ(i)C_i)(x,(y,j))    (def. of visible choice)
    
    =    (μ(j)C_j)(x,y)    (def. of concatenation)
    
    =    μ(j)C_j(x,y)    (def. of scalar mult.)

which is a non-negative value, since, both μ(j) and 
C_j(x,y) are non-negative.

Finally, note that for all x ∈:

    ∑_j ∈
     y ∈_j(iμ C_i)(x,(y,j))
    =    ∑_j ∈
     y ∈_jμ(j)C_j(x,y)    (by Eq. (<ref>))
     
    =    ∑_j ∈μ(j) ∑_y ∈_j C_j(x,y)    
     
    =    ∑_j ∈μ(j) · 1    (C_j:×_j→ are channels)
    
    =     1    (μ is a prob. dist.)



*





  * Idempotency of hidden choice:

    iμC_i 
    =    ∑_iμ(i)C_i   (def. of hidden choice)
    
    =    ∑_iμ(i)C    (since every C_i=C)
    
    =     C ∑_iμ(i)    
    
    =     C    (since μ is a prob. dist.)



  * Idempotency of visible choice:

    iμC_i 
    =    _iμ(i)C_i   (def. of visible choice)
    
    =    _iμ(i)C    (since every C_i=C)
    ≡     C    (by Lemma <ref>)


In the above derivation, we can apply 
Lemma <ref>
because every column of the channel on each side of the equivalence 
can be written as a convex combination of the zero-column extension
of the channel on the other side.



*





  * 
    iμjη C_i j 
    =    iμ( ∑_jη(j) C_i j)    (def. of hidden choice)
     
    =    ∑_iμ(i) ( ∑_jη(j) C_i j)    (def. of hidden choice)
     
    =    ∑_i,jη(i)η(j) C_i j   (reorganizing the sums)
     
    =    iμjη C_i j   (def. of hidden choice)



  * 
    iμjη C_i j 
    =    iμ( _j C_i j)    (def. of visible choice)
     
    =    _iμ(i) ( _jη(j) C_i j)    (def. of visible choice)
    ≡   _i jμ(i) η(j) C_i j   (by Lemma <ref>)
     
    =    iμjη C_i j   (def. of visible choice)

In the above derivation, we can apply 
Lemma <ref>
because every column of the channel on each side of the equivalence 
can be written as a convex combination of the zero-column extension
of the channel on the other side.


  * 
    iμjη C_i j 
    =    iμ( _j C_i j)    (def. of visible choice)
     
    =    ∑_iμ(i) ( _jη(j) C_i j)    (def. of hidden choice)
    ≡    _jη(j) ( ∑_iη(i) C_i j)    (by Lemma <ref>)
     
    =    jηiμ C_i j   (def. of operators)

In the above derivation, we can apply 
Lemma <ref>
because every column of the channel on each side of the equivalence 
can be written as a convex combination of the zero-column extension
of the channel on the other side.




*




  * Let us call ×→ the 
type of each channel C_i in the family {C_i}.
Then:

    πiμ C_i 
    =    π_iμ(i)C_i   (def. of hidden choice)
     
    =    ∑_y ∈ p(y) ·π(·) ∑_iμ(i)C_i(·,y) /p(y)   (def. of posterior )
     
    =    ∑_y ∈ p(y) ·∑_iμ(i)π(·) C_i(·,y) /p(y)   
    ≤    ∑_y ∈ p(y) ·∑_iμ(i) π(·) C_i(·,y) /p(y)   (by convexity of )
     
    =    ∑_iμ(i) ∑_y ∈ p(y) π(·) C_i(·,y) /p(y)   
    
    =    ∑_iμ(i) πC_i

where p(y) = ∑_x∈π(x) ∑_iμ(i)C_i(x,y).


  * Let us call ×_i→ the 
type of each channel C_i in the family {C_i}.
Then:

    πiμ C_i
    =    π_iμ(i)C_i   (def. of visible choice)
     
    =    ∑_y ∈ p(y) ·π(·) _iμ(i)C_i(·,y) /p(y)   (def. of posterior )
     
    =    ∑_y ∈ p(y) ·_iμ(i)π(·) C_i(·,y) /p(y)   
     
    =    ∑_y ∈ p(y) ·∑_iμ(i) π(·) C_i(·,y) /p(y)   (see (*) below)
     
    =    ∑_iμ(i) ∑_y ∈ p(y) π(·) C_i(·,y) /p(y)   
    
    =    ∑_iμ(i) πC_i

where p(y) = ∑_x∈π(x) ∑_iμ(i)C_i(x,y), and 
step (*) holds because in the vulnerability of a concatenation of matrices
every column will contribute to the vulnerability in proportion to its weight
in the concatenation, and hence it is possible to break the vulnerability of a 
concatenated matrix as the weighted sum of the vulnerabilities of its sub-matrices.




*


To see that U(μ,η) is convex on μ, note that:

    U(μ,η) 
    =    πiμ jη  C_i j   (by definition)
    ≤    ∑_iμ(i)  πjη  C_i j   (by Theorem <ref>)


To see that U(μ,η) is linear on η, note that:

    U(μ,η) 
    =    πiμ jη  C_i j   (by definition)
    
    =    πjη iμ  C_i j   (by Prop. <ref>)
    
    =    ∑_jη(j)  πiμ  C_i j   (by Theorem. <ref>)











§ PROPERTIES OF BINARY VERSIONS OF CHANNEL OPERATORS


In this section we derive some relevant properties of 
the binary versions of the hidden and visible choice 
operators.
We start with results regarding each operator
individually.

[Properties of the binary hidden choice]Propositionrespropertiesbinaryhiddenchoice

For any channels C_1 and C_2 of the same type, 
and any values 0 ≤ p,q ≤ 1, 
the binary hidden choice operator satisfies the following 
properties:


  * Idempotency:
C_1p C_1 = C_1

  * Commutativity: 
C_1p C_2 = C_2p̅ C_1

  * Associativity: 

    C_1p (C_2q C_3) = ( 1/q· C_1p C_2) qp̅· C_3
 
if q ≠ 0.

  * Absorption: 

    (C_1p C_2) q (C_1r C_2)
    = C_1(pq + q̅r) C_2.





We will prove each property separately.



  * Idempotency: 

    C_1p C_1
    =     p · C_1 + p̅· C_1   (def. of hidden choice)
    
    =     (p + p̅) · C_1   
    
    =     C_1   (p+p̅=1)



  * Commutativity:

    C_1p C_2
    =     p · C_1 + p̅· C_2   (def. of hidden choice)
    
    =    p̅· C_2 + p · C_1   
    
    =     C_2p̅ C_1   (def. of hidden choice)



  * Associativity:

    C_1p ( C_2q C_3 ) 
    
    =     p · C_1 + p̅ ( q · C_2 + q̅· C_3 )    (def. of hidden choice)
    
    =    p · C_1 + p̅q · C_2 + p̅q̅· C_3   
    
    =    q(p (1/q· C_1) + p̅· C_2) + q̅(p̅· C_3)    
    
    =    (1/q· C_1p C_2) qp̅· C_3   (def. of hidden choice)



  * Absorption: First note that:

    (C_1p C_2) q (C_1r C_2) 
    
    =    q (p C_1 + p̅ C_2) + q̅ (r C_1 + r̅ C_2)    (def. of hidden choice)
    
    =    pq C_1 + p̅q C_2 + q̅r C_1 + q̅r̅ C_2
    
    =    (pq + q̅r) C_1 + (p̅q + q̅r̅) C_2
    
    =    C_1(pq + q̅r) C_2   (*)

To complete the proof, note that in step (*) above,
pq + q̅r and p̅q + q̅r̅ form
a valid binary probability distribution (they are both 
non-negative, and they add up to 1), then apply the
definition of hidden choice.




[Properties of binary visible choice]Propositionrespropertiesbinaryvisiblechoice

For any compatible channels C_1 and C_2, 
and any values 0 ≤ p,q ≤ 1, 
the visible choice operator satisfies the following 
properties:


  * Idempotency: 
C_1p C_1≡ C_1

  * Commutativity: 
C_1p C_2≡ C_2p̅ C_1

  * Associativity: 
C_1p (C_2q C_3) ≡ ( 1/q· C_1p C_2) 
qp̅· C_3
if q ≠ 0.





We will prove each property separately.



  * Idempotency: C_1p C_1≡ C_1, by 
immediate application of Lemma <ref>,
since every column of the channel on each side of the equivalence 
can be written as a convex combination of the zero-column extension
of the channel on the other side.


  * Commutativity:

    C_1p C_2 
    =     p · C_1p̅· C_2   (def. of visible choice)
    ≡    p̅· C_2 p · C_1   (by Lemma <ref>)
    
    =    C_2p̅ C_1   (def. of visible choice).

In the above derivation, we can apply 
Lemma <ref>
because every column of the channel on each side of the equivalence 
can be written as a convex combination of the zero-column extension
of the channel on the other side.


  * Associativity:

    C_1p ( C_2q C_3 ) 
    =     p · C_1p̅ ( q · C_2q̅· C_3 )    (def. of visible choice)
    ≡     p · C_1( p̅q · C_2p̅q̅· C_3)    (by Lemma <ref>)
    
    =     q(p (1/q· C_1) p̅· C_2) q̅(p̅· C_3)    
    
    =    (1/q· C_1p C_2) qp̅· C_3   (def. of visible choice)

In the above derivation, we can apply 
Lemma <ref>
because every column of the channel on each side of the equivalence 
can be written as a convex combination of the zero-column extension
of the channel on the other side.




Now we turn our attention to the interaction between
hidden and visible choice operators.

A first result is that hidden choice does not distribute 
over visible choice.
To see why, note that C_1p (C_2q C_3)
and (C_1p C_2) q (C_1p C_3)
cannot be both defined: if the former is defined, then C_1 must have
the same type as C_2q C_3, whereas if the
latter is defined, C_1 must have the same type as C_2, but
C_2q C_3 and C_2 do not have the same type
(they have different output sets).

However, as the next result shows, visible choice distributes over 
hidden choice.

[Distributivity of p over q]Propositionresdistributivity

Let C_1, C_2 and C_3 be compatible channels,
and C_2 and C_3 have the same type.
Then, for any values 0 ≤ p,q ≤ 1:

    C_1p (C_2q C_3) ≡ (C_1p C_2) q (C_1p C_3).





    C_1p (C_2q C_3) 
    
    =     (C_1q C_1) p (C_2q C_3)    (idempotency of visible choice)
    
    =     p (q · C_1 + q̅· C_1) p̅(q · C_2 + q̅· C_3)    (def. of operators)
    
    =     (pq · C_1 + pq̅· C_1)  (p̅q · C_2 + p̅q̅· C_3)    
    ≡      (pq · C_1p̅q · C_2) + (pq̅· C_1p̅q̅· C_3)    (by Lemma <ref>)
    
    =     q(p · C_1p̅· C_2) + q̅(p · C_1p̅· C_3)    
    
    =     q(C_1p C_2) + q̅(C_1p C_3)     (def. of visible choice)
    
    =     (C_1p C_2) q (C_1p C_3)     (def. of hidden choice)

In the above derivation, we can apply 
Lemma <ref>
because every column of the channel on each side of the equivalence 
can be written as a convex combination of the zero-column extension
of the channel on the other side.




