Marion Daubignard
email: msdaubignard@gmail.com

Pierre-Alain Fouque
email: pierre-alain.fouque@ens.fr

Yassine Lakhnech
email: yassine.lakhnech@imag.fr

Generic Indifferentiability Proofs of Hash Designs

In this paper, we propose a formal analysis of domain extenders for hash functions in the indifferentiability framework. We define a general model for domain extenders and provide a unified proof of their security in the form of a generic reduction theorem. Our general model for domain exenders captures many iterated constructions such as domain extenders, modes of operation of symmetric cryptography such as CBC-MAC or blockciphers based on Feistel networks. Its proof has been carried out using the Computational Indistinguishability Logic of Barthe et al.. The theorem can help designers of hash functions justifying the security of their constructions: they only need to bound the probability of well-defined events. Our model allows to consider many SHA-3 finalists and is instantiated on two well-known constructions, namely Chop-MD and Sponge. Finally, the indifferentiability bounds which we prove are convincing since they match previous proofs.

I. INTRODUCTION

Motivation. Hash functions are the swiss army knife of cryptographers. They are used to generate unique identifiers in hash-and-sign signatures, as one-way functions for one-time-password, to break the structure of the input in key derivation functions and also for authentications... Recently, cryptographers have looked carefully at the security of these functions after the breakthrough discovery of differential attacks by Wang et al. on the MD4 family. Moreover, weaknesses in the Merkle-Damgard (MD) mode of operation [Mer89], [Dam89], standardly used to design hash functions, have been exposed (see [Jou04], [KS05], [KK06]). In response to all these attacks, the NIST decided to launch a competition in order to select the new standard SHA-3.

Hash functions are public functions that map arbitrarily long bitstrings to fixed-length bitstring. To construct a hash function, cryptographers first build a fixed inputlength function f : {0, 1} m → {0, 1} n , where n < m, called a compression function. They then increase the input domain to {0, 1} * using a domain extender, a.k.a. a mode of operation. This latter defines the way the compression function f is iterated to obtain a hash construction H f . Some security goals have been defined for H f such as collision, second-preimage or preimage resistance, but they are not sufficient to cover the needs of all applications of hash functions. Indeed, in security proofs of some cryptographic constructions using hash functions, cryptographers would like to model these latter as public random functions: this is the random oracle model (ROM) of [BR93]. Controversial [CGH04], the ROM is now superseded by the standard model. However, many practical schemes are only proved in the ROM. To increase confidence in these proofs, Coron et al. Indifferentiability captures the absence of generic adversaries against the domain extender. Informally, it means that there exists a convincing way to mimic the pair hash construction and compression function using a random oracle and a simulator. A nice composition property ensues: if the compression function behaves as a small random oracle, then the hash construction as a whole is safely modeled by a monolithic random oracle within a bigger cryptographic construction. Therefore, the domain extender does not introduce any structural weakness in the whole cryptographic construction. Consequently, and though it needs to be used with caution [RSS11], indifferentiability from a random oracle proves to be a relevant security criterion. It is worth noticing that it does capture the aforementioned weaknesses in the MD design, which is shown differentiable from a random oracle. Investigating the indifferentiability of new modes of operations proposed during the SHA-3 competition is an important issue.

To prove indifferentiability results, cryptographers need to show that two idealized systems are indistin-guishable. The first system captures the real setting: it is built from a random function in place of the compression function and a domain-extender which can query the former to compute its result. The second system is an idealized version of the first one, where the construction is replaced by a big random oracle RO and the compression function by a simulator S. To simulate the random function it replaces, S has access to RO. The main difficulty of the proof is that S should answer queries consistently while it cannot see the queries/answers of the adversary to RO.

Formal Model. As security proofs in general, indifferentiability proofs present a lot of technicalities and are hard to verify. Moreover, the quantifier order in the definition of security yields subtleties [RSS11] that recall those raised in universal composability frameworks as [Can01], [BPW03]. Yet, as cornerstones of many other cryptographic designs, hash constructions need strong and trusted security foundations. To achieve this, we believe that confidence in indifferentiability proofs can strongly benefit from a formal treatment.

Our Contribution. We propose to profit from the computational indistinguishability logic CIL proposed in [START_REF] Barthe | Computational indistinguishability logic[END_REF], whose rules are formalized in Coq. We prove a reduction theorem dedicated to indifferentiability of hash constructions in this framework. Our formalization of proofs thus contributes to bridging the gap towards their automated verification. We extend the semantics of [START_REF] Barthe | Computational indistinguishability logic[END_REF] with the notion of overlayers, that captures many iterated constructions: domain extenders, modes of operation of symmetric cryptography such as CBC-MAC or blockciphers based on Feistel networks. Our definition allows us to take into account many domain extenders used in the SHA-3 competition such as JH [Wu11], Keccak [START_REF] Bertoni | The keccak sha-3 submission[END_REF], Skein [FLS + 10] and BLAKE [START_REF] Aumasson | Sha-3 proposal blake[END_REF], the EMD transform [BR06], HMAC and NMAC modes [START_REF] Bellare | Pseudorandom functions revisited: The cascade construction and its concrete security[END_REF]. It generalizes the generic domain extenders proposed by Bhattacharyya et al. in [BMN09] since it allows post-processing and multiple inner-primitives. Then, we describe a generic simulator and prove directly in CIL a meta-theorem allowing to bound the indifferentiability of constructions from random oracles. To instantiate this theorem, users have to bound some inconsistency events that can happen in the simulator.

We show on two examples that the bounds provided by our theorem are convincing: for the ChopMD solution, we achieve the same result as Maurer and Tessaro in [MT07] in case of prefix-free padding and a better bound than that of Chang and Nandi in [CN08] in the general case. Finally, the application of our result on the sponge construction (underlying the Keccak design) highlights the lack of an additional term in the bound provided by Bertoni et al. in [START_REF] Bertoni | On the indifferentiability of the sponge construction[END_REF], as was anticipated but not justified by Bresson et al. in

[BCCM + 08].
Outline. The next section briefly provides background on CIL, while the generic definition to capture hash designs and a formal definition of their indifferentiability from a random oracle appear in section III. In section IV, we detail the construction of a generic simulator involved in our result. In V, we define characteristic graphs to capture events of bad simulation and state the reduction theorem. Finally, examples of application appear in section VI.

Notations. LISTS. Given a set A, we denote by A * (resp. A + ) the set of finite lists with elements in A (resp. non-empty finite lists). The empty list is denoted by [ ].

[L] n i=m denotes the sublist of L containing elements of L from the m-th to the n-th position. The append to the right of an element a ∈ A to a list L ∈ A * is denoted by L : a. The selective append of a to L, denoted by L.a, is defined by L.a = L, if a ∈ L and L.a = L : a, otherwise. Given an indexed set A = (a i ) i∈N , and an index set I, [a i ] i∈I denotes the list of elements a i for i ∈ I. Moreover, dom(L) denotes the set of first components of elements of L, while L(a) is the set of elements of L with first component a.

STRINGS. Given a bitstring w, |w| denotes the length of w. For s ≤ |w|, Last s (w) and First s (w) denote the suffix of w, respectively its prefix, of length s. For 1 ≤ m ≤ n ≤ |w|, w[m, n] denotes the substring of w starting with its m-th bit and ending its n-th bit. The concatenation of two bitstrings x and y is denoted by x||y. A string of length 0 is denoted by λ.

MISCELLANEOUS. ⌈x⌉ denotes the ceiling of x. We use 1 to denote the unit type. Given a finite set A, distributions on A are denoted D(A); given a ∈ A and d ∈ D(A), the probability of sampling a according to d is denoted by Pr[d = a]. The uniform distribution over A is denoted by U(A). We write to stand for elements we do not need to name.

II. ORACLE SYSTEMS AND ADVERSARIES

A. Formalization of Oracles and Adversaries

Following [START_REF] Barthe | Computational indistinguishability logic[END_REF], we use oracle systems to describe cryptographic schemes. Informally, an oracle system is composed of a finite list of stateful oracles that can be queried by an adversary. Each oracle has an implementation which is a probabilistic algorithm that may have access to other oracles. A query call to an oracle yields an output, called answer, and may modify the memory as a side effect.

Let n be a positive natural number, for each i = 1, • • • n, M i be a countable set of memories (states) and Definition II.1. An oracle system O is given by: EXAMPLE II.1. As an example of oracle system, we provide the system O, consisting of two oracles named F and K. Informally, F is a random function on bitstrings of length n and oracle K is F • F. A rigorous description of the implementations of F and K is given in Figure 1, where L F and L K are finite mappings that build the memory. The initial state is composed of the empty mappings. Initialization oracle and finalization oracle are idle.

M O = M 1 × • • • × M n . Furthermore, let o 1 , . . . , o n be disjoint names of oracles that operate on M O . An implementation of o i is a probabilistic algorithm Imp(o i ) oj 1 ,•
• a finite set N O = {o 1 , • • • , o n } of oracles that op- erate on M O equipped with their implementations Imp(o i ) oj 1 ,••• ,oj i ; • distinguished oracles o I ∈ N O ,
Oracle systems O and O ′ are called compatible, if they have the same set of oracle names, with same query and answer domains. Compatible systems can however differ in the oracle implementations and memories. We therefore use the notation

Imp O (o i ) (resp. Imp O ′ (o i )) to refer to the implementation of o i in O (resp. O ′ ).
With an oracle system O, adversaries interact by making queries and receiving answers. An interaction step produces an exchange (for an oracle system O), which is a triple (o, q, a) where o ∈ N O , q ∈ In(o) and a ∈ Out(o). Let Xch denote the set of exchanges. Final Definition II.2. An O-adversary A = (A, A ↓ ) is given by a countable set M A of adversary memories, an initial memory mA ∈ M A and functions for querying and updating:

Oracle F Imp O (F)(q, L F ) = if q ∈ dom(L F ) then return L F (q) else let a ← U({0, 1} n ) in L F := L F .(q, a); return a endif Oracle K Imp O (K) F (q, L K ) = if q ∈ dom(L K ) then return L K (q) else let a ← F(q) in let b ← F(a) in L K := L K .(q, b); return b endif
A : M A -→ D(Que × M A ) A ↓ : Xch × M A → D(M A )
Informally, the interaction between an oracle system and an adversary starts from the initial memory ( mA , mO ). Using A, A computes a query to O and updates its memory. Upon receiving a query, O updates its memory and replies to A, which in turn updates its memory. This goes on until A calls the finalization oracle. We formalize this interaction as the execution of a transition system, defined below.

Definition II.3. A transition system S consists of:

• a (countable non-empty) set M of memories (states), with a distinguished initial memory m; • a set Σ of actions, with a distinguished subset Σ F of finalization actions; • a (partial probabilistic) transition function st :

M -→ D(Σ × M). A partial execution sequence of S is a sequence η of the form m 0 act1 -→ m 1 act2 -→ . . . act k -→ m k such that m 0 = m, act i ∈ Σ, m i-1 , m i ∈ M, and Pr[st(m i-1 ) = (act i , m i )] > 0, for i = 1, . . . , k. If k = 1, then η is a step. If act k ∈ Σ F or m k ∈ dom(st)
, then η is an execution sequence of length k. A probabilistic transition system S induces a subdistribution on executions, denoted S, such that the probability P r[S = η] of a finite execution sequence η is

k i=1 P r[st(m i-1 ) = (act i , m i )].
A transition system is of height k ∈ N if all its executions have length at most k; in this case, S is a distribution.

