Games for Security under Adaptive Adversaries
Timos Antonopoulos

Tachio Terauchi

Yale University
New Haven, Connecticut, 06511, USA
Email: timos.antonopoulos@yale.edu

Waseda University
Shinjuku-ku, Tokyo, 169-8555, Japan
Email: terauchi@waseda.jp

from [5], [12]. The function LL is a login program that checks
if the input guess matches the secret password. Note thatthe running time of the program is proportional to the lengthof the common prefix of password and guess. Therefore,
the program is insecure against an adaptive attacker who can
observe the running times as he will be able to reveal theelements of password iteratively by crafting appropriate
inputs to be used as guess each time.1
More concretely, suppose that the alphabet of the password
is the binary {0, 1} for simplicity. Then, in the setting of
information flow, the situation is formalized as the program
Pins (s, v) that takes secret input s and public input v wheres, v ∈ {0, 1}` , ` is the length of the password, and Pins (s, v)
outputs the length of the common prefix of s and v, alongwith a boolean that expresses whether s is equal to v. Pins
I. I NTRODUCTION
is not non-interferent [6], [16], [22], [24] because there exist
This work is concerned with analyzing systems that operate inputs v, s1 , s2 such that Pins (s1 , v) 6= Pins (s2 , v), for example,
on secret information, such as users’ passwords. Information v = 0000, s1 = 0100, and s2 = 0010. (Formally, P is said toflow analysis [6], [16], [22], [24] is a well-established approach be non-interferent if and only if P(s1 , v) = P(s2 , v) for all
to detecting or proving the absence of attacks that steal the public inputs v and secret inputs s1 and s2 .) In this way, the nonsecrets by observing the execution behavior. For instance, non- interference based method of [5] is able to successfully detect
interference, which says that there is no information leakage the vulnerability. However, consider a correct login programfrom observable channels, has been used to check security that only reveals whether the guess matches the password oragainst timing channel attacks [1], [5]. Further, quantitative not. Such a program can be described as Psec (s, v) where
information flow is an extension of non-interference that maps Psec (s, v) = true if s = v and Psec (s, v) = false otherwise.
observable channels to the quantity of information leak, where Non-interference is insufficient to show the security of Psec .
information leak is formalized by information-theoretic notions Indeed, Psec (s1 , v) 6= Psec (s2 , v) for any v = s1 6= s2 .
Quantitative information flow (QIF) has been proposed as asuch as Shannon entropy [4], [8], [19], [25]. It has been applied
to measure the degree of security of systems against various formalism to cope with situations such as the above [4], [8],[19], [25].2 QIF maps programs to real numbers denoting theclasses of attacks [7], [9], [11], [27].
quantity of information leak so that the larger the leak quantity
the less secure the program. For example, the capacity QIF
Program Leaky Loginmeasure defines information leak to be the number of different
def LL(password, guess):for (int i = 0; i < guess.length; ++i):
outputs obtained by varying the secret input, maximum overif (password[i] != guess[i]):all public inputs. (Incidentally, capacity is equivalent to thereturn false
maximum Shannon entropy over the distributions of secrets,
return true
and to min entropy for uniformly distributed secrets [19].3 )Note that the capacity is 1 for non-interferent programs, 2 forFig. 1: Leaky login program

Abstract—This work explores methods for proving and disproving security of systems under adaptive adversaries. Adaptive
adversaries are ones which make their next move based on theprevious observations. Our first contribution is a new game based
characterization of security. We show that the game accurately
captures security of deterministic and probabilistic systems
against adaptive (probabilistic) adversaries. In addition, we build
on top of the game characterization and present techniques that
expedite proving the existence of attacker and defender strategies,
and consequently proving security or vulnerability of systems.
The first is what we call attack (and defense) slopes which give
simple sufficient criteria for existence of winning strategies (forattacker and defender). The second is reductions of one gameto another achieved by mapping a strategy of one to that of
the other. We show that such reductions can prove or disprovesecurity by reducing from a game of a secure system or reducing
to that of a non-secure system.

This work concerns analyzing the security of systems under
adaptive attacks in which the adversaries can make their next
move based on the previous observations. By itself, information
flow analysis is often insufficient for accurately detecting thepossibility of adaptive attacks or proving the absence thereof.
For instance, consider the code snippet shown in Fig. 1, adopted

1 Often, the output of the program (regular channel) is treated separatelyfrom observations related to the running time (side channel), but in this work
both are treated the same, bundled as an observation.
2 Another, orthogonal, approach is declassification which permits information
marked as “declassified” to leak for free [13], [17], [26] (also implicitly usedin [5]). However, the security would now depend on the correctness of thedeclassification policy.
3 Technically, capacity is defined to be the log of the number of outputs.