Definition II.4. Let O be an oracle system and A be an O-adversary . The composition A | O is a transition system such that M = M A × M O , the initial memory is ( mA , mO ), the set of actions is Σ = Xch, and Σ F = Xch F , and

st A|O (m A , m O ) def = let ((o, q), m ′ A ) ← A(m A ) in let (a, m ′ O ) ← Imp O (o)(q, m O ) in let m ′′ A ← A ↓ ((o, q, a), m ′ A ) in return ((o, q, a), (m ′′ A , m ′ O )) Let k : N O → N. An adversary is called k-bounded, if for every o ∈ N O , the number of queries to o in every execution of A | O is not greater than k(o).
An adversary is called bounded, if it is k-bounded for some k. Thus, k bounds the number of oracle calls that can be performed by an adversary. To meaningfully state security properties of oracle systems, we also bound the adversary's global running time. Therefore, we consider bounds of the form (k, t) ∈ (N O → N) × N and talk about (k, t)-bounded adversaries, whose set we denote Adv(k, t).

Security properties abstract away from the state of adversaries, and are modeled using traces. Informally, a trace τ is an execution sequence η from which the adversary memories have been erased.

Definition II.5. Let O be an oracle system.

• A partial trace is a sequence τ of the form m 0 act1 -→ m 1 act2 -→ . . . act k -→ m k , where m 0 , . . . , m k ∈ M O and act 1 , . . . , act k ∈ Xch such that for i = 1, . . . , k and act i = (o i , q i , a i ), Pr[Imp O (o i )(q i , m i-1 ) = (a i , m i )] > 0. A trace is a partial trace τ such that m 0 = mO and act k = (o F , , ). • An O-event E is a predicate over O-traces.
The probability of an event is derived directly from the definition of A | O. Indeed, each execution sequence η induces a trace T (η) simply by erasing the adversary memory at each step. Consequently, for each trace τ , we define the set T -1 (τ ) of execution sequences that are erased to τ , and for every event E the probability P r(A|O : E) = P r(A|O : T -1 (E)).

B. The Logic

The logic CIL features around twenty sound rules to reason on oracle systems. It is built to establish two kinds of judgments classically used to express concrete security notions and carry out their proofs. Namely, judgments capture that a function of the adversarial resources bounds the indistinguishability between two oracle systems or the probability that an event happens in an oracle system.

Rules of the logic formalize reasoning patterns that generally appear in cryptographic proofs. Rather than simply mimic frequent steps of proofs carried out in the game-based methodology [Sho04], CIL rules stem from classic programming language and concurrent systems proof techniques, such as bisimulation relations, embedding in a context or determinization. Furthermore, the proof system comprises interface rules allowing for input of results obtained by external reasoning. We elaborate a little on bisimulations and determinization concepts, since they are used in the proof of the result presented in this paper.

Bisimulation relations appear as a key notion to formally link two oracle systems. They are indeed equivalence relations on the memories of the systems and provide an explicit relation between probabilities of classes of partial executions in both systems. Therefore, events compatible with the partition yielded by the equivalence relation happen with equal probability in two bisimilar systems. In practise, unconditional bisimulation may be insufficient. Therefor, CIL uses the notion of bisimulation up to a condition.

Oracle system determinization allows to group states and thus partial executions that correspond to the same exchange sequence. As a result, where bisimulation relations fail to formalize anticipation or delay of sampling of some values from one oracle call to another one, determinization successfully capture that such modifications yield behaviors indistinguishable by an adversary.

III. OVERLAYERS AND SECURITY CRITERION

A. Overlayers

Many cryptographic functions are built by iterating a set of inner primitives: hash functions, CBC-MAC, blockciphers... Inner-primitives take as input bitstrings of fixed length. As hash functions take as input longer bitstrings, they are based on so-called domain extenders [Mer89], [Dam90]. These specify how the input message is split into blocks that can be treated by the inner-primitives.

In [BMN09], a formal definition for domain extenders is presented. Though applicable to several known constructions, this definition does not capture constructions that include a post-processing function. Post-processing is used to compute the global hash result out of the mul-tiple inner-primitive outputs. We emphasize that postprocessing does not perform calls to inner-primitives and that these take place before post-processing. For example, the ChopMD [CDMP05] and the sponge construction [START_REF] Bertoni | Sponge functions. Ecrypt Hash Workshop[END_REF] include a post-processing function.

EXAMPLE III.1. The sponge construction relies on an inner primitive F, which is a random function from {0, 1} r+c into {0, 1} r+c , where r is the length of blocks parsed during preprocessing. For an input x, the sponge construction needs l = m + k iterations, where m is the number r-blocks of the input and k is the number of r-blocks desired in the output. The inner primitive F is called at each iteration. The output size is parameterized by K ∈ N. While the general design deals with any possible K, in the sequel we assume for sake of simplicity that K = kr, and refer the readers to [START_REF] Bertoni | Sponge functions. Ecrypt Hash Workshop[END_REF] for more details. The construction comprises two phases. During the absorbing phase, the input is padded using an injective, easily computable and invertible function Pad sp that yields a bitstring x 1 || . . . ||x m of length m * r. Then, a bitwise xor operation is applied to x j and the first r-block of the previous answer of F to compute the next query to F. During the squeezing phase, F is queried k more times to get a collection of answers (a m+1 , . . . , a l ). The final output is then obtained by concatenation of the first r bits of each a j : First r (a m+1 )|| . . . ||First r (a l ). The implementation is provided in Figure 2.

Besides the limitation mentioned previously, we notice that the case of multiple inner-primitives is not dealt with in [BMN09]. For instance, the Grøstl [GKM + 11] construction is out of scope of this definition. Hence, we introduce a new definition based on the notion of overlayer that allows to capture all hash functions based on domain extenders we are aware of. A hash design can then be described as an overlayer applied to an oracle system, where this latter defines the inner-primitives. Informally, an overlayer consists in: 1) a function Θ that describes how an input

x is padded and cut into init(x) blocks w[r(m -1) + 1, rm]); a 0 := 0 r+c ; for j = 1 to m do q j := (xj||0 c ) ⊕ a j-1 ; let a j ← F (q j ) in Q := Q : (q j , a j ); endfor for j = m + 1 to l do q j := a j-1 ; let a j ← F (q j ) in Q := Q : (q j , a j ); endfor a f := Firstr(a m+1 )|| . . . ||Firstr(a l ); Lsp := Lsp.(x, a f , Q); return a f endif where init sp (x) = m + k, with m = |w|/r and m * r the length of the output of the sponge construction.

θ 1 (x), . . . , θ init(x) (x), with init(x) ∈ [0, L]; 2) a finite sequence [o 1 , . . . ,
Figure 2. Sponge Implementation before piv(x). We call piv(x) the pivot index. 4) functions H 1 , . . . , H L that compute the input queries to the inner-primitives; 5) a post-processing function H post . EXAMPLE III.2. Let us consider the sponge construction to comment some of the choices in the notion of overlayer. Assume that the padding yields a message of p blocks of length r and that the hash is of length kr. The sponge has a two-phase structure, and the post-processing function depends on all calls in the squeezing phase. The absorbing phase consists of p calls to the inner-primitive F, while there are k calls performed during the squeezing case. For this construction, [o 1 , . . . , o L ] is then a list where F is repeated L times. Any index in the absorbing phase and the first index of the squeezing phase is a valid pivot. In practice, it is better to choose the latest possible index for the pivot since it yields a better simulator, and hence, a tighter indifferentiability bound. For sponge, this is the first index of the squeezing phase.

Henceforth, we consider hash constructions that take as input bitstrings in a finite set In H and produce hash values in a finite set Out H , where In H and Out H are arbitrary finite sets. We also consider fixed an arbitrary oracle system O with oracles in N O .

Definition III.1. An O-overlayer h is a tuple ([o 1 , . . . , o L ], Θ, (H j ) j∈{1..L} , piv, H post ), where:

• [o 1 , . . . , o L ] is a sequence of oracles in N O . • Θ : In H → ({0, 1} ≤r ) + with Θ(x) =
(θ 1 (x), . . . , θ init(x) (x)) the input transformation and r > 0 the block length. • piv : In H → [1, L] outputs a pivot index such that piv(x) ≤ init(x). For simplicity, we require that there is an oracle o piv , that we call the pivot oracle, such that for any x, o piv(x) = o piv .

• functions H 1 : {0, 1} ≤r → In(o 1 ) and H j :

{0, 1} ≤r × Xch → In(o j ) for j = 2, . . . , L. • H post : In H × Out o piv × Xch * → Out H is the post- processing function.
Thus,

H post (x, y, Q) is the hash of x, when Q = (o k , q k , a k ) k∈[1,init(x)]
is the list of exchanges generated by the H j functions for x and y = a piv(x) . EXAMPLE III.3. Consider again the sponge construction. Then, the pivot is piv sp (x) = m + 1, H j (x j , (F, q j-1 , a j-1 )) = (x j ||0 c )⊕a j-1 for j = 1..p, and H post (x, a piv sp (x) , [(F, q j , a

j )] j>piv sp (x) ) = First r (a piv sp (x) )|| . . . ||First r (a initsp(x) ).
Moreover,

θ j (x) = x j for j ∈ [1..m], and θ j (x) = 0 r for j ∈ [m + 1, init(x) sp ].
We require overlayers to satisfy the following conditions that are met by all hash designs we know about:

1) the function Θ is injective;

2) H post only depends on pivot and post-pivot queries. Formally, for all lists Q and Q ′ and all x, y, if

[Q] k>piv(x) = [Q ′ ] k>piv(x) then H post (x, y, Q) = H post (x, y, Q ′ ). Therefore, we sometimes write H post (x, a piv(x) , [Q] k>piv(x) ) in- stead of H post (x, a piv(x) , Q).

Definition III.2. The composition of an O-overlayer h with O defines an oracle system which contains the oracles of O augmented with the overlayer oracle H

given by:

• the memory L H of oracle H is a mapping from In H to Out H × Xch * ; its initial value is the empty mapping. • The implementation of oracle H is given in fig- ure 3.

B. Security Definition of Hash Constructions

A widely accepted approach for proving properties of hash constructions consists in assuming idealized inner-primitives (e.g. random functions) and proving ), which is commonly named indifferentiability from a random oracle. In our framework, this notion is formalized as a comparison between two oracle systems: one where the real hash mode is used as an overlayer of an idealized (inner) oracle system, and another where the hash construction is idealized as a random oracle and a simulator makes up for the inner system. We thus introduce a notation for idealization by uniform functions before writing our formalization for indifferentiability.

Imp(H) o 1 ,...,o L (x, L H ) = if x ∈ dom(L H ) then return L H (x) else l := init(x); (x 1 , . . . , x l ) := Θ(x); q 1 := H 1 (x 1 ); let a 1 ← o 1 (q 1 ) in Q := [(o 1 , q 1 , a 1 )]; for j = 2 to l do q j := H j (x j , (o j-1 , q j-1 , a j-1 )); let a j ← Imp O (o j )(q j ) in Q := Q : (o j , q j , a j ); endfor a f := H post (x, a piv(x) , [Q] k>piv(x) ); L H := L H .(x, a f , Q); return a f endif
We denote by RO(H) the oracle implemented as a random function on Out H using a list (mapping) L H as follows: The oracle set S in this definition is usually refered to as the simulator. It is not a stand-alone oracle system, since it requires access to RO(H) to compute its outputs.

if x ∈ dom(L H ) then return L H (x) else let y ← U(Out H ) in L H := L H .(x,
IV. GENERIC SIMULATOR Indifferentiability proofs are difficult because one has to come up with a simulator which mimics the innerprimitives consistently despite the fact that it cannot access the list of the adversary calls to the hash oracle.

Consider for example the oracle system in Example II.1. To replace K by a random oracle and simulate F, we have to take into account that F(F(x)) = K(x) is true for any x ∈ {0, 1} n in the real setting. Hence, if an adversary queries F(x), gets y and then queries F(y), a simulator of F has to output an answer matching K(x). Otherwise, a distinguisher can perform this query and in case K(x) = F(y), claim to interact with the simulated world. Thus, the simulator should query K on x, and forward what it gets as a reply to the query F(y).

We can now extrapolate a simulation strategy. The key idea is to detect when an adversary has enough information to compute a hash value for some input x. In other words, when queried on a value q, the simulator has to determine whether and to which x the adversary can associate a hash value, given an answer for q. In case such an x is determined, the simulator queries the hash of x to get a result t. Then, it uses t to enforce that the remaining calls to the inner-primitives needed for computing the hash of x are consistent with t. Thus, the idea is to identify chains of queries that can correspond to a hash execution. Our simulator uses an algorithm which, given a list of oracle queries and a query to the pivot oracle, decides whether and for which hash input the latter is a pivot query. In case it is, this algorithm outputs a matching hash input and a list of pre-pivot queries, among the given list of queries. Such an algorithm is called a path-finder1 . Intuitively, it should have a non-trivial output as soon as there exists a satisfactory one, and any non-trivial output should correspond to a satisfying answer. This is captured by the following definition, where L S denotes a list variable containing all exchanges performed with the simulator so far.

Definition IV.1. A path-finder algorithm PathFinder takes as input a query q ∈ In o piv and list L S of queries and answers performed to oracles in O. Its output is either the triple (false, λ, [ ]), or a triple of the form (true, x, List), with (x, List) ∈ In H × Xch * such that: 1) for any answer y to q, if there exists x ∈ In H such that H(x) yields a list of queries Q satisfying

[Q] i<piv(x) ⊆ L S and [Q] i=piv(x) = (o piv , q, y), then PathFinder outputs (true, , ) 2) if
PathFinder(q, L S ) = (true, x, [(o 1 , q 1 , y 1 ), . . . , (o p-1 , q p-1 , y p-1 )]) then [(o 1 , q 1 , y 1 ), . . . , (o p-1 , q p-1 , y p-1 )] ⊆ L S , and this list corresponds to the beginning of a hash execution on x, namely:

       piv(x) = p, q 1 = H 1 (θ 1 (x)), ∀j ∈ [2..p -1], q j = H j (θ j (x), (o j-1 , q j-1 , y j-1 )) q = H p (θ p-1 (x), (o p-1 , q p-1 , a p-1 ))
We assume that the execution time of the path-finder algorithm is bounded by a function t PathFinder (Card(L S )).

When the simulator detects a pivot query that allows to say H(x) = t, it has to impose answers to pivot and post-pivot queries consistent with t. More precisely, consistency is achieved when applying H post to pivot answer and post-pivot exchanges yields t. To perform this task, we introduce another algorithm: the forward sampler.

Given x and t, there is a set of lists of exchanges [v j ] init(x) j=piv(x)+1 and values for y such that H post (x, y, [v j ] init(x) j=piv(x)+1 ) = t. We denote this set by PreIm(t). Informally, a forward sampler is an algorithm that samples an element in PreIm(t) while preserving the original distribution of ((y, [v j ] init(x) j=piv(x)+1 ), t). Obviously, a necessary condition for the existence of a forward sampler is that PreIm(t) is not empty.

Definition IV.2. A forward sampler

FwdSplr is an algorithm that takes as input a pair (x 0 , t 0 ) and outputs a distribution such that:

P r[U(Out H ) = t 0 ]P r[FwdSplr(x 0 , t 0 ) = (y 0 , L 0 )] = P r U(Out o piv ) = y 0 ∧ init(x) j=piv(x)+1 U(Out o j ) = y j ∧ L 0 = [v j ] init(x) j=piv(x)+1 ∧ (y 0 , L 0 ) ∈ PreIm(t 0 ) where v j = (o j , H j (θ j (x), v j-1
), y j ), for j = piv(x) + 1, . . . , init(x). We require that the execution time of FwdSplr is bounded by constant t FwdSplr . EXAMPLE IV.1. To get some intuition about this definition let us consider a degenerated case, where Out H = U(Out o piv ), the pivot is the last step of iteration and H post forwards the answer of the last query performed by the hash algorithm. Thus, intuitively, we expect that for each pair (x 0 , t 0 ), PreIm(t 0 ) is the singleton (t 0 , [ ]) and a forward sampler should output this pair with probability 1. We check that this is what our definition imposes:

P r[U(Out o piv ) = t 0 ∧ init(x) j=piv(x)+1 U(Out o j ) = y j ∧ [ ] = [v j ] init(x) j=piv(x)+1 ∧ (t 0 , [ ]) ∈ PreIm(t 0 )] = P r[U(Out o piv ) = t 0 ∧ (t 0 , [ ]) ∈ PreIm(t 0 )] = P r[U(Out o piv ) = t 0 ] = P r[U(Out H ) = t 0 ]. Therefore, P r[FwdSplr(x 0 , t 0 ) = (t 0 , [ ])] = 1.
We can now provide implementations of oracles in the generic simulator. We recall that L S (o i ) denotes the list of all tuples starting with o i appearing in L S and that if (o i , q, y) is one of these tuples, L S (o i , q) denotes the value y, which is unique by construction.

Definition IV.3. The generic simulator S is the following set of oracles compatible with O. They have a shared memory of the form L S ∈ Xch * , and the initial memory m of a system containing the simulator is chosen so that m.L S = [ ]. Moreover, o piv is implemented as follows:

Imp S (o piv ) H (q, L S ) = if q ∈ dom(L S (o piv )) then return L S (o piv , q) elsif PathFinder(q, L S ) = (true, x, List) then let t ← H(x) in (y, L) := FwdSplr(x,
Imp S (o) H (q, L S ) = if q ∈ dom(L S (o)) then return L S (o, q) else let y ← U(Out o ) in endif L S := L S .(o, q, y); return y
If we let c be a constant bounding the time necessary to search in L S , the implementation of o piv is (k s , t s )-bounded, where k s (H) = 0, and t FwdSplr + t PathFinder (Card(L S )) + c. The implementation of the other oracles is (0, c)-bounded.

This simulator works completely independently of the fact that multiple outputs may exist from which the path-finder has to choose. However, we notice that if it is possible that the path-finder can answer two distinct hash inputs x, x ′ for a pivot query, the simulator can only anticipate the adversary queries for one of these inputs to H. If the adversary can easily uncover such values, our simulation strategy is flawed and should yield a large indifferentiability bound, which can reflect a misconception in the hash construction or a bad choice of the pivot index.

V. THE THEOREM Even though path-finder and forward sampler algorithms may prevent some obvious inconsistencies introduced in the idealized system, there are still cases in which they are not sufficient. Namely, when a pivot query is made to the simulator, consistency can only be enforced if, on the one hand, the path-finder can detect that it is a pivot query, and on the other hand, the pivot and post-pivot queries are still fresh, i.e., answers to these queries have not been yet generated.

A. Capturing Dependencies: Anticipating System and Characteristic Graph

We want to capture dependencies enforced in the real setting by intermediate queries (performed by H to oracles in O) in addition to direct and anticipated queries. To this end, we start by defining an intermediate system, the anticipating system O ant , which is the real system augmented with the anticipation of the postpivot queries by oracle o piv , and visibility labels that we introduce later on. The implementations of oracles in this system can be found in figure 4. This hybrid system, by enforcing the computation of all exchanges ever playing a role in the answer to the adversary, highlights problematic configurations.

Then, we introduce the characteristic graph, a data structure dedicated to the representation of dependencies between exchanges. Vertices of the graph are exchanges (o, q, a) computed either via a direct query or and indirect one. If an edge links two vertices, it means that they can be successive exchanges in a hash computation. To formalize that an adversary does not acquire the same knowledge of direct queries and intermediate queries necessary to the computation of a hash value, the visibility map associates vertices to visibility labels in {Inv, P V is, V is} (standing for invisible, partially visible and visible and are ordered this way).. Intuitively, for an interaction with the anticipating system, pre-pivot intermediate exchanges are labelled invisible, while pivot and post-pivot are deemed partially visible. Moreover, direct exchanges are considered visible, as are exchanges anticipated by the simulator.

Formally, characteristic graphs are defined as follows.

Definition V.1. A characteristic graph CG is defined by a tuple (v root , V, E, V) where:

• a root v root , Imp O ant (H)(x, L H , L S ) = if x ∈ dom(L H ) then (a f , Q) := L H (x); L H := L H .(x, a f , Q); return a f else l := init(x); p := piv(x); (x 1 , . . . , x l ) := Θ(x); (o 1 , q 1 ) := H 1 (x 1 ); if q 1 ∈ dom(L S (o 1 )) then (a 1 , lbl) := L S (o 1 , q 1 ); Q := [(o 1 , q 1 , a 1 , lbl)]; else let a 1 ← U(Out o 1 ) in L S := L S .(o 1 , q 1 , a 1 , Inv); Q := [(o 1 , q 1 , a 1 , Inv)]; endif for j = 2 to p -1 do (o j , q j ) := H j (x j , (o j-1 , q j-1 , a j-1 )); if q j ∈ dom(L S (o j )) then (a j , lbl) := L S (o j , q j ); Q := Q : (o j , q j , a j , lbl); else let a j ← U(Out o j ) in L S := L S .(o j , q j , a j , Inv); Q := Q : (o j , q j , a j , Inv); endif endfor for j = p to l do (o j , q j ) := H j (x j , (o j-1 , q j-1 , a j-1 )); if q j ∈ dom(L S (o j )) then (a j , lbl) := L S (o j , q j ); L S := L S .(o j , q j , a j , max(P V is, lbl)); Q := Q : (o j , q j , a j , max(P V is, lbl)); else let a j ← U(Out o j ) in L S := L S .(o j , q j , a j , P V is); Q := Q : (o j , q j , a j , P V is); endif endfor a f := Hpost(x, a p , [Q] j>p ); L H := L H .(x, a f , Q); return a f endif If o i = o piv : Imp O ant (o i )(q, L S ) = if q ∈ dom(L S (o i )) then (y, ) := L S (o i , q); else let y ← U(Outo i ) in endif L S := L S .(o i , q, y, V is); return y Imp O ant (o piv )(q, L S , L H ) = if q ∈ dom(L S (o piv )|V is) then (y, V is) := L S (o piv , q); elsif PathFinder(q, L S ) = (true, x, List) then let t ← H(x) in (o piv , q, y) : L := Π 3 (L H (x)) j≥piv(x) ; L S := L S .((o piv , q, y, V is) : (L, V is)); elsif q ∈ dom(L S (o piv )|P V is, Inv) then (y, ) := L S (o piv , q); L S := L S .(o piv , q, y, V is); else let y ← U(Outo piv ) in L S := L S .(o piv , q, y, V is); endif return y
For tuple (o i , q, y, lbl) ∈ L S , L S (o i , q) denotes the pair (y, lbl) (which is unique by construction). We denote (L, lbl) a list of exchanges consisting in L except that all visibility labels are replaced by lbl, and (L|lbl) is the restriction of list L to elements of label lbl.

• a finite set of vertices V ⊆ Xch, • a set E ⊆ (V ∪ v root ) × {0, 1} ≤r × V of labeled edges such that: 1) (o 1 , q, a) ∈ V , (v root , x 1 , (o 1 , q, a)) ∈ E im- plies q = H 1 (x 1 ); 2) for j ≥ 2, ((o j-1 , q, a), x j , (o j , q ′ , a ′ )) ∈ E implies q ′ = H j (x j , (o j-1 , q, a)).
• V is a visibility map, which associates to every vertex in V a value in {Inv, P V is, V is}, • E contains all possible edges linking visible vertices:

1) for all visible vertex (o 1 , q, a), q = H 1 (x 1 ) implies (v root , x 1 , (o 1 , q, a)) ∈ E ; 2) for j ≥ 2, for all visible vertices ((o j-1 , q, a) and (o j , q ′ , a ′ )), if q ′ = H j (x j , (o j-1 , q, a)) then ((o j-1 , q, a), x j , (o j , q ′ , a ′ )) ∈ E.

The set of characteristic graphs is denoted by CG. We distinguish a particular graph CG init = (v root , [ ], ∅, V init ) with dom(V init ) = ∅ which we call the initial characteristic graph. We use the term nonvisible to refer to vertices which are either partially visible or invisible. Moreover, we talk about visibility of queries: the visibility of a query (o, q) is the same as that of the (unique) vertex v in a characteristic graph such that v = (o, q, ). Intuitively, we are interested in chains of exchanges exhibited by the characteristic graph. We thus introduce the following terminology.

Definition V.2. • Given a graph, a path is a chain v 0 l1 → v 1 l2 → • • • ln → v n of vertices v i such
that for all i, edge (v i , l i , v i+1 ) belongs to the graph.

• A rooted path is a path starting with vertex v root .

A vertex is rooted whenever it belongs to a rooted path.

• A meaningful path is a rooted path such that if [x 1 , . . . , x L ] is the list of labels on the sequence of edges, then there exists x such that ∀j = 1..L, θ j (x) = x j . • A meaningful path is said to be complete when L = init(x). In such cases, bitstring x is then said to label the meaningful path to which it corresponds.

B. Inconsistency Events

As foreseen previously, we face two main causes of inconsistencies. On the one hand, we can only expect that the path-finder detects pivot queries in case all pre-pivot queries have been performed before by the adversary, i.e. , in case they form up a rooted path of visible queries in the characteristic graph. On the other hand, a pivot or post-pivot query corresponding to a hash input x can be already bound to an answer at the moment when the simulator detects that it is asked a pivot query. In such a case, this latter carries on running the forward sampler, but when updating the list of queries, it stumbles upon a preexisting vertex.

As far as the characteristic graph is concerned, it means that we have to ensure three invariants:

1) no two meaningful rooted paths have a common vertex, 2) along meaningfully rooted paths, visibility labels increase, 3) no vertex creation results in linking a meaningfully rooted path with a preexisting vertex. Each time one of these invariants is broken, it corresponds to an inconsistency event, i.e. a case of bad simulation, acknowledged on the characteristic graph. However, probabilities are only defined over traces previously. As a result, we need to define a way to map traces to sequences of graphs. Intuitively, this can be done putting to use a function Γ mapping a state to a characteristic graph. Then, calls to oracles o i yield a sequence of length 1 and calls to the hash oracle are mapped to the sequence of graphs yield by applying function Γ to each intermediate state created during the iteration.

Definition V.3. Given a characteristic graph CG, v is a collision vertex, denoted v ∈ CollVertex(CG), if there exist at least two distinct edges having v as a target (i.e. there exists (v ′ , l ′ ) = (v ′′ , l ′′ ) such that edges (v ′ , l ′ , v) and (v ′′ , l ′′ , v) appear in the graph), and both of them belongs to a meaningfully rooted path going through v.

We now introduce inconsistency predicates (cf figure 5 -a), mapping a graph stage to a boolean value, and formalize inconsistency events using the temporal operator "eventually". Definition V.4. Let CG (o,q,y) -→ CG ′ be a graph stage. The inconsistency predicates are:

v, v ′ ∈ V ′ s.t. firstly, V ′ (v) = V is and V ′ (v ′ ) = V is, secondly, a meaningful path goes through v ′ in CG ′ and lastly edge (v ′ , , v) is in E ′ .
• Link evaluates to true if (o, q, y) is a visible vertex of CG ′ not belonging to CG and there exists a visible vertex (o ′ , q ′ , y ′ ) in V such that a visibly meaningfully rooted path of CG ′ goes through (o, q, y) and (o ′ , q ′ , y ′ ).

C. The Theorem

We can now state our theorem, according to which the indifferentiability between real and simulated systems is bounded by the probability of inconsistency events. THEOREM V.1. Let h be an O-overlayer. The composition of h and RO(O) yields an oracle system (H RO(O) , RO(O)). We denote by S the generic simulator and O ant the anticipating system, which we have defined above. Then, for all adversaries A ∈ Adv(k, t), 6.

We have built the anticipating system O ant out of the real system by changing the implementation of the pivot oracle so that it pre-computes the exchanges that the forward sampler is meant to anticipate inside the simulator. Therefore, perfect indistinguishability of the real system (H O , O) and the anticipated system O ant follows from an argument of determinization.

v 2 v 0 v 1 x 0 →2 x 1 →2 b-Vertices Involved in F Collide Figure 5. determinization (H O , O) ∼ 0 O ant Bisimulations up to condition φ relate O ant to FwdSpl Pr[φ] ≤ Pr[F Collide∨Reveal∨Link ] = ǫ O ant ∼ ǫ FwdSpl determinization FwdSpl ∼ 0 (RO(H), S RO(H) ) (H O , O) ∼ ǫ (RO(H), S RO(H) ) Figure 6. Sketch Of Proof
The motivation behind the next step in the proof is to break the dependency existing between a hash oracle input and the matching output. We show that O ant is indistinguishable of another system, denoted FwdSpl, which is defined as follows. On a fresh input, the hash oracle resamples all pre-pivot exchanges (no matter their freshness), which yields a pivot query. Then, the oracle draws a hash output uniformly at random and applies FwdSplr to compute a pivot answer and postpivot exchanges coherent with the hash output. As for the anticipating system, pre-pivot exchanges are deemed invisible and pivot and post-pivot ones partially visible.

Linking systems O ant and FwdSpl involves bisimulation-up-to arguments. Informally, we prove that invisible exchanges can be resampled up to some criterion, before getting rid of the test of this criterion and replacing original code with executions of forward sampler. Conditions on the bisimulation relations can be shown to hold as soon as no inconsistency predicate is broken. As a result, we can conclude that an adversary cannot distinguish between interacting with O ant and FwdSpl with a better advantage that the probability that Reveal, Collide or Link occurs.

Finally, we justify the perfect indistinguishability between FwdSpl and (RO(H), S RO(H) ) by a determinization argument: indeed, as the hash oracle in FwdSpl computes a sequence of exchanges independent from its answer during its execution, we consider that this constitutes an anticipation of computations that system (RO(H), S RO(H) ) only performs when necessary, i.e. when o piv is called on a pivot query.

Generalization. The theorem and proof provided here are expressed for inner-primitives with random functions. Dealing with random permutations yields minor changes in the detailed proof and adds a term in the bound of the indifferentiability advantage capturing failure of injectivity as a possible bad simulation event.

VI. APPLICATIONS

Our generic theorem reminds the importance of preventing length-extension attacks. Namely, applying the theorem on the MD mode yields a bound worth 1, as length extension always allows to realize event Reveal.

In our examples of application, we do not provide implementation for a path-finder algorithm (though to obtain an instantiated bound on the execution time we should), but only specify forward sampler algorithms.

As the events F Collide , F Reveal and F Link can intersect, we take care to evaluate slightly weaker events but which partly avoid that some overlapping increases artificially the bound. The following decomposition proves useful in both examples we develop.

As there is only one possible label for an edge between two vertices, when event F Collide happens and results in the creation of a collision vertex v 2 , then it necessarily involves vertices v 0 , v 1 linked to v 2 such that v 0 = v 1 . Without loss of generality, we suppose that v 0 is created before v 1 (see figure 5). We denote v 1 = ( , q 1 , a 1 ) and let RootCollide capture the event that v 0 = v root and v 1 is created such that the collision happens. Then necessarily, there exist j, x 0 →2 , x 1 →2 such that H 1 (x 0 →2 ) = H j (x 1 →2 , ( , q 1 , a 1 )) since they both equal the query part of v 2 . Furthermore, WkCollide is verified when v 0 = v root is ( , q 0 , a 0 ), and v 1 is created; i.e. when there exist (j, x 1 →2 ) and (j ′ , x 0 →2 ) such that H j (x 1 →2 , ( , q 1 , a 1 )) = H j ′ (x 0 →2 , ( , q 0 , a 0 ))Note that we reason on the appearance of v 1 in the graph, whether it is before or after creation of v 2 . It allows us to state that F Collide implies F RootCollide∨WkCollide . We define WkLink as the event in which a vertex v 1 is created and gets linked to a preexisting vertex v 2 , without imposing any visibility constraint on the vertices v 1 and v 2 . We can see that F Collide∨Reveal∨Link is implied by

F WkLink ∨ F RootCollide∨WkCollide ∨ F Reveal∧¬WkLink∧¬Collide .

A. The Sponge Construction

We define the forward sampler so that it parses a hash output t into k blocks of r bits and draws iteratively the c missing bits of the answers to pivot and postpivot queries. Its precise implementation is provided in appendix A.

If F WkCollide happens at the ℓ-th fresh query then there exist (j, x 1 →2 ) and (j ′ , x 0 →2 ) such that H j (x 1 →2 , (F, q 1 , a 1 )) = H j ′ (x 0 →2 , (F, q 0 , a 0 )), which imposes Last c (a 0 ) = Last c (a 1 ). Since a 1 is drawn uniformly at random, this happens with probability at most ℓ-1 2 c . Summing on ℓ yields a bound of ktot(ktot-1)

2 c+1
. When F RootCollide occurs, there exists v 1 such that H 1 (x 0 →2 ) = H j (x 1 →2 , (F, q 1 , a 1 )) for some labels x 0 →2 and x 1 →2 and index j. Hence, the last c bits of a 1 to be worth 0 c . The probability that this happens is bounded by ktot 2 c . If F WkLink happens at the ℓ-th direct query creating v 1 , then there exists v 2 to which v 1 gets linked by an edge (j, x j ). With a 1 drawn uniformly at random, the probability that there is a v 2 such that H j (x j , (F, q 1 , a 1 )) = q 2 is at most ℓ-1 2 c . Summing on ℓ, it results in a bound of ktot(ktot-1)

2 c+1
. Finally, we bound the probability of F Reveal∧¬WkLink∧¬Collide by k(F ) 2 c . Indeed, if this occurs, a vertex v 1 = (F, q 1 , a 1 ), non-visible, gets linked to v 2 = (F, q 2 , a 2 ), visible, by an edge labeled by (j, x j ). Since we assume ¬WkLink, necessarily, v 1 is created before v 2 . Realizing Reveal means that H j (x j , (F, q 1 , a 1 )) = q 2 . Since we assume ¬Collide, there is only one vertex v 1 which can satisfy this equation. With v 1 at most partially visible, the probability that a good query q 2 is issued is bounded by 1 2 c . To conclude, we sum over the total number of direct queries. THEOREM VI.1. We consider the sponge construction. For an adversary A ∈ Adv(k, t), . We obtain a greater bound, containing terms which are omitted in their final bound computation, as was first suggested in [BCCM + 08]. The missing term corresponds to the probability that length-extension attacks can be carried out, which, even though the authors propose a simulator different from ours, should not be overlooked in their computation.