Psec , and ` for Pins . Hence, based on the capacity measure, illustrates the games on deterministic systems with uniformlywe may conclude that Psec is reasonably secure, as it only distributed secrets, and Section V presents the slope-based
leaks a constant amount of information regardless of the secret approximations for such systems. Section VI presents the gamesize. However, it is easy to construct a situation in which the reductions. We discuss related work in Section VII and conclude
adversary is able to efficiently decipher the secret despite the the paper in Section VIII.
program only having a constant capacity QIF. For instance,
II. P RELIMINARIES
let Piq (s, v) be such that s ∈ {0, 1}` , v ∈ {1, ..., `}, andWe write N for the set of natural numbers {0, 1, . . .}, andPiq (s, v) = s[v − 1]. That is, Piq (s, v) leaks the v-th elementof s (see Fig. 2 in Section V). The capacity of Piq is 2 as there N+ for the set of positive natural numbers N \ {0}. R is theare only two possible outputs, but Piq is efficiently attackable set of real numbers, and we denote by [r1 , r2 ] the set of real
numbers {r ∈ R | r1 ≤ r ≤ r2 }. For a set D, we write D∗
by simply querying the secret one element at a time.
To address the issue, researchers have suggested to extend for the set of finite sequences of elements from D, and denote∗~ We denote thethe information flow analysis approach to compute QIF over elements of D with the vector notation d.
∗~~multiple attacker queries [15], and more generally over adaptive length of such a sequence with |d|. If d ∈ D and b ∈ D,~
attack strategies [7], [10], [11]. The latter works introduced the we denote with d · b the sequence obtained by appending b to
~ resulting in a sequence of length |d|~ + 1. We
notion of attack tree which is an important conceptual device the sequence d,denote with ε the empty sequence.
for reasoning about security against adaptive attacks.
As standard, we assume security parameter that describes
In this paper, we build on the previous works to explore
thesize of secrets. A system (or program) P is an indexed
new methods for accurately analyzing the security of systems
under adaptive adversaries. Our first contribution is a new family of functions (indexed by the security parameter) thatgame-based characterization of security, in which there are represent the input-output relation of the system. S is a securitytwo players attacker and defender such that the existence of parameter-indexed family of sets of secrets, I is a securitya winning strategy for the attacker implies that the system is parameter-indexed family of sets of attacker-controlled inputs,
insecure and that for the defender implies that it is secure. The and O is a security-parameter indexed family of observations.
game is inspired by the notion of attack trees mentioned above. A security parameter is a natural number that represents the
However, whereas the previous works have used the idea to size of secrets, and we write S` for the set of secrets of size
compute QIF for a particular attack strategy or maximum QIF `, and I` and O` for the corresponding attacker inputs andover all attack strategies of some bounded lengths, we show observations. Each indexed function P` is a function fromthat our game is able to accurately capture the existence or the S` × I` to probability distributions over O` . That is, for each∈ S` × I` , P` (s, v) = µ for some µ : O` → [0, 1] such
impossibility of efficient attacks, where efficiency is measured (s, v)P
by bounds on the number of attack steps and the probability of that o∈O` µ(o) = 1. We omit the security parameter when
the attack success. Importantly, our approach is able to derive it is clear from the context and write S, I, O, and P for S` ,I` , O` , and P` , respectively.
bounds that are parametric to size of the secrets.
The support of a probability distribution µ : O → [0, 1] is
Further, building on the game-based characterization, we
definedas standard: supp(µ) = {o ∈ O | µ(o) > 0}. For apropose approximation techniques, called attack slopes andprogramP , v ∈ I, and o ∈ O, we write P −1 (v, o) for the set
defense slopes, that can be used to show the existence of−1
attacker and defender winning strategies. Currently, the slope {s ∈ S | o ∈ supp(P (s, v))}. Roughly, P (v, o) is the set oftechnique is limited to deterministic systems and uniformly- secrets that have a non-zero probability of making P output odistributed secrets, but we expect it to be extendable to more on input v. We also extend the notation to a sequence of inputs
general settings. Finally, we continue capitalizing on the notion and observations so that for ~v = v1 , . . . , vn and ~o = o1 , . . . , on ,−1of game strategies to propose a form of reduction from one P (~v , ~o) is the set of secrets that have a non-zero probability
game to another, that aims to reuse the work done on proving of making P output oi on input vi for each i ∈ {1, . . . , n}.
−1−1
a system secure or vulnerable, on the analysis of new systems. Formally, P (~v , ~o) is defined inductively by: P (ε, ε) = S−1−1−1
The main contributions of the paper are summarized below. and P (~v · v, ~o · o) = P (~v , ~o) ∩ P (v, o).
We say that P` is deterministic if for all (s, v) ∈ S` × I` ,(1) A new game-based characterization of security under P (s, v) is a point mass (i.e. P (s, v)(o) = 1 for some o ∈ O ).
```adaptive adversaries (Section III).
We say that P is deterministic when P` is deterministic for(2) Approximation techniques called attack slopes and defense each `. In literature, deterministic systems are sometimes also
slopes (Section V).
called noiseless to contrast with the case where the attacker’s(3) Reductions between games that can be used to show that observation is subject to noise and cannot be made exact.
one game (and hence the corresponding system) is less For example, often in timing attacks, the attacker is not able
or more secure than the other (Section VI).
to know exactly how many loop iterations have taken place.
The rest of the paper is organized as follows. Section II Such noisy observations may be modeled by the more generalprovides some preliminary definitions. In Section III, we define probabilistic systems.
the games and prove that they accurately characterize the
For any two functions f : N+ → R and g : N+ → R, wesecurity of systems against adaptive adversaries. Section IV denote with (f op g), for op ∈ {+, −, ×, /}, the function oftype N+ → R that maps any n ∈ N+ to f (n) op g(n). For
III. G AMES
two functions f : N → R and g : N → R, we say that f > g, Definitions: For a program P , s ∈ S` , v ∈ I, and o ∈ O
if for all n ∈ N, f (n) > g(n). By abuse of notation, we often we denote with µ(o | s, v) the probability that P (s, v) will
implicitly treat an expression e on the security parameter ` as output o. That is, µ(o | s, v) = P (s, v)(o). We use µ(s | ~v , ~o)the function λ` ∈ N+ .e.
to denote the probability that the secret is s conditionally on
An attacker is a randomized algorithm A that attempts having observed the sequence ~o when given inputs ~v , whereto discover the secret by making some number of queries |~v | = |~o|. Using Bayes’ theorem, it can be shown that for any
to the system. As standard, we assume that A has the full s ∈ S` , ~v ∈ I ∗ , w ∈ I, ~o ∈ O∗ , and q ∈ O,
knowledge of the system. Formally, A takes as inputs a functionµ(q | s, w) · µ(s | ~v , ~o)η : I` → O` and a natural number n ∈ N and outputs anµ(s | ~v · w, ~o · q) = P. (1)00 v, ~o)element of S` . We restrict A(η, n) to call η at most n manys0 ∈S` µ(q | s , w) · µ(s | ~times. As standard, A is only allowed to use η “extensionally” Here, µ(s | ε, ε) = µ (s) where µ is the prior probability``
as an oracle, and it is not allowed to see the internals of distribution associated with S (cf. Section II).
`
η. Intuitively, A is not allowed to see the internals of theFor ~v ∈ I ∗ , w ∈ I, ~o ∈ I ∗ , and q ∈ O, where |~v | = |~o|,system once a secret has been fixed. Namely, η will be of we denote with µ(q | w; ~v , ~o) the probability of observing
the form λv ∈ I` .P` (s, v) for some s ∈ S` that the attacker the output q, by feeding the program the input w, underaims to recover. We impose no restriction on how the attacker the condition that we have already observed the sequencechooses the inputs to the system. Importantly, he may choose of observations ~o given inputs ~v . More formally, the definition
the inputs based on the outputs of previous oracle queries. of µ(q | w; ~v , ~o) is
Such an attacker is said to be adaptive [11].
Xµ(q | w; ~v , ~o) =µ(s | ~v , ~o) · µ(q | s, w).
(2)
The set of secrets S` are equipped with probability distribus∈S`
tion µ` : S` 7→ [0, 1]. For a distribution of secrets µ, we writePrs←µ [A] for the probability that the event A happens when Thus, from (1) and (2), for any s ∈ S` ,the secret s is chosen randomly according to the distribution µ.
µ(q | s, w) · µ(s | ~v , ~o)Therefore, for instance, Prs←µ [A(λv ∈ I` .P` (s, v), n) = s],(3)µ(s | ~v · w, ~o · q) =µ(q | w; ~v , ~o)is the probability that the attacker A recovers the secret s inn many queries to the system, when s is chosen randomly and therefore, for any s ∈ S` , where µ(s | ~v · w, ~o · q) =6 0,
according to the distribution µ. We formalize the notion ofµ(q | s, w) · µ(s | ~v , ~o)security against adaptive attackers as follows.
µ(q | w; ~v , ~o) =.
µ(s | ~v · w, ~o · q)
Definition II.1 (Security). Let  : N → [0, 1], f : N → N be
two mappings. We say that P is (f, )-secure if for any ` ∈ N+ Note that for any s ∈ S` , if µ(s | ~v · w, ~o · q) 6= 0 thenµ(s | ~v , ~o) 6= 0 and µ(q | s, w) 6= 0.
and any attacker A, we have
Pr [A(λv.P (s, v), f (`)) = s] < (`)

s←µ`

Otherwise, the program P is (f, )-insecure.

Game: We define the n-round r-confidence game, for n ∈ N
and r ∈ [0, 1] as follows. The game is played by two players,
Attacker and Defender.4 At any round i ∈ N of the game,we denote the position by h~v , ~o, ri i, where |~v | = |~o| = i andri ∈ [0, 1]. At round 0, the position is hε, ε, r0 i, where r0 is theconfidence parameter r. At each round, from position h~v , ~o, ri i,
Attacker makes the first move, and choosesw ∈ I and aPfunction rw : O → [0, 1], such that ri = q∈O µ(q | w; ~v , ~o) ·rw (q). Defender then replies with an observation q ∈ O. The
new position is then h~v · w, ~o · q, rw (q)i. In other words, theinput w is appended to the vector of inputs, the observation q
is appended to the vector of observations, and the confidence
parameter ri+1 is set to rw (q). Defender wins the game at roundn, at position h~v , ~o, rn i exactly when maxs∈S` µ(s | ~v , ~o) < rn .
Otherwise, Attacker wins at round n.

Notice that for any program P , and functions  : N → [0, 1]
and f : N → N the following hold:0• If P is (f, )-secure, then it is also (f,  )-secure for any00 : N → [0, 1] such that  <  .
0• If P is (f, )-insecure, then it is also (f , )-insecure for00
any f : N → N such that f < f .
It should be noted that this definition of security is used inour earlier work [23] and it also closely corresponds to thedefinition used in the DARPA STAC program [20].
Given an attacker algorithm A, we denote with µA theprobability distribution with which the attacker selects a public
input w ∈ I to feed into the program and observe the output.
Remark III.1. Defender, when it’s time for her move, canMore formally, for any ~v ∈ I ∗ , ~o ∈ O∗ with |~v | = |~o| andchoose any q ∈ O, without any condition on the probabilityw ∈ I, we denote with µA [~v , ~o](w) the probability that A willwith which q may be observed at that point. In fact, thechoose w ∈ I for the next input, after having observed theprobability of q being observed on public input w ∈ I, having
sequence ~o when having fed to the program the sequence of
already observed ~o on inputs ~v , could just as well be 0. In other
inputs ~v in the previous |~v | queries. By defining the attacker
algorithm in such a way, we allow both deterministic and
4 For convenience, we choose Defender to be female and Attacker to berandomized attacker algorithms.
male.

v ,~
o)
words µ(q | w; ~v , ~o) could be 0. Notice however, that for all Then, since µ(s | ~v · w, ~o · q) = µ(q|s,w)·µ(s|~by Equationµ(q|w;~v ,~o)such Pq ∈ O, Attacker can set rw (q) to 0, without affecting the (3), we have that the above is equal tosum q∈O µ(q | w; ~v , ~o) · rw (q), and as such without affectingPPPv , ~o](w) · µ(q | w; ~v , ~o)·s∈Sw∈Iq∈O µA [~the condition for constructing rw . If Defender chooses such
µ(s
|
~
v
·
w,
~
o
·
q)
Pr[A
(w,q) (ηs , n − 1) = s]a q, then she is bound to lose the game because after any
P
P
=
µ
[~
v
,
~
o
](w)
·
µ(q | w; ~v , ~o)·w∈Isubsequent moves, maxs∈S` µ(s | ~v , ~o) will not be strictly less
P q∈O Av · w, ~o · q) Pr[A(w,q) (ηs , n − 1) = s]than rw (q) = 0 at the end.
s∈S µ(s | ~PP=v , ~o](w) · µ(q | w; ~v , ~o)·As a result, at each round, after a move w ∈ I by Attacker,w∈Iq∈O µA [~Pr[AP
we can think of Defender as internally choosing a secret s ∈ S,
s←µ[~
v
·w,~
o
·q]
(w,q) (ηs , n − 1) = s]P=v , ~o](w) · q∈O µ(q | w; ~v , ~o)·that is probabilistically still possible, and then choosing anw∈I µA [~Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s].
observation q that is possible after executing the underlying
program P on inputs w and s, without disclosing what s is.
Under this interpretation, notice that Defender is allowed to For any
P w ∈ I, let rw : O → [0, 1] be any function such thatr=v , ~o) · rw (q).
q∈O µ(q | w; ~keep changing her secret s as the game progresses.
N
Claim: The value ofA strategy for a player is a set of rules that describes how
PPv , ~o](w) · q∈O µ(q | w; ~v , ~o)·the player moves given the history of moves played already.
w∈I µA [~Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s]
We say that Defender wins the n-round r-confidence game, if
she has a strategy to do so for any Attacker moves, startingat position hε, ε, ri. Similarly, we say Attacker wins the n- is less than r for any attacker A, if and only if for any w ∈ I,
round r-confidence game if he has a strategy to do so, for any Xµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] < r,Defender moves.
q∈O
In Section IV, we go through an example for a simplified
version of this game, corresponding to deterministic systems for any attacker A.
and uniformly-distributed secrets. As stated in the theorem Proof of Claim: Suppose that the sum above is less than r
below, the game completely characterizes (f, )-security.
for any attacker A. Suppose for contradiction that there existw ∈ I, and attacker A, such that
Theorem III.2. A program is (f, )-secure if and only if, forX+all ` ∈ N , Defender wins the f (`)-round (`)-confidenceµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] ≥ r.
game.
q∈O

Proof: Given ~v ∈ I ∗ and ~o ∈ O∗ , we denote with µ[~v , ~o]Then define the attacker A to be such that µA [~v , ~o](w) = 1
the probability distribution over S` , conditionally upon havingand µA [~v , ~o](w0 ) = 0 for all w0 6= w. Clearly then the value
observed ~o when given inputs ~v . Formally, for any s ∈ S` ,of the expression above is greater than or equal to r for someµ[~v , ~o](s) = µ(s | ~v , ~o). For what follows, we fix arbitraryattacker A, which is a contradiction. For the other direction,` ∈ N+ .
if for all w ∈ I it holds that
We will show by induction on n, that for all n ∈ N+ ,Xr ∈ [0, 1] and for all ~v ∈ I ∗ and ~o ∈ O∗ , it holds thatµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] < r,Prs←µ[~v,~o] [A(λv.P (s, v), n) = s] < r for any attacker A, if q∈Oand only if Defender wins the n-round r-confidence game fromfor any attacker A, then the expression above is less than r.
position h~v , ~o, ri on P .
For the base case, we have that n = 0. Then it holds that  (Claim)Prs←µ[~v,~o] [A(λv.P (s, v), n) = s] < r for any attacker A Claim: It holds that for all w in I and all attackers A,
if and only if maxs∈S µ(s | ~v , ~o) < r. That is because in Xµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] < r,
the worst case Attacker will choose the most likely secret s
q∈O−1
from P (~v , ~o), and succeed with probability µ(s | ~v , ~o). We
proceed to the inductive case. For s ∈ S, let ηs = λv.P (s, v). if and only if, for all w ∈ I with respective rw , there is a
Furthermore, for any attacker A, and any w ∈ I, q ∈ O, we q ∈ O with µ(q | w; ~v , ~o) > 0 such that for any attacker A
denote with A(w,q) the attacker that corresponds to how theattacker A operates after observing q ∈ O on their query toPrs←µ[~v·w,~o·q] [A(ηs , n − 1) = s] < rw (q).
ηs with w ∈ I. Then, notice that===Prs←µ[~v,~o] [A(ηs , n) = s]P
Pr[A(ηs , n) = s]
Ps∈S µ(s | ~v , ~o) · P
µ(s
|
~
v
,
~
o
)
·
v , ~o](w)·s∈Sw∈I µA [~
P
µ(q
|
s,
w)
·
Pr[A
(w,q) (ηs , n − 1) = s]
q∈O P
P
P
µ(s
|
~
v
,
~
o
) · µA [~v , ~o](w)·
s∈S
w∈I
q∈O
µ(q | s, w) · Pr[A(w,q) (ηs , n − 1) = s].

Proofof Claim: By definition, for any rw it holds that r =Pv , ~o) · rw (q). For the only if direction, supposeq∈O µ(q | w; ~that for all w ∈ I and all attackers A,
Xµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] < r.
q∈OThen for all w ∈ I, any rw that satisfies the game condition
and any attacker A,Xµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] <
q∈O

X
q∈O

µ(q | w; ~v , ~o) · rw (q).

Therefore, for all w ∈ I, rw : O → [0, 1] and attacker A, there
is a q ∈ O such thatPrs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] < rw (q).

But then it also follows that there is some w ∈ I, somerw : O → [0, 1] such that for all q ∈ O, there is an attacker
A, namely A−
v , ~o) > 0 then(w,q) , such that if µ(q | w; ~Prs←µ[~v·w,~o·q] [A(ηs , n − 1) = s] ≥ rw (q)as required.
By the induction hypothesis, it holds that

 (Claim)Prs←µ[~v·w,~o·q] [A(ηs , n − 1) = s] < rw (q),For each q ∈ O, let A+
q be the attacker that maximises theirprobability of success for the remaining n − 1 moves under
the probability distribution of secrets µ[~v · w, ~o · q]. Formally,
let A be the collection of all attackers, and for any q ∈ O let
A+q be the attacker such thatfor any attacker A, if and only if Defender has a winning
strategy for the (n − 1)-round rw (q)-confidence game from theposition h~v · w, ~o · q, rw (q)i. We showed that for any attacker
A, Prs←µ[~v,~o] [A(ηs , n) = s] < r if and only if for all w ∈ Iwith respective rw , there is a q ∈ O with µ(q | w; ~v , ~o) > 0
such that for any attacker A

Prs←µ[~v·w,~o·q] [A+q (ηs , n − 1) = s] =max Prs←µ[~v·w,~o·q] [A(ηs , n − 1) = s].

Prs←µ[~v·w,~o·q] [A(ηs , n − 1) = s] < rw (q).

(4)

A∈A

Let then A+ denote the attacker that behaves like A+
q once theobservation q is fixed, for every q ∈ O. We know that for allw ∈ I, rw : O → [0, 1] and any attacker A, there is a q ∈ Osuch thatPrs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] < rw (q).
For any w ∈ I and rw : O → [0, 1], let q ∈ O be theobservation that works for the attacker A+ . Then by definitionof A+ (Eq. 4), it follows that for any w ∈ I and rw : O →[0, 1], q ∈ O is such thatPrs←µ[~v·w,~o·q] [A(ηs , n − 1) = s] < rw (q).
for any attacker A.
For the if direction, suppose that for some w in I and some
attacker A,Xµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A(w,q) (ηs , n − 1) = s] ≥ r.
q∈O

Change A to A− so that the inequality above is actually anequality. In other words, for some w in I and the attacker A− ,Xµ(q | w; ~v , ~o) · Prs←µ[~v·w,~o·q] [A−(w,q) (ηs , n − 1) = s] = r.
q∈O

Then define rw to be such that for each q ∈ O with µ(q |w; ~v , ~o) > 0,
rw (q) = Prs←µ[~v·w,~o·q] [A−(w,q) (ηs , n − 1) = s].
Notice that since the sum above is equal to r, this mapping rw
satisfies the conditions of the game. But then notice that thefollowing immediately follows. There is some w ∈ I, somerw : O → [0, 1] and the attacker A− is such that for all q ∈ O,
if µ(q | w; ~v , ~o) > 0 thenPrs←µ[~v·w,~o·q] [A−(w,q) (ηs , n − 1) = s] ≥ rw (q).

By the induction hypothesis it follows that the latter holds if
and only if for all w ∈ I with respective rw , there is a q ∈ Owith µ(q | w; ~v , ~o) > 0, such that Defender has a winning
strategy for the (n − 1)-round rw (q)-confidence game from theposition h~v · w, ~o · q, rw (q)i. Finally, this holds if and only if
Defender has a winning strategy for the n-round r-confidence
game from the position h~v , ~o, ri, as required.
The intuition behind Attacker choosing a function rw is
as follows. When Attacker chooses a public input w ∈ I,
he does not know what q ∈ O Defender may reply with, so
he assigns different success goals for each q ∈ O using the
mapping rw : O → [0, 1], and lets Defender know of how hehas weighed all the different scenarios. Defender then, consultsthese targets, and replies with a q ∈ O trying to maximize her
chances of winning. We remind the reader that Defender can
reply with any q ∈ O irrespectively of the probability that sucha q could be output by the program at input w. This is because
these probabilities have been encoded in the constraints of how
Attacker can construct the mapping rw .
Remark III.3. It is worth noting that for the special case wherer = 1, at each position h~v , ~o, ri, and for any move w ∈ I,
the only function rw that satisfies the condition for Attacker’s
moves, is the one where rw (q) = 1 for all q ∈ O, for whichµ(q | w; ~v , ~o) > 0 holds. At the same time, as pointed out inRemark III.1, Defender should only consider responses q that
could be observed on input w and some secret s that is still
possible, or in other words q should be in supp(P (s, w)) forsome s ∈ P −1 (~v , ~o). Therefore the game reduces to the simpler
version where Attacker chooses w ∈ I and Defender choosess ∈ S` that is still in play, and replies with any observationq ∈ O possible by executing P (s, w).
N
Remark III.4. Attacker in the game does not need to consider
probabilistic moves. As it can be seen by the proof of
Theorem III.2, and in particular the second claim in it, there
is a deterministic attack stategy that is optimal for Attacker.

IV. D ETERMINISTIC S YSTEMS AND U NIFORMD ISTRIBUTIONSIn this section, we consider a simplified version of a game inwhich programs are deterministic and the distribution of secrets
is uniform. Also, for simplicity we assume that for each `, theset of secrets S` comprises binary strings of length `, that is,S` = {0, 1}` and µ` (s) = 1/2` for all s ∈ S` . Note that, in
this setting, for any s ∈ S` and w ∈ I, µ(q | s, w) is equal
to 1 for exactly one q ∈ O, and 0 for all others. Similarly, it
can be shown by induction, that for all s ∈ S` , ~v ∈ I ∗ and~o ∈ O, µ(s | ~v , ~o) is equal to |P −11(~v,~o)| if s ∈ P −1 (~v , ~o) and
0 otherwise. Therefore, by Eq. (2) we have thatµ(q | w; ~v , ~o) =1|P −1 (~v ,~o)|1
|P −1 (~
v ·w,~o·q)|=|P −1 (~v · w, ~o · q)|,|P −1 (~v , ~o)|where r is the initial confidence parameter. With rv (o1 ) being 0,
rv (o2 ) would have to be 12 , if he wants to win the 18 -confidence
game and satisfy the constraint with his move. But with sucha high value of rv (o2 ), Defender can win that position since1
1|P −1 (v,o2 )| < 2 . The best move for Attacker is to choose
1
rv (o1 ) to be 12
and rv (o2 ) to be 14 . This way for both oi ,1
|P −1 (v,oi )| ≥ rv (oi ), and
−1

−1

1 )|
2 )|
rv (o1 ) · |P |S(v,o+ rv (o2 ) · |P |S(v,o
=
4|
4|
1
12
1
4
= 12 · 16 + 4 · 16 =1
8.

For the rest of this section, Prs←Q [A(λv.P (s, v), n) = s]denotes the probability that the attacker algorithm can find thesecret s (using at most n calls to the program), when the secretis drawn uniformly at random from the set Q. In contrast,
for Pr[A(λv.P (s, v), n) = s], where the subscript s ← Q is
missing, denotes Prs←{s} [A(λv.P (s, v), n) = s].

when P −1 (~v , ~o) and P −1 (~v · w, ~o · q) are non-empty, and 0
otherwise. Let us call the setting uniform-deterministic.
Example IV.1. Let Psec be the program from Section I. Let
For uniform-deterministic games, Theorem III.2 implies thatf (`) = 2 · ` and (`) = 1 for all ` ∈ N+ . We show that the+a program P is (f, )-secure if and only if for all ` ∈ N ,program is (2 · `, 1)-secure, that is Attacker cannot find the
Defender wins the f (`)-round (`)-confidence game, wheresecret with absolute certainty after 2 · ` many tries. In orderat each round at position h~v , ~o, ri, Attacker has to ensure thatfor Defender to win the game, after f (`) rounds, |P −11(~v,~o)|P|P −1 (~
v ·w,~o·q)|
sec
r = q∈O |P −1 (~v,~o)| ·rw (q), and at the last round (at some−1must be strictly less than 1, or in other words, |Psec(~v , ~o)|must
1
position h~v , ~o, ri), it holds that |P −1 (~v,~o)| < r. Furthermore,
be strictly more than 1. That implies that the probability thatwhen Defender internally selects a secret value s, this value
the attacker algorithm will guess the secret is less than 1, as
directly determines the observation o she replies with, as for
expected.
N
any w ∈ I, P (s, w) can only take one value.
Given the simpler setting, it is now easier to provide someWe go through the simple example Pins and show that it isintuition for the game and why Attacker is allowed to change vulnerable, with only a linear number of tries.
the weight for the different choices by Defender, using a simple
Proposition IV.2. Attacker has a winning strategy for theexample. Consider a very simple game with only one round,(` + 1)-round 1-confidence game on program Pins .
where the initial set of secrets is S4 with 16 secrets, and there
Proof: We can show by induction on the number of rounds
are exactly two possible observations o1 and o2 in O, such thatfor any v ∈ I, |P −1 (v, o1 )| = 12 and |P −1 (v, o2 )| = 4. In that Attacker has a strategy, such that at each round i, at position−1(~v , ~o) ⊆this game, Defender would always reply with the observation h~v , ~o, 1i, there exists w ∈ {0, 1}i−1 such that Pins`−i+1}. This implies that at roundo1 , as the number of secrets compatible with that observation {w · z ∈ S` | z ∈ {0, 1}−1
1(~v , ~o)| = 1. We remind the reader, that according
is a lot higher, and as a result µ(s | v, o1 ) (equal to 12) is a ` + 1, |Pins
1
lot lower than µ(s | v, o2 ) (equal to 4 ). The actual probability to Remark III.3, Attacker needs to choose only an input w ∈ I
1
1
1
Attacker can guess the secret is 16·12· 12+ 16·4· 41 = 18 (after at each move, and not a mapping rw : O → [0, 1]. For the−1(ε, ε) =one round, the probability of correctly guessing the secret is base case, let i = 1. Then at the first round Pins
1
1
`
{z
∈
S
|
z
∈
{0,
1}
}
as
required.
For
theinductive
case,
for
12
of
the
16
secrets
and
for
4
of
them).
Withoutany`
12
4
further condition, if Defender chose o1 as her move, then she suppose that the statement holds for all i ≤ I, for some
could make it seem like the probability of Attacker’s success I ∈ N, and consider the case where i = I + 1. Then, by
1
the inductive hypothesis, there exists w ∈ {0, 1}I−1 such thatis 12
, which is less than the actual one (i.e., 18 ).
−1(~v , ~o) ⊆ {w · z ∈ S` | z ∈ {0, 1}`−I+1 }. Attacker thenIn our games, Attacker has way of dealing with this issue, Pinsby defining the function rv : O → [0, 1]. This way, Attacker chooses vI to be equal to any string that starts with w andcan define rv (o1 ) to be lower than rv (o2 ), giving the incentive Defender replies with oI ∈ O. Notice that if Defender replies−1(~v · vI , ~o · oI ) is empty, sinceto Defender to also consider o2 as a move. Concretely, suppose with oI < |w| = I − 1, then Pins
−1
that Attacker chose the function rv to be such that rv (o1 ) = 0. for all s ∈ Pins (~v , ~o), s = w · z for some z ∈ {0, 1}`−I+1
Then if Defender chose o1 as her move, she would require and therefore for all such s, prefix(s, vI ) ≥ |w|. Assume then1
that Defender replies with oI ≥ |w| = I − 1. Let yI be the|P −1 (v,o1 )| < 0 to win, which is not possible. She would thendefinitely choose o2 . It is, however, not to Attacker’s advantage prefix of vI of length oI + 1, and notice that by definition−1
to choose such extreme valuationsof rv . Recall that the game Pins(~v · vI , ~o · oI ) contains no secret with prefix yI . Let wIP
enforces the constraint r = q∈O µ(q | v; ~v , ~o) · rv (q) where be equal to the string obtained from yI by flipping the last
h~v , ~o, ri is the current game position.
This implies that, in our bit in that string. Then wI , of length oI + 1, is such thatP
−1
example, rv must satisfy r = i∈{1,2} µ(oi | v; ε, ε) · rv (oi ) Pins(~v · vI , ~o · oI ) ⊆ {wI · z ∈ S` | z ∈ {0, 1}`−oI +1 }. SinceoI ≥ I − 1, it follows that there exists u of length I, such that
−1
Pins(~v · vI , ~o · oI ) ⊆ {u · z ∈ S` | z ∈ {0, 1}`−I } as required.

Corollary IV.5. There exists a program P , that is (2, 1)insecure in the adaptive setting, but (2`/2 , 1)-secure in the
non-adaptive setting.

A. Adaptive vs. Non-adaptive attacks
V. ATTACK AND D EFENSE S LOPES
Adaptive attacks are naturally a lot more powerful than nonadaptive attacks, and here we demonstrate some strong lower
In this section, we use the game-characterization developed
bounds for the gap between the number of moves or tries earlier, to approximate the search of attack strategies onrequired by a non-adaptive attacker compared to the number programs, or show they are secure against attacks of certainof moves required by an adaptive attacker. First we need to length. We define the notion of slopes, which intuitively
define a non-adaptive game. Such a game would be like the describe how quickly an attacker can refine their knowledge
one defined for adaptive attacks, but where Attacker’s choices about the secret. In this section, we carry over the uniformdo not depend on Defender’s moves at all. In such a game, deterministic setting from Section IV.
Attacker can perform all his moves at the very beginning, andAttack Slope: Suppose a program P is such that there exists
Defender can reply with her moves after Attacker has finishedh ∈ [0, 1] and k ∈ N+ , where for each ~v ∈ I ∗ and ~o ∈ O∗
moving. The winning condition in the end is the same.
of the same length, there is a sequence w~ ∈ I k of length k,−1
The following example illustrates the gap between the power
·w,~
~ o·~
q )|
k |P (~
such that for any sequence ~q ∈ O , |P −1v(~≤ h, orv ,~o)|of an adaptive attacker and a non-adaptive one. It is an−1~ ~o · ~q)| = 1. We call such a pair of numbers (k, h),adaptation of an example presented in [7], generalized to the |P (~v · w,
theattackslope for P .
setting where the security bounds are parametric to the size of
secrets. Even though the generalization is easy to produce, we Lemma V.1. Let P be a program with a (k, h) attack slope,present it here for completeness.
with k ∈ N+ and h ∈ [0, 1]. Then, for any n ∈ N+ , P is
1
Example IV.3. Let Pdis be a program that discloses all the (n · k, hn ·2` )-insecure.
secret information but in two steps, parameterized by the secret
Proof: We will show by induction on n that Attacker wins
length `. For any `, the program has two inputs as usual, v ∈ I the (n · k)-round r-confidence game from any position h~v , ~o, ri,
and s ∈ S. For s ∈ S` , define s1 and s2 to be such that for r ≤1v ∈ I∗
hn ·|P −1 (~v ,~o)| . For what follows, fix arbitrary ~s = s1 · s2 , and |s1 | = ` − 1. Given v, we define v 1 and v 2 ,∗and ~o ∈ O . For the base case, suppose that n = 0. Then any
similarly. The program Pdis then operates as follows on inputs
position h~v , ~o, ri is a winning position for Attacker, for any
v and s. If v 1 · v 2 is equal to s1 · s2 then the program returns 1.
r ≤ |P −11(~v,~o)| , by definition.
Otherwise, if v 1 is equal to s1 , the program returns s2 . Finally,
For the inductive case, notice that by definition, there is
if none of the above hold, the program returns s1 .
a sequence w~ ∈ I k , such that for any sequence ~q ∈ Ok ,It is easy to see that an adaptive attacker can find the secret |P −1 (~v·w,~
~ o·~
q )|
≤ h. Let rw1 , rw2 , . . . , rwk be functions that|P −1 (~v ,~o)|in 2 steps. First they try any input v, on which the program,conformtotheallowed moves of Attacker. We will later define1in the worst case, will return the string s . At the second step,thefunctionr, and its valuation will determine that of all
1w
k
Attacker tries any string with prefix s , at which point the
the
other
functions.
It is worth noting again, that the choice of2
12
program will return s and the secret is simply s · s .
Neach wi , for 0 < i ≤ k does not depend on the choice of qj ,Lemma IV.4. There exists program P such that for each ` ∈ N, for j < i, from Defender, and Attacker needs to consider the
Attacker wins the 2-round 1-confidence adaptive game on P , previous moves of Defender to determine the whole sequence
but for all ` larger than some `0 ∈ N, Attacker does not win w,~ only at the very beginning of these k rounds. By definition
the (2`−1 − 1)-round 1-confidence non-adaptive game.
of rwi , for each 1 ≤ i < k, we know that
Proof: Consider the program Pdis from Example IV.3. It
P|P −1 (~
v ·w1 ,~
o·q1 )|
r=· rw1 (q1 ), andwas shown that Attacker can win the 2-round 1-confidence
q1 ∈O|P −1 (~
v ,~
o)|
−1
P
|P
(~
v
·w
···w
o·q1 ···qi+1 )|1i+1 ,~
game. We need to show that for large enough ` ∈ N, therwi (qi ) =· rwi+1 (qi+1 ).
qi+1 ∈O|P −1 (~
v ·w1 ···wi ,~o·q1 ···qi )|`−1
Defender wins the (2− 1)-round 1-confidence non-adaptive
game. Let m = 2`−1 − 1 and let ~x = x1 , . . . , xm be the Without being explicit in these expressions, we take thesequence of moves performed by the Attacker in the non- sum over only those observations for which the respective
adaptive game. Then, there is s1 ∈ {0, 1}`−1 , that is not a probability µ(q | w; ~v , ~o) = |P −1 (~v·w,~o·q)| is non-zero. From−1
prefix of any of the xi . Let S be the set of strings of length ` the equations above, it follows |Pthat (~v,~o)|that start with s1 . Defender then defines ~o to be the sequenceP
where for all 1 ≤ i ≤ m, oi = s1 . Then notice that (i) for|P −1 (~
v ·w1 ,~
o·q1 )|·r=q1 ∈O|P −1 (~v ,~o)|any s in S, and any xi , Pdis (s, xi ) = oi , and (ii) there areP|P −1 (~
v ·w1 ·w2 ,~o·q1 ·q2 )|0
1
1·
at least two secrets s and s in S, namely s · 0 and s · 1.
q2 ∈O
|P −1 (~
v ·w1 ,~
o·q1 )|−1
Therefore, by (i) S ⊆ Pdis(~x, ~o), and by (ii) |S| ≥ 2. Hence...
P1|P −1 (~
v ·w,~~ o·~q )|< 1, as required for Defender to win the game.
rw (qk ),|P −1 (~
x,~
o)|
−1
dis

qk ∈O |P(~v ·w1 ···wk−1 ,~o·q1 ···qk−1 )|kwhich is equal toPPP|P −1 (~
v ·w,~
~ o·~
q )|
r=
· rwk (qk )q1 ∈O
q2 ∈O . . .
qk ∈OP −1 (~
v ,~
o)
−1
P
|P (~
v ·w,~~ o·~q )|=· rwk (qk ).
q~∈O k
P −1 (~v ,~o)(5)Without loss of generality, assume that r is equal to1hn ·|P −1 (~v ,~o)| . Furthermore, define rwk (qk ) to be equal to1
valuation of rwk conforms with Eq. 5, sincehn ·|P −1 (~v ,~o)| . ThisP
for any w~ ∈ I k , q~∈Ok |P −1 (~v · w,
~ ~o · ~q)| = |P −1 (~v , ~o)| and−1P(~
v ·w,~~ o·~q )|thus q~∈Ok |P|P −1= 1. Then, notice that
(~
v ,~
o)|
rwk (qk ) =1hn ·|P −1 (~v ,~o)|= hn−1 ·h·|P1 −1 (~v,~o)|≤ hn−1 ·|P −11 (~v·w,~~ o·~q )| ,

for any ~q ∈ Ok . Thus, by the inductive hypothesis, Attacker
wins the (n − 1) · k-round rwk (qk )-confidence game from theposition h~v · w,
~ ~o · ~q, rwk (qk )i. Since this is the case for any~q ∈ Ok , it follows that Attacker wins the n-round r-confidence
game from the position h~v , ~o, ri.
Finally, by applying the induction statement, since|P −1 (ε, ε)| = |S` | = 2` , we have that Attacker can win thegame with n · k moves from hε, ε, hn1·2` i.

gain information about all the bits of the secret s. The same
result can just as easily be established by showing that the
program has a ( 12 , 1) attack slope. Let ~v ∈ I ∗ and ~o ∈ O∗ be
two sequences of public inputs and observations respectively,of length less than `. Then let v 0 be any natural less than `that is not in the sequence ~v . It is not difficult to see that,−1(~v ·v 0 ,~o·q)|
for any q ∈ O, |P |P −1< 12 , as the v 0 -th bit of s is
(~
v ,~
o)|
undetermined before, and determined by feeding v 0 as a public
input. This attack slope implies that IQ is (`, 1)-insecure. N
Defense Slope: Suppose a program P is such that there existsh ∈ N, where for each ~v ∈ I ∗ and ~o ∈ O∗ of the samelength, and for every w ∈ I, there exists qw ∈ O such that|P −1 (~v , ~o)| − |P −1 (~v · w, ~o · qw )| < h. We call such a number
h, the defense slope for P . A defense slope of h, indicates that
Attacker, at each round can exclude at best a constant number(bounded by h) of secrets.
Lemma V.4. Let P be a program with a defense slope h. Then)-secure.
for all n ∈ N, P is (n, (n+2)h2`

Proof: We show by induction on n, that if P has a defense
slope h, then for any ~v ∈ I ∗ and ~o ∈ O∗ , Defender wins then-round game starting at position h~v , ~o, ri, for r ≥ |P(n+2)h
−1 (~
v ,~
o)| .
This would imply that Defender wins the n-round game fromposition hε, ε, (n+2)hi, and thus P is (n, (n+2)h)-secure.
2`
2`
−1
We
note
that
h
>
0
since
|P
(~
v
,
~
o
)|
cannotbe less than
Example V.2. Consider the program Pins from Section I,
−1
|P
(~
v
·
w,
~
o
·
q
)|,
and
h
is
by
assumption
strictlylargerw
i.e. the Leaky Login program in Fig. 1. This program has
1
than
the
difference.
For
the
base
case,
let
n
=
0.
Then
for
a (1, 2 ) attack slope: let h~v , ~o, 1i be any position in the game.
∗∗any
position
~
v
∈
I
and
~
o
∈
O
,
Defenderwins
the0-round
Remember that O is a subset of N, where each observation
2h
1
corresponds to the largest common prefix of the secret and the game if |P −1 (~v,~o)| < r which holds since r ≥ |P −1 (~v,~o)| by+
input. Then, let o ∈ ~o, be the highest value, and let v ∈ ~v be assumption, and h ∈ N .
For the inductive case, suppose that for any w ∈ I, there
the input that generated that response. It follows that P −1 (~v , ~o)existsqw ∈ O, such that |P −1 (~v , ~o)| − |P −1 (~v · w, ~o · qw )| < h.
is the set of all secrets whose prefix of length o is equal tothe prefix of length o of v, but the next character in the secret Let w ∈ I be any choice of Attacker. By definition of a game,has to chose a function rw : O → [0, 1], such thatdiffers from the one in v. Then, let w be equal to the string Attacker−1P(~
v ·w,~
o·q)|
formed by flipping the (o + 1)-th character of v. Also let r = q∈O |P|P −1· rw (qw ). The latter is equal to
(~
v ,~
o)|
rw (q) = 1, for all q ∈ O. Let q be any response of Defender−1
P|P −1 (~
v ·w,~
o·q)|
v ·w,~
o·qw )|· rw (q) + |P |P (~· rw (qw )to w, and notice that any such response will at the very least−1 (~q∈O\{qw }|P −1 (~
v ,~
o)|
v ,~
o)|
reveal the value of the (o + 2)-th character of the secret. Thus
Let R be equal to maxq∈O\{qw } rw (q). Then|P −1 (~
v ·w,~o·q)|
is less than or equal to 12 . By Lemma V.1, Pins is|P −1 (~
v ,~
o)|
−1
n
P
|P −1 (~
v ·w,~
o·q)|
v ·w,~
o·qw )|(n, 22` )-insecure, and in particular it is (`, 1)-insecure, agreeingr≤· R + |P |P (~· rw (qw )−1 (~q∈O\{qw } P|P −1 (~
v ,~
o)|
v ,~
o)|
R
−1
with the statement of Proposition IV.2.
N= |P −1 (~v,~o)| · ( q∈O\{qw } |P (~v · w, ~o · q)|)−1

Program Index Querydef indexQuery(secret, index):
return (secret[index-1] == 1)

Fig. 2: Index Query program

Example V.3. As a further example, we consider the simple
program IQ presented in Fig. 2, over public inputs I` ={1, . . . , `} and observations {true, false}. On inputs s ∈ S`
and v ∈ I` , the program returns true if the v-th symbol of s is
1, and false otherwise. This is a trivially vulnerable program,where the attacker simply has to query one index at a time tov ·w,~
o·qw )|+ |P |P (~· rw (qw ).
−1 (~
v ,~
o)|

P
−1
Notice that(~v · w, ~o · q)| = |P −1 (~v , ~o)| −q∈O\{qw } |P
|P −1 (~v · w, ~o · qw )|, and hence, by assumption, the latter isstrictly less than|P −1 (~
v ·w,~
o·qw )|
R· rw (qw ).
|P −1 (~v ,~o)| · h +|P −1 (~v ,~o)|

By assumption r ≥ |P(n+2)h
−1 (~
v ,~
o)| , and thus it follows that(n + 2)h < R · h + |P −1 (~v · w, ~o · qw )| · rw (qw ).
which implies thatrw (qw ) > |P(n+2)h−R·h−1 (~v ·w,~
o·qw )| .

Furthermore, R ≤ 1, and hence

successive moves. For deterministic systems with uniform
distributions, this amounts to measuring how many secretsrw (qw ) > |P −1(n+1)·hare still possible under the sequence of observations from(~v ·w,~
o·qw )| .
multiple executions of the program under attack. When the
By the inductive hypothesis, Defender wins the (n − 1)programs are probabilistic, or in other words there is a nonround game from position h~v , ~o, rw (qw )i, which completes
trivial probability distribution over the observations, given a
the argument.
public input and a secret, comparisons between distributions
It is worth mentioning that the definition of defense slope
over the secrets is not immediate. There is no direct way ofdoes not put any constraints on the function rw : O → [0, 1]
comparing two distributions over the secrets and determining
selected at each round by Attacker.
that one corresponds to “better” knowledge than the other
Example V.5. Let Psec be the program from Section I. This without actually playing the game. It is not clear how toprogram has a defense slope of 2: let ~v ∈ I ∗ and ~o ∈ O∗ . compare even two distributions where the support of one is
For any w ∈ I, let qw = false. Then |P −1 (~v , ~o)| − |P −1 (~v · strictly larger than the support of the other.
w, ~o · false)| < 2 since the only secret excluded is the one
VI. R EDUCTIONS
equal to w. Then Lemma V.4 says that Psec is, for example,
In
this
sectionwe
present
a way of reducing a game strategy
2`−1 +4`−2 2`−1 +4(2 , 2` )-secure. For ` > 2, 1 ≥ 2` , and thereforeonone
programtothatofanother. Calculating the optimal`−2
it follows that Psec is even (2 , 1)-secure. In other words,
strategy
for
one
of
the
two
players in a game hinges on a`−2even with 2
moves, Attacker cannot know with absolutesequenceofalternationsin
optimizations,
resulting in highcertainty what the secret is.
Ncomplexity. As such, taking advantage of an existing strategy
While defense slopes provide sound bound on security, it for a game to produce one for a new game in a new setting
is incomplete. That is, secure programs do not need to have a is highly desirable, especially if such a reduction depends onstrong defense slope in general. The intuition is that sometimes mapping each level of alternations of one game to one level,a steep slope may be achievable for a restricted number of or a bounded number of levels of the other. Such reasoning ismoves and then flatten as the game proceeds. This is illustrated inherently more local, and is computationally more efficient.
with the next example.
The general idea behind a reduction from a program P1 toa program P2 is as follows. Suppose that it has already been
Example V.6. Let Ppar (s, v), be the program, that for any
established that Attacker has a winning strategy on P2 for the
input v ∈ I, it returns the parity of 1’s in s. Since the output
game with some number of rounds n and confidence r. To
and observation of Ppar does not depend on the public input,
establish a similar Attacker strategy for P1 , we check what
all the information Attacker can gain from this program is
move the unbeatable Attacker on P2 would make, and use thewhether the number of 1’s in the secret is even or odd, andmapping Φ to make a corresponding move on the P1 game.
additional queries to the program will not provide any more
Then for any response by Defender on that game on P1 , we use
1
information. Thus, for any  > 2 and any f > 1, Ppar isthe mapping Ω to make a Defender response move back on the(f, )-secure. For large enough ` it is then (`, (`+2)·2)-secure, game on P . Since we know that Attacker on P is unbeatable,2`
2
2
but notice that it does not have a defense slope of 2. This is and assuming the conditions for the mappings Φ, Ψ and Ω
because O = {0, 1} has exactly two values corresponding to hold, we can deduce that Attacker can also win the game on
the parity of s. No matter what input w we feed initially to P . See Fig. 3 for a depiction. We remark that a reduction
1
the program, and no matter which of the two parities qw we from a secure program P to a program P establishes security
12
observe, the size of |P −1 (w, qw )| will be half the size of all of the latter, while a reduction of a program P to an insecure2
secrets. Clearly |P −1 (ε, ε)| − |P −1 (w, qw )| ≥ 2, and thus the program P establishes that P is insecure. Thus, the reduction
1
2
defense slope of Ppar is not 2.
N can be used for both proving and disproving security.
Let P be a program defined over a set of secrets S with aConversely, an insecure program may not necessarily havea steep attack slope. That could happen when after some probability distribution µS , a set of public inputs I and a set ofsequences ~v ∈ I and ~o ∈ O, there is not always a sequence of observations O determined by the probability distribution µO .
moves w
~ ∈ I by Attacker that for any response ~q ∈ O would Namely for any s ∈ S and v ∈ I, the probability of observing−1(~v ·w,~~ o·~q)cause the sets P P −1
to be less than a slope h, but later o ∈ O is given by µO (o | s, v). We denote this using the tuple
(~
v ,~
o)
(S, I, O, µS , µO ). For ~v ∈ I ∗ and ~o ∈ O∗ , we define
moves may compensate for that with a slope even steeper than P(~v=,~o)
to be the probability distribution that maps every s ∈ S
h. This problem can sometimes be alleviated by reasoning over µS
k
k
to
µ
(s
| ~v , ~o).
Sa sequence of k moves w~ ∈ I and ~q ∈ O as the definition
LetP
be the program defined by (S1 , I1 , O1 , µS1 , µO1 )1of attack slope allows.
andP
bethe program defined by (S2 , I2 , O2 , µS2 , µO2 ). Let
2
We conclude this section with a small remark about the
Ξ
=
(Ψ,
Φ,
Ω) be a tuple of mappings of type:
restriction of these approximations on deterministic programs
over uniform distributions of secrets. Both the attack andΦ : I2 → I1
defense slopes depend on measuring in a combinatorialΨ : S2 → S1 , that is injective and total,
way the amount of change in knowledge Attacker has afterΩ : O1 × I2 → O2 .

<latexit sha1_base64="NOLh6dlVoBJoa+55aCR1zyEzeDw=">AAAB7XicbVBNSwMxEJ3Ur1q/qh69BFvBU9ntRU9S8OKxgv2AdinZNNvGZpMlyQpl6X/w4kERr/4fb/4b03YP2vpg4PHeDDPzwkRwYz3vGxU2Nre2d4q7pb39g8Oj8vFJ26hUU9aiSijdDYlhgkvWstwK1k00I3EoWCec3M79zhPThiv5YKcJC2IykjzilFgntav95phXB+WKV/MWwOvEz0kFcjQH5a/+UNE0ZtJSQYzp+V5ig4xoy6lgs1I/NSwhdEJGrOeoJDEzQba4doYvnDLEkdKupMUL9fdERmJjpnHoOmNix2bVm4v/eb3URtdBxmWSWibpclGUCmwVnr+Oh1wzasXUEUI1d7diOiaaUOsCKrkQ/NWX10m7XvO9mn9frzRu8jiKcAbncAk+XEED7qAJLaDwCM/wCm9IoRf0jj6WrQWUz5zCH6DPH5objnU=</latexit><latexit sha1_base64="MYKhGO6v5V5p8ZLMS8nKoo751Ug=">AAAB+HicbVDLSsNAFL2pr1ofjbp0M9gKrkrSja6k4EZ3FewD2hAm00k7dDIJMxOhhn6JGxeKuPVT3Pk3TtostPXAwOGce7lnTpBwprTjfFuljc2t7Z3ybmVv/+Cwah8dd1WcSkI7JOax7AdYUc4E7WimOe0nkuIo4LQXTG9yv/dIpWKxeNCzhHoRHgsWMoK1kXy7Wh9GWE8I5tnd3G/WfbvmNJwF0DpxC1KDAm3f/hqOYpJGVGjCsVID10m0l2GpGeF0XhmmiiaYTPGYDgwVOKLKyxbB5+jcKCMUxtI8odFC/b2R4UipWRSYyTylWvVy8T9vkOrwysuYSFJNBVkeClOOdIzyFtCISUo0nxmCiWQmKyITLDHRpquKKcFd/fI66TYbrtNw75u11nVRRxlO4QwuwIVLaMEttKEDBFJ4hld4s56sF+vd+liOlqxi5wT+wPr8Ad+Skos=</latexit>

I2<latexit sha1_base64="4nfuavVU+PqRvIxOBrH+n6IhDdY=">AAAB+HicbVC7TsMwFL0pr1IeDTCyWLRITFXSBSZUiYWxCPqQ2ihyXKe16jiR7SCVqF/CwgBCrHwKG3+D02aAliNZOjrnXt3jEyScKe0431ZpY3Nre6e8W9nbPzis2kfHXRWnktAOiXks+wFWlDNBO5ppTvuJpDgKOO0F05vc7z1SqVgsHvQsoV6Ex4KFjGBtJN+u1ocR1hOCeXY/95t13645DWcBtE7cgtSgQNu3v4ajmKQRFZpwrNTAdRLtZVhqRjidV4apogkmUzymA0MFjqjyskXwOTo3ygiFsTRPaLRQf29kOFJqFgVmMk+pVr1c/M8bpDq88jImklRTQZaHwpQjHaO8BTRikhLNZ4ZgIpnJisgES0y06apiSnBXv7xOus2G6zTcu2atdV3UUYZTOIMLcOESWnALbegAgRSe4RXerCfrxXq3PpajJavYOYE/sD5/AO7ikpU=</latexit>

S2<latexit sha1_base64="mP6cgE/eRwJhMFG2N2xSgZnPjbM=">AAAB+HicbVDLSsNAFL2pr1ofjbp0M9gKrkrSja6k4EZ3FewD2hAm00k7dDIJMxOhhn6JGxeKuPVT3Pk3TtostPXAwOGce7lnTpBwprTjfFuljc2t7Z3ybmVv/+Cwah8dd1WcSkI7JOax7AdYUc4E7WimOe0nkuIo4LQXTG9yv/dIpWKxeNCzhHoRHgsWMoK1kXy7Wh9GWE8I5tnd3Hfrvl1zGs4CaJ24BalBgbZvfw1HMUkjKjThWKmB6yTay7DUjHA6rwxTRRNMpnhMB4YKHFHlZYvgc3RulBEKY2me0Gih/t7IcKTULArMZJ5SrXq5+J83SHV45WVMJKmmgiwPhSlHOkZ5C2jEJCWazwzBRDKTFZEJlpho01XFlOCufnmddJsN12m4981a67qoowyncAYX4MIltOAW2tABAik8wyu8WU/Wi/VufSxHS1axcwJ/YH3+AN4Nkoo=</latexit>

I1<latexit sha1_base64="YPdX4MC01IfpYclDQWBRpGmveCY=">AAAB+HicbVC7TsMwFL0pr1IeDTCyWLRITFXSBSZUiYWxCPqQ2ihyXKe16jiR7SCVqF/CwgBCrHwKG3+D02aAliNZOjrnXt3jEyScKe0431ZpY3Nre6e8W9nbPzis2kfHXRWnktAOiXks+wFWlDNBO5ppTvuJpDgKOO0F05vc7z1SqVgsHvQsoV6Ex4KFjGBtJN+u1ocR1hOCeXY/9926b9echrMAWiduQWpQoO3bX8NRTNKICk04VmrgOon2Miw1I5zOK8NU0QSTKR7TgaECR1R52SL4HJ0bZYTCWJonNFqovzcyHCk1iwIzmadUq14u/ucNUh1eeRkTSaqpIMtDYcqRjlHeAhoxSYnmM0MwkcxkRWSCJSbadFUxJbirX14n3WbDdRruXbPWui7qKMMpnMEFuHAJLbiFNnSAQArP8Apv1pP1Yr1bH8vRklXsnMAfWJ8/7V2SlA==</latexit>

S1

Attacker chooses w ∈ I2
and rw : O2 → [0, 1] on P2
game

Attacker chooses Φ(w) ∈ I1
and rΦ(w) : O1 → [0, 1] on P1
game

Defender responds withΩ(q, w) ∈ O2 on P2 game

Defender responds withq ∈ O1 on P1 game<latexit sha1_base64="MqGnJ5QtjT8F0wrQQL8ww2MWs24=">AAAB7XicbVBNSwMxEJ3Ur1q/qh69BFvBU9ntRU9S8OKxgv2AdinZNNvGZpMlyQpl6X/w4kERr/4fb/4b03YP2vpg4PHeDDPzwkRwYz3vGxU2Nre2d4q7pb39g8Oj8vFJ26hUU9aiSijdDYlhgkvWstwK1k00I3EoWCec3M79zhPThiv5YKcJC2IykjzilFgntav9puHVQbni1bwF8Drxc1KBHM1B+as/VDSNmbRUEGN6vpfYICPacirYrNRPDUsInZAR6zkqScxMkC2uneELpwxxpLQrafFC/T2RkdiYaRy6zpjYsVn15uJ/Xi+10XWQcZmklkm6XBSlAluF56/jIdeMWjF1hFDN3a2Yjokm1LqASi4Ef/XlddKu13yv5t/XK42bPI4inME5XIIPV9CAO2hCCyg8wjO8whtS6AW9o49lawHlM6fwB+jzB6rdjoA=</latexit>

P2

P1<latexit sha1_base64="01zXljcbSlm0zBow6Z8N6WtYslw=">AAAB7HicbVBNT8JAEJ3iF+IX6tHLRjDxRFoueiR68YiJBRNoyHaZwobtttndmpCG3+DFg8Z49Qd589+4QA8KvmSSl/dmMjMvTAXXxnW/ndLG5tb2Tnm3srd/cHhUPT7p6CRTDH2WiEQ9hlSj4BJ9w43Ax1QhjUOB3XByO/e7T6g0T+SDmaYYxHQkecQZNVby6+1Bsz6o1tyGuwBZJ15BalCgPah+9YcJy2KUhgmqdc9zUxPkVBnOBM4q/UxjStmEjrBnqaQx6iBfHDsjF1YZkihRtqQhC/X3RE5jradxaDtjasZ61ZuL/3m9zETXQc5lmhmUbLkoygQxCZl/ToZcITNiagllittbCRtTRZmx+VRsCN7qy+uk02x4bsO7b9ZaN0UcZTiDc7gED66gBXfQBh8YcHiGV3hzpPPivDsfy9aSU8ycwh84nz+IB43T</latexit><latexit sha1_base64="XzX9zonNLpN8S6XOHGgbXima59M=">AAAB7HicbVBNT8JAEJ3iF+IX6tHLRjDxRFoueiR68YiJBRNoyHaZwobtttndmpCG3+DFg8Z49Qd589+4QA8KvmSSl/dmMjMvTAXXxnW/ndLG5tb2Tnm3srd/cHhUPT7p6CRTDH2WiEQ9hlSj4BJ9w43Ax1QhjUOB3XByO/e7T6g0T+SDmaYYxHQkecQZNVby6+2BVx9Ua27DXYCsE68gNSjQHlS/+sOEZTFKwwTVuue5qQlyqgxnAmeVfqYxpWxCR9izVNIYdZAvjp2RC6sMSZQoW9KQhfp7Iqex1tM4tJ0xNWO96s3F/7xeZqLrIOcyzQxKtlwUZYKYhMw/J0OukBkxtYQyxe2thI2poszYfCo2BG/15XXSaTY8t+HdN2utmyKOMpzBOVyCB1fQgjtogw8MODzDK7w50nlx3p2PZWvJKWZO4Q+czx+Ggo3S</latexit>⌦<latexit sha1_base64="5DH0qBCDX9Um72gKumgDPdGxo8A=">AAAB73icbVA9SwNBEJ3zM8avqKXNYiJYhbs0WknAxs4I5gOSI+xt5pIle3vn7p4QjvwJGwtFbP07dv4bN8kVmvhg4PHeDDPzgkRwbVz321lb39jc2i7sFHf39g8OS0fHLR2nimGTxSJWnYBqFFxi03AjsJMopFEgsB2Mb2Z++wmV5rF8MJME/YgOJQ85o8ZKnUrvLsIhrfRLZbfqzkFWiZeTMuRo9EtfvUHM0gilYYJq3fXcxPgZVYYzgdNiL9WYUDamQ+xaKmmE2s/m907JuVUGJIyVLWnIXP09kdFI60kU2M6ImpFe9mbif143NeGVn3GZpAYlWywKU0FMTGbPkwFXyIyYWEKZ4vZWwkZUUWZsREUbgrf88ipp1aqeW/Xua+X6dR5HAU7hDC7Ag0uowy00oAkMBDzDK7w5j86L8+58LFrXnHzmBP7A+fwBF6uPUQ==</latexit><latexit

O2<latexit sha1_base64="8Ax67XEhDUcqEFkJfDV423zKZnc=">AAAB+HicbVDLSsNAFL2pr1ofjbp0M9gKrkrSja6k4MadFewD2hAm00k7dDIJMxOhhn6JGxeKuPVT3Pk3TtostPXAwOGce7lnTpBwprTjfFuljc2t7Z3ybmVv/+Cwah8dd1WcSkI7JOax7AdYUc4E7WimOe0nkuIo4LQXTG9yv/dIpWKxeNCzhHoRHgsWMoK1kXy7Wh9GWE8I5tnd3G/WfbvmNJwF0DpxC1KDAm3f/hqOYpJGVGjCsVID10m0l2GpGeF0XhmmiiaYTPGYDgwVOKLKyxbB5+jcKCMUxtI8odFC/b2R4UipWRSYyTylWvVy8T9vkOrwysuYSFJNBVkeClOOdIzyFtCISUo0nxmCiWQmKyITLDHRpquKKcFd/fI66TYbrtNw75u11nVRRxlO4QwuwIVLaMEttKEDBFJ4hld4s56sF+vd+liOlqxi5wT+wPr8AejCkpE=</latexit>

O1<latexit sha1_base64="430nXJRwuEw5kxVmIbon1anGO0E=">AAAB+HicbVDLSsNAFL2pr1ofjbp0M9gKrkrSja6k4MadFewD2hAm00k7dDIJMxOhhn6JGxeKuPVT3Pk3TtostPXAwOGce7lnTpBwprTjfFuljc2t7Z3ybmVv/+Cwah8dd1WcSkI7JOax7AdYUc4E7WimOe0nkuIo4LQXTG9yv/dIpWKxeNCzhHoRHgsWMoK1kXy7Wh9GWE8I5tnd3Hfrvl1zGs4CaJ24BalBgbZvfw1HMUkjKjThWKmB6yTay7DUjHA6rwxTRRNMpnhMB4YKHFHlZYvgc3RulBEKY2me0Gih/t7IcKTULArMZJ5SrXq5+J83SHV45WVMJKmmgiwPhSlHOkZ5C2jEJCWazwzBRDKTFZEJlpho01XFlOCufnmddJsN12m4981a67qoowyncAYX4MIltOAW2tABAik8wyu8WU/Wi/VufSxHS1axcwJ/YH3+AOc9kpA=</latexit>

Fig. 3: Depiction of the mappings Φ, Ψ and Ω of a reduction: for all s ∈ S2 , w ∈ I2 and q ∈ O1 , µO1 (q | Ψ(s), Φ(w)) = µO2 (Ω(q, w) | s, w).
(~
v ,~
o )

(~
v ,~
o )

Then, given probability distributions µS11 1 and µS22 2 , we
(~
v ,~
o )
(~
v ,~
o )
say that µS22 2 = ΨhµS11 1 i, if∀s ∈ S2 , µS2 (s | ~v2 , ~o2 ) = µS1 (Ψ(s) | ~v1 , ~o1 ).
(~
v ,~
o )

Definition VI.1. Given probability distributions µS11 1 and
(~
v ,~
o )
µS22 2 , we say that the program P1 reduces via Ξ to the
(~
v ,~
o )
(~
v ,~
o )
program P2 and write it as (P1 , µS11 1 ) 4Ξ (P2 , µS22 2 ), if:• for all s ∈ S2 , w ∈ I2 and q ∈ O1 ,µO1 (q | Ψ(s), Φ(w)) = µO2 (Ω(q, w) | s, w)
and
(~
v ,~
o )
(~
v ,~
o )
µS22 2 = Ψ(µS11 1 ).
In such a case, we call the tuple of mappings Ξ a reductionof P1 to P2 .
•Lemma VI.3. Let P1 = (S1 , I1 , O1 , µS1 , µO1 ) and P2 =(S2 , I2 , O2 , µS2 , µO2 ) be two programs and let Ξ = (Ψ, Φ, Ω)
and ~v1 ∈ I1 , ~v2 ∈ I2 , ~o1 ∈ O1 , ~o2 ∈ O2 be such that
(~
v ,~
o )
(~
v ,~
o )
(P1 , µS11 1 ) 4Ξ (P2 , µS22 2 ). Then for any ~v ∈ I2∗ and
(~
v
·Φ(~
v
),~
o
·~
o
)
(~
v ·~
v ,~
o ·Ω(~o,~v ))1~o ∈ O1∗ , (P1 , µS11
) 4Ξ (P2 , µS22 2).

Proof: We need to show that for any ~v ∈ I2∗ and ~o ∈ O1∗ ,and for any s ∈ S2 , w ∈ I2 and q ∈ O1 , it holds that
• µO1 (q | Ψ(s), Φ(w)) = µO2 (Ω(q, w) | s, w), and
(~
v2 ·~
v ,~
o2 ·Ω(~o,~v ))(~v ·Φ(~
v ),~
o1 ·~
o)
• µS
= Ψ(µS11
).
2
(~
v ,~
o )

The first condition holds by assumption that (P1 , µS11 1 ) 4Ξ
(~
v ,~
o )
(P2 , µS22 2 ). For the second condition it suffices to show thatfor all ~v ∈ I2∗ , ~o ∈ O1∗ , and s ∈ S2 ,µS2 (s | ~v2 · ~v , ~o2 · Ω(~o, ~v )) = µS1 (Ψ(s) | ~v1 · Φ(~v ), ~o1 · ~o).

We proceed by induction on the length |~v | = |~o|. For thebase case, suppose that |~v | = |~o| = 0. Then the statement
(~
v ,~
o )
(~
v ,~
o )
holds by the assumption that µS22 2 = Ψ(µS11 1 ). For theLemma VI.2. Let P1 = (S1 , I1 , O1 , µS1 , µO1 ) and P2 = inductive case, suppose that the statement holds for all ~v and ~o(S2 , I2 , O2 , µS2 , µO2 ) be two programs and let Ξ = (Ψ, Φ, Ω) whose size is less than N , for some N ∈ N, and consider ~v and00
and ~v1 ∈ I1 , ~v2 ∈ I2 , ~o1 ∈ O1 , ~o2 ∈ O2 be such that ~o whose size is exactly N . We write ~v as ~v · w and ~o as ~o · q,
0
0
(~
v1 ,~
o1 )
(~
v2 ,~
o2 )
by the inductive hypothesis(P1 , µS1
) 4Ξ (P2 , µS2). Then, for all w ∈ I2 , q ∈ O1 , where |~v | = |~o | = N − 1.0 Then,(~v ·Φ(~
v ),~
o1 ·~
o0 )
(~
v ·~
v 0 ,~o2 ·Ω(~o0 ,~v 0 ))
we have that (P1 , µS11
) 4Ξ (P2 , µS22),
and ` ∈ N,P
which
immediately
implies
that
for
any
s
∈
S
,
w
∈
I
and
2
2
µO2 (Ω(q, w) | s0 , w) · µS2 (s0 | ~v2 , ~o2 ) =s0 ∈(S2 )`P
q ∈ O1 , it holds that00v1 , ~o1 )).
s0 ∈(S1 )` µO1 (q | s , Φ(w)) · µS1 (s | ~• µO1 (q | Ψ(s), Φ(w)) = µO2 (Ω(q, w) | s, w), and(~v2 ·~v 0 ,~o2 ·Ω(~o0 ,~v 0 ))(~v ·Φ(~v 0 ),~
o1 ·~
o0 )
(~
v1 ,~
o1 )
• µS
= Ψ(µS11).
Proof: By assumption that (P1 , µS1
)
4Ξ
2
(~
v2 ,~
o2 )
Furthermore,bydefinition,
0(P2 , µS2), we know that for all s∈
S2 ,µS2 (s | ~v2 · ~v 0 · w, ~o2 · Ω(~o0 , ~v 0 ) · Ω(q, w)) =µS2 (s0 | ~v2 , ~o2 ) = µS1 (Ψ(s0 ) | ~v1 , ~o1 ). This also00
implies that for all s ∈ S1 that are not in the imageµO2 (Ω(q,w)|s,w)·µS2 (s|~v2 ·~v 0 ,~o2 ·Ω(~o0 ,~v 0 ))of Ψ, µS1 (s00 | P~v1 , ~o1 ) must be equal to 0, since
X
,
0
0
0
0 0
0
µ
(Ω(q,
w)
|
s
,
w)
·
µ
(s
|
~
v
·
~
v
,
~
o
·
Ω(~
o
,
~
v
))
for
all
`
∈
N
µ
(Ψ(s
)
|
~
v
,
~
o
)
=
O
S
2
2
0
S
1
1
2
2
1
s ∈(Im(Ψ))`
P0s0 ∈(S2 )`Ps0 ∈(S2 )` µS2 (s 0 | ~v2 , ~o2 ) = 1 and by definition(6)
v1 , ~o1 ) is also equal to 1. Furthermore,s0 ∈(S1 )` µS1 (Ψ(s ) | ~
and
by
Lemma
VI.2,
the
denominatorofthelatterisequal
toby assumption, for all s ∈ S2 , w ∈ I2 and q ∈ O1 ,X
µO2 (Ω(q, w) | s, w) = µO1 (q | Ψ(s), Φ(w)), and thereforeµO1 (q | s00 , Φ(w)) · µS1 (s00 | ~v1 · Φ(~v 0 ), ~o1 · ~o0 )).
P00
00s ∈(S1 )`µ (Ω(q, w) | s , w) · µS2 (s | ~v2 , ~o2 ) =Ps0 ∈(S2 )` O200ThusµS2 (s | ~v2 · ~v 0 · w, ~o2 · Ω(~o0 , ~v 0 ) · Ω(q, w)) is equal to=µ (q | Ψ(s ), Φ(w)) · µS1 (Ψ(s ) | ~v1 , ~o1 )) =Ps0 ∈(S2 )` O1
00
00=
v1 , ~o1 )),µO1 (q | Ψ(s), Φ(w)) · µS1 (Ψ(s) | ~v1 · Φ(~v 0 ), ~o1 · ~o0 )s00 ∈(S1 )` µO1 (q | s , Φ(w)) · µS1 (s | ~X.
µO1 (q | s00 , Φ(w)) · µS1 (s00 | ~v1 · Φ(~v 0 ), ~o1 · ~o0 )as required.
First we present two lemmas that are used in the proof of
Theorem VI.4.

s00 ∈(S1 )`which is equal, by definition, to µS1 (Ψ(s) | ~v1 · Φ(~v ), ~o1 · ~o),as required.
(ε,ε)
(ε,ε)
It follows that if (P1 , µS1 ) 4Ξ (P2 , µS2 ), then for any
(Φ(~
v ),~
q)
(~
v ,Ω(~o,~v ))) 4Ξ (P2 , µS2).
~v ∈ I2∗ and ~o ∈ O1∗ , (P1 , µS1
The following theorem establishes the connection between
reductions of one program to another, and simulating a strategyof the latter as a strategy of the former.
Theorem VI.4. Let P1 = (S1 , I1 , O1 , µS1 , µO1 ) and P2 =(S2 , I2 , O2 , µS2 , µO2 ) be two programs, let ~v1 ∈ I1 , ~v2 ∈I2 , ~o1 ∈ O1 and ~o2 ∈ O2 , and let Ξ = (Ψ, Φ, Ω) be such that
(~
v ,~
o )
(~
v ,~
o )
(P1 , µS11 1 ) 4Ξ (P2 , µS22 2 ). Suppose also that Attacker
can win the n-round r-confidence game on P2 , starting from
(~
v ,~
o )
the initial distribution of secrets µS22 2 for some n ∈ N andr ∈ [0, 1]. Then Attacker can win the n-round r-confidence
(~
v ,~
o )
game on P1 starting with initial distribution of secrets µS11 1 .

Thus, by Lemma VI.2, for all q ∈ O1 , µO1 (q |Φ(w); ~v1 , ~o1 )) = µO2 (Ω(q, w) | w; ~v2 , ~o2 ).
Therefore rΦ(w) satisfies the constraints of a valid moveby Attacker1 . Let q ∈ O1 be any reply from Defender1 . By
(~
v ,~
o )
assumption that hµS22 2 , n, ri is a winning configuration for(~v ·w,~o2 ·Ω(q,w))
Attacker2 , it follows that hµS22, n−1, rw (Ω(q, w))i
is also a winning configuration for Attacker2 . By Lemma VI.3,(~v ·Φ(w),~
o1 ·q)(~
v ·w,~o2 ·Ω(q,w))(P1 , µS11
) 4Ξ (P2 , µS22). FurthermorerΦ(w) (q) = rw (Ω(q, w)). Thus, we can apply the inductive(~v ·Φ(w),~
o1 ·q)
hypothesis, and conclude that hµS11, n − 1, rΦ(w) (q)i
is a winning configuration for Attacker1 . As this is the case
(~
v ,~
o )
for any move q by Defender1 , it holds that hµS11 1 , n, ri is awinning configuration for Attacker1 as required.
A. Examples on simulating strategies

In Fig. 4, we present the two programs below called PR2 andPR3 whose structure is identical and with the only difference
Proof: In what follows, when Attacker can win the n-roundbetween them being that PR2 returns as output the number ofr-confidence game starting with initial probability distribution
indices in the two input strings where the bits agree, modulo
of secrets µS , we say that hµS , n, ri is a winning configuration2, whereas PR3 returns the same number but modulo 3. Theyfor Attacker. It should be noted that what we call a position
both also return a boolean indicating whether the two strings
h~v , ~o, ri in the game, with n remaining rounds, corresponds toare identical.
(~
v ,~
o)
the configuration hµS , n, ri, and vice versa.
The interesting, and somewhat unintuitive, observation about
The proof proceeds by induction on n ∈ N. For the basethese two programs, is that PR2 is (2` − 1, 1)-secure under
(~
v2 ,~
o2 )
case, suppose that n = 0. Then, since hµS2
, 0, ri is a a uniform initial distribution over the secrets, whereas PR3
winning configuration for Attacker in P2 , it follows that is (` + 1, 1)-insecure over the same distribution of secrets; a
(~
v ,~
o )
(~
v ,~
o )
maxs∈S2 µS22 2 (s) ≥ r. Let s be such that µS22 2 (s) ≥ r. vast difference in security for such similar programs. In what
(~
v2 ,~
o2 )
(~
v1 ,~
o1 )
(~
v1 ,~
o1 )
Since µS2
= Ψ(µS1), it follows that µS1(Ψ(s)) ≥ follows we aim to establish two strategy simulations, as defined
(~
v1 ,~
o1 )
r, and therefore, hµS1
, 0, ri is a winning configuration for in Definition VI.1, in order to show that PR2 is (2` − 1, 1)secure and PR3 is (` + 1, 1)-insecure. For this we will use the
Attacker in P1 .
For the inductive case, we distinguish the two attackers previous results where we showed that SL (i.e. program Psec`
and defenders by writing Attacker1 and Defender1 for the from Section I) is (2 − 1, 1)-secure and IQ is (`, 1)-insecure.
As explained earlier, to show security of a program P , weones on P1 , and Attacker2 and Defender2 for the ones on
P2 . Suppose the statement holds for all n < N , for some use a reduction from a known secure program to P , and to
0
0
(~
v ,~
o )
N ∈ N, and suppose hµS22 2 , N, ri is a winning configuration show insecurity of a program P , we use a reduction from P
for Attacker2 in P2 . Then, Attacker2 can choose w ∈ I2 to a known insecure program. As such, we present:• a reduction from the secure program SL to PR2, andand function rw : O2 → [0, 1], according to his winning• a reduction from PR3 to the insecure program IQ.
strategy. Let Attacker1 choose Φ(w) ∈ I1 and function rΦ(w) :O1 → [0, 1] defined as the function that maps any q ∈ O1 to These two reductions presented below are not necessarily trivial,rw (Ω(q, w)). First we show thatPrΦ(w) satisfies the constraints but they don’t require reasoning over extended sequences ofof a valid move by showing that q∈O1 µO1 (q | Φ(w); ~v1 , ~o1 )· move alternations, as showing security or insecurity directlyrΦ(w) (q) = r. Since for all q ∈ O1 , rΦ(w) (q) = rw (Ω(q, w)), over the games would require. Instead, the point of the
it suffices to show that for all q ∈ O1 , µO1 (q | Φ(w); ~v1 , ~o1 ) = reductions is to take advantage of the more global argumentµO2 (Ω(q, w) | w; ~v2 , ~o2 ), and that for any q 0 not in the image that was made for the established results proving security orof Ω, µO2 (q 0 | w; ~v2 , ~o2 ) = 0. It should be P
noted that the insecurity of the programs SL and IQ respectively. We use
second statement is impliedbythefirst,
sincethese two programs to demonstrate how reductions can be used,q∈O2 µO2 (q |Pw; ~v2 , ~o2 ) = 1 and also q∈O1 µO1 (q | Φ(w); ~v1 , ~o1 )) = 1.
but arguably, for these two particular programs, there are easier
By definition, µO1 (q | Φ(w); ~v1 , ~o1 )) is equal toways to prove security and insecurity.
X1) Reduction from SL to PR2: Let P1 be SL and P2 be PR2.
µO1 (q | s0 , Φ(w)) · µS2 (s0 | ~v1 , ~o1 ),We
fix a length of input secrets ` ∈ N for both programs, so thats0 ∈(S1 )`by S1 , I1 , S2 , and I2 we mean respectively (S1 )` , (I1 )` , (S2 )` ,and (I2 )` . We use the notation `2 to denote the value of ` mod 2.
and µO2 (Ω(q, w) | w; ~v2 , ~o2 ) is equal toAlso, because the initial distribution of secrets is uniform, forX(ε,ε)
i ∈ {1, 2} and any s ∈ Si , µSi (s) = |S1i | . We adopt theµO2 (Ω(q, w) | s0 , w) · µS2 (s0 | ~v2 , ~o2 ).
following notation. Since the set of observations O2 of P2 ares0 ∈(S2 )`Program PR2

Program PR3

def PR2(sec, val):if (sec == val == ""):
return (0, True)else:
res = PR2(sec.tail, val.tail)if (sec.head == val.head):return ((1+res[1])%2, res[2])else:
return (res[1], False)

def PR3(sec, val):if (sec == val == ""):
return (0, True)else:
res = PR3(sec.tail, val.tail)if (sec.head == val.head):return ((1+res[1])%3, res[2])else:
return (res[1], False)

Fig. 4: Programs PR2 and PR3 with the differences between two programs highlighted in red.

tuples over {0, 1} × {true, false}, for o ∈ O2 , we denote with Fix v ∈ I2 and o ∈ O2 , where o = (p, b), for p ∈ {0, 1} ando[1] the first component of o in {0, 1} and with o[2] its second b ∈ {true, false}. For the first condition, let s ∈ S2 , w ∈ I2
component in {true, false}. Given two inputs v, w ∈ I2 , we and q ∈ O1 = {true, false}. Since both SL and PR2 aredefine diff(v, w) to be the number of indices in the two inputs deterministic, there is exactly one possible output for SL(s, w),
where the bits differ, modulo 2. Furthermore, for two values either true or false. By definition, o[1], being equal to the firstp, q ∈ {0, 1}, we denote with p ⊕ q their sum modulo 2. Given component of the observation PR2(s, v), is the number ofv ∈ I2 and o ∈ O2 , let then Φ : I2 → I1 and Ψ : S2 → S1 common bits between s and v, modulo 2, and thus it is also
be the identity functions, and let Ω(v,o) : O1 × I2 → O2 be equal to the number of different bits modulo 2, summed to
the function that maps (b, w) to (diff(v, w) ⊕ o[1], b) where the length of s modulo 2. In other words, o[1] is equal tob ∈ {true, false} = O1 and w ∈ I2 . Let Ξ(v,o) be the tuple diff(s, v) ⊕ `2 , meaning that diff(s, v) = o[1] ⊕ `2 . Using the(Φ, Ψ, Ω(v,o) ) of mappings, where Ω(v,o) is parameterized by same reasoning, notice that PR2(s, w)[1] = diff(s, w)⊕`2 . The−−→v ∈ I2 and o ∈ O2 . With false we refer to a sequence of latter is equal to diff(s, v) ⊕ diff(v, w) ⊕ `2 , and consequently
observations, all of whose value is false, and where the length equal to o[1] ⊕ diff(v, w). Therefore, diff(s, w) = diff(v, w) ⊕o[1] ⊕ `2 . Hence PR2(s, w)[1] = diff(v, w) ⊕ o[1] ⊕ `2 ⊕ `2 =of the sequence is determined by the context.
We will show that for any v ∈ I2 , any o ∈ O2 , diff(v, w)⊕o[1]. We know that µO1 (q | s, w) = 1 if and only ifthere exists a sequence ~x ∈ I1 of length 2` /2, such that µO2 ((PR2(s, w)[1], q) | s, w) = 1, simply because SL returns−−→(v·~x,o[2]·~y)(v,o)(P1 , µS1
) 4Ξ(v,o) (P2 , µS2 ), where ~y = false and is true on inputs s ∈ S1 and w ∈ I1 if and only if the secondof length 2` /2. Then, by Theorem VI.4, it follows that if component of PR2 is true on the same inputs (while the first(v,o)
Attacker can win the game on P2 (i.e. PR2) from hµS2 , n, ri component is by definition PR2(s, w)[1]). From the argument
then Attacker can also win the game on P1 (i.e. SL) from above, it is the case that µO2 ((PR2(s, w)[1], q) | s, w) = 1
if and only if µO2 ((diff(v, w) ⊕ o[1], q) | s, w) = 1, and the(v·~
x,o[2]·~y)hµS1, n, ri. The sequence ~x will be such that Defenderresult follows.
(v·~
x,o[2]·~y ) `−1
has a winning strategy on P1 from hµS1,2
− 2, 1i
For the second condition, notice that µS2 (s | v, o) = µS1 (s |when o[2] is false. Thus it will follow that Defender has av·~
x, o[2]·~y ), since in the case that o[2] is true, both µS2 (s | v, o)(v,o)
winning strategy on the program PR2 from hµS2 , 2`−1 −2, 1i, and µ (s | v, o[2]) are 1 for s = v, and 0 for all otherS1
when o is such that o[2] = false. Since for any v ∈ I2 Defender values of s. Meanwhile, in the case where o[2] is false, both
can reply with some o ∈ O2 such that o[2] = false, Defender µ (s | v, o) and µ (s | v ·~x, o[2]·~y ) are 0 for all s ∈ S such
S2
S1
2
(ε,ε)
1
has a winning strategy from hµS2 , 2`−1 − 1, 1i, and the that diff(s, v) = 1, and for s = v, and equal to
for
|S
|/2−1
2
program PR2 is thus (2`−1 − 1, 1)-secure.
the remaining |S2 |/2 − 1 secrets. This completes the argument
Given v ∈ I2 , we define Xv to be the set of secrets x ∈ S1 for the reduction.
of length ` such that diff(v, x) = 1. Notice that X contains
2) Reduction from PR3 to IQ: We define P1 to be PR3 andexactly half the secrets from S1 . We then let ~x be a sequencePto be IQ. We again fix ` ∈ N and restrict the sets S1 , S2 , I1
2
comprising the elements of Xv in any order. When o[2] isand
I2 to inputs related to the security parameter ` as before.
false, notice that Defender has a winning strategy on P1(v·~x,o[2]·~y ) `−1Weremindthe reader that for IQ, for the security parameter `,from hµS1,2− 2, 1i. We assume that this has been(I)
isdefinedto be the set of integers {1, . . . , `}. We want2`
established earlier for the program P1 , but informally this is
to
show
that
for
any v ∈ I1 and (o, b) ∈ O1 , there exists an
because each guess from v · ~x by Attacker disqualifies only(ε,ε)
initialprobability
distribution of secrets µS2 and a reductionthat guess as a secret.
(v,o)
(ε,ε)
It remains to show that for any v ∈ I2 and o ∈ O2 , Ξ(v,o) , such that (P1 , µS1 ) 4Ξ(v,o) (P2 , µS2 ). Notice that−−→(v·~x,o[2]·~
y)
(v,o)
(ε,ε)
(P1 , µS1
) 4Ξ(v,o) (P2 , µS2 ), where ~y = false. To for any initial distribution of secrets µS , the program IQ (i.e.
2show the latter, by Definition VI.1, it suffices to show thatP2 ) is (`, 1)-insecure, as shown earlier in Example V.3. Given
the above reduction Ξ(v,o) , for any v ∈ I1 and (o, b) ∈ O1 ,• for all s ∈ S2 , w ∈ I2 and q ∈ O1 , µO1 (q | s, w) =and Theorem VI.4, it follows that PR3 is (` + 1, 1)-insecure.
µO2 ((diff(v, w) ⊕ o[1], q) | s, w), and• for all s ∈ S2 , µS2 (s | v, o) = µS1 (s | v · ~x, o[2] · ~y ).
It thus remains to be shown that for any v ∈ I1 , and any(ε,ε)(o, b) ∈ O1 , there exists µS2 and Ξ(v,o) = (Φ, Ψ, Ω) suchthat
• for all s ∈ S2 , w ∈ I2 and q ∈ O1 ,chosen by the attacker and a child node is added for eachpossible query output. They use quantitative information flow
(QIF) to measure the amount of information an attacker gains
by running a strategy. As standard in QIF [4], [8], [19], [25],µO1 (q | Ψ(s), Φ(w)) = µO2 (Ω(q, w) | s, w)
this is defined as the change in the attacker’s knowledge before
and after the attack. They also show that maximum information
andleakage over all attack strategies of some bounded length can• ∀s ∈ S2 , µS2 (s | ε, ε) = µS1 (s | v, o).
(ε,ε)
(v,o)
be computed by enumerating those strategies and computing
In fact, defining µS2 to be equal to µS1 suffices to handle
the corresponding QIF. Boreale and Pampaloni [7] extended
the second condition above. This is because IQ is (`, 1)the line of work to probabilistic systems.
insecure for any initial distribution of secrets under the same
Our work is inspired by, and builds on the above charstrategy for Attacker.
acterization of attack strategies as attack trees. New in our
For the other condition we proceed as follows. First wework is the introduction of the defender player, which was
define the function flip : I1 × N → I1 such that, given v =missing in the previous works, thus making the formalism
a1 . . . ai . . . an and i ∈ {1, . . . , n}, flip(v, i) = a1 . . . ai . . . ana full-blown game. Our game exactly captures security ofwhere 0 = 1 and 1 = 0. In other words, flip(v, i) is thesystems, that is, the existence of a winning strategy for thestring obtained by flipping the i-th bit of v. Fix v ∈ I1 anddefender player implies that the system is secure whereas that(o, b) ∈ O. We define Ξ(v,o) = (Φ, Ψ, Ω) to be such that forfor the attacker player implies that the system is insecure. We
all s ∈ S2 , w ∈ I2 and q = (m, b) ∈ O1 , Φ(w) = flip(v, w),
remark that a correspondence between a particular winning
Ψ(s) = s and Ω((m, b), w) to be true exactly when m is equal
strategy for these games and the attack trees could be made. For
to o + 1 mod 3 and the w-th bit of v is 0, or when m is equal tothe attack trees of [7], a strategy for an n-round game wouldo − 1 mod 3 and the w-th bit of v is 1. We define the value tonaturally correspond to a tree of height n, each of whose nodes
be false otherwise. Notice that µO1 ((o mod 3, b) | s, flip(v, w))
would additionally be labeled with the rw (q) values chosen by
is 0, since we flipped exactly one bit from v, and by definition
Attacker. A similar correspondence would be produced in theµO1 ((o mod 3, b0 ) | s, v)) = 1 for some b0 ∈ {true, false}. As
deterministic case, for the attack trees of [10], [11].
a result, for v = a1 · · · a` , we have the following cases:
Also, our results are given in the form of (f, )-security
When aw = 0 :which asserts precise bounds on the number of attacker queriesµO1 ((o + 1 mod 3, b) | s, flip(v, w)) = µO2 (true | s, w),
and the probability of his success, where the bounds can beµO1 ((o − 1 mod 3, b) | s, flip(v, w)) = µO2 (false | s, w),
parametric to the size of secrets. As we have shown, the gameWhen aw = 1 :based characterization is useful for deriving such parametricµO1 ((o + 1 mod 3, b) | s, flip(v, w)) = µO2 (false | s, w),
security bounds, as it allows strategy constructions that areµO1 ((o − 1 mod 3, b) | s, flip(v, w)) = µO2 (true | s, w).
parametric to the security parameter. In addition, building
To illustrate this, consider the case where aw = 0. Let s ∈ S1 be on the game-based formalism, we have proposed slopes andany secret, and suppose that for v ∈ I1 with its w-th bit being 0, game reductions which can expedite the process of proving or
P1 (s, v) = (o, b) for some (o, b) ∈ O1 . Then when we flip the disproving security.
As remarked before, the defense player’s move in our gamew-th bit of v, and only that bit, the output of P1 (s, flip(v, w))
canbe seen as her choosing a secret s internally and thenwill either be (o + 1 mod 3, b) or (o − 1 mod 3, b) for someb ∈ {true, false}. In the first case, it means that the w-th bit exhibiting the corresponding output o ∈ supp(P (s, v)) whereof s is 1, since o + 1 mod 3 implies the number of correct bits v is the input chosen by the attacker. This may be seen as if the
between flip(v, w) and s has increased by 1 and the w-th bit of defender changes the secret as the game progresses. Mardziel
v is 0. Again, this can be inferred because we flipped exactly et al. [14] investigates security against adaptive adversaries in a
one bit in v. Similarly, if P1 (s, flip(v, w)) = (o − 1 mod 3, b) setting where the defender may change secrets across multiple
it means that the w-th bit of s is 0. Hence P2 (s, w) will be attack queries. However, their work is orthogonal to ours sincetrue in the first case and false in the second case, as described whereas their change of secrets is a physical one that actually
above. The case where aw = 1 is similar. This completes the changes the secret of the running system, ours is a conceptual
means for proving or disproving security (defined by attackers’
argument.
probability of success) over all secrets distributed according toVII. R ELATED W ORK
some prior.
Closely related to our work is the work by Köpf andFinally, we remark that there are large body of works on
Basin [10], [11] that laid the foundation for formalizing using game theory for security [2], [3], [18], [21]. Like thesecurity under adaptive adversaries for deterministic systems. work by Mardziel et al., these works are orthogonal to ours
Importantly, they have introduced the notion of an attack tree as they concern settings in which the defender makes choicesthat captures an attacker’s strategy. Each node of the tree that exert physical influences, such as choosing which systemrepresents the attacker’s current knowledge (or, uncertainty) to run given some finite number of possibilities [2], [3]. It is
about the secrets, with the root node being the initial state interesting to note that, as shown in Remark III.4, probabilisticof his knowledge. Each node determines the next query input choices give no additional power to attackers in our setting

(this was also conjectured in [7], but not proved). This is instark contrast to the setting with defenders making physicalchoices where probabilistic attackers are shown to be strictly
more powerful than deterministic ones [2].
VIII. C ONCLUSION
We have presented a new game-based characterization of
security against adaptive adversaries. Our game is played by
two players, Attacker and Defender, and it can be used toderive precise security bounds of deterministic and probabilistic
systems. Importantly, the game allows one to derive security
bounds that are parametric to the size of secrets.
In addition, leveraging the game, we have proposed techniques, called slopes and reductions, that can be used to
expedite the process of deriving security bounds. The former
provides a sound approximation of the bounds (for deterministic
programs), and the latter can be used to convert an attacker
strategy over one program to that of another, thereby allowing
one reuse previously established secure or insecure instances
to show security or insecurity of new ones.
ACKNOWLEDGMENTS
We thank the anonymous reviewers for their useful comments
and the meticulous examination they performed on this work.
This work was supported by JSPS KAKENHI Grant Numbers 17H01720 and 18K19787, JSPS Core-to-Core Program,
A.Advanced Research Networks, Office of Naval Research(ONR) award N00014-17-1-2787 and DARPA award FA875015-2-0104.
R EFERENCES[1] J. Agat. Transforming out timing leaks. In POPL, 2000.
[2] M. S. Alvim, K. Chatzikokolakis, Y. Kawamoto, and C. Palamidessi.
Information leakage games. In 8th International Conference on Game
Theory for Security, 2017.
[3] M. S. Alvim, K. Chatzikokolakis, Y. Kawamoto, and C. Palamidessi.
Leakage and protocol composition in a game-theoretic perspective. In
POST, 2018.
[4] M. S. Alvim, K. Chatzikokolakis, C. Palamidessi, and G. Smith.
Measuring information leakage using generalized gain functions. In
CSF, 2012.
[5] T. Antonopoulos, P. Gazzillo, M. Hicks, E. Koskinen, T. Terauchi, and
S. Wei. Decomposition instead of self-composition for proving theabsence of timing channels. In PLDI, 2017.

[6] G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by
self-composition. Mathematical Structures in Computer Science, 21(6),2011.
[7] M. Boreale and F. Pampaloni. Quantitative information flow undergeneric leakage functions and adaptive adversaries. Logical Methods in
Computer Science, 11(4), 2015.
[8] D. Clark, S. Hunt, and P. Malacaria. Quantitative analysis of the leakageof confidential data. Electr. Notes Theor. Comput. Sci., 59(3), 2001.
[9] G. Doychev, B. Köpf, L. Mauborgne, and J. Reineke. Cacheaudit: A
tool for the static analysis of cache side channels. ACM Transactions on
Information and System Security, 18(1), 2015.
[10] B. Köpf and D. A. Basin. An information-theoretic model for adaptiveside-channel attacks. In CCS, 2007.
[11] B. Köpf and D. A. Basin. Automatically deriving information-theoretic
bounds for adaptive side-channel attacks. Journal of Computer Security,
19(1), 2011.
[12] S. Langkemper. The password guessing bug in Tenex. https://www.
sjoerdlangkemper.nl/2016/11/01/tenex-password-bug/, 2016.
[13] P. Li and S. Zdancewic. Downgrading policies and relaxed noninterference. In POPL, 2005.
[14] P. Mardziel, M. S. Alvim, M. W. Hicks, and M. R. Clarkson. Quantifying
information flow for dynamic secrets. In IEEE Symposium on Security
and Privacy, 2014.
[15] C. S. Pasareanu, Q. Phan, and P. Malacaria. Multi-run side-channel
analysis using symbolic execution and max-SMT. In CSF, 2016.
[16] A. Sabelfeld and A. C. Myers. Language-based information-flow security.
IEEE Journal on Selected Areas in Communications, 21(1), 2003.
[17] A. Sabelfeld and A. C. Myers. A model for delimited information release.
In ISSS, 2003.
[18] A. Sinha, F. Fang, B. An, C. Kiekintveld, and M. Tambe. Stackelberg
security games: Looking beyond a decade of success. In IJICAI, 2018.
[19] G. Smith. On the foundations of quantitative information flow. In
FOSSACS, 2009.
[20] DARPA space/time analysis for cybersecurity (STAC) program. http://www.darpa.mil/program/space-time-analysis-for-cybersecurity, 2017.
[21] M. Tambe. Security and game theory: algorithms, deployed systems,
lessons learned. Cambridge university press, 2011.
[22] T. Terauchi and A. Aiken. Secure information flow as a safety problem.
In SAS, 2005.
[23] T. Terauchi and T. Antonopoulos. A formal analysis of timing channel
security via bucketing. In POST, 2019.
[24] D. M. Volpano, C. E. Irvine, and G. Smith. A sound type system forsecure flow analysis. Journal of Computer Security, 4(2/3), 1996.
[25] H. Yasuoka and T. Terauchi. On bounding problems of quantitative
information flow. Journal of Computer Security, 19(6), 2011.
[26] S. Zdancewic and A. C. Myers. Robust declassification. In CSFW, 2001.
[27] D. Zhang, A. Askarov, and A. C. Myers. Language-based control andmitigation of timing channels. In PLDI, 2012.