Indiff(Sponge, RO(F), RO(Sponge), S) ≤ k 2 tot 2 c + k(F) 2 c where k tot = k(F) + L sp * k(H).

B. The ChopMD Construction

We consider the hash function ChopMD introduced in [CDMP05] and inspired of [DGH + 04]. For sake of completeness, we describe it in appendix A. It is obtained from the Merkle-Damgård construction by chopping off the last s bits of the output in order to prevent extension attacks.

On input (x, t), we define FwdSplr to sample uniformly the s missing bits to compute the result of the pivot query y piv(x) , and outputs the concatenation of t with these bits. Probability computations are very similar to the sponge case, see appendix A for details. THEOREM VI.2. We consider the ChopM D s construction. For an adversary A ∈ Adv(k, t),

Indiff(ChopM D s , F, RO(ChopM D s ), S) ≤ k 2 tot 2 n + k(F) 2 s where k tot = k(F) + L * k(H).
Indifferentiability results for the Chop construction already appear in various works. In [CDMP05], Coron et. al. determine a bound for this construction considering a random permutation in place of F. We only have a result for random functions, yet we notice that their proof results in a bound of O( (L.ktot) 2 2 s ), which is the same magnitude.

Later, Maurer and Tessaro show in [MT07] that using a prefix-free padding function yields a bound of O( (L * ktot) 2

n

). We obtain the same bound: no meaningful path can be obtained as an extension of a meaningful path, so that Reveal can only happen when y ′ = First n (q) belongs to an invisible vertex. As a consequence, the adversary has to guess all n bits of y ′ and our second term becomes k(F ) 2 n . Finally, our result slightly improves the

O( 3(n-s)(k(F )+k(H)) 2 s
) of Chang and Nandi in [CN08].

VII. CONCLUSION AND FUTURE WORK

In this paper, we have presented a generic reduction theorem to prove indifferentiability from a random oracle for hash constructions when their inner-primitives are modeled by random functions. In an attempt to develop a formal approach to security proofs, we have extended the framework of the logic CIL of [BDK + 10] with a formalization of modes of operationsoverlayers -and proven our theorem in this logic.

) = {0, 1} ≤2 64 , Out(ChopM D s ) = {0, 1} n-s Imp(ChopM D s ) F (x, L chop ) = if x ∈ dom(L chop ) then return L chop (x) else l := ⌈|x|/r⌉; w := x||10 l * r-|x|-1 ;
(w 1 , . . . , w l ) := (w[1, r], . . . , w[r(l -1) + 1, rl]); a 0 := 0 n ; for j = 1 to l do q j := a j-1 ||w j ; let a j ← F(q j ) in endfor a f := First n-s (a l );

L chop := L chop .(x, a f ); return a f endif

A. Additional Details Of Proofs Of Applications

1) The Sponge Construction: The implementation of the forward sampler used by the simulator for the sponge construction is as follows:

FwdSplr(x, t) = (t 0 , . . . , t k-1 ) := (t[1..r], . . . , t[(k -1)r + 1, r]); let t ′ ← U(c) in y 0 := t 0 ||t ′ ; q 1 := y 0 ; for j = 1 to k -1 do let t ′ j ← U({0, 1} c ) in y j := t j ||t ′ j ; v j := (F, q j , y j ); q j+1 := y j ; endfor return (y 0 , [v j ] j=(piv(x)+1)..(piv(x)+k-1) )

2) The ChopMD Construction: The implementation of the Chop construction can be found in figure 7. This section details the computations leading to the bound in the theorem instantiated with the ChopMD construction.

If WkCollide happens at the ℓ-th fresh query, then the equation between v 0 and v 1 imposes a 0 = a 1 . For a random a 1 , this happens with probability less than ℓ-1 2 n . Summing on ℓ, it results in a bound of ktot(ktot-1)

2 n+1
. In turn, if F RootCollide holds, then there exist j, x 0 →2 , x 1 →2 such that H 1 (x 0 →2 ) = H j (x 1 →2 , (F, q 1 , a 1 )). Necessarily, j > 1, otherwise v 1 = v 2 . It yields a 1 = 0 n , occuring with probability less than ktot 2 n . Then we bound of the probability that F WkLink occurs by ktot(ktot-1)

2 n+1
. Indeed, if it happens at the ℓ-th fresh query to F, then there exists a vertex v 2 to which v 1 gets linked by an edge (j, x j ). Since answer a 1 is random, the probability that there is a v 2 such that H j (x j , (F, q 1 , a 1 )) = q 2 is bounded by ℓ-1 2 n . We conlude by summing on ℓ.

Finally, when F Reveal∧¬WkLink∧¬Collide occurs, there exists a vertex v 1 = (F, q 1 , a 1 ), non-visible, which gets linked to v 2 = (F, q 2 , a 2 ), visible, by an edge labeled by (j, x j ). Again, ¬WkLink implies v 1 is created before v 2 . Since Reveal happens, H j (x j , (F, q 1 , a 1 )) = q 2 . Because of ¬Collide, there is only one satisfactory vertex v 1 . With v 1 at most partially visible, the probability that a satisfactory query q 2 is performed is bounded by 1 2 s . We then have to sum over the total number of direct queries issued, which provides a bound of k(F ) 2 s . These three bounds result in a global bound of

k 2 tot 2 n + k(F ) 2 s . B. CIL Rules Used in The Proof 1) Determinization: Definition A.1. Let O and O ′ be compatible oracle systems. O determinizes O ′ by distribution γ : M O → D(M ′′ O ), written O ≤ det,γ O ′ , iff firstly M O × M ′′ O = M O ′ ,
∈ N O , q ∈ In(o), a ∈ Out(o), m 1 , m 2 ∈ M O and m ′′ 2 ∈ M ′′ O : Pr[γ(m 2 ) = m ′′ 2 ] p 1 = m ′′ 1 ∈M ′′ O Pr[γ(m 1 ) = m ′′ 1 ] p 2 (m ′′ 1 )
where: -→ (m, m a ). For every O-adversary A and every

p 1 = P r[Imp O (o)(q, m 1 ) = (a, m 2 )] p 2 (m ′′ 1 ) = P r[Imp O ′ (o)(q, (m 1 , m ′′ 1 )) = (a, (m 2 , m ′′ 2 ))] We start
m ′′ ∈ M ′′ O : P r(A|O : η)P r[γ(m) = m ′′ ] = η ′ |π(η ′ )=η Last(η ′ )=((m,m ′′ ),ma) P r(A|O ′ : η ′ )
where τ ′ is any partial O ′ -execution.

LEMMA A.2. We consider two compatible oracle systems O and O ′ .

O ≤ det,γ O ′ I-Det O ∼ 0 O ′ Proof:
The previous lemma A.1 immediately results in Pr(A|O : E) = Pr(A|O ′ : E • π) for every O-event E and adversary A. In turn, this equality yields our result.

2) Forward Bisimulation-up-to: The idea behind this bisimulation is the following: states are grouped in classes according to an equivalence relation R. This relation is relevant if given two states in a same class, they offer the same possibility of evolution with the same probabilities. -→ >0 m 4 such that m 1 R m 3 , the following properties hold:

• stability: if m 2 R m 4 then φ((o, q, a), m 1 , m 2 ) ⇔ φ((o, q, a), m 3 , m 4 ) • compatibility: if φ((o, q, a), m 1 , m 2 ), then P r[Imp O+O ′ (o)(q, m 1 ) ∈ (a, C(m 2 ))] = P r[Imp O+O ′ (o)(q, m 3 ) ∈ (a, C(m 2 ))]
where C(m 2 ) is the equivalence class of m 2 under R, and

P r[Imp O+O ′ (o)(q, m 1 ) ∈ (a, C(m 2 ))] = m R m2 P r[Imp O+O ′ (o)(q, m 1 ) ∈ (a, m)].
we consider fixed O, O ′ , R and φ satisfying the above definition. The relation defined on states can be lifted to (partial) executions quite easily.

Definition A.3. Let η and η ′ be two partial execu- tions of A | O or A | O ′ of length k such that η = (m 0 , m 0 a ) act1 -→ (m 1 , m 1 a ) act2 -→ . . . act k -→ (m k , m k a ) and η ′ = (m ′ 0 , m 0 a ) act1 -→ (m ′ 1 , m 1 a ) act2 -→ . . . act k -→ (m ′ k , m k a ). They are said to be in relation by R, denoted η R η ′ , iff m i R m ′ i for all i ∈ [0..k]. The equivalence class of η is defined by C(η) = {η ′ | η R η ′ }. The O-class of η, denoted C O (η), is the intersection with O-traces of C(η).
Its probability is given by:

P r[A | O : C O (η)] = η ′ ∈C O (η) P r[A | O : η ′ ]
A similar definition can be written for O ′ .

Consider a state m 1 ∈ M O , in relation with m 3 ∈ M O ′ .
According to the definition of bisimulation up to, if we perform one step for which φ holds from m 1 and its successor or m 3 and its successor, then we can move to the same equivalence classes of states with the same probability. Say we have gone through such a step: m 1 act -→ m 2 and m 3 act -→ m 4 , and m 2 R m 4 . We can iterate the same reasoning on m 2 and m 4 . Informally, we can anticipate that if we perform a series of steps for which φ holds, it yields equivalence classes on executions with same probabilities in O and O ′ .

LEMMA A.3. Let η be a partial execution of A | O of length k such that η = (m 0 , m 0 a ) act1 -→ (m 1 , m 1 a ) act2 -→ . . . act k -→ (m k , m k a ). P r[A | O : C O (η)] = Π k i=1 P r[A | O : C O ((m i-1 , m i-1 a ) acti -→ (m i , m i a ))] where P r[A | O : C O ((m i-1 , m i-1 a ) acti -→ (m i , m i a ))] = mi R mi Pr[(m i-1 , m i-1 a ) acti -→ ( mi , m i a )]
We can now show that given related partial executions for which φ holds at every step, we have equal probabilities to make a next step not verifying φ when interacting with A | O as when interacting with

A | O ′ . LEMMA A.4. Let η be a partial execution of A | O of length k such that φ holds for each of its steps: η = (m 0 , m 0 a ) act1 -→ (m 1 , m 1 a ) act2 -→ . . . act k -→ (m k , m k a ) and ∀i = 1..k, φ(x i , m i-1 , m i ) • Let σ = (m k , m k a ) x k+1 -→ (m k+1 , m k+1 a ) be a step. Let η ′ = η • σ. If φ(x k+1 , m k , m k+1 ) then P r[A | O : C O (η ′ )] = P r[A | O ′ : C O ′ (η ′ )] • P r[A | O : η 0 • σ 0 ∧ (η 0 R η) ∧ ¬φ(σ 0 )] = P r[A | O ′ : η 0 • σ 0 ∧ (η 0 R η) ∧ ¬φ(σ 0 )] LEMMA A.5. We consider two compatible oracle sys- tems O and O ′ such that O ≡ R,ϕ O ′ . Then Pr[A | O : R = true ∧ G φ ] = Pr[A | O ′ : R = true ∧ G φ ].
3) Backwards Bisimulation-up-to: Forward bisimulation-up-to is powerful, but ill-conceived to capture arguments meant to tamper with values computed in past steps instead of changing the way we compute values in the current step or in future steps. This justifies the notion of backwards bisimulation-up-to, formally defined as follows.

Definition A.4. Let R ⊆ M O+O ′ × M O+O ′ be an equivalence relation and φ be a predicate. O and O ′ are in backwards bisimulation with R up to φ iff the initial states is alone in their equivalence class and for all m 1 (o,q,a)

-→ >0 m 2 and m ′ 2 such that m 2 R m ′ 2 we have:

• stability on an equivalence class: for all m ′ 1 ∈ M O+O ′ such that m ′ 1 (o,q,a) -→ >0 m ′ 2 and m ′ 1 R m 1 , φ((o, q, a), m 1 , m 2 ) ⇔ φ((o, q, a), m ′ 1 , m ′ 2 ) • backwards compatibility: if φ((o, q, a), m 1 , m 2 ) Pr[Imp O+O ′ (o)(q, C(m 1 )) = (a, m 2 )] = Pr[Imp O+O ′ (o)(q, C(m 1 )) = (a, m ′ 2 )]
where C(m 1 ) is the equivalence class of m 1 under R, and

Pr[Imp O+O ′ (o)(q, C(m 1 )) = (a, m 2 )] = m ′ 1 R m1 Pr[Imp O+O ′ (o)(q, m ′ 1 ) = (a, m 2 )]
We define a projection AdvT on partial executions which erases all oracle memories (only exchanges and adversarial memories are left). It defines the set of partial adversarial traces, for which we often use metavariable α. The fundamental property of backwards bisimulation is captured by the following lemma. It mostly states that the probability that a partial execution ends up in states (m, m a ) is constant on equivalence classes: it does not depend on the actual class representative m. And if

m k+1 ∈ M O , m ′ k+1 ∈ M O ′ such that m k+1 R m ′ k+1 : η∈PExec(A|O) | AdvT (η)=α G φ (T (η x k+1 -→ (m k+1 ,m k+1 a ))) Pr[A | O : η x k+1 -→ (m k+1 , m k+1 a )] = η∈PExec(A|O ′ ) | AdvT (η)=α G φ (T (η x k+1 -→ (m ′ k+1 ,m k+1 a ))) Pr[A | O ′ : η x k+1 -→ (m ′ k+1 , m k+1 a )]
LEMMA A.7. The following probabilities coincide

Pr[A | O : R = true ∧ G φ ] = Pr[A | O ′ : R = true ∧ G φ ]
4) Composition of Bisimulations: If we were to use bisimulations one after the other with the same condition φ, we would count twice the same bad simulation event, augmenting artificially by a factor of two the indistinguishability bound in our conclusion. To tackle this problem, we propose the following rule, which follows from A.5 and A.7.

LEMMA A.8. The following rule is sound:

O : ǫ F ¬φ O ≡ b R,φ O ′′ O ′′ ≡ R ′ ,φ O ′ I-2-Bis O ∼ ǫ O ′

C. Proof Of The Theorem

In this section we provide a detailed proof in CIL for the generic theorem V.1. The trees summing up the proof can be found in figure 8. Here is the outline of our reasoning. The proof starts with a layered oracle system implemented as in the definition, which we must relate to the anticipating system O ant . The formal relation between the real setting and the anticipating system is mostly one of determinization, though it seems easier to introduce intermediate systems Q 0 and Q 1 to write the underlying distribution properly. This is developped in C1 and corresponds to the left tree in figure 8.

Then, the anticipating system is progressively transformed into a system FwdSpl closer to the simulated setting. We show that the probability to distinguish between O ant and FwdSpl is bounded by the same bound as our theorem: Pr[A|O ant : F Collide∨Reveal∨Link ].

To justify this, we successively present a series of modified systems, from Q 2 to Q 4 , and the formal link existing between one and the next, before being able to conclude in C6. This corresponds to the middle tree in figure 8.

Eventually, we argue that FwdSpl is determinized by the simulated setting. The global conclusion finally follows from transitivity of the indistinguishabiltiy relation. We provide the specification of the intermediate system Q 0 in figure 9. It mostly consists in the anticipating system but the anticipation part. Namely the visibility labels are added and computed dynamically, and the branching is modified in o piv , but H is not called by o piv to anticipate post-pivot queries. Moreover, a list P ivot is added to the memory, to collect detected pivot queries, their answers and the value of x output by the pathfinder PathFinder. Memories of (H O , O) contain lists L oi , L H . Memories of Q 0 contain a shared table L S collecting all tuples of the form (o i , q, y, lbl), a list L H and list P ivot. This system is in bisimulation up to with the real setting, for relation R defined as follows. Memories m and m ′ are in relation iff they are equal when they belong to the same memory space and if m ∈ M (H O ,O) and m ′ ∈ M Q0 :

• (x, a f , Q) ∈ m.L H iff (x, a f , Q) ∈ m ′ .L H , but
the order of appearance might not be the same, • lists (m.L oi ) i and list m ′ .L S contain the same queries and answers, which we formalize as:

(1.) ∀(q, y) ∈ m.L oi , there exists a label lbl such that (o i , q, y, lbl) ∈ m ′ .L S ;

(2.) ∀(o i , q, y, lbl) ∈ m ′ .L S , (q, y) ∈ m.L oi .

We then have (H O , O) ≡ R,true Q 0 .

We now define a second intermediate system, Q 1 , which is similar to Q 0 but for the four lines starting with † in the implementation of o piv , which are replaced by:

let t ← H(x) in (o piv , q, y) : L := Π 3 (L H (x)) j≥piv(x) ; L S := L S .(L, V is);
To apply a determinization rule, we should separate L S into two tables L S and L ant S . However, we bypass this step and just provide the distribution γ induced by a memory on L ant S , table of anticipated queries. System Q 0 determinizes Q 1 for distribution γ for which we provide a constructive definition:

γ(m) = L ant S := [ ];
for q in dom(P ivot) do let (y, x) ← P ivot(q) in let t ← Imp Q0 (H)(x) in L := Π 3 (Last(L H (x))); L S := L S .([L] j>piv(x) , V is); L ant S := L ant S .([L] j>piv(x) , V is); endfor return L ant Sm.L S Finally, the justification of the step from Q 1 to O ant is again a perfect bisimulation relation R ′ induced by equality on lists L H and L S .

2) Redrawing Some Invisible Vertices: The idea behind this step is to allow the oracles to redraw new images for values of which the image has already been used, or in other words to resample some vertices. When can such a resampling be a problem for coherence of the simulation? The idea is to preserve the structure of the input characteristic graph during oracle calls. Of course, if the image we consider is visible or partially visible, we do not redraw it. Furthermore, even when the vertex we want to modify is invisible, we have to be careful. The idea is that we have to preserve paths existing in the input graph. To this end, we introduce a new terminology: a vertex v ′ is one of the next neighbors of a vertex v in graph CG iff there exists an edge (v, , v ′ ) between v and v ′ . The set of next neighbors of v in graph CG is denoted Next(v, CG). Every time we change an invisible vertex into another vertex, we want to modify its next neighbors so that the same edges still exist between them. This is doable only if such neighbors are non-visible. Besides, in case one of the next neighbors is a collision vertex, redrawing suppresses the collision and changes the structure of the graph. This is also a case we want to exclude.

Formally, we define a function ReSamp taking as input a query (o, q) and a memory m such that query (o, q) corresponds to a vertex (o, q, y) in m. The function outputs a boolean corresponding to whether we can redraw vertex (o, q, y) in memory m. The characteristic graph associated to m is Γ(m) = (v root , V, E, V). Function ReSamp : Que × M Oant → Bool maps ((o, q), m) to:

       true if V((o, q, y)) = Inv,
and Next((o, q, y),

Γ(m)) ∩ V -1 (V is) = ∅ and Next((o, q, y), Γ(m)) ∩ CollVertex(Γ(m)) = ∅ false otherwise.
In particular, we emphasize that for all values corresponding to partially visible and visible vertices, ReSamp outputs false.

To form up again the paths existing in the input Left tree

(H O , O) ∼ 0 O ant Middle tree O ant ∼ ǫ FwdSpl (U(H), S U (H) ) ≤ det,γ ′ FwdSpl I-Det (U(H), S U (H) ) ∼ 0 FwdSpl (H O , O) ∼ ǫ (U(H), S U (H) )
Left tree: graph, we define a function named Stitch : Xch × {Inv, P V is} × M Oant → M Oant , which takes as input a (possibly resampled) vertex (o, q, ỹ), a visibility label for this latter and a memory m and outputs a new memory m ′ . If (o, q, y) appears in the memory m for some y, Stitch modifies the memory so that (o, q, ỹ) replaces (o, q, y) with the visibility label given in input of Stitch and next neighbors of the vertex (o, q, y) in Γ(m) become next neighbors of the new vertex (o, q, ỹ) in Γ(m ′ ) (with the same edges). Thus, paths existing in the input graph exist in the output graph too.

(H O , O) ≡ R,true Q 0 I-Bis (H O , O) ∼ 0 Q 0 Q 0 ≤ det,γ Q 1 I-Det Q 0 ∼ 0 Q 1 Q 1 ≡ R ′ ,true O ant I-Bis Q 1 ∼ 0 O ant (H O , O) ∼ 0 O ant Middle tree: O ant : ǫ E F ¬φ ⇒ E UR O ant : ǫ F ¬φ O ant ≡ b R ′′ ,φ Q 2 Q 2 ≡ =,φ FwdSpl I-2-Bis O ant ∼ ǫ FwdSpl where E = F Collide∨Reveal∨Link
Formally, if (o, q, y) appears in the memory m and (o, q, ỹ) is the new vertex, Stitch outputs m ′ computed as follows. To build m ′ .L S , we start with m ′ .L S = m.L S and then proceed in the following way. For all edges ((o, q, y), l, (o ′ , q ′ , y ′ )) in Γ(m) where (o, q ′ , y ′ ) ∈ Next((o, q, y), Γ(m)), if j is an index such that q ′ = H j (l, (o, q, y)), then we let q = H j (l, (o, q, ỹ)). Then, if (o ′ , q) does not appear in m ′ .L S yet, (o ′ , q ′ , y ′ , lbl) is removed from m ′ .L S and (o ′ , q, y ′ , lbl) is added to m ′ .L S . If (o ′ , q) already appears in m ′ .L S , we do not modify it. Finally, we remove (o, q, y, ) from m ′ .L S and replace it by (o, q, ỹ, lbl), where lbl is given in input of Stitch. List m ′ .L H is then built out of m.L H by rebuilding the third component of every triple it contains: given

(x, a f , Q) ∈ m.L H , (x, a f , Q ′ ) is put in m ′ .L H , where Q ′ is the list of calls necessary to compute H(x) in m ′ .L S .
To write our new system Q 2 , we introduce an auxiliary procedure Adjust. It takes as input a query (o, q) and a visibility label lbl, resamples the vertex if it is possible and modifies the lists with Stitch, which adds the query and answer to list L S (o) with the desired visibility label. Its implemntation is as follows:

Adjust ((o, q), lbl, m) = if q ∈ dom(L S (o)) then if ReSamp((o, q), m) then let a ← U(o) in m ′ := Stitch((o, q, a), lbl, m); else (a, lbl ′ ) := L o (q); L S := L S .(o, q, a, max(lbl, lbl ′ )); endif else let a ← U(o) in L S := L S .
(o, q, a, lbl); endif return (o, q, L S (o, q)) Then, we can define the implementation of oracle H in the adjusted system as in figure 10, while both other oracles remain implemented as in O ant . The claim proven above justifies the existence and unicity of related adjusted states when φ holds.

To formalize our proof step, we use a relation of backwards bisimulation. Two states are in relation R ′′ iff they yield graphs with the same structure. Notice that we cannot turn a vertex into a collision vertex when we resample it: the fact that a collision occurs in a vertex depends only on its query part and we only change the answer. However, there is a possibility when we apply Stitch that we change the structure of the characteristic graph. Namely, we can stumble upon a preexisting vertex by computing a value q which already corresponds to a vertex. The set of values ỹ such that it happens is:

PbSet((o, q), m) = {ỹ ∈ Out(o) | ∃j s.t. q = H j (l, (o, q, ỹ)) ∈ dom(m.L S (o j ))} Imp Q2 (H)(x) = if x ∈ dom(L H ) then (a f , Q) := L H (x); L H := L H .(x, a f , Q); return a f else l := init(x); p := piv(x); (x 1 , . . . , x l ) := Θ(x); q 1 := H 1 (x 1 ); if q 1 ∈ dom(L S (o 1 )) then (a 1 , lbl) := L S (o 1 , q 1 ); Q := [(o 1 , q 1 , a 1 , lbl)]; else let a 1 ← U(o 1 ) in L S := L S .(o 1 , q 1 , a 1 , Inv); Q := [(o 1 , q 1 ,
a 1 , Inv)]; endif for j = 2 to p -1 do q j := H j (x j , (o j-1 , q j-1 , a j-1 )); if q j ∈ dom(L S (o j )) then (a j , lbl) := L S (o j , q j ); Q := Q : (o j , q j , a j , lbl); else let a j ← U(o j ) in L S := L S .(o j , q j , a j , Inv); Q := Q : (o j , q j , a j , Inv); endif endfor for j = p to l do q j := H j (x j , (o j-1 , q j-1 , a j-1 )); let (o j , q j , a j , lbl) ← Adjust((o j , q j ), P V is) in Q := Q : (o j , q j , a j , lbl);

endfor a f := H post (x, a p , [Q] j>p ); L H := L H .(x, a f , Q); return a f endif Figure 10. Implementation Of H In System Q 2
teristic graph exhibits no collision or non-resamplable vertex. This is naturally formalized as

φ 1 (m) =    CollVertex(Γ(m)) = ∅ ∀i, ∀(o, q, a) ∈ (m.L S (o i )|Inv), ReSamp((o, q), Γ(m)) = true
The second condition captures that neither Collide nor Reveal happen during the execution of the exchange, using the function mapping execution of exchanges to graph sequences defined in the previous section. We also impose that no query to oracles o i = o piv is labeled partially visible (this is P 1 ) and that all hash queries, if they have a matching pivot query that is visible, are not fresh hash queries (this is P 2 ).

φ 2 (xch, m 1 , m 2 ) = G ¬Collide∧¬Reveal (StTr(m 1 xch -→ m 2 )) ∧ P 1 (m 1 ) ∧ P 2 (m 1 , m 2 ) where            P 1 (m) is (xch = (o i , q, y) ∧ o i = o piv ∧ q ∈ dom(m.L S (o i ))) ⇒ V(q) = P V is P 2 (m, m) is (xch = (H, x, a f )∧ Π 3 ( m.L H )[piv(x)] ∈ dom(m.L S (o piv )|V is)) ⇒ x ∈ dom(m.L H ) We now let φ(xch, m 1 , m 2 ) = φ 1 (m 1 ) ∧ φ 2 (xch, m 1 , m 2 ). We must show that R ′′ is
) w.r.t. Γ(m ′ 1 ). Proof: We know that m 2 R ′′ m ′ 2 .
Hence there exist n ≥ 0 and a list [(o 1 , q 1 , a 1 ), . . . , (o n , q n , a n )] of distinct vertices such that, if we denote m 0 = m 2 and m n = m ′ 2 , we have: • For all i between 1 and n, we have m i = Stitch((o i , q i , a i ), Inv, m i-1 ). • For all i, ReSamp((o i , q i ), m i-1 ) or q i / ∈ m i-1 .L S (o i ).

• For all i, a i / ∈ PbSet((o i , q i ), m i-1 ). • For all i, if y i is the image of q i by o i in state m i-1 , then Card(Next((o i , q i , y i ), Γ(m i-1 ))) = Card(Next((o i , q i , a i ), Γ(m i ))). Let us define the following candidate for m ′ 1 :

m ′ 1 = Stitch((o 1 , q 1 , a 1 ), Inv, . . . Stitch((o n , q n , a n ), Inv, m 1 ) . . . )
The state m ′ 1 defined satisfies m 1 R ′′ m ′ 1 . Indeed, without loss of generality, we can assume that the (o i , q i ) are distinct. The stitching application has no effect on a state m if its first argument (o i , q i , a i ) is such that (o i , q i ) does not satisfy q i ∈ dom(m.L S (o i )).

Let us show now that every time a new vertex is added to m 1 .L S during the execution leading to m 2 , it is added in any state in relation with m 1 leading to m ′ 2 too.

Suppose that we reason about an exchange xch with an oracle o i . First, we argue that related states coincide on visible vertices, so in particular on visible parts of the domain of list L S (o i ). Moreover, the only invisible queries that can be asked without realizing Reveal are vertices directly linked to the root. If φ 1 holds, none of these vertices can be a collision vertex. Therefore, there is no possibility that their query part be resampled as neighbors of another vertex. Consequently, if an invisible query is asked and φ holds, it is in the domain of L S (o i ) for all related memories. Furthermore, in case we ask a partially visible query, either o i = o piv and it breaks P 1 , or it has to be visibly rooted, otherwise Reveal becomes true. Hence, since it has a visible (previous) neighbor and no other previous neighbor (otherwise it is a collision vertex), it cannot be resampled as a next neighbor of some vertex. As a result, it is in the domain of all related memories.

Suppose now that we reason on an exchange xch with H. The trick is to notice that our equivalence relation is built so that the same paths exist in related states. Consequently, if at step j, we meet the first query resulting in the addition of a new vertex in Γ(m 1 ), then it is also the first query resulting in the addition of a vertex in any related memory, or there would exist a rooted path in one graph and not the other. Furthermore, once we start adding vertices during the execution, we have to draw new vertices until the end, or we contradict φ by either creating a collision vertex or realizing Reveal. The conclusion follows. 2 ). This follows from the claim: if φ(xch, m 1 , m 2 ), then there is one possibility of state m1 , it is m ′ 1 . Moreover, φ 1 (m ′ 1 ) holds: no collision vertex or non-resamplable vertex can be created. This allows us to say that φ 1 (m 2 ) holds iff φ 1 (m ′ 2 ) holds. Therefore, if Reveal happens or a collision vertex is created, then it is in both cases. This justifies stability of G ¬Collide∧¬Reveal . Concerning P 1 , it only deals with input states. Visible vertices are equal in related states, so we only need to justify that there cannot exist a vertex which is partially visible in one state and invisible in the other. In fact, P 1 is not a stable property, but ¬Reveal ∧ φ 1 ∧ P 1 is. If ¬Reveal ∧ φ 1 holds for an exchange, then the only invisible queries that an adversary can perform are directly linked to the root, otherwise Reveal happens, and linked only to the root, since φ 1 holds. Since we do not resample the root, the set of invisible queries not breaking ¬Reveal ∧ φ 1 coincide in related states. Therefore, if visible and invisible queriable vertices coincide, P 1 holds for all or none of the states in relation. Finally, stability of P 2 follows from the visibility property imposed on the pivot: it has the same value in m 1 and m ′ 1 , so does L H . Stability follows.

We have to verify compatibility. We consider states m 1 , m 2 and m ′ 2 and an exchange xch = (o, q, a) such that m 1 xch -→ >0 m 2 and φ(xch, m 1 , m 2 ). The claim proves that there is only one state m ′ 1 such that m ′ 1 xch -→ >0 m ′ 2 and that executions starting in states m 1 and m ′ 1 lead to the same number of draws. It yields the equality between probabilities:

Pr[A | O ant : m 1 xch -→ >0 m 2 ] = Pr[Q 3 : m ′ 1 xch -→ >0 m ′ 2 ]
Then, we deduce from the one-to-one mapping between m 1 and m ′ 1 that it yields:

Pr[A | O ant : C(m 1 ) xch -→ >0 m 2 ] = Pr[Q 2 : C(m ′ 1 ) xch -→ >0 m ′ 2 ]
3) Replacing Adjust by Simple Sampling: We keep the same overall implementations but change the implementation of Adjust into:

Adjust ′ ((o, q), lbl) = let a ← U(o) in if q ∈ dom(L S (o)) then m ′ := Stitch((o, q, a), lbl, m); else L S := L S .(o, q, a, lbl); endif return (o, q, a)

In other words, we redraw a value for q, no matter whether it is resamplable, and do not take care of drawing it such that it does not create collisions. This yields a system we name Q 3 . This step is formalized using a bisimulation up to φ, with as a relation the equality of states. φ is obviously stable for this relation. Now let us check compatibility. Given that only the implementation of H possibly resamples vertices, the simulation is imperfect during an execution of H(x) (not necessarily called directly). It can happen if we resample a non-resamplable vertex.

Let v be the first vertex posing a simulation problem during an execution of H.

• If v has been resampled whereas it was visible and v is not the pivot then Reveal happens: the visibility label of the pivot is partially visible, so that sequence of labels has to increase. • If v has been resampled whereas it was a visible pivot query matching x, then P 2 is broken. We conclude that Q 2 ≡ =,φ Q 3 . 4) Changing Oracles in N O : In this step, we modify the implementation of the oracles in N O assuming that pivot queries are on the one hand always detected when queried directly, and on the other hand always asked before any of their matching post-pivot queries. It gives us a new system Q 4 , for which the implementations are provided in figure 11.

If the first assumption holds, we can safely simplify the end of the implementation of o piv by replacing the test of belonging to (L S (o piv )|P V is, Inv) by that of belonging to (L S (o piv )|Inv). If the second assumption holds, no partially visible query should be directly asked to an oracle o i = o piv . Indeed, the pivot query being queried on before implies that all post-pivot queries become visible vertices. We thus modify the implementation of o i = o piv by just checking if a query already belongs to dom(L S (o i )|Inv, V is) before drawing an answer.

The formal justification of this step is that Q 3 ≡ =,φ Q 4 . Indeed, the simulation is perfect except when:

• o piv is queried on a partially visible vertex, but does not branch in the path-finder branch, meaning the vertex is non-visibly meaningfully rooted. Yet, it is meaningfully rooted since it is partially visible. This is captured by Reveal.

• During an execution of o i , if we redraw a new answer to a partially visible query, but then P 1 is broken. 5) Changing H: In this last step, we define a system FwdSpl (see in figure 12) and replace the series of uniform sampling of the pivot and post-pivot vertices, followed by the computation of a f , by the sampling of a f and the execution of the forward sampler algorithm. According to the hypotheses we have formulated on this latter, both implementations yield equal distributions on the lists (L H , L S ) as soon as the forward sampler does not stumble on queries for which vertices already exist in the graph. This is taken care of since neither Collide nor Reveal happens. It follows that Q 4 ≡ =,φ FwdSpl 6) Conclusion Of The Tree In The Middle: We start by providing details about the application of rule I -2 -Bis. In the last three transformations, we have created systems Q 2 to FwdSpl, and such that Q 2 ≡ =,φ Q 3 , Q 3 ≡ =,φ Q 4 and Q 4 ≡ =,φ FwdSpl. From If o i = o piv : Imp Q4 (o i )(q) = if q ∈ dom(L S (o i )|Inv, V is) then (y, ) := L S (o i , q); else let y ← U(o i ) in endif L S := L S .(o i , q, y, V is); return y Imp Q4 (o piv ) H (q) = if q ∈ dom(L S (o piv )|V is) then (y, V is) := L S (o piv , q); elsif PathFinder(q, SG) = (true, x, List) then let t ← H(x) in (o piv , q, y) : L := Π 3 (L H (x)) j≥piv(x) ; L S := L S .((o piv , q, y, V is) : (L, V is)); elsif q ∈ dom(L S (o piv )|Inv) then (y, Inv) := L S (o piv , q); else let y ← U(o piv ) in endif L S := L S .(o piv , q, y, V is); return y these statements, we can deduce that Q 2 ≡ =,φ FwdSpl. As Q 2 is expressed as an adjusted system of O ant , we can apply rule I -2 -Bis.

Furthermore, we want to justify that F ¬φ yields that eventually, Collide, Reveal or Link happens, i.e. F ¬φ ⇒ F Collide∨Reveal∨Link . To do so, we prove that ¬P 1 and ¬P 2 imply that Reveal or Link have happened. Concerning P 1 , if when querying o i = o piv on q, q ∈ dom(m 1 .L S (o i )) is part of a partially visible vertex, then this latter is meaningfully rooted. If it is not visibly meaningfully rooted, then we can conclude that Reveal has happened. Otherwise, if all queries on the path from the root to our queried vertex are visible, since it is a post-pivot query, but still tagged with a partially visible label, it means that the matching pivot was not visibly meaningfully rooted at the time of its query. Consequently, we are sure that at some point, a query was issued to one of the o i 's to link two chains of visible vertices, i.e. Link has happened.

Finally, for property P 2 , if a fresh query on x is issued to H with a pivot already visible, it means that the pivot has been directly queried for, but that at the time of query, it was not visibly rooted (otherwise H(x) would have been called). Similarly to the previous event, we can show that either all queries before the pivot are visible, and at some point Link has happened, or there exists an invisible query on the path from the root to

  [CDMP05] propose to take into account the structure of the domain extender by showing a novel security criterion for them: indifferentiability from a random oracle. This notion is strongly inspired from the indifferentiability framework proposed by Maurer et al. [Mau02], [MRH04].

  the initialization oracle, and o F ∈ N O , the finalization oracle, with In(o F ) = {true, false} and Out(o F ) = 1; • an initial memory mO ∈ M O .

Figure 1 .

 1 Figure 1. Implementations of oracles F and K

Figure 3 .

 3 Figure 3. Implementation of the H Oracle

  t); L S := L S .((o piv , q, y) : L); else let y ← U(Out o piv ) in L S := L S .(o piv , q, y); endif return y For any o = o piv in N O :

Figure 4 .

 4 Figure 4. Implementations of the oracles in the anticipating system Oant

  In[START_REF] Bertoni | On the indifferentiability of the sponge construction[END_REF], Bertoni et. al. present a clever proof of the the sponge indifferentiability concluding to a bound of ktot(ktot+1)2 c+1

Figure 7 .

 7 Figure 7. ChopMD Implementation

  with the proof of a lemma formally linking probabilities of partial executions in both systems. We define a projection functionπ from A | O ′ -partial executions to A | O-partial executions by extending the projection from M O × M ′′ O to M O to executions. Informally, we can foresee that if we consider a partial execution η in A | O finishing with state m, we have to gather in a set all partial executions in A | O ′ finishing with state (m, m ′′ ) for a given m ′′ and projecting to η. Then, from the equation imposed for one query by the definition of determinization, we can extrapolate that the set of A | O ′ -partial executions weighs the same probability as trace η multiplied by the probability that m is mapped to m ′′ by γ. This is proven by the lemma below. LEMMA A.1. Let O and O ′ be such that O ≤ det,γ O ′ , and let η be a partial O-execution: η = ( mO , mA )

Definition A. 2 .

 2 Let φ ⊆ Xch × M O+O ′ × M O+O ′ be a step-predicate and let R ⊆ M O+O ′ × M O+O ′ be an equivalence relation. O and O ′ are in forward bisimulation up to φ, written O ≡ R,φ O ′ , iff m R m′ , and for all m 1 (o,q,a) -→ >0 m 2 and m 3 (o,q,a)

LEMMA A. 6 .

 6 Let α be a partial adversarial trace of length k α = m 0

  k a . Then, for all exchange act k+1 , all adversary memory m k+1 a and for all m k+1 , m ′ k+1 ∈ M O such that m k+1 R m ′ k+1 : η∈PExec(A|O) | AdvT (η)=α G φ (T (η

1)

  Relation Between (H O , O) and O ant -Left Tree:

Figure 8 .

 8 Figure 8. Trees Of The Proof Of The Generic Theorem

  Let us first check stability, i.e. that given m 1 xch -→ m 2 , and m ′ 2 such that m ′ 2 R ′′ m 2 , all states m1 in relation with m 1 such that m1 xch -→ m ′ 2 are such that φ(xch, m 1 , m 2 ) iff φ(xch, m1 , m ′

Figure 11 .

 11 Figure 11. Implementations Of Oracles In Q 4

  • ,oj i which: • has oracle access to the implementations of o j1 , • • • , o ji ; • takes as input a query in a finite query domain In(o i ) and a tuple of memories in k∈[1..n]-{j1,...,ji} M k ; • yields an answer in a finite answer domain Out(o i ) and updates the memories in M k , for k ∈ [1..n] -{j 1 , . . . , j i }. We stress that oracle o i thus shares memories with oracle o k for such indices k. An oracle implementation Imp(o i ) oj 1

  • ,oj i is called (α, t)-bounded, where α : {o j1 , • • • , o ji } → N and t ∈ N, if every execution of Imp(o i ) oj 1

  • ,oj i makes at most α(o jm ) calls to o jm , for j m ∈ {j 1 , . . . , j i }, and takes at most time t.

•

  Collide evaluates to true iff a collision vertex is created at this step, i.e. CollVertex(CG ′ ) -CollVertex(CG) = ∅. • Reveal evaluates to true if CG ′ contains a vertex which is the first visible vertex of a meaningful non-visibly rooted path: there exists

  Sketch of Proof. We present a proof sketch of this theorem in CIL developed in [Dau11], [BDK + 10]. An extended version of the proof can be found in appendix. To relate real and simulated oracle systems, we use O ant and another intermediate system FwdSpl, show indistinguishability relations between them and then use transitivity. Proof steps are outlined in figure

• S is (k s , t s )-bounded with k s (H) = 1, and t s = t FwdSplr + t PathFinder (k ′ + 1) + c, where k ′ = o∈O k(o). • the indifferentiability advantage is bounded by the probability of inconsistency events: Indiff(H, RO(O), S, ≤) P r[A|O ant : F Collide∨Reveal∨Link ] where t FwdSplr and t PathFinder respectively bound the execution time of forward sampler FwdSplr and pathfinder PathFinder used in the simulator.

  secondly, there exists m′′

O such that ( mO , m′′ O ) = m′ O and γ( mO ) = δ m′′ O , and lastly for all o

  ′′ m 2 , if φ(xch, m 1 , m 2 ), there exists a unique state m ′ 1 such that m 1 R ′′ m ′ 1 and m ′ Moreover, the same number of vertices are added in the graph Γ(m 2 ) w.r.t. Γ(m 1 ) and in the graph Γ(m ′ 2

	a
	relation of backwards bisimulation up to φ for our
	oracle system. We start by showing the following
	useful claim. Claim. Given m 1 that m ′ 2 R 1 xch -→ >0 m 2 , and a state m ′ 2 such xch -→ >0 m ′ 2 .

The algorithm is named after one of its plausible implementations, which involves building a particular graph. As we introduce a different graph construction for our theorem, we choose to introduce only this latter, which is the most relevant to the presentation of our result.

• If v has been resampled whereas it was partially visible, it means v belongs to the pivot and postpivot queries of another hash input x ′ . Necessarily the paths of x and x ′ meet in some vertex v ′ (not necessarily distinct of v), which is a collision vertex. The execution of H(x) realizes Collide at the moment of the query for v ′ .

Imp Oant (H)(x) = if x ∈ dom(L H ) then (a f , Q) := L H (x); L H := L H .(x, a f , Q); return a f else l := init(x); p := piv(x); (x 1 , . . . , x l ) := Θ(x);

(o 1 , q 1 ) := H 1 (x 1 ); if q 1 ∈ dom(L S (o 1 )) then (a 1 , lbl) := L S (o 1 , q 1 ); Q := [(o 1 , q 1 , a 1 , lbl)]; else let a 1 ← U(o 1 ) in L S := L S .(o 1 , q 1 , a 1 , Inv); Q := [(o 1 , q 1 , a 1 , Inv)]; endif for j = 2 to p -1 do q j := H j (x j , (o j-1 , q j-1 , a j-1 )); if q j ∈ dom(L S (o j )) then (a j , lbl) := L S (o j , q j ); Q := Q : (o j , q j , a j , lbl); else let a j ← U(o j ) in L S := L S .(o j , q j , a j , Inv); Q := Q : (o j , q j , a j , Inv); endif endfor for j = p to l do q j := H j (x j , (o j-1 , q j-1 , a j-1 )); if q j ∈ dom(L S (o j )) then (a j , lbl) := L S (o j , q j ); L S := L S .(o j , q j , a j , max(P V is, lbl)); Q := Q : (o j , q j , a j , max(P V is, lbl));

else let a j ← U(o j ) in L S := L S .(o j , q j , a j , P V is); Q := Q : (o j , q j , a j , P V is); endif endfor

Moreover, as the number of neighbors of a resampled vertex can potentially be modified by stitching, we impose that it is equal in two states in relation.

Formally, we impose the conditions: m R ′′ m ′ iff there exist n ≥ 0 and a list [(o 1 , q 1 , a 1 ), . . . , (o n , q n , a n )] of distinct vertices and labels, such that, if we denote m 0 = m and m n = m ′ :

Card(Next((o i , q i , a i ), Γ(m i ))), i.e. the stitch operation conserves the number of neighbors of the resampled vertex.

To be able to apply rule I -2 -Bis, we need a common set of conditions φ for backward and forward bisimulation relations. Therefore, we choose for φ the conjunction of every condition that we need to require in the next steps determining FwdSpl. To do so, we express two conditions on the execution of an exchange m 1 xch -→ m 2 , one is a condition on the characteristic graph from which we start (this is φ 1 ) and one is a condition on what happens during the exchange execution (this is φ 2 ).

The first condition expresses that the input charac-

a 1 , Inv)]; endif for j = 2 to p -1 do q j := H j (x j , (o j-1 , q j-1 , a j-1 )); if q j ∈ dom(L S (o j )) then (a j , lbl) := L S (o j , q j ); This concludes the discussion about the middle tree. 7) Determinization of FwdSpl to Obtain The Simulated System: As we did previously, we abuse a little the determinization rule and only provide the distribution yielded by a memory on anticipated queries in L S , which we name L ant S . To build possible anticipated components of state out of a state m = (L S , L H ) of the simulated system, we have to generate the list of queries matching every pair (x, a f ) in L H and to tag them with visibility labels. Given the first pair (x, a f ), this can be done by executing the implementation Imp FwdSpl (H) given as input x and the list L S where every vertex has been deemed visible.